Merge pull request #358 from pysmt/coverage/constants

Improve coverage

.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()

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

pysmt/test/smtlib/test_smtlibscript.py

@@ -26,6 +26,7 @@
 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 SmtLibIgnore(SmtLibIgnoreMixin):
                          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()

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()

pysmt/test/test_cvc4_quantifiers.py

@@ -19,7 +19,6 @@
 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,35 +29,26 @@ def test_bool(self):
         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):
         p, q = Symbol("p", INT), Symbol("q", INT)
         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):
         r, s = Symbol("r", REAL), Symbol("s", REAL)
         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__':

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 @@ def test_lira(self):
         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)
 
 
 

pysmt/test/test_interpolation.py

@@ -30,40 +30,38 @@ def test_selection(self):
         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

pysmt/test/test_regressions.py

@@ -34,7 +34,7 @@
 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 @@ def test_git_version(self):
         from pysmt import git_version
         v = git_version()
         self.assertIsNotNone(v)
-        parts = v.split(b"-")
+        parts = v.split("-")
         self.assertTrue(len(parts) , 4)
 
 

pysmt/test/test_walkers.py

@@ -91,7 +91,6 @@ def test_undefined_node(self):
         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 @@ def test_substitution_complex(self):
         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 @@ def test_substitution_term(self):
         # 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 @@ def test_substitution_on_functions(self):
         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 @@ def test_iterative_get_free_variables(self):
         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()