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‘附加到您的策略管道中。