有没有办法通过 CVC4 C++ API 解析 SMT-LIB2 字符串？答案

【问题标题】：Is there a way to parse SMT-LIB2 strings through the CVC4 C++ API?有没有办法通过 CVC4 C++ API 解析 SMT-LIB2 字符串？
【发布时间】：2020-06-04 19:22:44
【问题描述】：

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

【问题讨论】：

“方便”。可能不是一个合理的人的定义。这可以在 SMT-LIB command 级别以正常的方式完成（有关命令，请参见 SMT-LIB 2.6 第 3.9 节）。（FWIW 只是术语解析比听起来更难，因为术语可以生成隐式命令。）interactive shell 正在这样做，不应该使用私有 API。（这些可能已经潜入。）如果这个功能真的很重要，我会开始尝试理解那个代码。也许最近添加了更好的东西？
@Tim 因此，如果我理解正确，您可以使用带有字符串输入的解析器 api 单独解析 smt-lib 命令，然后使用 command.invoke() 在 smt 引擎上调用这些命令方法。这比在 z3 中更不方便，但很高兴知道它可以做到。
“单独的命令”。可用的是一系列命令。解析器尝试处理文本流。那可以包含多个命令。此外，文本中的命令也可以变成多个命令对象，因为语法糖被删除，例如[ :named ](github.com/CVC4/CVC4/blob/master/src/parser/smt2/Smt2.g#L2244).

标签： smt cvc4

【解决方案1】：

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

话虽如此，您最好直接在https://github.com/CVC4/CVC4/issues 询问他们是否有类似的东西。

【讨论】：