z3 - z3 C ++ API＆ite

Question

何かを見逃したかもしれませんが、z3 C ++ APIを使用してif-then-else式を作成する方法は何ですか？

そのためにCAPIを使用することもできますが、なぜC++APIにそのような関数がないのか疑問に思います。

よろしく、ジュリアン

Answer 1

CAPIとC++APIを混在させることができます。このファイルexamples/c++/example.cppには、CAPIを使用してif-then-else式を作成する例が含まれています。この関数は基本的に、参照カウンターを自動的に管理するC++の「スマートポインター」でto_exprラップします。Z3_astexpr

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";
}

iteC++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";
}