z3 - Z3 的“ctx-solver-simplify”和“ctx-simplify”之间的可满足性不一致

Question

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

我最初使用的是 Z3 的ctx-solver-simplify. 然而，由于我反复打很多电话，使用这种策略结果非常昂贵。因此，我尝试使用ctx-simplify仅执行局部简化的 Z3，但无论是否可满足，它仍应返回。

但是，我遇到了一些情况，它产生了简化，但不能令人满意。例如考虑以下内容：

(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-simplifyreturn unsatisifiable whilectx-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”附加到您的战术管道中。