Merge pull request #18 from pysmt/generator_tests_bugfix

Fixed problems in tests due to skip decorators
pysmt · Feb 24, 2015 · ec61b03 · ec61b03
2 parents 0dec7ec + 438c537
commit ec61b03
Show file tree

Hide file tree

Showing 6 changed files with 6 additions and 10 deletions.
diff --git a/pysmt/solvers/cvc4.py b/pysmt/solvers/cvc4.py
@@ -27,7 +27,7 @@
 from pysmt.solvers.eager import EagerModel
 
 class CVC4Solver(Solver, SmtLibBasicSolver, SmtLibIgnoreMixin):
-    LOGICS = pysmt.logics.PYSMT_LOGICS
+    LOGICS = pysmt.logics.PYSMT_QF_LOGICS
 
     def __init__(self, environment, logic, options=None):
         Solver.__init__(self,
@@ -38,7 +38,10 @@ def __init__(self, environment, logic, options=None):
         self.cvc4 = CVC4.SmtEngine(self.em)
         self.cvc4.setOption("produce-models", CVC4.SExpr("true"))
 
-        self.cvc4.setLogic(str(logic))
+        logic_name = str(logic)
+        if logic_name == "QF_BOOL":
+            logic_name = "QF_LRA"
+        self.cvc4.setLogic(logic_name)
         self.converter = CVC4Converter(environment, cvc4_exprMgr=self.em)
         self.declarations = set()
         return

diff --git a/pysmt/test/smtlib/test_parser_lra.py b/pysmt/test/smtlib/test_parser_lra.py
@@ -17,11 +17,9 @@
 #
 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)

diff --git a/pysmt/test/smtlib/test_parser_qf_lia.py b/pysmt/test/smtlib/test_parser_qf_lia.py
@@ -17,10 +17,8 @@
 #
 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)

diff --git a/pysmt/test/smtlib/test_parser_qf_lira.py b/pysmt/test/smtlib/test_parser_qf_lira.py
@@ -17,10 +17,8 @@
 #
 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)

diff --git a/pysmt/test/smtlib/test_parser_qf_lra.py b/pysmt/test/smtlib/test_parser_qf_lra.py
@@ -17,10 +17,8 @@
 #
 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)

diff --git a/pysmt/test/test_solving.py b/pysmt/test/test_solving.py
@@ -85,6 +85,7 @@ def test_examples_msat(self):
     def test_examples_cvc4(self):
         for (f, validity, satisfiability, logic) in get_example_formulae():
             try:
+                if not logic.quantifier_free: continue
                 v = is_valid(f, solver_name='cvc4')
                 s = is_sat(f, solver_name='cvc4')