mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
Added Xor to z3py
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
6ffaadd498
commit
345c7448ac
15
python/z3.py
15
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.
|
||||
|
||||
|
|
Loading…
Reference in a new issue