Z3 "ctx-solver-simplify"和"ctx-simplify"之间的满足性不一致

Question

我正在尝试制作 z3(我正在使用 z3py(来检查公式是否满足，如果满足，则简化它。

我最初使用的是Z3的ctx-solver-simplify。但是，由于我反复拨打许多电话，因此使用这种策略变得非常昂贵。因此，相反，我正在尝试使用 Z3 的ctx-simplify，它只执行局部简化，但它仍然应该返回它是否令人满意。

但是，我遇到了几个它产生简化但不能满足的坐姿。例如，请考虑以下事项：

(declare-const x Int)
(declare-const y Int)
(assert (and (< x 6) (and (not (> x 2)) (and (= x y) (and (not (< x 8)) (not (= x 4)))))))
(apply (then ctx-solver-simplify propagate-values (par-then (repeat (or-else split-clause skip)) propagate-ineqs)))
(apply (then ctx-simplify propagate-values (par-then (repeat (or-else split-clause skip)) propagate-ineqs)))

使用ctx-solver-simplify返回不满意，而ctx-simplify返回目标列表(如下所示(，因此满足(这显然是不正确的(。

(goal
(< x 6)
(not (> x 2))
(= x y)
(not (< x 8))
(not (= x 4))
:precision precise :depth 2)
)

谁能向我解释为什么会发生这种情况以及我是否正确使用这些策略？谢谢！

Answer 1

即使公式不满足，这些策略也可以返回目标。只有像 smt 这样的策略(以及为你调用 smt 的策略，如 qfbv(不会做到这一点。 您可以将"smt"附加到策略管道中。