c++ - 将 z3 C++ API ast(或求解器)对象转换为 SMTLIB 字符串

Question

我正在研究 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) (< y (+ x 3)))

我想要的是这样的(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。

Answer 1

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