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

Converting z3 C++ API ast (or solver) objects to SMTLIB string

本文关键字：对象 转换 字符串 SMTLIB c++ z3 API ast      更新时间：2023-10-16

我正在使用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)(& lt;Y (+ x 3))

我想要的是这样的东西(rise4fun link: http://rise4fun.com/Z3/aznC8):

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

我尝试过C API函数，如Z3_set_ast_print_mode, Z3_ast_to_string，但没有成功。我看了看Z3_benchmark_to_smtlib_string，但是这个帖子的Z3_benchmark_to_smtlib_string()的输入参数表明它只支持SMTLIB 1.0。

Z3_benchmark_to_smtlib_string是Z3用于此目的的唯一函数。就像你提到的那篇文章一样，它已经扩展到SMTLIB2。正如Leo在他对那篇文章的回复中所说，这是一个很少使用的旧函数，它可能不支持转储所有的特征(例如，解算器的参数)。最近，也有另一篇关于这个函数和旧版本Z3中的问题/bug的帖子(见这里)。

相关文章：