mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

Bugfix for And/Or operators in Python.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-05-29 17:33:03 +01:00
parent 4da56aa4df
commit 756645326b
1 changed files with 23 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/api/python/z3.py
View file

@ -899,6 +899,7 @@ def _coerce_expr_merge(s, a):
return s return s
else: else:
if __debug__: if __debug__:
_z3_assert(s1.ctx == s.ctx, "context mismatch")
_z3_assert(False, "sort mismatch") _z3_assert(False, "sort mismatch")
else: else:
return s return s
@ -1459,9 +1460,18 @@ def And(*args):
>>> And(P) >>> And(P)
And(p__0, p__1, p__2, p__3, p__4) And(p__0, p__1, p__2, p__3, p__4)
""" """
args = _get_args(args) last_arg = None
ctx = _ctx_from_ast_arg_list(args) if len(args) > 0:
last_arg = args[len(args)-1]
if isinstance(last_arg, Context):
ctx = args[len(args)-1]
args = args[:len(args)-1]
else:
ctx = main_ctx()
args = _get_args(args)
ctx_args = _ctx_from_ast_arg_list(args, ctx)
if __debug__: if __debug__:
_z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
_z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe") _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
if _has_probe(args): if _has_probe(args):
return _probe_and(args, ctx) return _probe_and(args, ctx)
@ -1480,9 +1490,18 @@ def Or(*args):
>>> Or(P) >>> Or(P)
Or(p__0, p__1, p__2, p__3, p__4) Or(p__0, p__1, p__2, p__3, p__4)
""" """
args = _get_args(args) last_arg = None
ctx = _ctx_from_ast_arg_list(args) if len(args) > 0:
last_arg = args[len(args)-1]
if isinstance(last_arg, Context):
ctx = args[len(args)-1]
args = args[:len(args)-1]
else:
ctx = main_ctx()
args = _get_args(args)
ctx_args = _ctx_from_ast_arg_list(args, ctx)
if __debug__: if __debug__:
_z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
_z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe") _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
if _has_probe(args): if _has_probe(args):
return _probe_or(args, ctx) return _probe_or(args, ctx)