Можно ли в 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)

Что я хотел бы сделать, так это пропустить вторую проверку насыщенности, если первая проверка сбоя является ненадежной / насыщенной. Можно ли это сделать? Я считаю, что смог бы сделать это, если бы использовал 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 / unsat проверяет на основе предыдущего результата.

Решение состоит в том, чтобы использовать API более высокого уровня, доступный на любом количестве основных языков, таких как C / C++ / C# / O'Caml / Python / Java / Scheme / Haskell, где вы можете запрограммировать такое взаимодействие.