Fix Flake8 violations in Python API #5332

orsinium · 2021-06-05T06:27:22Z

This PR fixes most of the flake8 violations in Python API, except autogenerated files, so the following command passes:

flake8 --max-line-length=123 --ignore=F403,F405 z3/z3{,num,poly,printer,rcf,types,util}.py

orsinium · 2021-06-05T06:27:46Z

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):


z3/z3.py:1191:16: E741 ambiguous variable name 'l

orsinium · 2021-06-05T06:28:02Z

src/api/python/z3/z3.py

@@ -5486,9 +5486,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={}):


z3/z3.py:5730:5: F811 redefinition of unused '__deepcopy__' from line 5489

orsinium · 2021-06-05T06:28:26Z

src/api/python/z3/z3.py

@@ -5834,7 +5828,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__()))]


z3/z3.py:5837:124: E501 line too long (138 > 123 characters

orsinium · 2021-06-05T06:29:04Z

src/api/python/z3/z3.py

@@ -5793,9 +5790,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={}):


z3/z3.py:5922:5: F811 redefinition of unused '__deepcopy__' from line 5796

orsinium · 2021-06-05T06:29:19Z

src/api/python/z3/z3.py

@@ -6179,9 +6179,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={}):


z3/z3.py:6270:5: F811 redefinition of unused '__deepcopy__' from line 6182

orsinium · 2021-06-05T06:29:37Z

src/api/python/z3/z3.py

@@ -9130,12 +9127,14 @@ def set_default_rounding_mode(rm, ctx=None):
    if is_fprm_value(rm):
        _dflt_rounding_mode = rm.decl().kind()
    else:
-        _z3_assert(_dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO or


z3/z3.py:9133:68: W504 line break after binary operator z3/z3.py:9134:72: W504 line break after binary operator z3/z3.py:9135:72: W504 line break after binary operator z3/z3.py:9136:77: W504 line break after binary operator

orsinium · 2021-06-05T06:29:53Z

src/api/python/z3/z3.py

@@ -9564,10 +9563,11 @@ class FPNumRef(FPRef):
    """

    def sign(self):
-        l = (ctypes.c_int)()


z3/z3.py:9567:9: E741 ambiguous variable name 'l'

orsinium · 2021-06-05T06:30:28Z

src/api/python/z3/z3.py

@@ -9564,10 +9563,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:


z3/z3.py:9568:77: E712 comparison to False should be 'if cond is False:' or 'if not cond:'

orsinium · 2021-06-05T06:31:38Z

src/api/python/z3/z3.py

@@ -10709,14 +10709,6 @@ def SubSeq(s, offset, length):
    return Extract(s, offset, length)


-def Strings(names, ctx=None):


z3/z3.py:10712:1: F811 redefinition of unused 'Strings' from line 10694

Both implementations are the same but the first is in a better place and the second has a better docstring. So, I took docstring from the second, moved it into the first, and removed the second.

orsinium · 2021-06-05T06:31:54Z

src/api/python/z3/z3.py

@@ -10820,17 +10812,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):


z3/z3.py:10827:1: F811 redefinition of unused 'IndexOf' from line 10823

orsinium · 2021-06-05T06:32:08Z

src/api/python/z3/z3.py

@@ -11124,7 +11114,6 @@ def user_prop_pop(ctx, num_scopes):


 def user_prop_fresh(id, ctx):
-    prop = _prop_closures.get(id)


z3/z3.py:11127:5: F841 local variable 'prop' is assigned to but never used

orsinium · 2021-06-05T06:32:38Z

src/api/python/z3/z3rcf.py

@@ -12,7 +12,6 @@
 from .z3 import *
 from .z3core import *
 from .z3printer import *
-from fractions import Fraction


z3/z3rcf.py:15:1: F401 'fractions.Fraction' imported but unused

orsinium · 2021-06-05T06:33:00Z

src/api/python/z3/z3util.py

@@ -243,7 +243,7 @@ def _f():
                    emsg = "{}\n{}".format(assume, emsg)
                return emsg

-            assert is_proved == False, _f()


z3/z3util.py:246:30: E712 comparison to False should be 'if cond is False:' or 'if not cond:'

orsinium · 2021-06-05T06:33:13Z

src/api/python/z3/z3util.py

@@ -261,7 +261,7 @@ def _f():
    if models is None:  # unknown
        print("E: cannot solve !")
        return None, None
-    elif models == False:  # unsat


z3/z3util.py:264:17: E712 comparison to False should be 'if cond is False:' or 'if not cond:'

orsinium · 2021-06-05T06:33:53Z

src/api/python/z3/z3util.py

@@ -446,9 +446,9 @@ def myBinOp(op, *L):
        L = L[0]

    if z3_debug():
-        assert all(not isinstance(l, bool) for l in L)


z3/z3util.py:449:48: E741 ambiguous variable name 'l'

And it is actually confusing, I had hard times trying to visually find where is l and where is L

orsinium · 2021-06-05T06:34:31Z

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",


Here and everywhere below where I didn't left a comment, E501 line too long

orsinium · 2021-06-17T07:09:51Z

Thank you!

orsinium added 3 commits June 5, 2021 08:08

Fix flake8 violations in z3.py

c51044a

Fix flake8 violations in z3printer.py

58668c7

Fix flake8 violations in z3rcf.py and z3util.py

cca1f1c

orsinium commented Jun 5, 2021

View reviewed changes

do not allocate list on every call to set_default_rounding_mode

e531e51

NikolajBjorner merged commit 589f99e into Z3Prover:master Jun 16, 2021

orsinium deleted the flake8-123 branch June 17, 2021 07:09

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix Flake8 violations in Python API #5332

Fix Flake8 violations in Python API #5332

orsinium commented Jun 5, 2021

orsinium Jun 5, 2021

orsinium Jun 5, 2021

orsinium Jun 5, 2021

orsinium Jun 5, 2021

orsinium Jun 5, 2021

orsinium Jun 5, 2021

orsinium Jun 5, 2021

orsinium Jun 5, 2021

orsinium Jun 5, 2021

orsinium Jun 5, 2021

orsinium Jun 5, 2021

orsinium Jun 5, 2021

orsinium Jun 5, 2021

orsinium Jun 5, 2021

orsinium Jun 5, 2021

orsinium Jun 5, 2021

orsinium commented Jun 17, 2021

		@@ -1188,11 +1188,11 @@ def _coerce_exprs(a, b, ctx=None):
		return (a, b)


		def _reduce(f, l, a):

		@@ -10709,14 +10709,6 @@ def SubSeq(s, offset, length):
		return Extract(s, offset, length)


		def Strings(names, ctx=None):

		@@ -10820,17 +10812,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):

		@@ -11124,7 +11114,6 @@ def user_prop_pop(ctx, num_scopes):


		def user_prop_fresh(id, ctx):
		prop = _prop_closures.get(id)

Fix Flake8 violations in Python API #5332

Fix Flake8 violations in Python API #5332

Conversation

orsinium commented Jun 5, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

orsinium commented Jun 17, 2021