为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调用，如果您得到了解决方案，则添加一个不允许该模型的附加断言，并查询一个新的模型。有关如何在Python中执行此操作的答案，请参阅Python：Trying to find all solutions to a boolean formula using Z3 in python中的脚本。您可以在C/Java等语言中执行相同的操作；或者使用提供此类开箱即用命令的高级绑定。