z3 - 是否可以在 Z3 中编码条件SAT 检查？

Question

假设我有以下问题（我已经简化了我的问题）

;; declare variables
(declare-const X0 Int)
(assert (>= X0 0))
(assert (<= X0 1))
(declare-const X1 Int)
(assert (>= X1 0))
(assert (<= X1 1))
(declare-const X2 Int)
(assert (>= X2 0))
(assert (<= X2 1))

;; two sat checks
(push)
(assert (= (0 (+ X1 X2))))
(check-sat)
(pop)
(push)
(assert (= (0 (+ X1 X2 X3))))
(check-sat)
(pop)

如果第一次SAT检查是未饱和/饱和，我想做的是跳过第二次SAT检查。是否有可能做到这一点？我相信如果我将 Z3 与 python 一起使用（运行 sat 检查，获取结果，并在结果上使用 python if 语句来确定是否运行第二次检查），我可以做到这一点，但我想用 smt 做到这一点-lib。这（很容易）可能吗？

Answer 1

没有。SMTLib 语言 ( http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf ) 没有任何“控制结构”供您发布sat 检查基于先前的结果。

解决方案是使用更高级别的 API，该 API 可从任意数量的宿主语言中获得，例如 C/C++/C#/O'Caml/Python/Java/Scheme/Haskell，您可以在其中编写此类交互。