Repository: pysmt/pysmt

Issue:
Create node does not raise TypeError
When a node with an invalid type is created multiple times, PysmtTypeError is raised only on the first time.

This is because function `FormulaManger::create_node()` type checks the node only when it is created.
If the node is already present in the `FormulaManager.formulae` map, the formula is simply returned without invoking the typechecker.

## Minimal Example
```python
>>> from pysmt.exceptions import PysmtTypeError
>>> from pysmt.shortcuts import Times, Int, Real

>>> def try_building_node():
...     try:
...             a = Times(Int(2), Real(4))
...             print(f"Successfully built {a}")
...     except PysmtTypeError:
...             print("Node is not well-formed, as expected.")
...

>>> try_building_node()
Node is not well-formed, as expected.

>>> try_building_node()
Successfully built (2 * 4.0)
```

## Consequences on smtlib parsing
When parsing a smtlib script, if a TypeError is raised while building an arithmetic operator, function `SmtLibParser::__init__::fix_real` tries interpreting as reals the constant operands that were initially interpreted as integers.
There are two connected problems:

### Un-coerced expression
If the same arithmetic expression is built twice in the smtlib script, the second occurrence does not raise the TypeError and integers are not fixed.
In the following example, while the first occurrence of `(* 1 x)` is fixed into `(* 1.0 x)`, the second one is not fixed and results in a type error when trying to build the LT node.
```python
TEST_SMTLIB=\
"""
(declare-fun x () Real)
(assert (< (* 1 x) 0))
(assert (< 2 (* 1 x)))
"""
p = SmtLibParser()
script = p.get_script(StringIO(TEST_SMTLIB))
```

### Un-raised TypeError
If no integer constant is found, and therefore the arguments are not changed, `SmtLibParser::__init__::fix_real` should avoid retrying to apply again the same operator, and should raise directly a TypeError.
This is implemented by checking https://github.com/pysmt/pysmt/blob/71c35b0b82f7ea63240218777940bed06a18c60c/pysmt/smtlib/parser/parser.py#L353
which is always False (`args` is a tuple and `new_args` is a list).

While this bug should only result in a missed optimization opportunity, in combination with the `create_node` problem, it results in not finding an actual type violation. 
If `op` is actually not well-formed, when invoked again on the same arguments no TypeError is raised.

This already happens (although uncatched) in the current test suite. For example, this test should result in a type error (LT is not a BV operator), which instead is missed (no TypeError is raised).
https://github.com/pysmt/pysmt/blob/71c35b0b82f7ea63240218777940bed06a18c60c/pysmt/test/test_regressions.py#L459

Discussion:

Solution patch:
diff --git a/ci/install_unix.sh b/ci/install_unix.sh
index 401f9a20..d8048e90 100755
--- a/ci/install_unix.sh
+++ b/ci/install_unix.sh
@@ -73,7 +73,7 @@ then
     git clone https://github.com/swig/swig.git
     cd swig
     git checkout v4.0.2
-    ./autogen.sh && ./configure && make
+    ./autogen.sh && ./configure --without-pcre && make
     sudo make install
     cd ..
 fi
diff --git a/pysmt/cmd/install.py b/pysmt/cmd/install.py
index 213fad2b..3c7b0368 100755
--- a/pysmt/cmd/install.py
+++ b/pysmt/cmd/install.py
@@ -56,7 +56,8 @@ def get_requested_solvers():
         keys = requested_solvers_str.split(",")
         requested_solvers = [x.lower().strip() for x in keys]
         if "all" in requested_solvers:
-            requested_solvers = [x.InstallerClass.SOLVER for x in INSTALLERS if x != "cvc4"]
+            requested_solvers = [x.InstallerClass.SOLVER for x in INSTALLERS
+                                 if x.InstallerClass.SOLVER != "cvc4"]
     return requested_solvers
 
 
diff --git a/pysmt/cmd/installers/msat.py b/pysmt/cmd/installers/msat.py
index 5a015e69..bbdb59a7 100644
--- a/pysmt/cmd/installers/msat.py
+++ b/pysmt/cmd/installers/msat.py
@@ -45,7 +45,7 @@ def __init__(self, install_dir, bindings_dir, solver_version,
 
         archive_name = archive_name_template.format(**format)
 
-        native_link = "http://mathsat.fbk.eu/download.php?file={archive_name}"
+        native_link = "https://mathsat.fbk.eu/release/{archive_name}"
 
         SolverInstaller.__init__(self, install_dir=install_dir,
                                  bindings_dir=bindings_dir,
diff --git a/pysmt/formula.py b/pysmt/formula.py
index ed1266a3..7053b9b9 100644
--- a/pysmt/formula.py
+++ b/pysmt/formula.py
@@ -89,7 +89,9 @@ def _do_type_check(self, formula):
     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 e26ff856..f1ff1869 100644
--- a/pysmt/smtlib/parser/parser.py
+++ b/pysmt/smtlib/parser/parser.py
@@ -344,13 +344,15 @@ def fix_real(op, *args):
                 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 2ae7c9de..e54cef53 100644
--- a/pysmt/test/smtlib/test_smtlibscript.py
+++ b/pysmt/test/smtlib/test_smtlibscript.py
@@ -27,7 +27,7 @@
 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 @@ def test_define_fun_serialize_complex_type(self):
         # 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 @@ def test_all_parsing(self):
         # 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 c3912ba5..66de8653 100644
--- a/pysmt/test/test_regressions.py
+++ b/pysmt/test/test_regressions.py
@@ -456,13 +456,20 @@ def test_parse_exception(self):
             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 ccb98d0e..f9653bd2 100644
--- a/pysmt/test/test_typechecker.py
+++ b/pysmt/test/test_typechecker.py
@@ -212,6 +212,15 @@ def super_bad_function():
         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)