Source code for pysmt.factory

#
# 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.
#
"""Factories are used to build new Solvers or Quantifier Eliminators
without the need of specifying them. For example, the user can simply
require a Solver that is able to deal with quantified theories, and
the factory will return one such solver among the available ones.
This makes it possible to write algorithms that do not depend on a
particular solver.
"""

from functools import partial
from six import iteritems

from pysmt.exceptions import (NoSolverAvailableError, SolverRedefinitionError,
                              NoLogicAvailableError,
                              SolverAPINotFound)
from pysmt.logics import QF_UFLIRA, LRA, QF_UFLRA
from pysmt.logics import AUTO as AUTO_LOGIC
from pysmt.logics import most_generic_logic, get_closer_logic
from pysmt.logics import convert_logic_from_string
from pysmt.oracles import get_logic
from pysmt.solvers.qelim import (ShannonQuantifierEliminator,
                                 SelfSubstitutionQuantifierEliminator)
from pysmt.solvers.solver import SolverOptions
from pysmt.solvers.portfolio import Portfolio

DEFAULT_SOLVER_PREFERENCE_LIST = ['msat', 'z3', 'cvc4', 'yices', 'btor',
                                  'picosat', 'bdd']
DEFAULT_QELIM_PREFERENCE_LIST = ['z3', 'msat_fm', 'msat_lw', 'bdd',
                                 'shannon', 'selfsub']
DEFAULT_INTERPOLATION_PREFERENCE_LIST = ['msat', 'z3']
DEFAULT_LOGIC = QF_UFLIRA
DEFAULT_QE_LOGIC = LRA
DEFAULT_INTERPOLATION_LOGIC = QF_UFLRA


[docs]class Factory(object): """Factory used to build Solver, QuantifierEliminators, Interpolators etc. This class contains the logic to magically select the correct solver. Moreover, this is the class providing the shortcuts is_sat, is_unsat etc. """ def __init__(self, environment, solver_preference_list=None, qelim_preference_list=None, interpolation_preference_list=None): self.environment = environment self._all_solvers = None self._all_unsat_core_solvers = None self._all_qelims = None self._all_interpolators = None self._generic_solvers = {} # if solver_preference_list is None: solver_preference_list = DEFAULT_SOLVER_PREFERENCE_LIST self.solver_preference_list = solver_preference_list if qelim_preference_list is None: qelim_preference_list = DEFAULT_QELIM_PREFERENCE_LIST self.qelim_preference_list = qelim_preference_list if interpolation_preference_list is None: interpolation_preference_list = DEFAULT_INTERPOLATION_PREFERENCE_LIST self.interpolation_preference_list = interpolation_preference_list # self._default_logic = DEFAULT_LOGIC self._default_qe_logic = DEFAULT_QE_LOGIC self._default_interpolation_logic = DEFAULT_INTERPOLATION_LOGIC self._get_available_solvers() self._get_available_qe() self._get_available_interpolators() def get_solver(self, name=None, logic=None, **options): SolverClass, closer_logic = \ self._get_solver_class(solver_list=self._all_solvers, solver_type="Solver", preference_list=self.solver_preference_list, default_logic=self.default_logic, name=name, logic=logic) return SolverClass(environment=self.environment, logic=closer_logic, **options) def get_unsat_core_solver(self, name=None, logic=None, unsat_cores_mode="all"): SolverClass, closer_logic = \ self._get_solver_class(solver_list=self._all_unsat_core_solvers, solver_type="Solver supporting Unsat Cores", preference_list=self.solver_preference_list, default_logic=self.default_logic, name=name, logic=logic) return SolverClass(environment=self.environment, logic=closer_logic, generate_models=True, unsat_cores_mode=unsat_cores_mode) def get_quantifier_eliminator(self, name=None, logic=None): SolverClass, closer_logic = \ self._get_solver_class(solver_list=self._all_qelims, solver_type="Quantifier Eliminator", preference_list=self.qelim_preference_list, default_logic=self.default_qe_logic, name=name, logic=logic) return SolverClass(environment=self.environment, logic=closer_logic) def get_interpolator(self, name=None, logic=None): SolverClass, closer_logic = \ self._get_solver_class(solver_list=self._all_interpolators, solver_type="Interpolator", preference_list=self.interpolation_preference_list, default_logic=self._default_interpolation_logic, name=name, logic=logic) return SolverClass(environment=self.environment, logic=closer_logic) def _get_solver_class(self, solver_list, solver_type, preference_list, default_logic, name=None, logic=None): if len(solver_list) == 0: raise NoSolverAvailableError("No %s is available" % solver_type) logic = convert_logic_from_string(logic) if name is not None: if name not in solver_list: raise NoSolverAvailableError("%s '%s' is not available" % \ (solver_type, name)) if logic is not None and \ name not in self._filter_solvers(solver_list, logic=logic): raise NoSolverAvailableError("%s '%s' does not support logic %s"% (solver_type, name, logic)) SolverClass = solver_list[name] if logic is None: try: logic = most_generic_logic(SolverClass.LOGICS) except NoLogicAvailableError: if default_logic in SolverClass.LOGICS: logic = default_logic else: raise NoLogicAvailableError("Cannot automatically select a logic") closer_logic = get_closer_logic(SolverClass.LOGICS, logic) return SolverClass, closer_logic if logic is None: logic = default_logic solvers = self._filter_solvers(solver_list, logic=logic) if solvers is not None and len(solvers) > 0: # Pick the first solver based on preference list SolverClass = self._pick_favorite(preference_list, solver_list, solvers) closer_logic = get_closer_logic(SolverClass.LOGICS, logic) return SolverClass, closer_logic else: raise NoSolverAvailableError("No %s is available for logic %s" % (solver_type, logic)) def _pick_favorite(self, preference_list, solver_list, solvers): for candidate in preference_list: if candidate in solvers: return solver_list[candidate] raise NoSolverAvailableError( "Cannot find a matching solver in the preference list: %s " % solvers) def add_generic_solver(self, name, args, logics, unsat_core_support=False): from pysmt.smtlib.solver import SmtLibSolver if name in self._all_solvers: raise SolverRedefinitionError("Solver %s already defined" % name) self._generic_solvers[name] = (args, logics) solver = partial(SmtLibSolver, args, LOGICS=logics) solver.LOGICS = logics solver.UNSAT_CORE_SUPPORT = unsat_core_support self._all_solvers[name] = solver # Extend preference list accordingly self.solver_preference_list.append(name) def is_generic_solver(self, name): return name in self._generic_solvers def get_generic_solver_info(self, name): return self._generic_solvers[name] def _get_available_solvers(self): installed_solvers = {} self._all_solvers = {} self._all_unsat_core_solvers = {} try: from pysmt.solvers.z3 import Z3Solver installed_solvers['z3'] = Z3Solver except SolverAPINotFound: pass try: from pysmt.solvers.msat import MathSAT5Solver installed_solvers['msat'] = MathSAT5Solver except SolverAPINotFound: pass try: from pysmt.solvers.cvc4 import CVC4Solver installed_solvers['cvc4'] = CVC4Solver except SolverAPINotFound: pass try: from pysmt.solvers.yices import YicesSolver installed_solvers['yices'] = YicesSolver except SolverAPINotFound: pass try: from pysmt.solvers.bdd import BddSolver installed_solvers['bdd'] = BddSolver except SolverAPINotFound: pass try: from pysmt.solvers.pico import PicosatSolver installed_solvers['picosat'] = PicosatSolver except SolverAPINotFound: pass try: from pysmt.solvers.btor import BoolectorSolver installed_solvers['btor'] = BoolectorSolver except SolverAPINotFound: pass # If ENV_SOLVER_LIST is set, only a subset of the installed # solvers will be available. if ENV_SOLVER_LIST is not None: for s in ENV_SOLVER_LIST: try: v = installed_solvers[s] self._all_solvers[s] = v except KeyError: pass else: self._all_solvers = installed_solvers for k,s in iteritems(self._all_solvers): try: if s.UNSAT_CORE_SUPPORT: self._all_unsat_core_solvers[k] = s except AttributeError: pass def _get_available_qe(self): self._all_qelims = {} try: from pysmt.solvers.z3 import Z3QuantifierEliminator self._all_qelims['z3'] = Z3QuantifierEliminator except SolverAPINotFound: pass try: from pysmt.solvers.msat import (MSatFMQuantifierEliminator, MSatLWQuantifierEliminator) self._all_qelims['msat_fm'] = MSatFMQuantifierEliminator self._all_qelims['msat_lw'] = MSatLWQuantifierEliminator except SolverAPINotFound: pass try: from pysmt.solvers.bdd import BddQuantifierEliminator self._all_qelims['bdd'] = BddQuantifierEliminator except SolverAPINotFound: pass # Pure-python always present self._all_qelims['shannon'] = ShannonQuantifierEliminator self._all_qelims['selfsub'] = SelfSubstitutionQuantifierEliminator def _get_available_interpolators(self): self._all_interpolators = {} try: from pysmt.solvers.z3 import Z3Interpolator self._all_interpolators['z3'] = Z3Interpolator except SolverAPINotFound: pass try: from pysmt.solvers.msat import MSatInterpolator self._all_interpolators['msat'] = MSatInterpolator except SolverAPINotFound: pass
[docs] def set_solver_preference_list(self, preference_list): """Defines the order in which to pick the solvers. The list is not required to contain all the solvers. It is possible to define a subsets of the solvers, or even just one. The impact of this, is that the solver will never be selected automatically. Note, however, that the solver can still be selected by calling it by name. """ assert preference_list is not None assert len(preference_list) > 0 self.solver_preference_list = preference_list
[docs] def set_qelim_preference_list(self, preference_list): """Defines the order in which to pick the solvers.""" assert preference_list is not None assert len(preference_list) > 0 self.qelim_preference_list = preference_list
[docs] def set_interpolation_preference_list(self, preference_list): """Defines the order in which to pick the solvers.""" assert preference_list is not None assert len(preference_list) > 0 self.interpolation_preference_list = preference_list
def _filter_solvers(self, solver_list, logic=None): """ Returns a dict <solver_name, solver_class> including all and only the solvers directly or indirectly supporting the given logic. A solver supports a logic if either the given logic is declared in the LOGICS class field or if a logic subsuming the given logic is declared in the LOGICS class field. If logic is None, the map will contain all the known solvers """ res = {} if logic is not None: for s, v in iteritems(solver_list): for l in v.LOGICS: if logic <= l: res[s] = v break return res else: solvers = solver_list return solvers
[docs] def all_solvers(self, logic=None): """ Returns a dict <solver_name, solver_class> including all and only the solvers directly or indirectly supporting the given logic. A solver supports a logic if either the given logic is declared in the LOGICS class field or if a logic subsuming the given logic is declared in the LOGICS class field. If logic is None, the map will contain all the known solvers """ return self._filter_solvers(self._all_solvers, logic=logic)
[docs] def has_solvers(self, logic=None): """ Returns true if self.all_solvers(logic) is non-empty """ return len(self.all_solvers(logic=logic)) > 0
[docs] def all_quantifier_eliminators(self, logic=None): """Returns a dict <qelim_name, qelim_class> including all and only the quantifier eliminators directly or indirectly supporting the given logic. A qelim supports a logic if either the given logic is declared in the LOGICS class field or if a logic subsuming the given logic is declared in the LOGICS class field. If logic is None, the map will contain all the known quantifier eliminators """ return self._filter_solvers(self._all_qelims, logic=logic)
[docs] def all_unsat_core_solvers(self, logic=None): """ Returns a dict <solver_name, solver_class> including all and only the solvers supporting unsat core extraction and directly or indirectly supporting the given logic. A solver supports a logic if either the given logic is declared in the LOGICS class field or if a logic subsuming the given logic is declared in the LOGICS class field. If logic is None, the map will contain all the known solvers """ return self._filter_solvers(self._all_unsat_core_solvers, logic=logic)
[docs] def all_interpolators(self, logic=None): """ Returns a dict <solver_name, solver_class> including all and only the solvers supporting interpolation and directly or indirectly supporting the given logic. A solver supports a logic if either the given logic is declared in the LOGICS class field or if a logic subsuming the given logic is declared in the LOGICS class field. If logic is None, the map will contain all the known solvers """ return self._filter_solvers(self._all_interpolators, logic=logic)
## ## Wrappers: These functions are exported in shortcuts ## def Solver(self, name=None, logic=None, **options): return self.get_solver(name=name, logic=logic, **options) def UnsatCoreSolver(self, name=None, logic=None, unsat_cores_mode="all"): return self.get_unsat_core_solver(name=name, logic=logic, unsat_cores_mode=unsat_cores_mode) def QuantifierEliminator(self, name=None, logic=None): return self.get_quantifier_eliminator(name=name, logic=logic) def Interpolator(self, name=None, logic=None): return self.get_interpolator(name=name, logic=logic) def is_sat(self, formula, solver_name=None, logic=None, portfolio=None): if logic is None or logic == AUTO_LOGIC: logic = get_logic(formula, self.environment) if portfolio is not None: solver = Portfolio(solvers_set=portfolio, environment=self.environment, logic=logic, generate_models=False, incremental=False) else: solver = self.Solver(name=solver_name, logic=logic, generate_models=False, incremental=False) with solver: return solver.is_sat(formula) def get_model(self, formula, solver_name=None, logic=None): if logic is None or logic == AUTO_LOGIC: logic = get_logic(formula, self.environment) with self.Solver(name=solver_name, logic=logic, generate_models=True, incremental=False) as solver: solver.add_assertion(formula) if solver.solve(): return solver.get_model() return None def get_implicant(self, formula, solver_name=None, logic=None): mgr = self.environment.formula_manager if logic is None or logic == AUTO_LOGIC: logic = get_logic(formula, self.environment) with self.Solver(name=solver_name, logic=logic) \ as solver: solver.add_assertion(formula) check = solver.solve() if not check: return None else: model = solver.get_model() atoms = formula.get_atoms() res = [] for a in atoms: fv = a.get_free_variables() if any(v in model for v in fv): if solver.get_value(a).is_true(): res.append(a) else: assert solver.get_value(a).is_false() res.append(mgr.Not(a)) return mgr.And(res) def get_unsat_core(self, clauses, solver_name=None, logic=None): if logic is None or logic == AUTO_LOGIC: logic = get_logic(self.environment.formula_manager.And(clauses), self.environment) with self.UnsatCoreSolver(name=solver_name, logic=logic) \ as solver: for c in clauses: solver.add_assertion(c) check = solver.solve() if check: return None return solver.get_unsat_core() def is_valid(self, formula, solver_name=None, logic=None, portfolio=None): if logic is None or logic == AUTO_LOGIC: logic = get_logic(formula, self.environment) if portfolio is not None: solver = Portfolio(solvers_set=portfolio, environment=self.environment, logic=logic, generate_models=False, incremental=False) else: solver = self.Solver(name=solver_name, logic=logic, generate_models=False, incremental=False) with solver: return solver.is_valid(formula) def is_unsat(self, formula, solver_name=None, logic=None, portfolio=None): if logic is None or logic == AUTO_LOGIC: logic = get_logic(formula, self.environment) if portfolio is not None: solver = Portfolio(solvers_set=portfolio, environment=self.environment, logic=logic, generate_models=False, incremental=False) else: solver = self.Solver(name=solver_name, logic=logic, generate_models=False, incremental=False) with solver: return solver.is_unsat(formula) def qelim(self, formula, solver_name=None, logic=None): if logic is None or logic == AUTO_LOGIC: logic = get_logic(formula, self.environment) with self.QuantifierEliminator(name=solver_name, logic=logic) as qe: return qe.eliminate_quantifiers(formula) def binary_interpolant(self, formula_a, formula_b, solver_name=None, logic=None): if logic is None or logic == AUTO_LOGIC: _And = self.environment.formula_manager.And logic = get_logic(_And(formula_a, formula_b)) with self.Interpolator(name=solver_name, logic=logic) as itp: return itp.binary_interpolant(formula_a, formula_b) def sequence_interpolant(self, formulas, solver_name=None, logic=None): if logic is None or logic == AUTO_LOGIC: _And = self.environment.formula_manager.And logic = get_logic(_And(formulas)) with self.Interpolator(name=solver_name, logic=logic) as itp: return itp.sequence_interpolant(formulas) @property def default_logic(self): return self._default_logic @default_logic.setter def default_logic(self, value): self._default_logic = value @property def default_qe_logic(self): return self._default_qe_logic @default_qe_logic.setter def default_qe_logic(self, value): self._default_qe_logic = value
# EOC Factory # Check if we have a restriction on which solvers to make available in # the current System Environment # # If PYSMT_SOLVER is "all" or unset, keep the Default preference list # # If PYSMT_SOLVER is "None" (literal None), the preference list will be empty # # Otherwise PYSMT_SOLVER is treated as a comma-separated list: e.g. # "msat, z3, cvc4" # import os ENV_SOLVER_LIST = os.environ.get("PYSMT_SOLVER") if ENV_SOLVER_LIST is not None: if ENV_SOLVER_LIST.lower() == "all": ENV_SOLVER_LIST = None elif ENV_SOLVER_LIST.lower() == "none": ENV_SOLVER_LIST = [] else: # E.g. "msat, z3" ENV_SOLVER_LIST = [s.strip() \ for s in ENV_SOLVER_LIST.lower().split(",")]