也许我错过了什么，但什么是构建使用Z3 C ++ API一个if-then-else表达式的方法是什么？
我可以使用C API的，但我不知道为什么存在C ++ API中没有这样的功能。
看起来，朱利安
Answer 1:
我们可以混合使用C和C ++的API。 文件examples/c++/example.cpp包含使用C API来创建的if-then-else表达式的例子。 该功能to_expr基本上包装一Z3_ast与C ++“智能指针” expr自动管理引用计数我们。
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";
}
我只是说了ite功能的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";
}
文章来源: z3 C++ API & ite
