Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Portfolio Solver #284

Merged
merged 3 commits into from Nov 2, 2016
Merged

Portfolio Solver #284

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
f10e782
Portfolio Solver
marcogario Oct 16, 2016
d626c45
BTOR: Fix issues in Solver
marcogario Oct 29, 2016
b680e66
Merge remote-tracking branch 'origin/master' into portfolio
marcogario Oct 29, 2016
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
47 changes: 32 additions & 15 deletions pysmt/factory.py
View file
Open in desktop
Expand Up @@ -35,6 +35,8 @@
from pysmt.logics import convert_logic_from_string
from pysmt.oracles import get_logic
from pysmt.solvers.qelim import ShannonQuantifierEliminator
from pysmt.solvers.solver import SolverOptions
from pysmt.solvers.portfolio import Portfolio

DEFAULT_SOLVER_PREFERENCE_LIST = ['msat', 'z3', 'cvc4', 'yices', 'btor',
'picosat', 'bdd']
Expand Down Expand Up @@ -463,19 +465,24 @@ def UnsatCoreSolver(self, quantified=False, name=None, logic=None,
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):
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)
with self.Solver(name=solver_name, logic=logic,
generate_models=False, incremental=False) \
as solver:
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):
Expand Down Expand Up @@ -530,20 +537,30 @@ def get_unsat_core(self, clauses, solver_name=None, logic=None):

return solver.get_unsat_core()

def is_valid(self, formula, solver_name=None, logic=None):
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)
with self.Solver(name=solver_name, logic=logic,
generate_models=False,
incremental=False) as solver:
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):
if logic is None or logic == AUTO_LOGIC:
logic = get_logic(formula, self.environment)
with self.Solver(name=solver_name, logic=logic,
generate_models=False,
incremental=False) as solver:
def is_unsat(self, formula, solver_name=None, logic=None, portfolio=None):
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):
Expand Down