将 z3 C++ API ast（或求解器）对象转换为 SMTLIB 字符串答案

【问题标题】：Converting z3 C++ API ast (or solver) objects to SMTLIB string将 z3 C++ API ast（或求解器）对象转换为 SMTLIB 字符串
【发布时间】：2014-03-28 23:53:49
【问题描述】：

我正在玩 z3 和其他 SMT 求解器，并想检查其他求解器（如 boolector）胜过 z3 的情况，反之亦然。为此，我需要一种将声明和断言转换为其他 SMT 求解器可以识别的 SMT-LIB2 格式的方法。

例如，对于这个例子

void print_as_smtlib2_string() {
    context c;
    expr x = c.int_const("x");
    expr y = c.int_const("y");
    solver s(c);

    s.add(x >= 1);
    s.add(y < x + 3);
    std::cout << s.check() << "\n";

    Z3_set_ast_print_mode(c, Z3_PRINT_SMTLIB_COMPLIANT);

    std::cout << "\nSolver is:\n";
    std::cout << s << "\n";
}

我得到类似的东西：坐

求解器是：（求解器 (>= x 1) (

我想要的是这样的（rise4fun 链接：http://rise4fun.com/Z3/aznC8）：

(declare-const x Int)
(declare-const y Int)
(assert (>= x 1))
(assert (< y (+ x 3)))
(check-sat)

我尝试过 Z3_set_ast_print_mode、Z3_ast_to_string 等 C API 函数，但都没有成功。我查看了 Z3_benchmark_to_smtlib_string 但这篇文章 Input arguments of Z3_benchmark_to_smtlib_string() 表明它只支持 SMTLIB 1.0。

【问题讨论】：

标签： c++ api z3 smt

【解决方案1】：

Z3_benchmark_to_smtlib_string 是 Z3 用于此目的的唯一函数。就像您提到的帖子一样，它已扩展到 SMTLIB2。正如 Leo 在他对该帖子的回复中所说，这是一个很少使用的旧功能，并且它可能不支持转储所有功能（例如求解器上的参数）。最近，还有一篇关于此功能的帖子以及旧版本 Z3 中的问题/错误（请参阅here）。

【讨论】：