c - Z3:从字符串中解析术语

Question

是否有解析一般(非 bool )术语的 Z3 C API 调用？例如。像这样:(+ a b)?据我所知，Z3_parse_smtlib2_string 函数仅解析断言中的公式，这些公式完全是 bool 类型。

Answer 1

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