z3 C++ API & ite

Question

Forse mi sono perso qualcosa, ma qual è il modo di costruire un'espressione if-then-else usando l'API z3 C++?

Potrei usare l'API C per questo, ma mi chiedo perché non ci sia tale funzione nell'API C++.

saluti, Julien

Answer 1

Possiamo mescolare l'API C e C++. Il file examples/c++/example.cpp contiene un esempio che utilizza l'API C per creare l'espressione if-then-else. La funzione to_expr consiste essenzialmente nel wrapping di Z3_ast con il "puntatore intelligente" C++ expr che gestisce automaticamente i contatori di riferimento per noi.

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. Sarà disponibile nella prossima versione (v4.3.2). Se vuoi, puoi aggiungere al file z3++.h nel tuo sistema. Un buon posto per includere sia dopo la funzione 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); 
} 

Usando questa funzione, possiamo scrivere:

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