smt - 为 CVC4 SMT 查询生成多个模型

Question

我可以为如下查询获取多个模型吗？

(set-logic LIA)
(set-option :produce-models true)

(declare-const x Int)
(assert (< x 20))
(check-sat)
(get-model)

而不仅仅是

sat
(
(define-fun x () Int 0)
)

我想得到 0, 1, -1, 2, ...

Answer 1

SMTLib 语言没有检索“所有模型”的机制。所以，如果你一定要只使用 SMTLib，你就不能这样做；至少不容易。

但是，大多数求解器（当然包括 cvc4 和 z3）都可以使用高级语言编写脚本。这个想法是check-sat打电话，如果你得到一个解决方案，你添加一个不允许该模型的附加断言，并查询一个新的。请参阅此答案以了解如何在 z3 中执行此操作，如 Python 中的脚本：尝试在 python 中使用 Z3 查找布尔公式的所有解决方案。你可以从 C/Java 等做同样的事情；或使用提供这种开箱即用命令的更高级别的绑定。