我在以下看似微不足道的基准测试中尝试了几种 SMT 求解器(CVC3、CVC4 和 Z3):
(set-logic LIA)
(set-info :smt-lib-version 2.0)
(assert (forall (( x Int)) (forall ((y Int)) (= y x))))
(check-sat)
(exit)
求解器都返回未知。我知道这是一个无法确定的片段(很好的非线性),但我希望会有一些简单的实例化启发式方法可以解决它。我还尝试使用常量添加一些额外的断言,但没有帮助。
有没有办法解决这些问题,SMT 中量化算术的推理限制是什么?
最佳答案
垫是正确的,qe
预处理器可能非常昂贵。此外,它对来自软件验证工具(例如VCC)的公式无效。 , Poirot , Dafny , VeriFast , Why3 , 和 ESCJava2 .它是无效的,因为这些应用程序生成的公式还包含未解释的函数、数组等。
正如 Pad 的回答所暗示的那样,Z3 是引擎的集合。它提供 API 和命令,允许用户选择将使用哪个引擎(或引擎组合)来解决问题。当用户只是说 (check-sat)
试图猜测解决输入公式的最佳引擎是什么。猜测是基于用户提供的输入公式和注释的结构(例如:set-logic
命令)。我们不断扩展自动检测的片段集以及我们提供的引擎集。
话虽如此,令人尴尬的是Z3漏掉了LIA
这样的片段。并且没有自动应用 qe
它的程序。对于 LIA
公式,qe
通常是最好的选择。基于 E 匹配或 MBQI 的替代方案无效,因为它们适用于完全不同的片段。
我只是committed code检测 LIA
(即使不使用 set-logic
)。更改已在 unstable
中可用(进行中)分支。它将在明天的每晚构建和下一个正式版本中提供。
关于z3 - SMT 中量化算术的推理限制是什么?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/14988298/