From 589f99eea9a2cf019ecfcedc9f91925e78762053 Mon Sep 17 00:00:00 2001 From: Gram Date: Wed, 16 Jun 2021 17:49:47 +0200 Subject: [PATCH] Fix Flake8 violations in Python API (#5332) * Fix flake8 violations in z3.py * Fix flake8 violations in z3printer.py * Fix flake8 violations in z3rcf.py and z3util.py * do not allocate list on every call to set_default_rounding_mode --- src/api/python/z3/z3.py | 69 +++++------ src/api/python/z3/z3printer.py | 206 +++++++++++++++++++++++++-------- src/api/python/z3/z3rcf.py | 1 - src/api/python/z3/z3util.py | 8 +- 4 files changed, 189 insertions(+), 95 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 62e3fbd79b5..fe711d4f038 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1188,11 +1188,11 @@ def _coerce_exprs(a, b, ctx=None): return (a, b) -def _reduce(f, l, a): - r = a - for e in l: - r = f(r, e) - return r +def _reduce(func, sequence, initial): + result = initial + for element in sequence: + result = func(result, element) + return result def _coerce_expr_list(alist, ctx=None): @@ -5492,9 +5492,6 @@ def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal= self.goal = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs) Z3_goal_inc_ref(self.ctx.ref(), self.goal) - def __deepcopy__(self, memo={}): - return Goal(False, False, False, self.ctx, self.goal) - def __del__(self): if self.goal is not None and self.ctx.ref() is not None: Z3_goal_dec_ref(self.ctx.ref(), self.goal) @@ -5799,9 +5796,6 @@ def __init__(self, v=None, ctx=None): self.ctx = ctx Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector) - def __deepcopy__(self, memo={}): - return AstVector(self.vector, self.ctx) - def __del__(self): if self.vector is not None and self.ctx.ref() is not None: Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector) @@ -5840,7 +5834,13 @@ def __getitem__(self, i): return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx) elif isinstance(i, slice): - return [_to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, ii), self.ctx) for ii in range(*i.indices(self.__len__()))] + result = [] + for ii in range(*i.indices(self.__len__())): + result.append(_to_ast_ref( + Z3_ast_vector_get(self.ctx.ref(), self.vector, ii), + self.ctx, + )) + return result def __setitem__(self, i, v): """Update AST at position `i`. @@ -6185,9 +6185,6 @@ def __init__(self, f, ctx): if self.f is not None: Z3_func_interp_inc_ref(self.ctx.ref(), self.f) - def __deepcopy__(self, memo={}): - return FuncInterp(self.f, self.ctx) - def __del__(self): if self.f is not None and self.ctx.ref() is not None: Z3_func_interp_dec_ref(self.ctx.ref(), self.f) @@ -9131,17 +9128,21 @@ def get_default_rounding_mode(ctx=None): return RNA(ctx) +_ROUNDING_MODES = frozenset({ + Z3_OP_FPA_RM_TOWARD_ZERO, + Z3_OP_FPA_RM_TOWARD_NEGATIVE, + Z3_OP_FPA_RM_TOWARD_POSITIVE, + Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN, + Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY +}) + + def set_default_rounding_mode(rm, ctx=None): global _dflt_rounding_mode if is_fprm_value(rm): _dflt_rounding_mode = rm.decl().kind() else: - _z3_assert(_dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO or - _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE or - _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE or - _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN or - _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY, - "illegal rounding mode") + _z3_assert(_dflt_rounding_mode in _ROUNDING_MODES, "illegal rounding mode") _dflt_rounding_mode = rm @@ -9570,10 +9571,11 @@ class FPNumRef(FPRef): """ def sign(self): - l = (ctypes.c_int)() - if Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(l)) == False: + num = (ctypes.c_int)() + nsign = Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(l)) + if nsign is False: raise Z3Exception("error retrieving the sign of a numeral.") - return l.value != 0 + return num.value != 0 """The sign of a floating-point numeral as a bit-vector expression. @@ -10698,7 +10700,7 @@ def String(name, ctx=None): def Strings(names, ctx=None): - """Return string constants""" + """Return a tuple of String constants. """ ctx = _get_ctx(ctx) if isinstance(names, str): names = names.split(" ") @@ -10715,14 +10717,6 @@ def SubSeq(s, offset, length): return Extract(s, offset, length) -def Strings(names, ctx=None): - """Return a tuple of String constants. """ - ctx = _get_ctx(ctx) - if isinstance(names, str): - names = names.split(" ") - return [String(name, ctx) for name in names] - - def Empty(s): """Create the empty sequence of the given sort >>> e = Empty(StringSort()) @@ -10826,17 +10820,15 @@ def Replace(s, src, dst): return SeqRef(Z3_mk_seq_replace(src.ctx_ref(), s.as_ast(), src.as_ast(), dst.as_ast()), s.ctx) -def IndexOf(s, substr): - return IndexOf(s, substr, IntVal(0)) - - -def IndexOf(s, substr, offset): +def IndexOf(s, substr, offset=None): """Retrieve the index of substring within a string starting at a specified offset. >>> simplify(IndexOf("abcabc", "bc", 0)) 1 >>> simplify(IndexOf("abcabc", "bc", 2)) 4 """ + if offset is None: + offset = IntVal(0) ctx = None if is_expr(offset): ctx = offset.ctx @@ -11130,7 +11122,6 @@ def user_prop_pop(ctx, num_scopes): def user_prop_fresh(id, ctx): - prop = _prop_closures.get(id) _prop_closures.set_threaded() new_prop = UsePropagateBase(None, ctx) _prop_closures.set(new_prop.id, new_prop.fresh()) diff --git a/src/api/python/z3/z3printer.py b/src/api/python/z3/z3printer.py index 471c2e951ab..f9df0a99d50 100644 --- a/src/api/python/z3/z3printer.py +++ b/src/api/python/z3/z3printer.py @@ -37,38 +37,111 @@ def _z3_assert(cond, msg): # Z3 operator names to Z3Py _z3_op_to_str = { - Z3_OP_TRUE: "True", Z3_OP_FALSE: "False", Z3_OP_EQ: "==", Z3_OP_DISTINCT: "Distinct", - Z3_OP_ITE: "If", Z3_OP_AND: "And", Z3_OP_OR: "Or", Z3_OP_IFF: "==", Z3_OP_XOR: "Xor", - Z3_OP_NOT: "Not", Z3_OP_IMPLIES: "Implies", Z3_OP_IDIV: "/", Z3_OP_MOD: "%", - Z3_OP_TO_REAL: "ToReal", Z3_OP_TO_INT: "ToInt", Z3_OP_POWER: "**", Z3_OP_IS_INT: "IsInt", - Z3_OP_BADD: "+", Z3_OP_BSUB: "-", Z3_OP_BMUL: "*", Z3_OP_BOR: "|", Z3_OP_BAND: "&", - Z3_OP_BNOT: "~", Z3_OP_BXOR: "^", Z3_OP_BNEG: "-", Z3_OP_BUDIV: "UDiv", Z3_OP_BSDIV: "/", Z3_OP_BSMOD: "%", - Z3_OP_BSREM: "SRem", Z3_OP_BUREM: "URem", Z3_OP_EXT_ROTATE_LEFT: "RotateLeft", Z3_OP_EXT_ROTATE_RIGHT: "RotateRight", - Z3_OP_SLEQ: "<=", Z3_OP_SLT: "<", Z3_OP_SGEQ: ">=", Z3_OP_SGT: ">", - Z3_OP_ULEQ: "ULE", Z3_OP_ULT: "ULT", Z3_OP_UGEQ: "UGE", Z3_OP_UGT: "UGT", - Z3_OP_SIGN_EXT: "SignExt", Z3_OP_ZERO_EXT: "ZeroExt", Z3_OP_REPEAT: "RepeatBitVec", - Z3_OP_BASHR: ">>", Z3_OP_BSHL: "<<", Z3_OP_BLSHR: "LShR", - Z3_OP_CONCAT: "Concat", Z3_OP_EXTRACT: "Extract", Z3_OP_BV2INT: "BV2Int", - Z3_OP_ARRAY_MAP: "Map", Z3_OP_SELECT: "Select", Z3_OP_STORE: "Store", - Z3_OP_CONST_ARRAY: "K", Z3_OP_ARRAY_EXT: "Ext", - Z3_OP_PB_AT_MOST: "AtMost", Z3_OP_PB_LE: "PbLe", Z3_OP_PB_GE: "PbGe", Z3_OP_PB_EQ: "PbEq", - Z3_OP_SEQ_CONCAT: "Concat", Z3_OP_SEQ_PREFIX: "PrefixOf", Z3_OP_SEQ_SUFFIX: "SuffixOf", - Z3_OP_SEQ_UNIT: "Unit", Z3_OP_SEQ_CONTAINS: "Contains", Z3_OP_SEQ_REPLACE: "Replace", - Z3_OP_SEQ_AT: "At", Z3_OP_SEQ_NTH: "Nth", Z3_OP_SEQ_INDEX: "IndexOf", - Z3_OP_SEQ_LAST_INDEX: "LastIndexOf", Z3_OP_SEQ_LENGTH: "Length", Z3_OP_STR_TO_INT: "StrToInt", Z3_OP_INT_TO_STR: "IntToStr", - Z3_OP_SEQ_IN_RE: "InRe", Z3_OP_SEQ_TO_RE: "Re", - Z3_OP_RE_PLUS: "Plus", Z3_OP_RE_STAR: "Star", Z3_OP_RE_OPTION: "Option", Z3_OP_RE_UNION: "Union", Z3_OP_RE_RANGE: "Range", - Z3_OP_RE_INTERSECT: "Intersect", Z3_OP_RE_COMPLEMENT: "Complement", - Z3_OP_FPA_IS_NAN: "fpIsNaN", Z3_OP_FPA_IS_INF: "fpIsInf", Z3_OP_FPA_IS_ZERO: "fpIsZero", - Z3_OP_FPA_IS_NORMAL: "fpIsNormal", Z3_OP_FPA_IS_SUBNORMAL: "fpIsSubnormal", - Z3_OP_FPA_IS_NEGATIVE: "fpIsNegative", Z3_OP_FPA_IS_POSITIVE: "fpIsPositive", + Z3_OP_TRUE: "True", + Z3_OP_FALSE: "False", + Z3_OP_EQ: "==", + Z3_OP_DISTINCT: "Distinct", + Z3_OP_ITE: "If", + Z3_OP_AND: "And", + Z3_OP_OR: "Or", + Z3_OP_IFF: "==", + Z3_OP_XOR: "Xor", + Z3_OP_NOT: "Not", + Z3_OP_IMPLIES: "Implies", + + Z3_OP_IDIV: "/", + Z3_OP_MOD: "%", + Z3_OP_TO_REAL: "ToReal", + Z3_OP_TO_INT: "ToInt", + Z3_OP_POWER: "**", + Z3_OP_IS_INT: "IsInt", + Z3_OP_BADD: "+", + Z3_OP_BSUB: "-", + Z3_OP_BMUL: "*", + Z3_OP_BOR: "|", + Z3_OP_BAND: "&", + Z3_OP_BNOT: "~", + Z3_OP_BXOR: "^", + Z3_OP_BNEG: "-", + Z3_OP_BUDIV: "UDiv", + Z3_OP_BSDIV: "/", + Z3_OP_BSMOD: "%", + Z3_OP_BSREM: "SRem", + Z3_OP_BUREM: "URem", + + Z3_OP_EXT_ROTATE_LEFT: "RotateLeft", + Z3_OP_EXT_ROTATE_RIGHT: "RotateRight", + + Z3_OP_SLEQ: "<=", + Z3_OP_SLT: "<", + Z3_OP_SGEQ: ">=", + Z3_OP_SGT: ">", + + Z3_OP_ULEQ: "ULE", + Z3_OP_ULT: "ULT", + Z3_OP_UGEQ: "UGE", + Z3_OP_UGT: "UGT", + Z3_OP_SIGN_EXT: "SignExt", + Z3_OP_ZERO_EXT: "ZeroExt", + + Z3_OP_REPEAT: "RepeatBitVec", + Z3_OP_BASHR: ">>", + Z3_OP_BSHL: "<<", + Z3_OP_BLSHR: "LShR", + + Z3_OP_CONCAT: "Concat", + Z3_OP_EXTRACT: "Extract", + Z3_OP_BV2INT: "BV2Int", + Z3_OP_ARRAY_MAP: "Map", + Z3_OP_SELECT: "Select", + Z3_OP_STORE: "Store", + Z3_OP_CONST_ARRAY: "K", + Z3_OP_ARRAY_EXT: "Ext", + + Z3_OP_PB_AT_MOST: "AtMost", + Z3_OP_PB_LE: "PbLe", + Z3_OP_PB_GE: "PbGe", + Z3_OP_PB_EQ: "PbEq", + + Z3_OP_SEQ_CONCAT: "Concat", + Z3_OP_SEQ_PREFIX: "PrefixOf", + Z3_OP_SEQ_SUFFIX: "SuffixOf", + Z3_OP_SEQ_UNIT: "Unit", + Z3_OP_SEQ_CONTAINS: "Contains", + Z3_OP_SEQ_REPLACE: "Replace", + Z3_OP_SEQ_AT: "At", + Z3_OP_SEQ_NTH: "Nth", + Z3_OP_SEQ_INDEX: "IndexOf", + Z3_OP_SEQ_LAST_INDEX: "LastIndexOf", + Z3_OP_SEQ_LENGTH: "Length", + Z3_OP_STR_TO_INT: "StrToInt", + Z3_OP_INT_TO_STR: "IntToStr", + + Z3_OP_SEQ_IN_RE: "InRe", + Z3_OP_SEQ_TO_RE: "Re", + Z3_OP_RE_PLUS: "Plus", + Z3_OP_RE_STAR: "Star", + Z3_OP_RE_OPTION: "Option", + Z3_OP_RE_UNION: "Union", + Z3_OP_RE_RANGE: "Range", + Z3_OP_RE_INTERSECT: "Intersect", + Z3_OP_RE_COMPLEMENT: "Complement", + + Z3_OP_FPA_IS_NAN: "fpIsNaN", + Z3_OP_FPA_IS_INF: "fpIsInf", + Z3_OP_FPA_IS_ZERO: "fpIsZero", + Z3_OP_FPA_IS_NORMAL: "fpIsNormal", + Z3_OP_FPA_IS_SUBNORMAL: "fpIsSubnormal", + Z3_OP_FPA_IS_NEGATIVE: "fpIsNegative", + Z3_OP_FPA_IS_POSITIVE: "fpIsPositive", } # List of infix operators _z3_infix = [ Z3_OP_EQ, Z3_OP_IFF, Z3_OP_ADD, Z3_OP_SUB, Z3_OP_MUL, Z3_OP_DIV, Z3_OP_IDIV, Z3_OP_MOD, Z3_OP_POWER, - Z3_OP_LE, Z3_OP_LT, Z3_OP_GE, Z3_OP_GT, Z3_OP_BADD, Z3_OP_BSUB, Z3_OP_BMUL, Z3_OP_BSDIV, Z3_OP_BSMOD, Z3_OP_BOR, Z3_OP_BAND, - Z3_OP_BXOR, Z3_OP_BSDIV, Z3_OP_SLEQ, Z3_OP_SLT, Z3_OP_SGEQ, Z3_OP_SGT, Z3_OP_BASHR, Z3_OP_BSHL + Z3_OP_LE, Z3_OP_LT, Z3_OP_GE, Z3_OP_GT, Z3_OP_BADD, Z3_OP_BSUB, Z3_OP_BMUL, + Z3_OP_BSDIV, Z3_OP_BSMOD, Z3_OP_BOR, Z3_OP_BAND, + Z3_OP_BXOR, Z3_OP_BSDIV, Z3_OP_SLEQ, Z3_OP_SLT, Z3_OP_SGEQ, Z3_OP_SGT, Z3_OP_BASHR, Z3_OP_BSHL, ] _z3_unary = [Z3_OP_UMINUS, Z3_OP_BNOT, Z3_OP_BNEG] @@ -83,33 +156,53 @@ def _z3_assert(cond, msg): Z3_OP_BAND: 5, Z3_OP_BXOR: 6, Z3_OP_BOR: 7, - Z3_OP_LE: 8, Z3_OP_LT: 8, Z3_OP_GE: 8, Z3_OP_GT: 8, Z3_OP_EQ: 8, Z3_OP_SLEQ: 8, Z3_OP_SLT: 8, Z3_OP_SGEQ: 8, Z3_OP_SGT: 8, - Z3_OP_IFF: 8, + Z3_OP_LE: 8, Z3_OP_LT: 8, Z3_OP_GE: 8, Z3_OP_GT: 8, Z3_OP_EQ: 8, Z3_OP_SLEQ: 8, + Z3_OP_SLT: 8, Z3_OP_SGEQ: 8, Z3_OP_SGT: 8, Z3_OP_IFF: 8, Z3_OP_FPA_NEG: 1, Z3_OP_FPA_MUL: 2, Z3_OP_FPA_DIV: 2, Z3_OP_FPA_REM: 2, Z3_OP_FPA_FMA: 2, Z3_OP_FPA_ADD: 3, Z3_OP_FPA_SUB: 3, - Z3_OP_FPA_LE: 8, Z3_OP_FPA_LT: 8, Z3_OP_FPA_GE: 8, Z3_OP_FPA_GT: 8, Z3_OP_FPA_EQ: 8 + Z3_OP_FPA_LE: 8, Z3_OP_FPA_LT: 8, Z3_OP_FPA_GE: 8, Z3_OP_FPA_GT: 8, Z3_OP_FPA_EQ: 8, } # FPA operators _z3_op_to_fpa_normal_str = { - Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven()", Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway()", - Z3_OP_FPA_RM_TOWARD_POSITIVE: "RoundTowardPositive()", Z3_OP_FPA_RM_TOWARD_NEGATIVE: "RoundTowardNegative()", + Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven()", + Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway()", + Z3_OP_FPA_RM_TOWARD_POSITIVE: "RoundTowardPositive()", + Z3_OP_FPA_RM_TOWARD_NEGATIVE: "RoundTowardNegative()", Z3_OP_FPA_RM_TOWARD_ZERO: "RoundTowardZero()", - Z3_OP_FPA_PLUS_INF: "fpPlusInfinity", Z3_OP_FPA_MINUS_INF: "fpMinusInfinity", - Z3_OP_FPA_NAN: "fpNaN", Z3_OP_FPA_PLUS_ZERO: "fpPZero", Z3_OP_FPA_MINUS_ZERO: "fpNZero", - Z3_OP_FPA_ADD: "fpAdd", Z3_OP_FPA_SUB: "fpSub", Z3_OP_FPA_NEG: "fpNeg", Z3_OP_FPA_MUL: "fpMul", - Z3_OP_FPA_DIV: "fpDiv", Z3_OP_FPA_REM: "fpRem", Z3_OP_FPA_ABS: "fpAbs", - Z3_OP_FPA_MIN: "fpMin", Z3_OP_FPA_MAX: "fpMax", - Z3_OP_FPA_FMA: "fpFMA", Z3_OP_FPA_SQRT: "fpSqrt", Z3_OP_FPA_ROUND_TO_INTEGRAL: "fpRoundToIntegral", - - Z3_OP_FPA_EQ: "fpEQ", Z3_OP_FPA_LT: "fpLT", Z3_OP_FPA_GT: "fpGT", Z3_OP_FPA_LE: "fpLEQ", + Z3_OP_FPA_PLUS_INF: "fpPlusInfinity", + Z3_OP_FPA_MINUS_INF: "fpMinusInfinity", + Z3_OP_FPA_NAN: "fpNaN", + Z3_OP_FPA_PLUS_ZERO: "fpPZero", + Z3_OP_FPA_MINUS_ZERO: "fpNZero", + Z3_OP_FPA_ADD: "fpAdd", + Z3_OP_FPA_SUB: "fpSub", + Z3_OP_FPA_NEG: "fpNeg", + Z3_OP_FPA_MUL: "fpMul", + Z3_OP_FPA_DIV: "fpDiv", + Z3_OP_FPA_REM: "fpRem", + Z3_OP_FPA_ABS: "fpAbs", + Z3_OP_FPA_MIN: "fpMin", + Z3_OP_FPA_MAX: "fpMax", + Z3_OP_FPA_FMA: "fpFMA", + Z3_OP_FPA_SQRT: "fpSqrt", + Z3_OP_FPA_ROUND_TO_INTEGRAL: "fpRoundToIntegral", + + Z3_OP_FPA_EQ: "fpEQ", + Z3_OP_FPA_LT: "fpLT", + Z3_OP_FPA_GT: "fpGT", + Z3_OP_FPA_LE: "fpLEQ", Z3_OP_FPA_GE: "fpGEQ", - Z3_OP_FPA_FP: "fpFP", Z3_OP_FPA_TO_FP: "fpToFP", Z3_OP_FPA_TO_FP_UNSIGNED: "fpToFPUnsigned", - Z3_OP_FPA_TO_UBV: "fpToUBV", Z3_OP_FPA_TO_SBV: "fpToSBV", Z3_OP_FPA_TO_REAL: "fpToReal", - Z3_OP_FPA_TO_IEEE_BV: "fpToIEEEBV" + Z3_OP_FPA_FP: "fpFP", + Z3_OP_FPA_TO_FP: "fpToFP", + Z3_OP_FPA_TO_FP_UNSIGNED: "fpToFPUnsigned", + Z3_OP_FPA_TO_UBV: "fpToUBV", + Z3_OP_FPA_TO_SBV: "fpToSBV", + Z3_OP_FPA_TO_REAL: "fpToReal", + Z3_OP_FPA_TO_IEEE_BV: "fpToIEEEBV", } _z3_op_to_fpa_pretty_str = { @@ -131,8 +224,19 @@ def _z3_assert(cond, msg): ] +_ASSOC_OPS = frozenset({ + Z3_OP_BOR, + Z3_OP_BXOR, + Z3_OP_BAND, + Z3_OP_ADD, + Z3_OP_BADD, + Z3_OP_MUL, + Z3_OP_BMUL, +}) + + def _is_assoc(k): - return k == Z3_OP_BOR or k == Z3_OP_BXOR or k == Z3_OP_BAND or k == Z3_OP_ADD or k == Z3_OP_BADD or k == Z3_OP_MUL or k == Z3_OP_BMUL + return k in _ASSOC_OPS def _is_left_assoc(k): @@ -938,18 +1042,18 @@ def pp_unary_param(self, a, d, xs): return seq1(self.pp_name(a), [to_format(p), arg]) def pp_extract(self, a, d, xs): - h = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0) - l = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 1) + high = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0) + low = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 1) arg = self.pp_expr(a.arg(0), d + 1, xs) - return seq1(self.pp_name(a), [to_format(h), to_format(l), arg]) + return seq1(self.pp_name(a), [to_format(high), to_format(low), arg]) def pp_loop(self, a, d, xs): - l = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0) + low = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0) arg = self.pp_expr(a.arg(0), d + 1, xs) if Z3_get_decl_num_parameters(a.ctx_ref(), a.decl().ast) > 1: - h = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 1) - return seq1("Loop", [arg, to_format(l), to_format(h)]) - return seq1("Loop", [arg, to_format(l)]) + high = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 1) + return seq1("Loop", [arg, to_format(low), to_format(high)]) + return seq1("Loop", [arg, to_format(low)]) def pp_set(self, id, a): return seq1(id, [self.pp_sort(a.sort())]) diff --git a/src/api/python/z3/z3rcf.py b/src/api/python/z3/z3rcf.py index d8175b2d147..019e372e212 100644 --- a/src/api/python/z3/z3rcf.py +++ b/src/api/python/z3/z3rcf.py @@ -12,7 +12,6 @@ from .z3 import * from .z3core import * from .z3printer import * -from fractions import Fraction def _to_rcfnum(num, ctx=None): diff --git a/src/api/python/z3/z3util.py b/src/api/python/z3/z3util.py index fac4328957d..071e2b60e05 100644 --- a/src/api/python/z3/z3util.py +++ b/src/api/python/z3/z3util.py @@ -243,7 +243,7 @@ def _f(): emsg = "{}\n{}".format(assume, emsg) return emsg - assert is_proved == False, _f() + assert is_proved is False, _f() to_prove = Implies(assume, to_prove) @@ -261,7 +261,7 @@ def _f(): if models is None: # unknown print("E: cannot solve !") return None, None - elif models == False: # unsat + elif models is False: # unsat return True, None else: # sat if z3_debug(): @@ -446,9 +446,9 @@ def myBinOp(op, *L): L = L[0] if z3_debug(): - assert all(not isinstance(l, bool) for l in L) + assert all(not isinstance(val, bool) for val in L) - L = [l for l in L if is_expr(l)] + L = [val for val in L if is_expr(val)] if L: if len(L) == 1: return L[0]