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)
)
有人可以向我解释为什么会这样，以及我是否正确使用了战术？谢谢！

我正在尝试使z3（我正在使用z3py）来检查公式是否可满足，如果可满足，则对其进行简化。我最初使用Z3的ctx-solver-simplify。但是，由于我是...

Answer 1

即使这些公式不能令人满意，这些策略也可以返回目标。只有像smt这样的策略（以及像qfbv这样为您调用smt的策略）才能做到这一点。您可以将'smt'附加到战术管道中。