Merge pull request #372 from pysmt/coverage/clean_up

CI: Tests clean-up and disable coverage

.coveragerc

@@ -1,5 +1,6 @@
 [run]
 omit = pysmt/cmd/*
+       pysmt/test/*
 
 [report]
 exclude_lines =

pysmt/test/examples.py

@@ -117,6 +117,13 @@ def get_full_example_formulae(environment=None):
                     logic=pysmt.logics.QF_BOOL
                 ),
 
+            Example(hr="((x | y) & (! (x | y)))",
+                    expr=And(Or(x, y), Not(Or(x, y))),
+                    is_valid=False,
+                    is_sat=False,
+                    logic=pysmt.logics.QF_BOOL
+                ),
+
             #
             #  LIA
             #

pysmt/test/test_back.py

@@ -63,7 +63,7 @@ def do_back(self, solver_name, z3_string_buffer=False):
                 try:
                     s = Solver(name=solver_name, logic=logic)
                     term = s.converter.convert(formula)
-                    if solver_name == "z3" and z3_string_buffer:
+                    if solver_name == "z3":
                         if z3_string_buffer:
                             res = s.converter.back_via_smtlib(term)
                         else:

pysmt/test/test_typechecker.py

@@ -170,16 +170,16 @@ def test_assert_args(self):
 
 
     def test_decorator_typecheck_result(self):
+        from pysmt.fnode import FNode, FNodeContent
+        from pysmt.operators import AND
         @typecheck_result
         def good_function():
             return self.x
 
         @typecheck_result
         def super_bad_function():
-            sb = And(self.x, self.y)
-            # !!! This hurts so badly  !!!
-            # !!! Do not try this at home !!!
-            sb._content.args[0] = self.p
+            sb = FNode(FNodeContent(node_type=AND, args=(self.p, self.p),
+                                    payload=None), -1)
             return sb
 
         good_function()

pysmt/test/test_walkers.py

@@ -15,8 +15,9 @@
 #   See the License for the specific language governing permissions and
 #   limitations under the License.
 #
-import pysmt.operators as op
+from six.moves import xrange
 
+import pysmt.operators as op
 from pysmt.shortcuts import FreshSymbol, Symbol, Int, Bool, ForAll
 from pysmt.shortcuts import And, Or, Iff, Not, Function, Real
 from pysmt.shortcuts import LT, GT, Plus, Minus, Equals
@@ -27,8 +28,7 @@
 from pysmt.formula import FormulaManager
 from pysmt.test.examples import get_example_formulae
 from pysmt.exceptions import UnsupportedOperatorError
-
-from six.moves import xrange
+from pysmt.substituter import MSSubstituter
 
 
 class TestWalkers(TestCase):
@@ -144,21 +144,25 @@ def test_substitution_on_quantifiers(self):
 
     def test_substitution_complex(self):
         x, y = FreshSymbol(REAL), FreshSymbol(REAL)
-
         # y = 0 /\ (Forall x. x > 3 /\ y < 2)
         f = And(Equals(y, Real(0)),
                 ForAll([x], And(GT(x, Real(3)), LT(y, Real(2)))))
 
-        if "MSS" in str(self.env.SubstituterClass):
-            subs = {y: Real(0),
-                    ForAll([x], And(GT(x, Real(3)), LT(Real(0), Real(2)))): TRUE()}
-        else:
-            assert "MGS" in str(self.env.SubstituterClass)
-            subs = {y: Real(0),
-                    ForAll([x], And(GT(x, Real(3)), LT(y, Real(2)))): TRUE()}
+        subs = {y: Real(0),
+                ForAll([x], And(GT(x, Real(3)), LT(y, Real(2)))): TRUE()}
         f_subs = substitute(f, subs).simplify()
         self.assertEqual(f_subs, TRUE())
 
+    def test_substitution_complex_mss(self):
+        x, y = FreshSymbol(REAL), FreshSymbol(REAL)
+        # y = 0 /\ (Forall x. x > 3 /\ y < 2)
+        f = And(Equals(y, Real(0)),
+                ForAll([x], And(GT(x, Real(3)), LT(y, Real(2)))))
+        subs = {y: Real(0),
+                ForAll([x], And(GT(x, Real(3)), LT(Real(0), Real(2)))): TRUE()}
+        f_subs = MSSubstituter(env=self.env).substitute(f, subs).simplify()
+        self.assertEqual(f_subs, TRUE())
+
     def test_substitution_term(self):
         x, y = FreshSymbol(REAL), FreshSymbol(REAL)
 

pysmt/type_checker.py

@@ -67,7 +67,7 @@ def _get_key(self, formula, **kwargs):
     def get_type(self, formula):
         """ Returns the pysmt.types type of the formula """
         res = self.walk(formula)
-        if not self.be_nice and  res is None:
+        if not self.be_nice and res is None:
             raise TypeError("The formula '%s' is not well-formed" % str(formula))
         return res