在尝试解决大型非线性实际算术问题时，我使用答案文字和显式含义来跟踪每个断言，如其他帖子中所建议的那样 . 它应该等同于使用SMT2格式的（！（...）：named p1）语法 . 但是，似乎两种方法在内部都有不同的处理方式 .
以下SMT2代码给出了UNKNOWN结果，解释为“（不完整（理论算术））”：
(set-option :print-success false)
(set-option :produce-unsat-cores true) ; enable generation of unsat cores
(set-option :produce-models true) ; enable model generation
(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)
(declare-const p5 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 (=> p5 (< x3 0.0)))
(check-sat p1 p2 p3)
(get-info:reason-unknown)
另一方面，以下SMT2代码给出了正确的答案，UNSAT，并产生了一个信息丰富的不满核心（p4，p5）：
(set-option :print-success false)
(set-option :produce-unsat-cores true) ; enable generation of unsat cores
(set-option :produce-models true) ; enable model generation
(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)
(assert (! (= x1 (/ 1.0 (* x2 x2))) :named p1))
(assert (! (not (= x2 0.0)) :named p2))
(assert (! (= x3 (* 2.0 x1)) :named p3))
(assert (! (= x3 5.0) :named p4))
(assert (! (< x3 0) :named p5))
(check-sat)
(get-unsat-core)
;(get-model)
我的具体问题是：
-
如何解释这种不同的行为？跟踪非线性实方程和不等式的推荐做法是什么？
-
SMT2的（！（...）：命名p1）语法的等效OCaml API调用是什么？是assert_and_track吗？
我在Linux下使用ml-ng分支的Z3版本4.3.2 .
非常感谢！
1 回答
几个月前，新的ML API已经集成到unstable分支中，并且ml-ng分支已被删除 . 添加了一些错误修正/扩展，值得更新 .
assert_and_track完全符合您的怀疑，并且内部转换为给定的第一个示例 .
行为的差异由
(check-sat p1 p2 p3)解释，缺少p4和p5 . 一旦添加了这两个版本，两个版本的行为完全相同，它们产生相同的不饱和核心 .