Print object information on Z3TypeError (WIP)

ref #776
AdaCore · Oct 14, 2022 · 4512f0b · 4512f0b
1 parent e91b737
commit 4512f0b
Showing 1 changed file with 20 additions and 4 deletions.
diff --git a/rflx/expression.py b/rflx/expression.py
@@ -951,7 +951,9 @@ def z3expr(self) -> z3.ArithRef:
         left = self.left.z3expr()
         right = self.right.z3expr()
         if not isinstance(left, z3.ArithRef) or not isinstance(right, z3.ArithRef):
-            raise Z3TypeError("subtracting non-arithmetic terms")
+            raise Z3TypeError(
+                f"subtracting non-arithmetic terms: {repr(left)} - {repr(right)}, {str(left)} - {str(right)}, {type(left)} - {type(right)}; {repr(self.left)} - {repr(self.right)}; {repr(self.left.type_)} - {repr(self.right.type_)}; {type(self.left.z3expr())} - {type(self.right.z3expr())}"
+            )
         return left - right
 
 
@@ -1210,6 +1212,8 @@ def ada_expr(self) -> ada.Expr:
     @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:
         if self.type_ == rty.BOOLEAN:
+            if isinstance(self.type_, rty.Integer):
+                raise ValueError(f"{repr(self)}")
             return z3.Bool(self.name)
         if self.negative:
             return -z3.Int(self.name)
@@ -1947,7 +1951,15 @@ def z3expr(self) -> z3.BoolRef:
         left = self.left.z3expr()
         right = self.right.z3expr()
         if not isinstance(left, z3.ArithRef) or not isinstance(right, z3.ArithRef):
-            raise Z3TypeError("less relation between non-arithmetic terms")
+            l = None
+            r = None
+            if isinstance(self.left, Variable):
+                l = type(z3.Int(self.left.name))
+            if isinstance(self.right, Variable):
+                r = type(z3.Int(self.right.name))
+            raise Z3TypeError(
+                f"less relation between non-arithmetic terms: {repr(left)} - {repr(right)}, {str(left)} - {str(right)}, {type(left)} - {type(right)}; {repr(self.left)} - {repr(self.right)}; {repr(self.left.type_)} - {repr(self.right.type_)}; {type(self.left.z3expr())} - {type(self.right.z3expr())} | {l}, {r}"
+            )
         return left < right
 
 
@@ -2031,7 +2043,9 @@ def z3expr(self) -> z3.BoolRef:
         left = self.left.z3expr()
         right = self.right.z3expr()
         if not isinstance(left, z3.ArithRef) or not isinstance(right, z3.ArithRef):
-            raise Z3TypeError("greater-equal relation between non-arithmetic terms")
+            raise Z3TypeError(
+                f"less relation between non-arithmetic terms: {repr(left)} - {repr(right)}, {str(left)} - {str(right)}, {type(left)} - {type(right)}"
+            )
         return left >= right
 
 
@@ -2060,7 +2074,9 @@ def z3expr(self) -> z3.BoolRef:
         left = self.left.z3expr()
         right = self.right.z3expr()
         if not isinstance(left, z3.ArithRef) or not isinstance(right, z3.ArithRef):
-            raise Z3TypeError("greater relation between non-arithmetic terms")
+            raise Z3TypeError(
+                f"less relation between non-arithmetic terms: {repr(left)} - {repr(right)}, {str(left)} - {str(right)}, {type(left)} - {type(right)}; {repr(self.left)} - {repr(self.right)}; {repr(self.left.type_)} - {repr(self.right.type_)}; {type(self.left.z3expr())} - {type(self.right.z3expr())}"
+            )
         return left > right