Repository: pysmt/pysmt
Pull request #785 (2024-10-07 14:00:03)

Fix Create node does not raise type error
Fixes: https://github.com/pysmt/pysmt/issues/784

This fixes the issue by type-checking every newly created node even when it is found in the `formulae` map.
No overhead should have been added as the type is cached.

This also fixes the tests where a type error in smtlib was not noticed, and adds new ones.

Minor: This also fixes the decision on retrying building a type-invalid node in the smtlib parser. Namely, if there are no integer constants within the arguments, there is nothing to change and an exception is directly raised.

<!--

- [ ] For bugs or new features, make sure there is a test showing the bug or demonstrating the use of the new feature
- [ ] Are all tests green?
- [ ] (First contribution only) You accepted the licensing terms by adding name and email to the CONTRIBUTORS file (see https://github.com/pysmt/pysmt/blob/master/docs/development.rst#licensing).

-->


Patch:
diff --git a/pysmt/formula.py b/pysmt/formula.py
index ed1266a..7053b9b 100644
--- a/pysmt/formula.py
+++ b/pysmt/formula.py
@@ -89,7 +89,9 @@ class FormulaManager(object):
     def create_node(self, node_type, args, payload=None):
         content = FNodeContent(node_type, args, payload)
         if content in self.formulae:
-            return self.formulae[content]
+            n = self.formulae[content]
+            self._do_type_check(n)
+            return n
         else:
             n = FNode(content, self._next_free_id)
             self._next_free_id += 1
diff --git a/pysmt/smtlib/parser/parser.py b/pysmt/smtlib/parser/parser.py
index e26ff85..f1ff186 100644
--- a/pysmt/smtlib/parser/parser.py
+++ b/pysmt/smtlib/parser/parser.py
@@ -344,13 +344,15 @@ class SmtLibParser(object):
                 get_type = self.env.stc.get_type
                 get_free_variables = self.env.fvo.get_free_variables
                 new_args = []
+                changed = False
                 for x in args:
                     if get_type(x).is_int_type() and\
                        len(get_free_variables(x)) == 0:
                         new_args.append(mgr.ToReal(x))
+                        changed = True
                     else:
                         new_args.append(x)
-                if args == new_args:
+                if not changed:
                     raise
                 return op(*new_args)
 


Test patch:
diff --git a/pysmt/test/smtlib/test_smtlibscript.py b/pysmt/test/smtlib/test_smtlibscript.py
index 2ae7c9d..e54cef5 100644
--- a/pysmt/test/smtlib/test_smtlibscript.py
+++ b/pysmt/test/smtlib/test_smtlibscript.py
@@ -27,7 +27,7 @@ from pysmt.smtlib.script import smtlibscript_from_formula, evaluate_command
 from pysmt.smtlib.parser import get_formula_strict, get_formula, SmtLibParser
 from pysmt.solvers.smtlib import SmtLibIgnoreMixin
 from pysmt.logics import QF_UFLIRA
-from pysmt.exceptions import UndefinedLogicError, PysmtValueError
+from pysmt.exceptions import UndefinedLogicError, PysmtValueError, PysmtTypeError
 
 
 
@@ -175,6 +175,29 @@ class TestSmtLibScript(TestCase):
         # No exceptions are thrown
         self.assertEqual(smtlib_script.replace('var', '__var0'), script.commands[0].serialize_to_string())
 
+    def test_twice_fix_real(self):
+        smtlib_script = "\n".join([
+            '(declare-fun r () Real)',
+            '(assert (< (* 1 r) 0))',
+            '(assert (< 2 (* 1 r)))'
+        ])
+        stream = StringIO(smtlib_script)
+        parser = SmtLibParser()
+        _ = parser.get_script(stream)
+        # No exceptions are thrown
+        self.assertTrue(True)
+
+    def test_type_error(self):
+        smtlib_script = "\n".join([
+            "(declare-sort B 0)",
+            "(declare-const e B)",
+            "(declare-const x Bool)",
+            "(assert (= e x))",
+        ])
+        stream = StringIO(smtlib_script)
+        parser = SmtLibParser()
+        with self.assertRaises(PysmtTypeError):
+            _ = parser.get_script(stream)
 
     def test_evaluate_command(self):
         class SmtLibIgnore(SmtLibIgnoreMixin):
@@ -233,14 +256,19 @@ class TestSmtLibScript(TestCase):
         # Create a small file that tests all commands of smt-lib 2
         parser = SmtLibParser()
 
+        te = 0
         nie = 0
         for cmd in DEMO_SMTSCRIPT:
             try:
                 next(parser.get_command_generator(StringIO(cmd)))
             except NotImplementedError:
                 nie += 1
+            except PysmtTypeError:
+                te += 1
         # There are currently 3 not-implemented commands
         self.assertEqual(nie, 3)
+        # There is currently 1 type error
+        self.assertEqual(te, 1)
 
 DEMO_SMTSCRIPT = [ "(declare-fun a () Bool)",
                    "(declare-fun b () Bool)",
diff --git a/pysmt/test/test_regressions.py b/pysmt/test/test_regressions.py
index c3912ba..66de865 100644
--- a/pysmt/test/test_regressions.py
+++ b/pysmt/test/test_regressions.py
@@ -456,13 +456,20 @@ class TestRegressions(TestCase):
             self.assertEqual(ex.pos_info[1], 19)
 
     def test_parse_bvconst_width(self):
-        smtlib_input = "(assert (> #x10 #x10))"
+        smtlib_input = "(assert (bvugt #x10 #x10))"
         parser = SmtLibParser()
         buffer_ = StringIO(smtlib_input)
         expr = parser.get_script(buffer_).get_last_formula()
         const = expr.args()[0]
         self.assertEqual(const.bv_width(), 8, const.bv_width())
 
+    def test_parse_bvconst_type_check(self):
+        smtlib_input = "(assert (> #x10 #x10))"
+        parser = SmtLibParser()
+        buffer_ = StringIO(smtlib_input)
+        with self.assertRaises(PysmtTypeError):
+            _ = parser.get_script(buffer_).get_last_formula()
+
     def test_equality_typing(self):
         x = Symbol('x', BOOL)
         y = Symbol('y', BOOL)
diff --git a/pysmt/test/test_typechecker.py b/pysmt/test/test_typechecker.py
index ccb98d0..f9653bd 100644
--- a/pysmt/test/test_typechecker.py
+++ b/pysmt/test/test_typechecker.py
@@ -212,6 +212,15 @@ class TestSimpleTypeChecker(TestCase):
         with self.assertRaises(PysmtTypeError):
             super_bad_function()
 
+    def test_multiple_creations(self):
+        def bad_formula():
+            return Times(self.p, self.r)
+        with self.assertRaises(PysmtTypeError):
+            bad_formula()
+        # When building the same formula a second time, should raise again.
+        with self.assertRaises(PysmtTypeError):
+            bad_formula()
+
     def test_examples(self):
         for (f, _, _, _) in get_example_formulae():
             self.assertIs(f.get_type(), BOOL, f)