Source code for pysmt.solvers.solver

#
# 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.
#
from six.moves import xrange

from pysmt.typing import BOOL
from pysmt.solvers.options import SolverOptions
from pysmt.exceptions import (SolverReturnedUnknownResultError, PysmtValueError,
                              PysmtTypeError, SolverStatusError)


[docs]class Solver(object): """Represents a generic SMT Solver.""" # Define the supported logics for the Solver LOGICS = [] # Class defining options for the Solver OptionsClass = SolverOptions def __init__(self, environment, logic, **options): if logic is None: raise PysmtValueError("Cannot provide 'None' as logic") self.environment = environment self.pending_pop = False self.logic = logic self.options = self.OptionsClass(**options) self._destroyed = False return def solve(self, assumptions=None): """Returns the satisfiability value of the asserted formulas. Assumptions is a list of Boolean variables or negations of boolean variables. If assumptions is specified, the satisfiability result is computed assuming that all the specified literals are True. A call to solve([a1, ..., an]) is functionally equivalent to:: push() add_assertion(And(a1, ..., an)) res = solve() pop() return res but is in general more efficient. Other convenience methods (is_sat, is_unsat, is_valid) are wrappers around this function. :returns: Whether the assertion stack is satisfiable w.r.t. the given assumptions (if given) :rtype: bool """ raise NotImplementedError
[docs] def get_model(self): """Returns an instance of Model that survives the solver instance. Restrictions: Requires option generate_models to be set to true (default) and can be called only after :py:func:`solve` (or one of the derived methods) returned sat or unknown, if no change to the assertion set occurred. """ raise NotImplementedError
[docs] def is_sat(self, formula): """Checks satisfiability of the formula w.r.t. the current state of the solver. Previous assertions are taken into account. :type formula: FNode :returns: Whether formula is satisfiable :rtype: bool """ assert formula in self.environment.formula_manager, \ "Formula does not belong to the current Formula Manager" if not self.options.incremental: # If not incremental, we only need to assert and solve. self.add_assertion(formula) # We do not allow two calls to solve() def solve_error(*args, **kwargs): raise SolverStatusError("Cannot call is_sat twice when incrementality is disable") res = self.solve() self.solve = solve_error self.is_sat = solve_error return res # Try to be incremental using push/pop but fallback to # solving under assumption if push/pop is not implemented use_solving_under_assumption = False try: self.push() except NotImplementedError: use_solving_under_assumption = True if use_solving_under_assumption: res = self.solve([formula]) else: self.add_assertion(formula) res = self.solve() self.pending_pop = True return res
[docs] def is_valid(self, formula): """Checks validity of the formula w.r.t. the current state of the solver. Previous assertions are taken into account. See :py:func:`is_sat` :type formula: FNode :returns: Whether formula is valid :rtype: bool """ Not = self.environment.formula_manager.Not return not self.is_sat(Not(formula))
[docs] def is_unsat(self, formula): """Checks unsatisfiability of the formula w.r.t. the current state of the solver. Previous assertions are taken into account. See :py:func:`is_sat` :type formula: FNode :returns: Whether formula is unsatisfiable :rtype: bool """ return not self.is_sat(formula)
[docs] def get_values(self, formulae): """Returns the value of the expressions if a model was found. Requires option generate_models to be set to true (default) and can be called only after :py:func:`solve` (or to one of the derived methods) returned sat or unknown, if no change to the assertion set occurred. :type formulae: Iterable of FNodes :returns: A dictionary associating to each expr a value :rtype: dict """ res = {} for f in formulae: v = self.get_value(f) res[f] = v return res
[docs] def push(self, levels=1): """Push the current context of the given number of levels. :type levels: int """ raise NotImplementedError
[docs] def pop(self, levels=1): """Pop the context of the given number of levels. :type levels: int """ raise NotImplementedError
[docs] def exit(self): """Exits from the solver and closes associated resources.""" if not self._destroyed: self._exit() self._destroyed = True
def _exit(self): """Exits from the solver and closes associated resources.""" raise NotImplementedError
[docs] def reset_assertions(self): """Removes all defined assertions.""" raise NotImplementedError
[docs] def add_assertion(self, formula, named=None): """Add assertion to the solver.""" raise NotImplementedError
[docs] def solve(self, assumptions=None): """Returns the satisfiability value of the asserted formulas. Assumptions is a list of Boolean variables or negations of boolean variables. If assumptions is specified, the satisfiability result is computed assuming that all the specified literals are True. A call to solve([a1, ..., an]) is functionally equivalent to: push() add_assertion(And(a1, ..., an)) res = solve() pop() return res but is in general more efficient. """ raise NotImplementedError
[docs] def print_model(self, name_filter=None): """Prints the model (if one exists). An optional function can be passed, that will be called on each symbol to decide whether to print it. """ raise NotImplementedError
[docs] def get_value(self, formula): """Returns the value of formula in the current model (if one exists). This is a simplified version of the SMT-LIB function get_values """ raise NotImplementedError
[docs] def get_py_value(self, formula): """Returns the value of formula as a python type. E.g., Bool(True) is translated into True. This simplifies writing code that branches on values in the model. """ res = self.get_value(formula) assert res.is_constant() return res.constant_value()
[docs] def get_py_values(self, formulae): """Returns the values of the formulae as python types. Returns a dictionary mapping each formula to its python value. """ res = {} for f in formulae: v = self.get_py_value(f) res[f] = v return res
def __enter__(self): """Manages entering a Context (i.e., with statement)""" return self def __exit__(self, exc_type, exc_val, exc_tb): """Manages exiting from Context (i.e., with statement) The default behaviour is "close" the solver by calling the py:func:`exit` method. """ self.exit() def _assert_no_function_type(self, item): """Enforces that argument 'item' cannot be a FunctionType. Raises TypeError. """ if item.is_symbol() and item.symbol_type().is_function_type(): raise PysmtTypeError("Cannot call get_value() on a FunctionType") def _assert_is_boolean(self, formula): """Enforces that argument 'formula' is of type Boolean. Raises TypeError. """ if formula.get_type() != BOOL: raise PysmtTypeError("Argument must be boolean.")
class IncrementalTrackingSolver(Solver): """A solver that keeps track of the asserted formulae This class provides tracking of the assertions that are stored inside the solver, the last executed command and the last solving result. It requires the extending class to implement the following proxy methods: * _reset_assertions * _add_assertion * _solve * _push * _pop The semantics of each function is the same as the non-proxy version except for _add_assertion that is supposed to return a result (of any type) that will constitute the elements of the self.assertions list. """ def __init__(self, environment, logic, **options): """See py:func:`Solver.__init__()`.""" Solver.__init__(self, environment, logic, **options) self._last_result = None self._last_command = None self._assertion_stack = [] self._backtrack_points = [] @property def last_command(self): """Returns the name of the laste executed command""" return self._last_command @property def last_result(self): """Returns the result of the last call to solve(). Returns True, False or "unknown": the last result of the last call to solve(). If solve has never been called, None is returned """ return self._last_result @property def assertions(self): """Returns the list of assertions that are still in the solver. Returns the list of results of calls to _add_assertion() that are still asserted in the solver """ return self._assertion_stack def _reset_assertions(self): raise NotImplementedError def reset_assertions(self): self._reset_assertions() self._last_command = "reset_assertions" def _add_assertion(self, formula, named=None): """Assert the formula in the solver. This must return the asserted formula (as an FNode) exactly as it was asserted in the solver, thus accounting for rewritings, simplifications, etc. :returns: The asserted formula :rtype: :py:class: """ raise NotImplementedError def add_assertion(self, formula, named=None): tracked = self._add_assertion(formula, named=named) self._assertion_stack.append(tracked) self._last_command = "assert" def _solve(self, assumptions=None): raise NotImplementedError def solve(self, assumptions=None): try: res = self._solve(assumptions=assumptions) self._last_result = res return res except SolverReturnedUnknownResultError: self._last_result = "unknown" raise finally: self._last_command = "solve" def _push(self, levels=1): raise NotImplementedError def push(self, levels=1): self._push(levels=levels) point = len(self._assertion_stack) for _ in xrange(levels): self._backtrack_points.append(point) self._last_command = "push" def _pop(self, levels=1): raise NotImplementedError def pop(self, levels=1): self._pop(levels=levels) for _ in xrange(levels): point = self._backtrack_points.pop() self._assertion_stack = self._assertion_stack[0:point] self._last_command = "pop"
[docs]class UnsatCoreSolver(object): """A solver supporting unsat core extraction""" UNSAT_CORE_SUPPORT = True
[docs] def get_unsat_core(self): """Returns the unsat core as a set of formulae. After a call to solve() yielding UNSAT, returns the unsat core as a set of formulae """ raise NotImplementedError
[docs] def get_named_unsat_core(self): """Returns the unsat core as a dict of names to formulae. After a call to solve() yielding UNSAT, returns the unsat core as a dict of names to formulae """ raise NotImplementedError
[docs]class Model(object): """An abstract Model for a Solver. This class provides basic services to operate on a model returned by a solver. This class is used as superclass for more specific Models, that are solver dependent or by the EagerModel class. """ def __init__(self, environment): self.environment = environment self._converter = None
[docs] def get_value(self, formula, model_completion=True): """Returns the value of formula in the current model (if one exists). If model_completion is True, then variables not appearing in the assignment are given a default value, otherwise an error is generated. This is a simplified version of the SMT-LIB funtion get_values . """ raise NotImplementedError
[docs] def get_values(self, formulae, model_completion=True): """Evaluates the values of the formulae in the current model. Evaluates the values of the formulae in the current model returning a dictionary. """ res = {} for f in formulae: v = self.get_value(f, model_completion=model_completion) res[f] = v return res
[docs] def get_py_value(self, formula, model_completion=True): """Returns the value of formula as a python type. E.g., Bool(True) is translated into True. This simplifies writing code that branches on values in the model. """ res = self.get_value(formula, model_completion=model_completion) assert res.is_constant() return res.constant_value()
[docs] def get_py_values(self, formulae, model_completion=True): """Returns the values of the formulae as python types. Returns the values of the formulae as python types. in the current model returning a dictionary. """ res = {} for f in formulae: v = self.get_py_value(f, model_completion=model_completion) res[f] = v return res
@property def converter(self): """Get the Converter associated with the Solver.""" return self._converter @converter.setter def converter(self, value): self._converter = value def __getitem__(self, idx): return self.get_value(idx, model_completion=True) def __str__(self): return "\n".join([ "%s := %s" % (var, value) for (var, value) in self])
class Converter(object): """A Converter implements functionalities to convert expressions. There are two key methods: convert() and back(). The first performs the forward conversion (pySMT -> Solver API), the second performs the backwards conversion (Solver API -> pySMT) """ def convert(self, formula): """Convert a PySMT formula into a Solver term.""" raise NotImplementedError def back(self, expr): """Convert an expression of the Solver into a PySMT term.""" raise NotImplementedError