mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

finally expose some easier to use basics could be used in cases such as #5496

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-21 21:22:30 -07:00
parent aa05298950
commit 1975e486ee
1 changed files with 15 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/rewriter/bool_rewriter.h
View file

@ -137,6 +137,11 @@ public:
mk_eq(lhs, rhs, r);
return r;
}
expr_ref mk_xor(expr* a, expr* b) {
expr_ref result(m());
mk_xor(a, b, result);
return result;
}
void mk_iff(expr * lhs, expr * rhs, expr_ref & result) { mk_eq(lhs, rhs, result); }
void mk_xor(expr * lhs, expr * rhs, expr_ref & result);
void mk_and(unsigned num_args, expr * const * args, expr_ref & result) {
@ -169,6 +174,16 @@ public:
mk_and(args.size(), args.data(), result);
return result;
}
expr_ref mk_and(expr* a, expr* b) {
expr_ref result(m());
mk_and(a, b, result);
return result;
}
expr_ref mk_or(expr* a, expr* b) {
expr_ref result(m());
mk_or(a, b, result);
return result;
}
void mk_and(expr * arg1, expr * arg2, expr_ref & result) {
expr * args[2] = {arg1, arg2};