From cef7ec2157afc882f0e2cc4883b527be39aea7b2 Mon Sep 17 00:00:00 2001 From: Guang Chen Date: Sun, 13 Sep 2015 13:25:01 +0800 Subject: [PATCH] fix implies(expr const &, expr const &) in z3++.h --- src/api/c++/z3++.h | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index f43ba83e5..9a340698a 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -642,13 +642,7 @@ namespace z3 { */ friend expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; } - friend expr implies(expr const & a, expr const & b) { - check_context(a, b); - assert(a.is_bool() && b.is_bool()); - Z3_ast r = Z3_mk_implies(a.ctx(), a, b); - a.check_error(); - return expr(a.ctx(), r); - } + friend expr implies(expr const & a, expr const & b); friend expr implies(expr const & a, bool b); friend expr implies(bool a, expr const & b); @@ -891,6 +885,13 @@ namespace z3 { }; + inline expr implies(expr const & a, expr const & b) { + check_context(a, b); + assert(a.is_bool() && b.is_bool()); + Z3_ast r = Z3_mk_implies(a.ctx(), a, b); + a.check_error(); + return expr(a.ctx(), r); + } inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); } inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }