From e0adca60cc90950f943e70e0b73d82255ae113f6 Mon Sep 17 00:00:00 2001 From: Johannes Kliemann Date: Wed, 12 Oct 2022 15:30:49 +0000 Subject: [PATCH] Print object information on Z3TypeError (WIP) ref #776 --- rflx/expression.py | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/rflx/expression.py b/rflx/expression.py index 6eaf4d179..6b8772017 100644 --- 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,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("less 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())} | {type(z3.Int(self.left.name))}, {type(z3.Int(self.right.name))}" + ) return left < right @@ -2031,7 +2037,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 +2068,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