z3 - 带减法的 Z3 ast_to_string() API

Question

问题很简单。我使用 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 求解器。有没有其他方法可以避免这种情况？

Answer 1

记得设置：

Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB2_COMPLIANT);

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