z3 C++ API & ite

Question

Może coś przeoczyłem, ale jaki jest sposób konstruowania wyrażenia if-then-else za pomocą API C++ z3?

Mogę użyć do tego API C, ale zastanawiam się, dlaczego nie ma takiej funkcji w API C++.

pozdrowienia, Julien

Answer 1

Możemy mieszać C i C++ API. Plik examples/c++/example.cpp zawiera przykład wykorzystujący API C do utworzenia wyrażenia if-then-else. Funkcja to_expr zasadniczo owija Z3_ast za pomocą "inteligentnego wskaźnika" C++ expr, który automatycznie zarządza licznikami referencyjnymi dla nas.

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

I just added the ite function to the C++ API. Będzie dostępny w następnym wydaniu (v4.3.2). Jeśli chcesz, możesz dodać do pliku z3++.h w swoim systemie. Dobrym miejscem na to jest po funkcji 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); 
} 

Za pomocą tej funkcji możemy napisać:

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