为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等中执行同样的操作。；或者使用提供这种开箱即用命令的更高级绑定。