From c430fe26aa306ab8cc4141f1ab55e789a748a225 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 4 Jan 2013 08:29:25 -0800 Subject: [PATCH] Add ite operator to the C++ API Signed-off-by: Leonardo de Moura --- examples/c++/example.cpp | 10 ++++++++++ src/api/c++/z3++.h | 13 +++++++++++++ 2 files changed, 23 insertions(+) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 9e92d99ab..1f127e8e4 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -337,6 +337,15 @@ void ite_example() { std::cout << "term: " << ite << "\n"; } +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"; +} + /** \brief Small example using quantifiers. */ @@ -889,6 +898,7 @@ int main() { error_example(); std::cout << "\n"; numeral_example(); std::cout << "\n"; ite_example(); std::cout << "\n"; + ite_example2(); std::cout << "\n"; quantifier_example(); std::cout << "\n"; unsat_core_example1(); std::cout << "\n"; unsat_core_example2(); std::cout << "\n"; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index fca009cea..7875e6ef3 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -620,6 +620,19 @@ namespace z3 { return expr(a.ctx(), r); } + /** + \brief Create the if-then-else expression ite(c, t, e) + + \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); + } + friend expr operator==(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = Z3_mk_eq(a.ctx(), a, b);