使用含义与 :named 机制跟踪非线性实数算术断言给出了不同的答案

Question

在尝试解决大型非线性实数算术问题时，我按照其他帖子中的建议，使用答案文字和显式蕴涵来跟踪每个断言。它应该等同于使用 SMT2 格式的 (! (...) :named p1) 语法。不过，似乎这两种方法在内部的处理方式不同。

以下 SMT2 代码给出了未知结果，并附有解释“（不完整（理论算术））”：

(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，并生成了一个信息丰富的 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 的 (! (...) :named p1) 语法的等效 OCaml API 调用是什么？是assert_and_track吗？

我正在使用 Linux 下 ml-ng 分支的 Z3 版本 4.3.2。

非常感谢！

Answer 1

几个月前，新的 ML API 已集成到不稳定分支中，而 ml-ng 分支已被删除。添加了一些 bugfixes/extensions 值得更新。

assert_and_track 做的正是您所怀疑的，它在内部被翻译成给出的第一个例子。

行为上的差异由缺少 p4 和 p5 的 (check-sat p1 p2 p3) 解释。添加这些后，两个版本的行为完全相同，并且它们产生相同的不饱和核心。

使用含义与 :named 机制跟踪非线性实数算术断言给出了不同的答案

Tracking nonlinear real arithmetic assertions using implications versus the :named mechanism gives different answers

z3