首页 文章

将z3 C API ast（或解算器）对象转换为SMTLIB字符串

提问于
浏览 次
2

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

例如，对于此示例

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)

我已经尝试过C API函数，例如Z3_set_ast_print_mode，Z3_ast_to_string，但还没有成功 . 我查看了Z3_benchmark_to_smtlib_string，但是这篇文章Input arguments of Z3_benchmark_to_smtlib_string()表明它只支持SMTLIB 1.0 .

c++ api z3 smt

1 回答

  • 1

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

    回复于

相关问题