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

Merge pull request #218 from cgcgbcbc/fix/implies

Browse source 
fix implies(expr const &, expr const &) in z3++.h
This commit is contained in:
Christoph M. Wintersteiger 2015-10-19 14:29:07 +01:00
parent d4e0de8f84 cef7ec2157
commit 1364f39f61
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

@ -647,13 +647,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);
@ -897,6 +891,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); }