我有一个可以动态生成 SMT-LIB 格式的表达式的程序，我正在尝试将这些表达式连接到 CVC4 以测试可满足性并获取模型。我想知道是否有一种方便的方法可以通过 CVC4 C++ API 解析这些字符串，或者最好将生成的 SMT-LIB 代码存储在文件中并将输入重定向到 cvc4 可执行文件。
问问题
148 次
1 回答
0
粗略看看他们的 API 并没有发现任何明显的东西，所以我认为他们不支持这种操作模式。一般来说，“动态”加载这样的语句是很棘手的，因为一个表达式本身没有多大意义：你必须在一个定义了所有相关类型的上下文中，以及你的所有定义表达式依赖，包括选择适当的逻辑。也就是说，例如，为什么z3中的相应函数有额外的参数：https ://z3prover.github.io/api/html/classz3_1_1context.html#af2b9bef14b4f338c7bdd79a1bb155a0f
话虽如此，您最好的选择可能是直接在https://github.com/CVC4/CVC4/issues询问他们是否有类似的东西。
于 2020-06-04T23:50:13.783 回答