Source code for pysmt.test

#
# 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 os
from functools import wraps

try:
    import unittest2 as unittest
except ImportError:
    import unittest

from pysmt.environment import get_env, reset_env
skipIf = unittest.skipIf


[docs]class TestCase(unittest.TestCase): """Wrapper on the unittest TestCase class. This class provides setUp and tearDown methods for pySMT in which a fresh environment is provided for each test. """
[docs] def setUp(self): self.env = reset_env()
[docs] def tearDown(self): pass
if "assertRaisesRegex" not in dir(unittest.TestCase): assertRaisesRegex = unittest.TestCase.assertRaisesRegexp
[docs] def assertValid(self, formula, msg=None, solver_name=None, logic=None): """Assert that formula is VALID.""" self.assertTrue(self.env.factory.is_valid(formula=formula, solver_name=solver_name, logic=logic), msg=msg)
[docs] def assertSat(self, formula, msg=None, solver_name=None, logic=None): """Assert that formula is SAT.""" self.assertTrue(self.env.factory.is_sat(formula=formula, solver_name=solver_name, logic=logic), msg=msg)
[docs] def assertUnsat(self, formula, msg=None, solver_name=None, logic=None): """Assert that formula is UNSAT.""" self.assertTrue(self.env.factory.is_unsat(formula=formula, solver_name=solver_name, logic=logic), msg=msg)
class skipIfSolverNotAvailable(object): """Skip a test if the given solver is not available.""" def __init__(self, solver): self.solver = solver def __call__(self, test_fun): msg = "%s not available" % self.solver cond = self.solver not in get_env().factory.all_solvers() @unittest.skipIf(cond, msg) @wraps(test_fun) def wrapper(*args, **kwargs): return test_fun(*args, **kwargs) return wrapper class skipIfQENotAvailable(object): """Skip a test if the given solver is not available.""" def __init__(self, qe): self.qe = qe def __call__(self, test_fun): msg = "Quantifier Eliminator %s not available" % self.qe cond = self.qe not in get_env().factory.all_quantifier_eliminators() @unittest.skipIf(cond, msg) @wraps(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 = not get_env().factory.has_solvers(logic=self.logic) @unittest.skipIf(cond, msg) @wraps(test_fun) def wrapper(*args, **kwargs): return test_fun(*args, **kwargs) return wrapper class skipIfNoUnsatCoreSolverForLogic(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 = "Unsat Core Solver for %s not available" % self.logic cond = len(get_env().factory.all_unsat_core_solvers(logic=self.logic)) == 0 @unittest.skipIf(cond, msg) @wraps(test_fun) def wrapper(*args, **kwargs): return test_fun(*args, **kwargs) return wrapper class skipIfNoQEForLogic(object): """Skip a test if there is no quantifier eliminator for the given logic.""" def __init__(self, logic): self.logic = logic def __call__(self, test_fun): msg = "Quantifier Eliminator for %s not available" % self.logic cond = len(get_env().factory.all_quantifier_eliminators(logic=self.logic)) == 0 @unittest.skipIf(cond, msg) @wraps(test_fun) def wrapper(*args, **kwargs): return test_fun(*args, **kwargs) return wrapper # Export a main function main = unittest.main # Export SkipTest SkipTest = unittest.SkipTest