2013-01-04 31 views
5

多分私は何かを忘れていましたが、z3 C++ APIを使ってif-then-else式を構築する方法は何ですか?z3 C++ API&ite

私はそのためにC APIを使うことができましたが、C++ APIにそのような機能がないのはなぜかと思います。

に関して、 ジュリアン

答えて

7

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

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。次のリリース(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"; 
} 
+0

関連の質問:http://stackoverflow.com/questions/24566727/implement-z3 -maximize-in-c –

関連する問題