diff --git a/python/z3.py b/python/z3.py index 9348e5b59..9d9d03e55 100644 --- a/python/z3.py +++ b/python/z3.py @@ -1328,6 +1328,21 @@ def Implies(a, b, ctx=None): b = s.cast(b) return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx) +def Xor(a, b, ctx=None): + """Create a Z3 Xor expression. + + >>> p, q = Bools('p q') + >>> Xor(p, q) + Xor(p, q) + >>> simplify(Xor(p, q)) + Not(p) == q + """ + ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx)) + s = BoolSort(ctx) + a = s.cast(a) + b = s.cast(b) + return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx) + def Not(a, ctx=None): """Create a Z3 not expression or probe.