z3 C++ API &网站 [英] z3 C++ API & ite
问题描述
也许我错过了一些东西,但是使用 z3 C++ API 构造 if-then-else 表达式的方法是什么?
Maybe I missed something, but what is the way of constructing an if-then-else expression using the z3 C++ API ?
我可以为此使用 C API,但我想知道为什么 C++ API 中没有这样的函数.
I could use the C API for that, but I'm wondering why there is no such function in the C++ API.
问候,朱利安
推荐答案
我们可以混合使用 C 和 C++ API.文件 examples/c++/example.cpp
包含一个使用 C API 创建 if-then-else 表达式的示例.函数 to_expr
本质上是用 C++智能指针"expr
包装了一个 Z3_ast
,它会自动为我们管理引用计数器.
We can mix the C and C++ APIs. The file examples/c++/example.cpp
contains an example using the C API to create the if-then-else expression. The function to_expr
is essentially wrapping a Z3_ast
with the C++ "smart pointer" expr
that automatically manages the reference counters for us.
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
之后:
I just added the ite
function to the C++ API. It will be available in the next release (v4.3.2). If you want you can add to the z3++.h
file in your system. A good place to include is after the function 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);
}
使用这个函数,我们可以写:
Using this function, we can write:
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 &网站的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!