有办法通过CVC4 C++ API解析SMT 2字符串吗？

Question

我有一个程序，可以动态生成SMT格式的表达式，我正在尝试将这些表达式连接到CVC4，以测试可满足性并得到模型。我想知道是否有一种通过CVC4 C++ API解析这些字符串的方便方法，或者最好将生成的SMT代码存储在一个文件中并将输入重定向到cvc4可执行文件。

Answer 1

粗略地看一下他们的API并没有发现任何明显的东西，所以我认为他们不支持这种操作模式。一般来说，加载这样的语句“动态”是很棘手的，因为表达式本身并没有多大意义:您必须在一个上下文中定义所有相关的类型，以及表达式所依赖的所有定义，包括选择正确的逻辑。这就是为什么z3中的对应函数有额外的参数：https://z3prover.github.io/api/html/classz3_1_1context.html#af2b9bef14b4f338c7bdd79a1bb155a0f

话虽如此，你最好还是直接问一下https://github.com/CVC4/CVC4/issues，看看他们是否有类似的东西。