Remove lru_cache from z3expr functions

ref #776
AdaCore · Oct 19, 2022 · fc2df98 · fc2df98
1 parent 9384183
commit fc2df98
Showing 1 changed file with 1 addition and 40 deletions.
diff --git a/rflx/expression.py b/rflx/expression.py
@@ -1,4 +1,4 @@
-# pylint: disable=too-many-lines,too-many-ancestors,too-many-arguments,method-cache-max-size-none
+# pylint: disable=too-many-lines,too-many-ancestors,too-many-arguments
 
 from __future__ import annotations
 
@@ -11,7 +11,6 @@
 from copy import copy
 from dataclasses import dataclass
 from enum import Enum
-from functools import lru_cache
 from itertools import groupby
 from operator import itemgetter
 from sys import intern
@@ -333,7 +332,6 @@ def simplified(self) -> Expr:
     def ada_expr(self) -> ada.Expr:
         return ada.Not(self.expr.ada_expr())
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.BoolRef:
         z3expr = self.expr.z3expr()
         if not isinstance(z3expr, z3.BoolRef):
@@ -632,7 +630,6 @@ def symbol(self) -> str:
     def ada_expr(self) -> ada.Expr:
         return ada.And(*[t.ada_expr() for t in self.terms])
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.BoolRef:
         z3exprs = [t.z3expr() for t in self.terms]
         boolexprs = [t for t in z3exprs if isinstance(t, z3.BoolRef)]
@@ -677,7 +674,6 @@ def symbol(self) -> str:
     def ada_expr(self) -> ada.Expr:
         return ada.Or(*[t.ada_expr() for t in self.terms])
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.BoolRef:
         z3exprs = [t.z3expr() for t in self.terms]
         boolexprs = [t for t in z3exprs if isinstance(t, z3.BoolRef)]
@@ -806,7 +802,6 @@ def simplified(self) -> Expr:
     def ada_expr(self) -> ada.Expr:
         return ada.Number(self.value, self.base)
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ArithRef:
         return z3.IntVal(self.value)
 
@@ -876,7 +871,6 @@ def symbol(self) -> str:
     def ada_expr(self) -> ada.Expr:
         return ada.Add(*[t.ada_expr() for t in self.terms])
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ArithRef:
         terms = [t for t in map(lambda e: e.z3expr(), self.terms) if isinstance(t, z3.ArithRef)]
         if len(terms) != len(self.terms):
@@ -905,7 +899,6 @@ def symbol(self) -> str:
     def ada_expr(self) -> ada.Expr:
         return ada.Mul(*[t.ada_expr() for t in self.terms])
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ArithRef:
         terms = [t for t in map(lambda e: e.z3expr(), self.terms) if isinstance(t, z3.ArithRef)]
         if len(terms) != len(self.terms):
@@ -946,7 +939,6 @@ def symbol(self) -> str:
     def ada_expr(self) -> ada.Expr:
         return ada.Sub(self.left.ada_expr(), self.right.ada_expr())
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ArithRef:
         left = self.left.z3expr()
         right = self.right.z3expr()
@@ -974,7 +966,6 @@ def symbol(self) -> str:
     def ada_expr(self) -> ada.Expr:
         return ada.Div(self.left.ada_expr(), self.right.ada_expr())
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ArithRef:
         left = self.left.z3expr()
         right = self.right.z3expr()
@@ -1002,7 +993,6 @@ def symbol(self) -> str:
     def ada_expr(self) -> ada.Expr:
         return ada.Pow(self.left.ada_expr(), self.right.ada_expr())
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ArithRef:
         left = self.left.z3expr()
         right = self.right.z3expr()
@@ -1030,7 +1020,6 @@ def symbol(self) -> str:
     def ada_expr(self) -> ada.Expr:
         return ada.Mod(self.left.ada_expr(), self.right.ada_expr())
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ArithRef:
         left = self.left.simplified().z3expr()
         right = self.right.z3expr()
@@ -1141,7 +1130,6 @@ def variables(self) -> list[Variable]:
     def ada_expr(self) -> ada.Expr:
         return ada.Literal(self.identifier)
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         if self.identifier == ID("True"):
             return z3.BoolVal(True)
@@ -1207,7 +1195,6 @@ def variables(self) -> list[Variable]:
     def ada_expr(self) -> ada.Expr:
         return ada.Variable(self.identifier, self.negative)
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         if self.type_ == rty.BOOLEAN:
             return z3.Bool(self.name)
@@ -1473,7 +1460,6 @@ def ada_expr(self) -> ada.Expr:
         assert isinstance(result, ada.Expr)
         return result
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         raise NotImplementedError
 
@@ -1502,7 +1488,6 @@ def ada_expr(self) -> ada.Expr:
             self.prefix.ada_expr(), *[e.ada_expr() for e in self.elements], negative=self.negative
         )
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         raise NotImplementedError
 
@@ -1584,7 +1569,6 @@ def substituted(
     def ada_expr(self) -> ada.Expr:
         return ada.Selected(self.prefix.ada_expr(), ID(self.selector), self.negative)
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         if self.negative:
             return -z3.Int(self.representation)
@@ -1680,7 +1664,6 @@ def representation(self) -> str:
     def ada_expr(self) -> ada.Expr:
         return ada.Call(self.identifier, [a.ada_expr() for a in self.args], {}, self.negative)
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         raise NotImplementedError
 
@@ -1735,7 +1718,6 @@ def representation(self) -> str:
     def ada_expr(self) -> ada.Expr:
         return ada.Slice(self.prefix.ada_expr(), self.first.ada_expr(), self.last.ada_expr())
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         raise NotImplementedError
 
@@ -1754,7 +1736,6 @@ def _check_type_subexpr(self) -> RecordFluxError:
     def ada_expr(self) -> ada.Expr:
         raise NotImplementedError
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         raise NotImplementedError
 
@@ -1812,7 +1793,6 @@ def length(self) -> Expr:
     def ada_expr(self) -> ada.Expr:
         return ada.Aggregate(*[e.ada_expr() for e in self.elements])
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         return z3.BoolVal(False)
 
@@ -1844,7 +1824,6 @@ def simplified(self) -> Expr:
     def ada_expr(self) -> ada.Expr:
         return ada.String(self.data)
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         return z3.BoolVal(False)
 
@@ -1885,7 +1864,6 @@ def ada_expr(self) -> ada.Expr:
         ]
         return ada.NamedAggregate(*elements)
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         raise NotImplementedError
 
@@ -1942,7 +1920,6 @@ def simplified(self) -> Expr:
     def ada_expr(self) -> ada.Expr:
         return ada.Less(self.left.ada_expr(), self.right.ada_expr())
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.BoolRef:
         left = self.left.z3expr()
         right = self.right.z3expr()
@@ -1971,7 +1948,6 @@ def simplified(self) -> Expr:
     def ada_expr(self) -> ada.Expr:
         return ada.LessEqual(self.left.ada_expr(), self.right.ada_expr())
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.BoolRef:
         left = self.left.z3expr()
         right = self.right.z3expr()
@@ -1997,7 +1973,6 @@ def simplified(self) -> Expr:
     def ada_expr(self) -> ada.Expr:
         return ada.Equal(self.left.ada_expr(), self.right.ada_expr())
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.BoolRef:
         left = self.left.z3expr()
         right = self.right.z3expr()
@@ -2026,7 +2001,6 @@ def simplified(self) -> Expr:
     def ada_expr(self) -> ada.Expr:
         return ada.GreaterEqual(self.left.ada_expr(), self.right.ada_expr())
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.BoolRef:
         left = self.left.z3expr()
         right = self.right.z3expr()
@@ -2055,7 +2029,6 @@ def simplified(self) -> Expr:
     def ada_expr(self) -> ada.Expr:
         return ada.Greater(self.left.ada_expr(), self.right.ada_expr())
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.BoolRef:
         left = self.left.z3expr()
         right = self.right.z3expr()
@@ -2081,7 +2054,6 @@ def simplified(self) -> Expr:
     def ada_expr(self) -> ada.Expr:
         return ada.NotEqual(self.left.ada_expr(), self.right.ada_expr())
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.BoolRef:
         left = self.left.z3expr()
         right = self.right.z3expr()
@@ -2106,7 +2078,6 @@ def symbol(self) -> str:
     def ada_expr(self) -> ada.Expr:
         return ada.In(self.left.ada_expr(), self.right.ada_expr())
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.BoolRef:
         raise NotImplementedError
 
@@ -2127,7 +2098,6 @@ def symbol(self) -> str:
     def ada_expr(self) -> ada.Expr:
         return ada.NotIn(self.left.ada_expr(), self.right.ada_expr())
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.BoolRef:
         raise NotImplementedError
 
@@ -2214,7 +2184,6 @@ def ada_expr(self) -> ada.Expr:
         assert isinstance(result, ada.Expr)
         return result
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         if len(self.condition_expressions) != 1:
             raise Z3TypeError("more than one condition")
@@ -2298,7 +2267,6 @@ def ada_expr(self) -> ada.Expr:
         assert isinstance(result, ada.Expr)
         return result
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         raise NotImplementedError
 
@@ -2404,7 +2372,6 @@ def simplified(self) -> Expr:
     def ada_expr(self) -> ada.Expr:
         return ada.ValueRange(self.lower.ada_expr(), self.upper.ada_expr())
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         raise NotImplementedError
 
@@ -2503,7 +2470,6 @@ def simplified(self) -> Expr:
     def ada_expr(self) -> ada.Expr:
         return ada.Conversion(self.identifier, self.argument.ada_expr())
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         raise NotImplementedError
 
@@ -2622,7 +2588,6 @@ def precedence(self) -> Precedence:
     def ada_expr(self) -> ada.Expr:
         raise NotImplementedError
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         raise NotImplementedError
 
@@ -2772,7 +2737,6 @@ def precedence(self) -> Precedence:
     def ada_expr(self) -> ada.Expr:
         raise NotImplementedError
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         raise NotImplementedError
 
@@ -2903,7 +2867,6 @@ def precedence(self) -> Precedence:
     def ada_expr(self) -> ada.Expr:
         raise NotImplementedError
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         raise NotImplementedError
 
@@ -2979,7 +2942,6 @@ def precedence(self) -> Precedence:
     def ada_expr(self) -> ada.Expr:
         raise NotImplementedError
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         raise NotImplementedError
 
@@ -3295,7 +3257,6 @@ def ada_expr(self) -> ada.Expr:
         ]
         return ada.CaseExpr(self.expr.ada_expr(), choices)
 
-    @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         raise NotImplementedError