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
push(levels=1)[source]

Push the current context of the given number of levels.

pop(levels=1)[source]

Pop the context of the given number of levels.

exit()[source]

Exits from the solver and closes associated resources.

reset_assertions()[source]

Removes all defined assertions.

add_assertion(formula, named=None)[source]

Add assertion to the solver.

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

get_py_value(formula)[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)[source]

Returns the values of the formulae as python types.

Returns a dictionary mapping each formula to its python value.

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.

sequence_interpolant(formulas)[source]

Returns a sequence interpolant for the conjunction of formulas, or None if the problem is satisfiable.

exit()[source]

Destroys the solver and closes associated resources.

class pysmt.solvers.solver.UnsatCoreSolver[source]

A solver supporting unsat core extraction

get_unsat_core()[source]

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

get_named_unsat_core()[source]

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

Exceptions

This module contains all custom exceptions of pySMT.

exception pysmt.exceptions.PysmtException[source]

Base class for 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.NonLinearError[source]

The provided expression is not linear.

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.

exception pysmt.exceptions.PysmtModeError[source]

The current mode is not supported for this operation

exception pysmt.exceptions.PysmtImportError[source]
exception pysmt.exceptions.PysmtValueError[source]
exception pysmt.exceptions.PysmtTypeError[source]
exception pysmt.exceptions.PysmtSyntaxError(message, pos_info=None)[source]
exception pysmt.exceptions.PysmtIOError[source]

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.

args()[source]

Returns the subformulae.

arg(idx)[source]

Return the given subformula at the given position.

get_free_variables()[source]

Return the set of Symbols that are free in the formula.

get_atoms()[source]

Return the set of atoms appearing in the formula.

simplify()[source]

Return a simplified version of the formula.

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_algebraic_constant()[source]

Test whether the formula is an Algebraic Constant

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_true()[source]

Test whether the formula is the True Boolean constant.

is_false()[source]

Test whether the formula is the False Boolean constant.

is_toreal()[source]

Test whether the node is the ToReal operator.

is_forall()[source]

Test whether the node is the ForAll operator.

is_exists()[source]

Test whether the node is the Exists operator.

is_quantifier()[source]

Test whether the node is a Quantifier.

is_and()[source]

Test whether the node is the And operator.

is_or()[source]

Test whether the node is the Or operator.

is_not()[source]

Test whether the node is the Not operator.

is_plus()[source]

Test whether the node is the Plus operator.

is_minus()[source]

Test whether the node is the Minus operator.

is_times()[source]

Test whether the node is the Times operator.

is_div()[source]

Test whether the node is the Division operator.

is_implies()[source]

Test whether the node is the Implies operator.

is_iff()[source]

Test whether the node is the Iff operator.

is_ite()[source]

Test whether the node is the Ite operator.

is_equals()[source]

Test whether the node is the Equals operator.

is_le()[source]

Test whether the node is the LE (less than equal) relation.

is_lt()[source]

Test whether the node is the LT (less than) relation.

is_bool_op()[source]

Test whether the node is a Boolean operator.

is_theory_relation()[source]

Test whether the node is a theory relation.

is_theory_op()[source]

Test whether the node is a theory operator.

is_ira_op()[source]

Test whether the node is an Int or Real Arithmetic operator.

is_lira_op(**kwargs)

Test whether the node is a IRA operator.

is_bv_op()[source]

Test whether the node is a BitVector operator.

is_array_op()[source]

Test whether the node is an array operator.

is_bv_not()[source]

Test whether the node is the BVNot operator.

is_bv_and()[source]

Test whether the node is the BVAnd operator.

is_bv_or()[source]

Test whether the node is the BVOr operator.

is_bv_xor()[source]

Test whether the node is the BVXor operator.

is_bv_concat()[source]

Test whether the node is the BVConcat operator.

is_bv_extract()[source]

Test whether the node is the BVConcat operator.

is_bv_ult()[source]

Test whether the node is the BVULT (unsigned less than) relation.

is_bv_ule()[source]

Test whether the node is the BVULE (unsigned less than) relation.

is_bv_neg()[source]

Test whether the node is the BVNeg operator.

is_bv_add()[source]

Test whether the node is the BVAdd operator.

is_bv_mul()[source]

Test whether the node is the BVMul operator.

is_bv_udiv()[source]

Test whether the node is the BVUDiv operator.

is_bv_urem()[source]

Test whether the node is the BVURem operator.

is_bv_lshl()[source]

Test whether the node is the BVLShl (logical shift left) operator.

is_bv_lshr()[source]

Test whether the node is the BVLShr (logical shift right) operator.

is_bv_rol()[source]

Test whether the node is the BVRol (rotate left) operator.

is_bv_ror()[source]

Test whether the node is the BVRor (rotate right) operator.

is_bv_zext()[source]

Test whether the node is the BVZext (zero extension) operator.

is_bv_sext()[source]

Test whether the node is the BVSext (signed extension) operator.

is_bv_sub()[source]

Test whether the node is the BVSub (subtraction) operator.

is_bv_slt()[source]

Test whether the node is the BVSLT (signed less-than) operator.

is_bv_sle()[source]

Test whether the node is the BVSLE (signed less-than-or-equal-to) operator.

is_bv_comp()[source]

Test whether the node is the BVComp (comparison) operator.

is_bv_sdiv()[source]

Test whether the node is the BVSDiv (signed division) operator.

is_bv_srem()[source]

Test whether the node is the BVSRem (signed reminder) operator.

is_bv_ashr()[source]

Test whether the node is the BVAshr (arithmetic shift right) operator.

is_select()[source]

Test whether the node is the SELECT (array select) operator.

is_store()[source]

Test whether the node is the STORE (array store) operator.

is_array_value()[source]

Test whether the node is an array value operator.

bv_width()[source]

Return the BV width of the formula.

bv_extract_start()[source]

Return the starting index for BVExtract.

bv_extract_end()[source]

Return the ending index for BVExtract.

bv_rotation_step()[source]

Return the rotation step for BVRor and BVRol.

bv_extend_step()[source]

Return the extension step for BVZext and BVSext.

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_function_application()[source]

Test whether the node is a Function application.

is_term()[source]

Test whether the node is a term.

All nodes are terms, except for function definitions.

symbol_type()[source]

Return the type of the Symbol.

symbol_name()[source]

Return the name of the Symbol.

constant_value()[source]

Return the value of the Constant.

constant_type()[source]

Return the type of the Constant.

bv2nat()[source]

Return the unsigned value encoded by the BitVector.

bv_unsigned_value()[source]

Return the unsigned value encoded by the BitVector.

bv_signed_value()[source]

Return the signed value encoded by the BitVector.

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()
function_name()[source]

Return the Function name.

quantifier_vars()[source]

Return the list of quantified variables.

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

get_quantified_version()[source]

Returns the quantified version of logic.

is_quantified()[source]

Return whether the logic supports quantifiers.

pysmt.logics.get_logic_by_name(name)[source]

Returns the Logic that matches the provided name.

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.

pysmt.logics.get_closer_pysmt_logic(target_logic)[source]

Returns the closer logic supported by PYSMT.

pysmt.logics.get_closer_smtlib_logic(target_logic)[source]

Returns the closer logic supported by SMT-LIB 2.0.

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.

pysmt.operators.new_node_type(node_id=None, node_str=None)[source]

Adds a new node type to the list of custom node types and returns the ID.

pysmt.operators.op_to_str(node_id)[source]

Returns a string representation of the given node.

pysmt.operators.all_types()[source]

Returns an iterator over all base and custom types.

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(formula)[source]

Removes all the annotations for the given formula

remove_annotation(formula, annotation)[source]

Removes the given annotation for the given formula

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.

annotations(formula)[source]

Returns a dictionary containing all the annotations for the given formula as keys and the respective values. None is returned if formula has no annotations.

all_annotated_formulae(annotation, value=None)[source]

Returns the set of all the formulae having the given annotation key. If Value is specified, only the formula having the specified value are returned.

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.BVType(width=32)[source]

Returns the BV type for the given width.

pysmt.typing.FunctionType(return_type, param_types)[source]

Returns Function Type with the given arguments.

pysmt.typing.ArrayType(index_type, elem_type)[source]

Returns the Array type with the given arguments.

pysmt.typing.Type(name, arity=0)[source]

Returns the Type Declaration with the given name (sort declaration).