Merge pull request #12 from pysmt/skip_for_logic_clean

 Improved test handling when solvers are not available

pysmt/logics.py

@@ -462,7 +462,7 @@ def __gt__(self, other):
 #
 PYSMT_LOGICS = [QF_BOOL, QF_IDL, QF_LIA, QF_LRA, QF_RDL, QF_UF, QF_UFIDL,
                 QF_UFLIA, QF_UFLRA, QF_UFLIRA,
-                BOOL, LRA, LIA, UFLIRA ]
+                BOOL, LRA, LIA, UFLIRA, UFLRA ]
 
 PYSMT_QF_LOGICS = [l for l in PYSMT_LOGICS if l.quantifier_free]
 

pysmt/test/__init__.py

@@ -20,6 +20,7 @@
 from functools import wraps
 
 from pysmt.shortcuts import reset_env, get_env
+from pysmt.decorators import deprecated
 
 class TestCase(unittest.TestCase):
     """Wrapper on the unittest TestCase class.
@@ -34,8 +35,10 @@ def setUp(self):
     def tearDown(self):
         pass
 
-
+@deprecated("skipIfNoSolverForLogic (be specific about expectations!)")
 def skipIfNoSolverAvailable(test_fun):
+    """Skip the test if no solver is available."""
+
     msg = "No solver available"
     cond = len(get_env().factory.all_solvers()) == 0
     @unittest.skipIf(cond, msg)
@@ -46,6 +49,7 @@ def wrapper(self, *args, **kwargs):
 
 
 class skipIfSolverNotAvailable(object):
+    """Skip a test if the given solver is not available."""
 
     def __init__(self, solver):
         self.solver = solver
@@ -58,4 +62,19 @@ def __call__(self, test_fun):
         def wrapper(*args, **kwargs):
             return test_fun(*args, **kwargs)
         return wrapper
-
+
+
+class skipIfNoSolverForLogic(object):
+    """Skip a test if there is no solver for the given logic."""
+
+    def __init__(self, logic):
+        self.logic = logic
+
+    def __call__(self, test_fun):
+        msg = "Solver for %s not available" % self.logic
+        cond = len(get_env().factory.all_solvers(logic=self.logic)) == 0
+        @unittest.skipIf(cond, msg)
+        @wraps(test_fun)
+        def wrapper(*args, **kwargs):
+            return test_fun(*args, **kwargs)
+        return wrapper

pysmt/test/smtlib/parser_utils.py

@@ -18,11 +18,11 @@
 import os
 import unittest
 
-from pysmt.test import skipIfNoSolverAvailable
 from pysmt.shortcuts import Solver, reset_env
 from pysmt.smtlib.parser import SmtLibParser
 from pysmt.smtlib.script import check_sat_filter
 from pysmt.logics import QF_LIA, QF_LRA, LRA, QF_UFLIRA
+from pysmt.exceptions import NoSolverAvailableError
 
 SMTLIB_DIR = "pysmt/test/smtlib"
 SMTLIB_TEST_FILES = [
@@ -87,15 +87,17 @@
 #  $ nosetests pysmt/test/smtlib/test_parser_qf_lra.py
 # The function 'execute_script_fname' is a generator that
 # returns the correct arguments for the test
-@skipIfNoSolverAvailable
 def execute_script_fname(smtfile, logic, expected_result):
     """Read and call a Solver to solve the instance"""
 
     reset_env()
     assert os.path.exists(smtfile)
     parser = SmtLibParser()
     script = parser.get_script_fname(smtfile)
-    log = script.evaluate(Solver(logic=logic))
+    try:
+        log = script.evaluate(Solver(logic=logic))
+    except NoSolverAvailableError:
+        raise unittest.SkipTest("No solver for logic %s." % logic)
 
     res = check_sat_filter(log)
     if res:

pysmt/test/smtlib/test_parser_lra.py

@@ -17,8 +17,11 @@
 #
 import os
 from pysmt.logics import LRA
+from pysmt.test import skipIfNoSolverForLogic
 from pysmt.test.smtlib.parser_utils import execute_script_fname, SMTLIB_TEST_FILES, SMTLIB_DIR
 
+
+@skipIfNoSolverForLogic(LRA)
 def test_generator():
     for (logic, f, expected_result) in SMTLIB_TEST_FILES:
         smtfile = os.path.join(SMTLIB_DIR, f)

pysmt/test/smtlib/test_parser_qf_lia.py

@@ -17,8 +17,10 @@
 #
 import os
 from pysmt.logics import QF_LIA
+from pysmt.test import skipIfNoSolverForLogic
 from pysmt.test.smtlib.parser_utils import execute_script_fname, SMTLIB_TEST_FILES, SMTLIB_DIR
 
+@skipIfNoSolverForLogic(QF_LIA)
 def test_generator():
     for (logic, f, expected_result) in SMTLIB_TEST_FILES:
         smtfile = os.path.join(SMTLIB_DIR, f)

pysmt/test/smtlib/test_parser_qf_lira.py

@@ -17,8 +17,10 @@
 #
 import os
 from pysmt.logics import QF_UFLIRA
+from pysmt.test import skipIfNoSolverForLogic
 from pysmt.test.smtlib.parser_utils import execute_script_fname, SMTLIB_TEST_FILES, SMTLIB_DIR
 
+@skipIfNoSolverForLogic(QF_UFLIRA)
 def test_generator():
     for (logic, f, expected_result) in SMTLIB_TEST_FILES:
         smtfile = os.path.join(SMTLIB_DIR, f)

pysmt/test/smtlib/test_parser_qf_lra.py

@@ -17,8 +17,10 @@
 #
 import os
 from pysmt.logics import QF_LRA
+from pysmt.test import skipIfNoSolverForLogic
 from pysmt.test.smtlib.parser_utils import execute_script_fname, SMTLIB_TEST_FILES, SMTLIB_DIR
 
+@skipIfNoSolverForLogic(QF_LRA)
 def test_generator():
     for (logic, f, expected_result) in SMTLIB_TEST_FILES:
         smtfile = os.path.join(SMTLIB_DIR, f)

pysmt/test/test_euf.py

@@ -17,12 +17,14 @@
 #
 from pysmt.shortcuts import *
 from pysmt.typing import INT, REAL, FunctionType
-from pysmt.test import TestCase, skipIfSolverNotAvailable, skipIfNoSolverAvailable
+from pysmt.logics import UFLRA, UFLIRA
+from pysmt.test import TestCase
+from pysmt.test import skipIfSolverNotAvailable, skipIfNoSolverForLogic
+
 
 class TestEUF(TestCase):
 
-    @skipIfSolverNotAvailable("msat")
-    @skipIfSolverNotAvailable("z3")
+    @skipIfNoSolverForLogic(UFLIRA)
     def test_euf(self):
         ftype1 = FunctionType(REAL, [REAL])
         ftype2 = FunctionType(REAL, [REAL, INT])
@@ -32,12 +34,10 @@ def test_euf(self):
 
         check = Equals(Function(f, [Real(1)]), Function(g, (Real(2), Int(4))))
 
-        self.assertTrue(is_sat(check, solver_name="msat"),
-                        "Formula was expected to be sat")
-        self.assertTrue(is_sat(check, solver_name="z3"),
+        self.assertTrue(is_sat(check, logic=UFLIRA),
                         "Formula was expected to be sat")
 
-    @skipIfNoSolverAvailable
+    @skipIfNoSolverForLogic(UFLRA)
     def test_quantified_euf(self):
         ftype1 = FunctionType(REAL, [REAL, REAL])
 
@@ -53,11 +53,10 @@ def test_quantified_euf(self):
 
         check = Implies(axiom, And(test1, test2))
 
-        self.assertTrue(is_valid(check, quantified=True),
+        self.assertTrue(is_valid(check, logic=UFLRA),
                         "Formula was expected to be valid")
 
 
-
     def test_simplify(self):
         ftype1 = FunctionType(REAL, [REAL, REAL])
 

pysmt/test/test_formula.py

@@ -22,7 +22,8 @@
 from pysmt.shortcuts import Symbol, is_sat, is_valid, Implies, GT, Plus
 from pysmt.shortcuts import get_env
 from pysmt.environment import Environment
-from pysmt.test import TestCase, skipIfNoSolverAvailable
+from pysmt.test import TestCase, skipIfNoSolverForLogic
+from pysmt.logics import QF_BOOL
 from pysmt.exceptions import NonLinearError
 from pysmt.formula import FormulaManager
 
@@ -480,14 +481,14 @@ def test_exactly_one(self):
         self.assertEqual(c, self.mgr.Bool(False),
                          "ExactlyOne should not allow 2 symbols to be True")
 
-    @skipIfNoSolverAvailable
+    @skipIfNoSolverForLogic(QF_BOOL)
     def test_exactly_one_is_sat(self):
         symbols = [ self.mgr.Symbol("s%d"%i, BOOL) for i in range(5) ]
         c = self.mgr.ExactlyOne(symbols)
         all_zero = self.mgr.And([self.mgr.Iff(s, self.mgr.Bool(False))
                                   for s in symbols])
         test_zero = self.mgr.And(c, all_zero)
-        self.assertFalse(is_sat(test_zero),
+        self.assertFalse(is_sat(test_zero, logic=QF_BOOL),
                          "ExactlyOne should not allow all symbols to be False")
 
 

pysmt/test/test_int.py

@@ -17,11 +17,12 @@
 #
 from pysmt.shortcuts import *
 from pysmt.typing import INT, REAL
-from pysmt.test import TestCase, skipIfNoSolverAvailable
+from pysmt.test import TestCase, skipIfNoSolverForLogic
+from pysmt.logics import QF_LIA, QF_UFLIRA
 
 class TestLIA(TestCase):
 
-    @skipIfNoSolverAvailable
+    @skipIfNoSolverForLogic(QF_LIA)
     def test_eq(self):
         varA = Symbol("At", INT)
         varB = Symbol("Bt", INT)
@@ -30,10 +31,10 @@ def test_eq(self):
                 GT(varA, Minus(varB, Int(1))))
         g = Equals(varA, varB)
 
-        self.assertTrue(is_valid(Iff(f, g)),
+        self.assertTrue(is_valid(Iff(f, g), logic=QF_LIA),
                         "Formulae were expected to be equivalent")
 
-    @skipIfNoSolverAvailable
+    @skipIfNoSolverForLogic(QF_LIA)
     def test_lira(self):
         varA = Symbol("A", REAL)
         varB = Symbol("B", INT)
@@ -43,7 +44,8 @@ def test_lira(self):
                     GT(varA, Minus(varB, Real(1))))
             g = Equals(varB, Int(0))
 
-            self.assertTrue(is_unsat(And(f, g, Equals(varA, Real(1.2)))),
+            self.assertTrue(is_unsat(And(f, g, Equals(varA, Real(1.2))),
+                                     logic=QF_UFLIRA),
                             "Formula was expected to be unsat")
 
 

pysmt/test/test_logics.py

@@ -105,11 +105,11 @@ def test_get_logics_min(self):
 
     def test_get_solver_by_logic(self):
         if len(get_env().factory.all_solvers()) > 0:
-            s = Solver(logic=pysmt.logics.UFLIRA)
+            s = Solver(logic=pysmt.logics.QF_BOOL)
             self.assertIsNotNone(s)
         else:
             with self.assertRaises(NoSolverAvailableError):
-                Solver(logic=pysmt.logics.UFLIRA)
+                Solver(logic=pysmt.logics.QF_BOOL)
 
         with self.assertRaises(NoSolverAvailableError):
             Solver(logic="p")

pysmt/test/test_models.py

@@ -18,13 +18,13 @@
 from pysmt.shortcuts import Solver, Symbol, And, Real, GT, LT, Implies, FALSE
 from pysmt.shortcuts import get_env
 from pysmt.typing import BOOL, REAL
-from pysmt.test import TestCase, skipIfNoSolverAvailable
-from pysmt.logics import QF_UFLIRA
+from pysmt.test import TestCase, skipIfNoSolverForLogic
+from pysmt.logics import QF_UFLIRA, QF_LRA, QF_BOOL
 
 
 class TestModels(TestCase):
 
-    @skipIfNoSolverAvailable
+    @skipIfNoSolverForLogic(QF_LRA)
     def test_get_model(self):
         varA = Symbol("A", BOOL)
         varB = Symbol("B", REAL)
@@ -35,7 +35,7 @@ def test_get_model(self):
 
         model = None
         for solver_name in get_env().factory.all_solvers(logic=QF_UFLIRA):
-            with Solver(name=solver_name) as s:
+            with Solver(name=solver_name, logic=QF_LRA) as s:
                 s.add_assertion(f1)
                 check = s.solve()
                 self.assertTrue(check)
@@ -44,11 +44,11 @@ def test_get_model(self):
             # Here the solver is gone
             self.assertEquals(model[varA], FALSE())
 
-    @skipIfNoSolverAvailable
+    @skipIfNoSolverForLogic(QF_BOOL)
     def test_get_py_value_model(self):
         varA = Symbol("A", BOOL)
 
-        with Solver() as s:
+        with Solver(logic=QF_BOOL) as s:
             s.add_assertion(varA)
             s.solve()
             model = s.get_model()

pysmt/test/test_msat_back.py

@@ -19,15 +19,14 @@
 from pysmt.shortcuts import FreshSymbol, GT, And, Plus, Real, Int, LE, Iff
 from pysmt.shortcuts import is_valid, get_env
 from pysmt.typing import REAL, INT
-from pysmt.test import TestCase
+from pysmt.test import TestCase, skipIfSolverNotAvailable
 from pysmt.test.examples import get_example_formulae
 from pysmt.logics import QF_UFLIRA
 
 
 class TestBasic(TestCase):
 
-    @unittest.skipIf('msat' not in get_env().factory.all_solvers(),
-                     "MathSAT is not available.")
+    @skipIfSolverNotAvailable("msat")
     def test_msat_back_simple(self):
         from pysmt.solvers.msat import MathSAT5Solver, MSatConverter
 
@@ -44,14 +43,12 @@ def test_msat_back_simple(self):
         term = new_converter.convert(f)
         res = new_converter.back(term)
 
-        # Checking equality is not enough: see net test as MathSAT can
-        # change the shape of the formula into a logically equivalent
-        # form.
-        self.assertTrue(is_valid(Iff(f, res)))
+        # Checking equality is not enough: MathSAT can change the
+        # shape of the formula into a logically equivalent form.
+        self.assertTrue(is_valid(Iff(f, res), logic=QF_UFLIRA))
 
 
-    @unittest.skipIf('msat' not in get_env().factory.all_solvers(),
-                     "MathSAT is not available.")
+    @skipIfSolverNotAvailable("msat")
     def test_msat_back_not_identical(self):
         from pysmt.solvers.msat import MathSAT5Solver, MSatConverter
 
@@ -68,8 +65,7 @@ def test_msat_back_not_identical(self):
         self.assertFalse(f == res)
 
 
-    @unittest.skipIf('msat' not in get_env().factory.all_solvers(),
-                     "MathSAT is not available.")
+    @skipIfSolverNotAvailable("msat")
     def test_msat_back_formulae(self):
         from pysmt.solvers.msat import MathSAT5Solver, MSatConverter
 
@@ -81,7 +77,7 @@ def test_msat_back_formulae(self):
             if logic.quantifier_free:
                 term = new_converter.convert(formula)
                 res = new_converter.back(term)
-                self.assertTrue(is_valid(Iff(formula, res)))
+                self.assertTrue(is_valid(Iff(formula, res), logic=QF_UFLIRA))
 
 
 

pysmt/test/test_regressions.py

@@ -21,7 +21,7 @@
                              Div, LT, LE, Int, ToReal)
 from pysmt.shortcuts import Solver, is_valid, get_env, is_sat
 from pysmt.typing import REAL, BOOL, INT, FunctionType
-from pysmt.test import TestCase, skipIfSolverNotAvailable, skipIfNoSolverAvailable
+from pysmt.test import TestCase, skipIfSolverNotAvailable, skipIfNoSolverForLogic
 from pysmt.logics import QF_UFLIRA, QF_BOOL
 
 
@@ -86,7 +86,7 @@ def test_simplifying_int_plus_changes_type_of_expression(self):
         new_type = get_type(f)
         self.assertEqual(new_type, old_type)
 
-    @skipIfNoSolverAvailable
+    @skipIfNoSolverForLogic(QF_UFLIRA)
     def test_nary_operators_in_solver_converter(self):
         """Conversion of n-ary operators was not handled correctly by converters."""
         x = Symbol("x")