如何解决为 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 等中做同样的事情；或使用提供此类开箱即用命令的更高级别绑定。
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 dio@foxmail.com 举报，一经查实，本站将立刻删除。
