From 20a6b41c5c89a61a61a5762c13efb9b6b8e444b5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 Apr 2016 10:49:16 -0700 Subject: [PATCH] coalescing is-int check for python 2.x, issue #572 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 211b6777e..848883ba3 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -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)