我在以下看似微不足道的基准测试中尝试了几种 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 http://vcc.codeplex.com/, Poirot http://research.microsoft.com/en-us/projects/poirot/, Dafny http://research.microsoft.com/en-us/projects/dafny/, VeriFast http://www.cs.kuleuven.be/~bartj/verifast/, Why3 http://why3.lri.fr/, and ESCJava2 http://kindsoftware.com/products/opensource/ESCJava2/。它并不有效，因为这些应用程序生成的公式还包含未解释的函数、数组等。
正如 Pad 的回答所暗示的那样，Z3 是引擎的集合。它提供 API 和命令，允许用户选择使用哪个引擎（或引擎组合）来解决问题。当用户刚刚说(check-sat)尝试猜测解决输入公式的最佳引擎是什么。猜测是基于输入公式的结构和用户提供的注释（例如：set-logic命令）。我们正在不断扩展自动检测的片段集以及我们提供的引擎集。
话虽这么说，但令人尴尬的是，Z3 错过了诸如此类的片段LIA并且没有自动应用qe对其进行程序。为了LIA公式，qe通常是最好的选择。基于 E-matching 或 MBQI 的替代方案并不有效，因为它们适用于完全不同的片段。
I just 提交的代码 http://z3.codeplex.com/SourceControl/changeset/97bf9418f721检测到LIA（即使当set-logic未使用）。该更改已在unstable（正在进行中）分支。它将在明天的夜间版本和下一个正式版本中提供。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
