API Reference¶

Shortcuts ¶

Provides the most used functions in a nicely wrapped API.

This module defines a global environment, so that most methods can be called without the need to specify an environment or a FormulaManager. Functions trying to access the global environment should use the method get_env(). Keep in mind that the global state of the environment might lead to inconsistency and unexpected bugs. This is particularly true for tests. For tests it is recommended to perform an environment reset in the setUp phase, to be guaranteed that a fresh environment is used (this is the default behavior of pysmt.test.TestCase ).

Solver, Model, QuantifierEliminator, Interpolator, and UnsatCoreSolver ¶

class pysmt.solvers.solver.Solver(environment, logic, **options)[source]¶: Represents a generic SMT Solver.

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.

class pysmt.solvers.qelim.QuantifierEliminator[source]¶

class pysmt.solvers.interpolation.Interpolator[source]¶

class pysmt.solvers.solver.UnsatCoreSolver[source]¶: A solver supporting unsat core extraction

Environment ¶

The Environment is a key structure in pySMT. It contains multiple singleton objects that are used throughout the system, such as the FormulaManager, Simplifier, HRSerializer, SimpleTypeChecker.

Exceptions ¶

This module contains all custom exceptions of pySMT.

Factory ¶

Factories are used to build new Solvers or Quantifier Eliminators without the need of specifying them. For example, the user can simply require a Solver that is able to deal with quantified theories, and the factory will return one such solver among the available ones. This makes it possible to write algorithms that do not depend on a particular solver.

FNode ¶

FNode are the building blocks of formulae.

Formula ¶

The FormulaManager is used to create formulae.

All objects are memoized so that two syntactically equivalent formulae are represented by the same object.

The FormulaManager provides many more constructors than the operators defined (operators.py). This is because many operators are rewritten, and therefore are only virtual. Common examples are GE, GT that are rewritten as LE and LT. Similarly, the operator Xor is rewritten using its definition.

Logics ¶

Describe all logics supported by pySMT and other logics defined in the SMTLIB and provides methods to compare and search for particular logics.

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.

Oracles ¶

This module provides classes used to analyze and determine properties of formulae.

SizeOracle provides metrics about the formula

QuantifierOracle says whether a formula is quantifier free

TheoryOracle says which logic is used in the formula.

FreeVarsOracle provides variables that are free in the formula

AtomsOracle provides the set of boolean atoms in the formula

TypesOracle provides the list of types in the formula

Parsing ¶

pysmt.parsing.parse(string)[source]¶: Parse an hr-string.

pysmt.parsing.HRParser(env=None)[source]¶: Parser for HR format of pySMT.

Printers ¶

Simplifier ¶

SMT-LIB ¶

Defines constants for the commands of the SMT-LIB

Substituter ¶

Type-Checker ¶

This module provides basic services to perform type checking and reasoning about the type of formulae.

SimpleTypeChecker provides the pysmt.typing type of a formula

The functions assert_*_args are useful for testing the type of arguments of a given function.

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.

Walkers ¶

Provides walkers to navigate formulas.

Two types of walkers are provided: DagWalker and TreeWalker.

Internally, the Walkers have a dictionary that maps each FNode type to the appropriate function to be called. When subclassing a Walker remember to specify an action for the nodes of interest. Nodes for which a behavior has not been specified will raise a NotImplementedError exception.

Finally, an experimental meta class is provided called CombinerWalker. This class takes a list of walkers and returns a new walker that applies all the walkers to the formula. The idea is that multiple information can be extracted from the formula by navigating it only once.

class pysmt.walkers.DagWalker(env=None, invalidate_memoization=False)[source]¶

DagWalker treats the formula as a DAG and performs memoization of the intermediate results.

This should be used when the result of applying the function to a formula is always the same, independently of where the formula has been found; examples include substitution and solving.

Due to memoization, a few more things need to be taken into account when using the DagWalker.

:func _get_key needs to be defined if additional arguments via keywords need to be shared. This function should return the key to be used in memoization. See substituter for an example.

class pysmt.walkers.TreeWalker(env=None)[source]¶

TreeWalker treats the formula as a Tree and does not perform memoization.

This should be used when applying a the function to the same formula is expected to yield different results, for example, serialization. If the operations are functions, consider using the DagWalker instead.

The recursion within walk_ methods is obtained by using the ‘yield’ keyword. In practice, each walk_ method is a generator that yields its arguments. If the generator returns None, no recursion will be performed.

class pysmt.walkers.IdentityDagWalker(env=None, invalidate_memoization=None)[source]¶

This class traverses a formula and rebuilds it recursively identically.

This could be useful when only some nodes needs to be rewritten but the structure of the formula has to be kept.