带减法的 Z3 ast_to_string() API答案

【问题标题】：Z3 ast_to_string() API with Subtraction带减法的 Z3 ast_to_string() API
【发布时间】：2012-05-31 11:52:34
【问题描述】：

问题很简单。我使用 C API 接口在 Z3 中断言以下语句。

(assert(>= (xA 1) (- (yB 0) period))))

现在，有时，我需要检查已输入的断言类型以及 SatSolver 中的结果。我通过使用 ast_to_string() API 生成一个文本文件来做到这一点。这个 API 将我上面的语句返回为 -

(assert(>= (xA 1) (+ (yB 0) (* -1 period))))

当我将此文件提供给 Sat Solver 时，它会向我抱怨错误 -

（错误“错误：第 150 行第 56 列：找不到 id -1。”）

那么，我必须手动修复代码中的所有 -1 并运行 sat 求解器。有没有其他方法可以避免这种情况？

【问题讨论】：

标签： z3

【解决方案1】：

记得设置：

Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB2_COMPLIANT);

在使用 ast_to_string() 之前，以便输出公式符合 SMTLIB 2.0 格式。

【讨论】：

并不能真正解决问题。例如，我在输出中得到了关注 - (assert(let ((?x28 (xA 1))) (>= ?x28 0))) 所以它最终会扼杀将其打印到文件的好处。
问题是输出是否可以被Z3解析。最后，SMTLIB 是机器可读的格式，而不是人类可读的格式。