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 {