一个小例子表明，当NRA断言由与（sat p1 ... pn）检查相关的前提pi标记时，非线性实数算术（NRA）求解器受到阻碍 .
以下SMT2示例返回具有正确模型的SAT：
(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)
(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)
(assert (=> p1 (= x1 (/ 1.0 (* x2 x2)))))
(assert (=> p2 (not (= x2 0.0))))
(assert (=> p3 (= x3 (* 2.0 x1))))
(assert (=> p4 (= x3 5.0)))
(assert (and p1 p2 p3 p4))
(check-sat)
(get-model)
以下语义上等效的示例返回unknown：
(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)
(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)
(assert (=> p1 (= x1 (/ 1.0 (* x2 x2)))))
(assert (=> p2 (not (= x2 0.0))))
(assert (=> p3 (= x3 (* 2.0 x1))))
(assert (=> p4 (= x3 5.0)))
(check-sat p1 p2 p3 p4)
(get-model)
而且，模型查询返回的模型不正确！
使用第一种风格对我来说不是一个选择，因为我特别感兴趣从UNSAT问题实例中获取不满核心，并且我希望动态组合“活动”前提 . 但是，通过将前提与“和”连接起来，可以防止不满足的核心 生产环境 .
看起来第一个例子（assert（和p1 p2 p3 p4））在预处理步骤中以某种方式被简化，因此NRA求解器一起查看所有四个约束并能够解决它们 . 这似乎不是使用第二个例子的情况（check-sat p1 p2 p3 p4） .
我错过了什么吗？谢谢！
PS：我正在使用不稳定分支的Z3版本4.4.0（加载2015-03-26） .
1 回答
这种行为差异可以解释为Z3在使用假设时运行不同的求解器 . 如果不需要假设，增量特征，证明或理论组合，它将运行一个新的求解器（NLSAT），而当需要这些特征中的至少一个时，它会回退到一个更老的，更弱的求解器，它快速放弃回报未知 . 您可以使用-v：100运行Z3并报告
然而，无效模型确实不应该默认输出 .