为 CVC4 SMT 查询生成多个模型

问题描述

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

(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,...

解决方法

SMTLib 语言没有检索“所有模型”的机制。因此，如果您只能使用 SMTLib，则不能这样做；至少不容易。

但是，大多数求解器（肯定包括 cvc4 和 z3）都可以使用高级语言编写脚本。这个想法是进行 check-sat 调用，如果您得到解决方案，则添加一个禁止该模型的附加断言，并查询新的断言。请参阅此答案以了解如何在 z3 中执行此操作，如 Python 脚本所示：Trying to find all solutions to a boolean formula using Z3 in python。你可以从 C/Java 等中做同样的事情；或使用提供此类开箱即用命令的更高级别绑定。