Skip to content

Commit

Permalink
Merge pull request #72 from pysmt/quant_elim_selector
Browse files Browse the repository at this point in the history 
Improved Quantifiler Elimination selection by making it more consistent with solver selection.
  • Loading branch information
marcogario committed Apr 16, 2015
2 parents 7cfb250 + 7d3ca3c commit 2d42b3c
Show file tree
Hide file tree
Showing 9 changed files with 217 additions and 142 deletions.
5 changes: 5 additions & 0 deletions docs/CHANGES.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,11 @@ General:
solvers. Dedicated shortcuts (get_unsat_core and UnsatCoreSolver)
have been added.

* QuantifierEliminator and qelim shortcuts, as well as the respective
factory methods can now accept a 'logic' parameter that allows to
select a quantifier eliminator instance supporting a given logic
(analogously to what happens for solvers).



0.2.4: 2015-03-15 -- PicoSAT
Expand Down
243 changes: 127 additions & 116 deletions pysmt/factory.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,17 +26,17 @@
from functools import partial
from six import iteritems

from pysmt.exceptions import NoSolverAvailableError, SolverRedefinitionError
from pysmt.logics import QF_UFLIRA
from pysmt.exceptions import (NoSolverAvailableError, SolverRedefinitionError,
NoLogicAvailableError)
from pysmt.logics import QF_UFLIRA, LRA
from pysmt.logics import AUTO as AUTO_LOGIC
from pysmt.logics import most_generic_logic, get_closer_logic
from pysmt.oracles import get_logic

import pysmt.solvers.solver

DEFAULT_SOLVER_PREFERENCE_LIST = ['msat', 'z3', 'cvc4', 'yices', 'picosat', 'bdd']
DEFAULT_QELIM_PREFERENCE_LIST = ['z3', 'msat_fm', 'msat_lw']
DEFAULT_LOGIC = QF_UFLIRA
DEFAULT_QE_LOGIC = LRA

class Factory(object):

Expand All @@ -45,7 +45,7 @@ def __init__(self, environment,
qelim_preference_list=None):
self.environment = environment
self._all_solvers = None
self._unsat_core_solvers = None
self._all_unsat_core_solvers = None
self._all_qelims = None
self._generic_solvers = {}

Expand All @@ -57,6 +57,7 @@ def __init__(self, environment,
qelim_preference_list = DEFAULT_QELIM_PREFERENCE_LIST
self.qelim_preference_list = qelim_preference_list
self._default_logic = DEFAULT_LOGIC
self._default_qe_logic = DEFAULT_QE_LOGIC

self._get_available_solvers()
self._get_available_qe()
Expand All @@ -69,41 +70,17 @@ def get_solver(self, quantified=False, name=None, logic=None):
if quantified is True:
logic = self.default_logic.get_quantified_version

if name is not None:
if name in self._all_solvers:
if logic is None:
SolverClass = self._all_solvers[name]
logic = most_generic_logic(SolverClass.LOGICS)
else:
if name in self.all_solvers(logic=logic):
SolverClass = self._all_solvers[name]
else:
raise NoSolverAvailableError("Solver '%s' does not" \
" support logic %s" %
(name, logic))

closer_logic = get_closer_logic(SolverClass.LOGICS, logic)
return SolverClass(environment=self.environment,
logic=closer_logic,
user_options={"generate_models":True})
else:
raise NoSolverAvailableError("Solver %s is not available" % name)

if logic is None:
logic = self.default_logic

solvers = self.all_solvers(logic=logic)
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)

if solvers is not None and len(solvers) > 0:
# Pick the first solver based on preference list
SolverClass = self.pick_favorite_solver(solvers)
closer_logic = get_closer_logic(SolverClass.LOGICS, logic)
return SolverClass(environment=self.environment,
logic=closer_logic,
user_options={"generate_models":True})
else:
raise NoSolverAvailableError("No solver is available for logic %s" %\
logic)
return SolverClass(environment=self.environment,
logic=closer_logic,
user_options={"generate_models" : True})


def get_unsat_core_solver(self, quantified=False, name=None,
Expand All @@ -114,75 +91,84 @@ def get_unsat_core_solver(self, quantified=False, name=None,
if quantified is True:
logic = self.default_logic.get_quantified_version

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,
user_options={"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_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)

if name is not None:
if name in self._unsat_core_solvers:
if logic is None:
SolverClass = self._unsat_core_solvers[name]
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)
else:
if name in self.all_unsat_core_solvers(logic=logic):
SolverClass = self._unsat_core_solvers[name]
except NoLogicAvailableError:
if default_logic in SolverClass.LOGICS:
logic = default_logic
else:
raise NoSolverAvailableError("Solver '%s' does not" \
" support logic %s" %
(name, logic))

closer_logic = get_closer_logic(SolverClass.LOGICS, logic)
return SolverClass(environment=self.environment,
logic=closer_logic,
user_options={"generate_models" : True,
"unsat_cores_mode" : unsat_cores_mode})
else:
raise NoSolverAvailableError("Solver %s has no support for " \
"unsat cores" % name)
raise NoLogicAvailableError("Cannot automatically select a logic")

closer_logic = get_closer_logic(SolverClass.LOGICS, logic)

return SolverClass, closer_logic

if logic is None:
logic = self.default_logic
logic = default_logic

solvers = self.all_unsat_core_solvers(logic=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_solver(solvers)
SolverClass = self._pick_favorite(preference_list, solver_list, solvers)
closer_logic = get_closer_logic(SolverClass.LOGICS, logic)
return SolverClass(environment=self.environment,
logic=closer_logic,
user_options={"generate_models" : True,
"unsat_cores_mode" : unsat_cores_mode})
else:
raise NoSolverAvailableError("No solver supporting unsat cores is" \
" available for logic %s" % logic)

return SolverClass, closer_logic


def get_quantifier_eliminator(self, name=None):
if len(self._all_qelims) == 0:
raise NoSolverAvailableError("No quantifier eliminator is available")

if name is None:
QElimClass = self.pick_favorite_qelim(self._all_qelims)
elif name in self._all_qelims:
QElimClass = self._all_qelims[name]
else:
raise NoSolverAvailableError("No quantifier eliminator %s" % name)
raise NoSolverAvailableError("No %s is available for logic %s" %
(solver_type, logic))

return QElimClass(self.environment)


def pick_favorite_solver(self, solvers):
for candidate in self.solver_preference_list:
def _pick_favorite(self, preference_list, solver_list, solvers):
for candidate in preference_list:
if candidate in solvers:
return self._all_solvers[candidate]
return solver_list[candidate]
raise NoSolverAvailableError(
"Cannot find a matching solver in the preference list: %s "% solvers)


def pick_favorite_qelim(self, qelims):
for candidate in self.qelim_preference_list:
if candidate in qelims:
return self._all_qelims[candidate]
raise NoSolverAvailableError("Cannot find a matching quantifier " \
"eliminator in the preference list")
"Cannot find a matching solver in the preference list: %s " % solvers)


def add_generic_solver(self, name, args, logics, unsat_core_support=False):
Expand All @@ -203,7 +189,7 @@ def get_generic_solver_info(self, name):

def _get_available_solvers(self):
self._all_solvers = {}
self._unsat_core_solvers = {}
self._all_unsat_core_solvers = {}

try:
from pysmt.solvers.z3 import Z3Solver
Expand Down Expand Up @@ -252,7 +238,7 @@ def _get_available_solvers(self):
for k,s in iteritems(self._all_solvers):
try:
if s.UNSAT_CORE_SUPPORT:
self._unsat_core_solvers[k] = s
self._all_unsat_core_solvers[k] = s
except AttributeError:
pass

Expand Down Expand Up @@ -295,8 +281,7 @@ def set_qelim_preference_list(self, preference_list):
assert len(preference_list) > 0
self.qelim_preference_list = preference_list


def all_solvers(self, logic=None):
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.
Expand All @@ -308,17 +293,45 @@ def all_solvers(self, logic=None):
"""
res = {}
if logic is not None:
for s, v in iteritems(self._all_solvers):
for s, v in iteritems(solver_list):
for l in v.LOGICS:
if logic <= l:
res[s] = v
break
return res
else:
solvers = self._all_solvers
solvers = solver_list

return solvers


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)


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)


def all_unsat_core_solvers(self, logic=None):
"""
Returns a dict <solver_name, solver_class> including all and only
Expand All @@ -329,23 +342,10 @@ 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(self._unsat_core_solvers):
for l in v.LOGICS:
if logic <= l:
res[s] = v
break
return res
else:
solvers = self._unsat_core_solvers
return self._filter_solvers(self._all_unsat_core_solvers, logic=logic)

return solvers

def all_qelims(self):
return self._all_qelims

##
## Wrappers: These functions are exported in shortcuts
Expand All @@ -363,8 +363,8 @@ def UnsatCoreSolver(self, quantified=False, name=None, logic=None,
unsat_cores_mode=unsat_cores_mode)


def QuantifierEliminator(self, name=None):
return self.get_quantifier_eliminator(name=name)
def QuantifierEliminator(self, name=None, logic=None):
return self.get_quantifier_eliminator(name=name, logic=logic)

def is_sat(self, formula, solver_name=None, logic=None):
if logic == AUTO_LOGIC:
Expand Down Expand Up @@ -414,8 +414,11 @@ def is_unsat(self, formula, solver_name=None, logic=None):
as solver:
return solver.is_unsat(formula)

def qelim(self, formula, solver_name=None):
with self.QuantifierEliminator(name=solver_name) as qe:
def qelim(self, formula, solver_name=None, logic=None):
if logic == AUTO_LOGIC:
logic = get_logic(formula, self.environment)

with self.QuantifierEliminator(name=solver_name, logic=logic) as qe:
return qe.eliminate_quantifiers(formula)

@property
Expand All @@ -425,3 +428,11 @@ def default_logic(self):
@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
2 changes: 1 addition & 1 deletion pysmt/logics.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -652,7 +652,7 @@ def most_generic_logic(logics):
res = [ l for l in logics if all(l >= x for x in logics)]

if len(res) != 1:
raise NoLogicAvailableError("Could not find the most generic"
raise NoLogicAvailableError("Could not find the most generic "
"logic for %s." % str(logics))
return res[0]

Expand Down

0 comments on commit 2d42b3c

Please sign in to comment.