mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

fix implies(expr const &, expr const &) in z3++.h

Browse source
This commit is contained in:
Guang Chen 2015-09-13 13:25:01 +08:00 committed by cgcgbcbc
parent a7a0deed3f
commit cef7ec2157
1 changed files with 8 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/api/c++/z3++.h
View file

@ -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); }