5
多分私は何かを忘れていましたが、z3 C++ APIを使ってif-then-else式を構築する方法は何ですか?z3 C++ API&ite
私はそのためにC APIを使うことができましたが、C++ APIにそのような機能がないのはなぜかと思います。
に関して、 ジュリアン
多分私は何かを忘れていましたが、z3 C++ APIを使ってif-then-else式を構築する方法は何ですか?z3 C++ API&ite
私はそのためにC APIを使うことができましたが、C++ APIにそのような機能がないのはなぜかと思います。
に関して、 ジュリアン
私たちは、CおよびC++ APIを混在させることができます。ファイルexamples/c++/example.cpp
には、C APIを使用してif-then-else式を作成する例が含まれています。 to_expr
関数は、本来、参照カウンタを自動的に管理するC++の "スマートポインタ" expr
でZ3_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";
}
関連の質問:http://stackoverflow.com/questions/24566727/implement-z3 -maximize-in-c –