From 2704fb5fd57dad24cf1081ce2b0be537317a3a8d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Aug 2021 10:51:39 -0700 Subject: [PATCH] expose n-ary xor --- src/api/c++/z3++.h | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 72cd364c6..bd20a86f9 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1210,6 +1210,7 @@ namespace z3 { friend expr implies(bool a, expr const & b); 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 ite(expr const & c, expr const & t, expr const & e); @@ -2384,6 +2385,14 @@ namespace z3 { args.check_error(); 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 {