Repository: pysmt/pysmt
Pull request #358 (2016-10-11 15:09:29)

Improve coverage
This PR improves coverage of the test suites by mostly adding new tests.

In detail:
* Disable coverage counting for lines containing "NotImplementedError" (e.g., abstract methods)
* Add tests for constants.py
* Simplify tests for CVC4 Quantifiers
* Fixed wrong test in test_int.py
* Increase coverage for interpolator.py
* Removed unused functions in pysmt.utils
* Increase coverage for walkers.generic.Walker
* Increase coverage for SmtLibIgnoreMixin



Patch:
diff --git a/.coveragerc b/.coveragerc
index f919876..16c42d9 100644
--- a/.coveragerc
+++ b/.coveragerc
@@ -1,2 +1,12 @@
 [run]
 omit = pysmt/cmd/*
+
+[report]
+exclude_lines =
+    # Disable specific lines
+    pragma: no cover
+    # Skip methods that are not implemented
+    raise NotImplementedError
+
+    # Skip main methods
+    main()
\ No newline at end of file
diff --git a/pysmt/__init__.py b/pysmt/__init__.py
index c859148..d7006ab 100644
--- a/pysmt/__init__.py
+++ b/pysmt/__init__.py
@@ -38,6 +38,6 @@ def git_version():
         import subprocess
         git_version = subprocess.check_output(["git", "describe", "--dirty=-wip"],
                                               stderr=subprocess.STDOUT)
-        return git_version.strip()
+        return git_version.strip().decode('ascii')
     except subprocess.CalledProcessError:
-        return __version__
+        return __version__ # pragma: no cover
diff --git a/pysmt/utils.py b/pysmt/utils.py
index 37aa0f9..d9b67eb 100644
--- a/pysmt/utils.py
+++ b/pysmt/utils.py
@@ -1,7 +1,22 @@
+#
+# This file is part of pySMT.
+#
+#   Copyright 2014 Andrea Micheli and Marco Gario
+#
+#   Licensed under the Apache License, Version 2.0 (the "License");
+#   you may not use this file except in compliance with the License.
+#   You may obtain a copy of the License at
+#
+#       http://www.apache.org/licenses/LICENSE-2.0
+#
+#   Unless required by applicable law or agreed to in writing, software
+#   distributed under the License is distributed on an "AS IS" BASIS,
+#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#   See the License for the specific language governing permissions and
+#   limitations under the License.
+#
 import re
-import io
 import itertools
-from six import PY2
 
 
 def all_assignments(bool_variables, env):
@@ -43,14 +58,6 @@ def twos_complement(val, bits):
 # Python Compatibility Functions
 #
 
-
-def BufferedTextReader(fname):
-    if PY2:
-        return io.BufferedReader(io.FileIO(fname, 'r'))
-    else:
-        return io.TextIOWrapper(open(fname, 'rb'))
-
-
 def interactive_char_iterator(handle):
     c = handle.read(1)
     while c:
@@ -70,14 +77,3 @@ def quote(name, style='|'):
         return "%s%s%s" % (style, name, style)
     else:
         return name
-
-
-def unquote(name, style='|'):
-    if name.startswith(style):
-        if name.endswith(style):
-            name = name.replace("%s" % style, "\\%s" % style).replace("\\\\", "\\")
-            return name[1:-1]
-        else:
-            raise ValueError("Malformed Name")
-    else:
-        return name
diff --git a/pysmt/walkers/__init__.py b/pysmt/walkers/__init__.py
index b7657f9..733493f 100644
--- a/pysmt/walkers/__init__.py
+++ b/pysmt/walkers/__init__.py
@@ -32,6 +32,10 @@ multiple information can be extracted from the formula by navigating
 it only once.
 
 """
+
+__all__ = ["DagWalker", "TreeWalker", "IdentityDagWalker"]
+
+
 from pysmt.walkers.dag import DagWalker
 assert DagWalker
 


Test patch:
diff --git a/pysmt/test/smtlib/test_smtlibscript.py b/pysmt/test/smtlib/test_smtlibscript.py
index d2492b0..c729559 100644
--- a/pysmt/test/smtlib/test_smtlibscript.py
+++ b/pysmt/test/smtlib/test_smtlibscript.py
@@ -26,6 +26,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
 
+
 class TestSmtLibScript(TestCase):
 
     def test_basic_operations(self):
@@ -126,6 +127,33 @@ class TestSmtLibScript(TestCase):
                          solver=mock)
 
 
+    def test_smtlibignore_mixin(self):
+        """In SmtLibIgnoreMixin, all SMT-LIB methods return None."""
+        class SmtLibIgnore(SmtLibIgnoreMixin):
+            pass
+
+        solver = SmtLibIgnore()
+        self.assertIsNone(solver.set_logic(None))
+        self.assertIsNone(solver.declare_fun(None))
+        self.assertIsNone(solver.declare_const(None))
+        self.assertIsNone(solver.define_fun(None, None, None, None))
+        self.assertIsNone(solver.declare_sort(None, None))
+        self.assertIsNone(solver.define_sort(None, None, None))
+        self.assertIsNone(solver.assert_(None))
+        self.assertIsNone(solver.get_assertions())
+        self.assertIsNone(solver.check_sat())
+        self.assertIsNone(solver.get_proof())
+        self.assertIsNone(solver.get_unsat_core())
+        self.assertIsNone(solver.get_values(None))
+        self.assertIsNone(solver.get_assignment())
+        self.assertIsNone(solver.push())
+        self.assertIsNone(solver.pop())
+        self.assertIsNone(solver.get_option(None))
+        self.assertIsNone(solver.set_option(None, None))
+        self.assertIsNone(solver.get_info(None))
+        self.assertIsNone(solver.set_info(None, None))
+        self.assertIsNone(solver.exit())
+
     def test_all_parsing(self):
         # Create a small file that tests all commands of smt-lib 2
         parser = SmtLibParser()
diff --git a/pysmt/test/test_constants.py b/pysmt/test/test_constants.py
new file mode 100644
index 0000000..c9956cb
--- /dev/null
+++ b/pysmt/test/test_constants.py
@@ -0,0 +1,89 @@
+#
+# This file is part of pySMT.
+#
+#   Copyright 2014 Andrea Micheli and Marco Gario
+#
+#   Licensed under the Apache License, Version 2.0 (the "License");
+#   you may not use this file except in compliance with the License.
+#   You may obtain a copy of the License at
+#
+#       http://www.apache.org/licenses/LICENSE-2.0
+#
+#   Unless required by applicable law or agreed to in writing, software
+#   distributed under the License is distributed on an "AS IS" BASIS,
+#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#   See the License for the specific language governing permissions and
+#   limitations under the License.
+#
+from six import PY2
+from pysmt.test import TestCase, main
+
+from pysmt.constants import Fraction, Integer, HAS_GMPY
+from pysmt.constants import is_pysmt_fraction, is_pysmt_integer
+from pysmt.constants import is_python_integer, is_python_boolean, is_python_rational
+from pysmt.constants import pysmt_integer_from_integer
+from pysmt.constants import to_python_integer
+from pysmt.constants import pysmt_fraction_from_rational
+
+
+class TestConstants(TestCase):
+
+    def test_is_methods(self):
+        from fractions import Fraction as pyFraction
+
+        self.assertFalse(is_pysmt_fraction(4))
+        self.assertTrue(is_pysmt_fraction(Fraction(4)))
+
+        self.assertFalse(is_pysmt_integer(4.0))
+        self.assertTrue(is_pysmt_integer(Integer(4)))
+
+        self.assertTrue(is_python_integer(int(2)))
+        if PY2:
+            self.assertTrue(is_python_integer(long(2)))
+        if HAS_GMPY:
+            from gmpy2 import mpz
+            self.assertTrue(is_python_integer(mpz(1)))
+
+        if HAS_GMPY:
+            from gmpy2 import mpz, mpq
+            self.assertTrue(is_python_rational(mpz(1)))
+            self.assertTrue(is_python_rational(mpq(1)))
+        if PY2:
+            self.assertTrue(is_python_rational(long(1)))
+
+        self.assertTrue(is_python_rational(pyFraction(5)))
+        self.assertTrue(is_python_rational(3))
+
+        self.assertTrue(is_python_boolean(True))
+        self.assertTrue(is_python_boolean(False))
+
+    def test_pysmt_integer_from_integer(self):
+        from fractions import Fraction as pyFraction
+
+        self.assertEqual(Integer(4), pysmt_integer_from_integer(4))
+        self.assertEqual(Integer(4), pysmt_integer_from_integer(Integer(4)))
+        self.assertEqual(Integer(4), pysmt_integer_from_integer(Fraction(4)))
+        self.assertEqual(Integer(4), pysmt_integer_from_integer(pyFraction(4)))
+
+    def test_to_python_integer(self):
+        from fractions import Fraction as pyFraction
+
+        res = long(4) if PY2 else int(4)
+        self.assertEqual(res, to_python_integer(pysmt_integer_from_integer(4)))
+        self.assertEqual(res, to_python_integer(pysmt_integer_from_integer(Integer(4))))
+        self.assertEqual(res, to_python_integer(pysmt_integer_from_integer(Fraction(4))))
+        self.assertEqual(res, to_python_integer(pysmt_integer_from_integer(pyFraction(4))))
+
+
+    def test_pysmt_fraction_from_rational(self):
+        from fractions import Fraction as pyFraction
+
+        self.assertEqual(Fraction(4,5), pysmt_fraction_from_rational("4/5"))
+        self.assertEqual(Fraction(4,5), pysmt_fraction_from_rational(pyFraction(4,5)))
+        self.assertEqual(Fraction(4,5), pysmt_fraction_from_rational(Fraction(4,5)))
+        self.assertEqual(Fraction(4), pysmt_fraction_from_rational(4))
+        self.assertEqual(Fraction(4), pysmt_fraction_from_rational(Integer(4)))
+
+
+if __name__ == '__main__':
+    main()
diff --git a/pysmt/test/test_cvc4_quantifiers.py b/pysmt/test/test_cvc4_quantifiers.py
index d16e8a2..f64281a 100644
--- a/pysmt/test/test_cvc4_quantifiers.py
+++ b/pysmt/test/test_cvc4_quantifiers.py
@@ -19,7 +19,6 @@ from pysmt.test import TestCase, main, skipIfSolverNotAvailable
 from pysmt.shortcuts import Symbol, ForAll, Solver, LT, Real, Int, Implies
 from pysmt.typing import REAL, INT
 from pysmt.logics import LRA, LIA
-from pysmt.exceptions import SolverReturnedUnknownResultError
 
 
 class TestCVC4Quantifiers(TestCase):
@@ -30,11 +29,8 @@ class TestCVC4Quantifiers(TestCase):
         f = ForAll([x], Implies(x,y))
         with Solver(name='cvc4', logic=LIA) as s:
             s.add_assertion(f)
-            try:
-                res = s.solve()
-                self.assertTrue(res)
-            except SolverReturnedUnknownResultError:
-                pass
+            res = s.solve()
+            self.assertTrue(res)
 
     @skipIfSolverNotAvailable('cvc4')
     def test_int(self):
@@ -42,11 +38,8 @@ class TestCVC4Quantifiers(TestCase):
         f = ForAll([p], Implies(LT(Int(0), p), LT(q, p)))
         with Solver(name='cvc4', logic=LIA) as s:
             s.add_assertion(f)
-            try:
-                res = s.solve()
-                self.assertTrue(res)
-            except SolverReturnedUnknownResultError:
-                pass
+            res = s.solve()
+            self.assertTrue(res)
 
     @skipIfSolverNotAvailable('cvc4')
     def test_real(self):
@@ -54,11 +47,8 @@ class TestCVC4Quantifiers(TestCase):
         f = ForAll([r], Implies(LT(Real(0), r), LT(s, r)))
         with Solver(name='cvc4', logic=LRA) as s:
             s.add_assertion(f)
-            try:
-                res = s.solve()
-                self.assertTrue(res)
-            except SolverReturnedUnknownResultError:
-                pass
+            res = s.solve()
+            self.assertTrue(res)
 
 
 if __name__ == '__main__':
diff --git a/pysmt/test/test_int.py b/pysmt/test/test_int.py
index 5d1c08b..8929f84 100644
--- a/pysmt/test/test_int.py
+++ b/pysmt/test/test_int.py
@@ -15,7 +15,8 @@
 #   See the License for the specific language governing permissions and
 #   limitations under the License.
 #
-from pysmt.shortcuts import *
+from pysmt.shortcuts import (Symbol, And, Iff, Equals, LT, GT, Minus,
+                             Plus, Real, Int, ToReal)
 from pysmt.typing import INT, REAL
 from pysmt.test import TestCase, skipIfNoSolverForLogic, main
 from pysmt.logics import QF_LIA, QF_UFLIRA
@@ -40,13 +41,16 @@ class TestLIA(TestCase):
         varB = Symbol("B", INT)
 
         with self.assertRaises(TypeError):
-            f = And(LT(varA, Plus(varB, Real(1))),
-                    GT(varA, Minus(varB, Real(1))))
-            g = Equals(varB, Int(0))
+            f = And(LT(varA, Plus(varA, Real(1))),
+                    GT(varA, Minus(varB, Int(1))))
 
-            self.assertUnsat(And(f, g, Equals(varA, Real(1.2))),
-                             "Formula was expected to be unsat",
-                             logic=QF_UFLIRA)
+        f = And(LT(varA, Plus(varA, Real(1))),
+                GT(varA, ToReal(Minus(varB, Int(1)))))
+        g = Equals(varA, ToReal(varB))
+
+        self.assertUnsat(And(f, g, Equals(varA, Real(1.2))),
+                         "Formula was expected to be unsat",
+                         logic=QF_UFLIRA)
 
 
 
diff --git a/pysmt/test/test_interpolation.py b/pysmt/test/test_interpolation.py
index 8a8d43f..2278343 100644
--- a/pysmt/test/test_interpolation.py
+++ b/pysmt/test/test_interpolation.py
@@ -30,40 +30,38 @@ class TestInterpolation(TestCase):
         with self.assertRaises(NoSolverAvailableError):
             Interpolator(name="nonexistent")
 
-
     @skipIfSolverNotAvailable('z3')
     def test_binary_interpolant_z3(self):
         self._test_binary_interpolant('z3')
 
-
     @skipIfSolverNotAvailable('msat')
     def test_binary_interpolant_msat(self):
         self._test_binary_interpolant('msat')
 
-
     @skipIfSolverNotAvailable('z3')
     def test_sequence_interpolant_z3(self):
         self._test_sequence_interpolant('z3')
 
-
     @skipIfSolverNotAvailable('msat')
     def test_sequence_interpolant_msat(self):
         self._test_sequence_interpolant('msat')
 
-
     def _test_binary_interpolant(self, name):
         itp = Interpolator(name=name)
         self._bool_example(itp, True)
         self._real_example(itp, True)
         self._int_example(itp, True)
 
-
     def _test_sequence_interpolant(self, name):
         itp = Interpolator(name=name)
         self._bool_example(itp, False)
         self._real_example(itp, False)
         self._int_example(itp, False)
 
+    @skipIfSolverNotAvailable('msat')
+    def test_context(self):
+        with Interpolator() as itp:
+            self._bool_example(itp, False)
 
     def _bool_example(self, itp, binary):
         # Bool Example
diff --git a/pysmt/test/test_regressions.py b/pysmt/test/test_regressions.py
index 0419672..6ef7eb1 100644
--- a/pysmt/test/test_regressions.py
+++ b/pysmt/test/test_regressions.py
@@ -34,7 +34,7 @@ from pysmt.test.examples import get_example_formulae
 from pysmt.environment import Environment
 from pysmt.rewritings import cnf_as_set
 from pysmt.smtlib.parser import SmtLibParser
-from pysmt.smtlib.commands import DECLARE_FUN, DEFINE_FUN
+from pysmt.smtlib.commands import DECLARE_FUN
 from pysmt.smtlib.script import SmtLibCommand
 from pysmt.logics import get_closer_smtlib_logic
 from pysmt.constants import Fraction
@@ -415,7 +415,7 @@ class TestRegressions(TestCase):
         from pysmt import git_version
         v = git_version()
         self.assertIsNotNone(v)
-        parts = v.split(b"-")
+        parts = v.split("-")
         self.assertTrue(len(parts) , 4)
 
 
diff --git a/pysmt/test/test_walkers.py b/pysmt/test/test_walkers.py
index 7128e28..6af65c9 100644
--- a/pysmt/test/test_walkers.py
+++ b/pysmt/test/test_walkers.py
@@ -91,7 +91,6 @@ class TestWalkers(TestCase):
         with self.assertRaises(UnsupportedOperatorError):
             tree_walker.walk(varA)
 
-
     def test_walker_is_complete(self):
         op.ALL_TYPES.append(-1)
         with self.assertRaises(AssertionError):
@@ -160,7 +159,6 @@ class TestWalkers(TestCase):
         f_subs = substitute(f, subs).simplify()
         self.assertEqual(f_subs, TRUE())
 
-
     def test_substitution_term(self):
         x, y = FreshSymbol(REAL), FreshSymbol(REAL)
 
@@ -173,7 +171,6 @@ class TestWalkers(TestCase):
         # therefore the substitution does not yield any result.
         self.assertEqual(f_subs, f)
 
-
     def test_substitution_on_functions(self):
         i, r = FreshSymbol(INT), FreshSymbol(REAL)
         f = Symbol("f", FunctionType(BOOL, [INT, REAL]))
@@ -189,7 +186,6 @@ class TestWalkers(TestCase):
         phi_sub = substitute(phi, {r: Real(0), i: Int(0)}).simplify()
         self.assertEqual(phi_sub, Function(f, [Int(1), Real(-2)]))
 
-
     def test_iterative_get_free_variables(self):
         f = Symbol("x")
         for _ in xrange(1000):
@@ -198,6 +194,16 @@ class TestWalkers(TestCase):
         cone = f.get_free_variables()
         self.assertEqual(cone, set([Symbol("x")]))
 
+    def test_walk_error(self):
+        """All walk methods by default call walk_error."""
+        from pysmt.walkers import DagWalker
+
+        x = Symbol("x")
+        w = DagWalker()
+        for o in op.ALL_TYPES:
+            with self.assertRaises(UnsupportedOperatorError):
+                w.functions[o](x)
+
 
 if __name__ == '__main__':
     main()