z3 - SMT 中量化算术的推理限制是什么？

Question

我在以下看似微不足道的基准测试中尝试了几种 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 中量化算术的推理限制是什么？

Answer 1

垫是正确的，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 中可用(进行中)分支。它将在明天的每晚构建和下一个正式版本中提供。