是否可以在 Z3 中编码条件SAT 检查？答案

【问题标题】：Is it possible to encode conditional sat checks in Z3?是否可以在 Z3 中编码条件SAT 检查？
【发布时间】：2021-08-18 01:16:07
【问题描述】：

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

;; 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)

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

【问题讨论】：

标签： z3 smt-lib

【解决方案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，您可以在其中编写此类交互.

【讨论】：