API Reference¶
Solver, Model, QuantifierEliminator, Interpolator, and UnsatCoreSolver¶
-
class
pysmt.solvers.solver.
Solver
(environment, logic, **options)[source]¶ Represents a generic SMT Solver.
-
OptionsClass
¶ alias of
pysmt.solvers.options.SolverOptions
-
solve
(assumptions=None)[source]¶ 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) Return type: bool
-
get_model
()[source]¶ 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
solve()
(or one of the derived methods) returned sat or unknown, if no change to the assertion set occurred.
-
is_sat
(formula)[source]¶ Checks satisfiability of the formula w.r.t. the current state of the solver.
Previous assertions are taken into account.
Returns: Whether formula is satisfiable Return type: bool
-
is_valid
(formula)[source]¶ Checks validity of the formula w.r.t. the current state of the solver.
Previous assertions are taken into account. See
is_sat()
Returns: Whether formula is valid Return type: bool
-
is_unsat
(formula)[source]¶ Checks unsatisfiability of the formula w.r.t. the current state of the solver.
Previous assertions are taken into account. See
is_sat()
Returns: Whether formula is unsatisfiable Return type: bool
-
get_values
(formulae)[source]¶ 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
solve()
(or to one of the derived methods) returned sat or unknown, if no change to the assertion set occurred.Returns: A dictionary associating to each expr a value Return type: dict
-
print_model
(name_filter=None)[source]¶ 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.
-
get_value
(formula)[source]¶ Returns the value of formula in the current model (if one exists).
This is a simplified version of the SMT-LIB function get_values
-
-
class
pysmt.solvers.solver.
Model
(environment)[source]¶ 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.
-
get_value
(formula, model_completion=True)[source]¶ 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 function get_values .
-
get_values
(formulae, model_completion=True)[source]¶ Evaluates the values of the formulae in the current model.
Evaluates the values of the formulae in the current model returning a dictionary.
-
get_py_value
(formula, model_completion=True)[source]¶ 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.
-
get_py_values
(formulae, model_completion=True)[source]¶ 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.
-
satisfies
(formula, solver=None)[source]¶ Checks whether the model satisfies the formula.
The optional solver argument is used to complete partial models.
-
converter
¶ Get the Converter associated with the Solver.
-
-
class
pysmt.solvers.interpolation.
Interpolator
[source]¶ -
binary_interpolant
(a, b)[source]¶ Returns a binary interpolant for the pair (a, b), if And(a, b) is unsatisfiable, or None if And(a, b) is satisfiable.
-
Exceptions¶
This module contains all custom exceptions of pySMT.
-
exception
pysmt.exceptions.
UnknownSmtLibCommandError
[source]¶ Raised when the parser finds an unknown command.
-
exception
pysmt.exceptions.
SolverReturnedUnknownResultError
[source]¶ This exception is raised if a solver returns ‘unknown’ as a result
-
exception
pysmt.exceptions.
UnknownSolverAnswerError
[source]¶ Raised when the a solver returns an invalid response.
-
exception
pysmt.exceptions.
NoSolverAvailableError
[source]¶ No solver is available for the selected Logic.
-
exception
pysmt.exceptions.
UndefinedLogicError
[source]¶ This exception is raised if an undefined Logic is attempted to be used.
-
exception
pysmt.exceptions.
InternalSolverError
[source]¶ Generic exception to capture errors provided by a solver.
-
exception
pysmt.exceptions.
NoLogicAvailableError
[source]¶ Generic exception to capture errors caused by missing support for logics.
-
exception
pysmt.exceptions.
SolverRedefinitionError
[source]¶ Exception representing errors caused by multiple definition of solvers having the same name.
-
exception
pysmt.exceptions.
SolverNotConfiguredForUnsatCoresError
[source]¶ Exception raised if a solver not configured for generating unsat cores is required to produce a core.
-
exception
pysmt.exceptions.
SolverStatusError
[source]¶ Exception raised if a method requiring a specific solver status is incorrectly called in the wrong status.
-
exception
pysmt.exceptions.
ConvertExpressionError
(message=None, expression=None)[source]¶ Exception raised if the converter cannot convert an expression.
-
exception
pysmt.exceptions.
UnsupportedOperatorError
(message=None, node_type=None, expression=None)[source]¶ The expression contains an operator that is not supported.
The argument node_type contains the unsupported operator id.
-
exception
pysmt.exceptions.
SolverAPINotFound
[source]¶ The Python API of the selected solver cannot be found.
-
exception
pysmt.exceptions.
UndefinedSymbolError
(name)[source]¶ The given Symbol is not in the FormulaManager.
FNode¶
FNode are the building blocks of formulae.
-
class
pysmt.fnode.
FNodeContent
(node_type, args, payload)¶ -
args
¶ Alias for field number 1
-
node_type
¶ Alias for field number 0
-
payload
¶ Alias for field number 2
-
-
class
pysmt.fnode.
FNode
(content, node_id)[source]¶ FNode represent the basic structure for representing a formula.
FNodes are built using the FormulaManager, and should not be explicitly instantiated, since the FormulaManager takes care of memoization, thus guaranteeing that equivalent are represented by the same object.
An FNode is a wrapper to the structure FNodeContent. FNodeContent defines the type of the node (see operators.py), its arguments (e.g., for the formula A /B, args=(A,B)) and its payload, content of the node that is not an FNode (e.g., for an integer constant, the payload might be the python value 1).
The node_id is an integer uniquely identifying the node within the FormulaManager it belongs.
-
substitute
(subs, interpretations=None)[source]¶ Return a formula in which subformula have been substituted.
subs is a dictionary mapping terms to be substituted with their substitution. interpretations is a dictionary mapping function symbols to an FunctionInterpretation objects describing the semantics of the function.
-
size
(measure=None)[source]¶ Return the size of the formula according to the given metric.
See
SizeOracle
-
get_type
()[source]¶ Return the type of the formula by calling the Type-Checker.
See
SimpleTypeChecker
-
is_constant
(_type=None, value=None)[source]¶ Test whether the formula is a constant.
Optionally, check that the constant is of the given type and value.
-
is_bool_constant
(value=None)[source]¶ Test whether the formula is a Boolean constant.
Optionally, check that the constant has the given value.
-
is_real_constant
(value=None)[source]¶ Test whether the formula is a Real constant.
Optionally, check that the constant has the given value.
-
is_int_constant
(value=None)[source]¶ Test whether the formula is an Integer constant.
Optionally, check that the constant has the given value.
-
is_bv_constant
(value=None, width=None)[source]¶ Test whether the formula is a BitVector constant.
Optionally, check that the constant has the given value.
-
is_string_constant
(value=None)[source]¶ Test whether the formula is a String constant.
Optionally, check that the constant has the given value.
-
is_symbol
(type_=None)[source]¶ Test whether the formula is a Symbol.
Optionally, check that the symbol has the given type.
-
is_literal
()[source]¶ Test whether the formula is a literal.
A literal is a positive or negative Boolean symbol.
-
is_lira_op
(**kwargs)¶ Test whether the node is a IRA operator.
-
serialize
(threshold=None)[source]¶ Returns a human readable representation of the formula.
The threshold parameter can be used to limit the amount of the formula that will be printed. See
HRSerializer
-
to_smtlib
(daggify=True)[source]¶ Returns a Smt-Lib string representation of the formula.
The daggify parameter can be used to switch from a linear-size representation that uses ‘let’ operators to represent the formula as a dag or a simpler (but possibly exponential) representation that expands the formula as a tree.
See
SmtPrinter
-
is_term
()[source]¶ Test whether the node is a term.
All nodes are terms, except for function definitions.
-
bv_str
(fmt='b')[source]¶ Return a string representation of the BitVector.
- fmt: ‘b’ : Binary
- ‘d’ : Decimal ‘x’ : Hexadecimal
The representation is always unsigned
-
bv_bin_str
(reverse=False)[source]¶ Return the binary representation of the BitVector as string.
The reverse option is provided to deal with MSB/LSB.
-
array_value_get
(index)[source]¶ Returns the value of this Array Value at the given index. The index must be a constant of the correct type.
This function is equivalent (but possibly faster) than the following code:
m = self.array_value_assigned_values_map() try: return m[index] except KeyError: return self.array_value_default()
-
Logics¶
Describe all logics supported by pySMT and other logics defined in the SMTLIB and provides methods to compare and search for particular logics.
-
class
pysmt.logics.
Theory
(arrays=None, arrays_const=None, bit_vectors=None, floating_point=None, integer_arithmetic=None, real_arithmetic=None, integer_difference=None, real_difference=None, linear=None, uninterpreted=None, custom_type=None, strings=None)[source]¶ Describes a theory similarly to the SMTLIB 2.0.
-
class
pysmt.logics.
Logic
(name, description, quantifier_free=False, theory=None, **theory_kwargs)[source]¶ Describes a Logic similarly to the way they are defined in the SMTLIB 2.0
Note: We define more Logics than the ones defined in the SMTLib 2.0. See LOGICS for a list of all the logics and SMTLIB2_LOGICS for the restriction to the ones defined in SMTLIB2.0
-
pysmt.logics.
convert_logic_from_string
(name)[source]¶ Helper function to parse function arguments.
This takes a logic or a string or None, and returns a logic or None.
-
pysmt.logics.
get_logic_name
(**logic_kwargs)[source]¶ Returns the name of the Logic that matches the given properties.
See get_logic for the list of parameters.
-
pysmt.logics.
get_logic
(quantifier_free=False, arrays=False, arrays_const=False, bit_vectors=False, floating_point=False, integer_arithmetic=False, real_arithmetic=False, integer_difference=False, real_difference=False, linear=True, uninterpreted=False, custom_type=False, strings=False)[source]¶ Returns the Logic that matches the given properties.
Equivalent (but better) to executing get_logic_by_name(get_logic_name(…))
-
pysmt.logics.
most_generic_logic
(logics)[source]¶ Given a set of logics, return the most generic one.
If a unique most generic logic does not exists, throw an error.
-
pysmt.logics.
get_closer_logic
(supported_logics, logic)[source]¶ Returns the smaller supported logic that is greater or equal to the given logic. Raises NoLogicAvailableError if the solver does not support the given logic.
Operators¶
This module defines all the operators used internally by pySMT.
Note that other expressions can be built in the FormulaManager, but they will be rewritten (during construction) in order to only use these operators.
SMT-LIB¶
Defines constants for the commands of the SMT-LIB
-
class
pysmt.smtlib.annotations.
Annotations
(initial_annotations=None)[source]¶ Handles and stores (key,value) annotations for formulae
-
add
(formula, annotation, value=None)[source]¶ Adds an annotation for the given formula, possibly with the specified value
-
remove_value
(formula, annotation, value)[source]¶ Removes the given annotation for the given formula
-
has_annotation
(formula, annotation, value=None)[source]¶ Returns True iff the given formula has the given annotation. If Value is specified, True is returned only if the value is matching.
-
Typing¶
This module defines the types of the formulae handled by pySMT.
- In the current version these are:
- Bool
- Int
- Real
- BVType
- FunctionType
- ArrayType
Types are represented by singletons. Basic types (Bool, Int and Real) are constructed here by default, while BVType and FunctionType relies on a factory service. Each BitVector width is represented by a different instance of BVType.
-
class
pysmt.typing.
PySMTType
(decl=None, basename=None, args=None)[source]¶ Class for representing a type within pySMT.
Instances of this class are used to represent sorts. The subclass FunctionType is used to represent function declarations.
-
class
pysmt.typing.
PartialType
(name, definition)[source]¶ PartialType allows to delay the definition of a Type.
A partial type is equivalent to SMT-LIB “define-sort” command.
-
pysmt.typing.
FunctionType
(return_type, param_types)[source]¶ Returns Function Type with the given arguments.