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

expose n-ary xor

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-14 10:51:39 -07:00
parent 764e033bf4
commit 2704fb5fd5
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1210,6 +1210,7 @@ namespace z3 {
friend expr implies(bool a, expr const & b); friend expr implies(bool a, expr const & b);
friend expr mk_or(expr_vector const& args); friend expr mk_or(expr_vector const& args);
friend expr mk_xor(expr_vector const& args);
friend expr mk_and(expr_vector const& args); friend expr mk_and(expr_vector const& args);
friend expr ite(expr const & c, expr const & t, expr const & e); friend expr ite(expr const & c, expr const & t, expr const & e);
@ -2384,6 +2385,14 @@ namespace z3 {
args.check_error(); args.check_error();
return expr(args.ctx(), r); return expr(args.ctx(), r);
} }
inline expr mk_xor(expr_vector const& args) {
if (args.empty())
return args.ctx().bool_val(false);
expr r = args[0];
for (unsigned i = 1; i < args.size(); ++i)
r = r ^ args[i];
return r;
}
class func_entry : public object { class func_entry : public object {