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