Z3：从字符串中解析词条答案

【问题标题】：Z3: Parse Term from StringZ3：从字符串中解析词条
【发布时间】：2014-06-16 15:34:25
【问题描述】：

是否有解析通用（非布尔）术语的 Z3 C API 调用？例如。像这样的东西：(+ a b)?据我所知，Z3_parse_smtlib2_string 函数仅解析断言中的公式，这些公式完全属于布尔类型。

【问题讨论】：

define-fun sum () Int (+ x y) 这样的东西不满足你，为什么不呢？到目前为止，您尝试了什么，它是如何失败的？
Michael，我之前尝试使用 Z3_parse_smtlib2_string 解析类似的内容，但它只返回术语 true。
z3 是 SAT Modulo Theories 的求解器，因此其结果为真或假（SAT 或 UNSAT），您希望从该示例中得到什么结果？

【解决方案1】：

解析器 (Z3_parse_smtlib2_string) 解析 SMT-LIB2 基准。这种格式的基准定义了一个逻辑公式。如果输入不包含任何断言，则此公式为“真”。这就是解析器在您的情况下返回“true”的原因。 Z3 不公开术语的解析工具。您可以通过创建一个特殊谓词“MyHolds”来解决此问题，该谓词采用合适类型的术语。然后，您创建一个将断言“(assert (MyHolds ))”作为唯一断言的基准。然后，您可以从解析器的结果中删除 MyHolds 以取回您的术语。

【讨论】：