mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

coalescing is-int check for python 2.x, issue #572

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-04-21 10:49:16 -07:00
parent 417c80edbc
commit 20a6b41c5c
1 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -52,7 +52,7 @@ import math
if sys.version < '3':
def _is_int(v):
return isinstance(v, int) or isinstance(v, long)
return isinstance(v, (int, long))
else:
def _is_int(v):
return isinstance(v, int)
@ -95,7 +95,7 @@ def append_log(s):
def to_symbol(s, ctx=None):
"""Convert an integer or string into a Z3 symbol."""
if isinstance(s, int):
if _is_int(s):
return Z3_mk_int_symbol(_get_ctx(ctx).ref(), s)
else:
return Z3_mk_string_symbol(_get_ctx(ctx).ref(), s)
@ -3627,7 +3627,7 @@ def Extract(high, low, a):
return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
if __debug__:
_z3_assert(low <= high, "First argument must be greater than or equal to second argument")
_z3_assert(isinstance(high, int) and high >= 0 and isinstance(low, int) and low >= 0, "First and second arguments must be non negative integers")
_z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0, "First and second arguments must be non negative integers")
_z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression")
return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
@ -3849,7 +3849,7 @@ def SignExt(n, a):
fe
"""
if __debug__:
_z3_assert(isinstance(n, int), "First argument must be an integer")
_z3_assert(_is_int(n), "First argument must be an integer")
_z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
@ -3876,7 +3876,7 @@ def ZeroExt(n, a):
8
"""
if __debug__:
_z3_assert(isinstance(n, int), "First argument must be an integer")
_z3_assert(_is_int(n), "First argument must be an integer")
_z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
@ -3899,7 +3899,7 @@ def RepeatBitVec(n, a):
aaaa
"""
if __debug__:
_z3_assert(isinstance(n, int), "First argument must be an integer")
_z3_assert(_is_int(n), "First argument must be an integer")
_z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx)
@ -4580,7 +4580,7 @@ class ParamsRef:
name_sym = to_symbol(name, self.ctx)
if isinstance(val, bool):
Z3_params_set_bool(self.ctx.ref(), self.params, name_sym, val)
elif isinstance(val, int):
elif _is_int(val):
Z3_params_set_uint(self.ctx.ref(), self.params, name_sym, val)
elif isinstance(val, float):
Z3_params_set_double(self.ctx.ref(), self.params, name_sym, val)
@ -5627,7 +5627,7 @@ class ModelRef(Z3PPObject):
x -> 1
f -> [1 -> 0, else -> 0]
"""
if isinstance(idx, int):
if _is_int(idx):
if idx >= len(self):
raise IndexError
num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model)
@ -9310,7 +9310,7 @@ def IndexOf(s, substr, offset):
ctx = _get_ctx2(s, substr, ctx)
s = _coerce_seq(s, ctx)
substr = _coerce_seq(substr, ctx)
if isinstance(offset, int):
if _is_int(offset):
offset = IntVal(offset, ctx)
return SeqRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)