z3 C++ API&ite

Question

也许我错过了什么,但是使用z3 C++ API构建if-then-else表达式的方法是什么？

我可以使用C API,但我想知道为什么C++ API中没有这样的函数.

问候,朱利安

Answer 1

我们可以混合使用C和C++ API.该文件examples/c++/example.cpp包含一个使用C API创建if-then-else表达式的示例.该函数to_expr实际上是Z3_ast用C++"智能指针" 包装一个,它expr为我们自动管理引用计数器.

void ite_example() {
    std::cout << "if-then-else example\n";
    context c;

    expr f    = c.bool_val(false);
    expr one  = c.int_val(1);
    expr zero = c.int_val(0);
    expr ite  = to_expr(c, Z3_mk_ite(c, f, one, zero));

    std::cout << "term: " << ite << "\n";
}

我刚刚将该ite函数添加到C++ API中.它将在下一版本(v4.3.2)中提供.如果需要,可以添加到z3++.h系统中的文件.包含的好地方是功能之后implies:

/**
   \brief Create the if-then-else expression <tt>ite(c, t, e)</tt>

   \pre c.is_bool()
*/
friend expr ite(expr const & c, expr const & t, expr const & e) {
    check_context(c, t); check_context(c, e);
    assert(c.is_bool());
    Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
    c.check_error();
    return expr(c.ctx(), r);
}

使用此功能,我们可以写:

void ite_example2() {
    std::cout << "if-then-else example2\n";
    context c;
    expr b = c.bool_const("b");
    expr x = c.int_const("x");
    expr y = c.int_const("y");
    std::cout << (ite(b, x, y) > 0) << "\n";
}