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 ).

pysmt.shortcuts.get_env()[source]

Returns the global environment.

Returns:The global environment
Return type:Environment
pysmt.shortcuts.reset_env()[source]

Resets the global environment, and returns the new one.

Returns:A new environment after resetting the global environment
Return type:Environment
pysmt.shortcuts.get_type(formula)[source]

Returns the type of the formula.

Parameters:formula (FNode) – The target formula
Returns:The type of the formula
pysmt.shortcuts.simplify(formula)[source]

Returns the simplified version of the formula.

Parameters:formula (FNode) – The target formula
Returns:The simplified version of the formula
Return type:Fnode
pysmt.shortcuts.substitute(formula, subs)[source]

Applies the substitutions defined in the dictionary to the formula.

Parameters:
  • formula (FNode) – The target formula
  • subs (A dictionary from FNode to FNode) – Specify the substitutions to apply to the formula
Returns:

Formula after applying the substitutions

Return type:

Fnode

pysmt.shortcuts.serialize(formula, threshold=None)[source]

Provides a string representing the formula.

Parameters:
  • formula (Integer) – The target formula
  • threshold – Specify the threshold
Returns:

A string representing the formula

Return type:

string

pysmt.shortcuts.get_free_variables(formula)[source]

Returns the free variables of the formula.

Parameters:formula (FNode) – The target formula
Returns:Free variables in the formula
pysmt.shortcuts.get_atoms(formula)[source]

Returns the set of atoms of the formula.

Parameters:formula (FNode) – The target formula
Returns:the set of atoms of the formula
pysmt.shortcuts.get_formula_size(formula, measure=None)[source]

Returns the size of the formula as measured by the given counting type.

See pysmt.oracles.SizeOracle for details.

Parameters:
  • formula (FNode) – The target formula
  • measure – Specify the measure/counting type
Returns:

The size of the formula as measured by the given counting type.

pysmt.shortcuts.ForAll(variables, formula)[source]
\[\forall v_1, \cdots, v_n . \varphi(v_1, \cdots, v_n)\]
pysmt.shortcuts.Exists(variables, formula)[source]
\[\exists v_1, \cdots, v_n . \varphi(v_1, \cdots, v_n)\]
pysmt.shortcuts.Function(vname, params)[source]
\[vname(p_1, \cdots, p_n)\]
pysmt.shortcuts.Not(formula)[source]
\[\lnot \varphi\]
pysmt.shortcuts.Implies(left, right)[source]
\[l \rightarrow r\]
pysmt.shortcuts.Iff(left, right)[source]
\[l \leftrightarrow r \]
pysmt.shortcuts.GE(left, right)[source]
\[l \ge r\]
pysmt.shortcuts.Minus(left, right)[source]
\[l - r \]
pysmt.shortcuts.Times(*args)[source]
\[x_1 \times x_2 \cdots \times x_n\]
pysmt.shortcuts.Pow(left, right)[source]
\[l ^ r\]
pysmt.shortcuts.Div(left, right)[source]
\[\frac{l}{r}\]
pysmt.shortcuts.Equals(left, right)[source]
\[l = r\]
pysmt.shortcuts.GT(left, right)[source]
\[l > r\]
pysmt.shortcuts.LE(left, right)[source]
\[l \le r\]
pysmt.shortcuts.LT(left, right)[source]
\[l < r\]
pysmt.shortcuts.Ite(iff, left, right)[source]
\[\text{ If } i \text{ Then } l \text{ Else } r\]
pysmt.shortcuts.Symbol(name, typename=Bool)[source]

Returns a symbol with the given name and type.

Parameters:
  • name – Specify the name
  • typename – Specify the typename
Returns:

A symbol with the given name and type

pysmt.shortcuts.FreshSymbol(typename=Bool, template=None)[source]

Returns a symbol with a fresh name and given type.

Parameters:
  • typename – Specify the typename
  • template – Specify the template
Returns:

A symbol with a fresh name and a given type

pysmt.shortcuts.Int(value)[source]

Returns an Integer constant with the given value.

Parameters:value – Specify the value
Returns:An Integer constant with the given value
pysmt.shortcuts.Bool(value)[source]

Returns a Boolean constant with the given value.

Parameters:value – Specify the value
Returns:A Boolean constant with the given value
pysmt.shortcuts.Real(value)[source]

Returns a Real constant with the given value.

Parameters:value – Specify the value
Returns:A Real constant with the given value
pysmt.shortcuts.TRUE()[source]

Returns the Boolean constant TRUE.

returns: The Boolean constant TRUE

pysmt.shortcuts.FALSE()[source]

Returns the Boolean constant FALSE.

returns: The Boolean constant FALSE

pysmt.shortcuts.And(*args)[source]
\[\varphi_0 \land \cdots \land \varphi_n \]
pysmt.shortcuts.Or(*args)[source]
\[\varphi_0 \lor \cdots \lor \varphi_n \]
pysmt.shortcuts.Plus(*args)[source]
\[\varphi_0 + \cdots + \varphi_n \]
pysmt.shortcuts.ToReal(formula)[source]

Explicit cast of a term into a Real term.

pysmt.shortcuts.AtMostOne(*args)[source]

At most one can be true at anytime.

Cardinality constraint over a set of boolean expressions.

pysmt.shortcuts.ExactlyOne(*args)[source]

Given a set of boolean expressions requires that exactly one holds.

pysmt.shortcuts.AllDifferent(*args)[source]

Given a set of non-boolean expressions, requires that each of them has value different from all the others

pysmt.shortcuts.Xor(left, right)[source]

Returns the XOR of left and right

Parameters:
  • left (FNode) – Specify the left BV
  • right (FNode) – Specify the right BV
Returns:

The XOR of left and right

pysmt.shortcuts.Min(*args)[source]

Minimum over a set of real or integer terms.

pysmt.shortcuts.Max(*args)[source]

Maximum over a set of real or integer terms

pysmt.shortcuts.EqualsOrIff(left, right)[source]

Returns Equals() or Iff() depending on the type of the arguments.

This can be used to deal with ambiguous cases where we might be dealing with both Theory and Boolean atoms.

pysmt.shortcuts.BV(value, width=None)[source]

Returns a constant of type BitVector.

value can be either: - a string of 0s and 1s - a string starting with “#b” followed by a sequence of 0s and 1s - an integer number s.t. 0 <= value < 2**width

In order to create the BV representation of a signed integer, the SBV() method shall be used.

Parameters:
  • value – Specify the value
  • width – Specify the width
Returns:

A constant of type BitVector

Return type:

FNode

pysmt.shortcuts.SBV(value, width=None)[source]

Returns a constant of type BitVector interpreting the sign.

If the specified value is an integer, it is converted in the 2-complement representation of the given number, otherwise the behavior is the same as BV().

Parameters:
  • value – Specify the value
  • width – Specify the width of the BV
Returns:

A constant of type BitVector interpreting the sign.

Return type:

FNode

pysmt.shortcuts.BVOne(width=None)[source]

Returns the unsigned one constant BitVector.

Parameters:width – Specify the width of the BitVector
Returns:The unsigned one constant BitVector
Return type:FNode
pysmt.shortcuts.BVZero(width=None)[source]

Returns the zero constant BitVector.

Parameters:width – Specify the width of the BitVector
Returns:The unsigned zero constant BitVector
Return type:FNode
pysmt.shortcuts.BVNot(formula)[source]

Returns the bitwise negation of the bitvector

Parameters:formula – The target formula
Returns:The bitvector Not(bv)
Return type:FNode
pysmt.shortcuts.BVAnd(left, right)[source]

Returns the Bit-wise AND of two bitvectors of the same size.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The bit-wise AND of left and right

Return type:

FNode

pysmt.shortcuts.BVOr(left, right)[source]

Returns the Bit-wise OR of two bitvectors of the same size.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The bit-wise OR of left and right

Return type:

FNode

pysmt.shortcuts.BVXor(left, right)[source]

Returns the Bit-wise XOR of two bitvectors of the same size.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The bit-wise XOR of left and right

Return type:

FNode

pysmt.shortcuts.BVConcat(left, right)[source]

Returns the Concatenation of the two BVs

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The concatenation of the two BVs

Return type:

FNode

pysmt.shortcuts.BVExtract(formula, start=0, end=None)[source]

Returns the slice of formula from start to end (inclusive).

Parameters:
  • formula – The target formula
  • start – Specify the start index
  • end – Specify the end index
Returns:

The slice of formula from start to end (inclusive)

Return type:

Fnode

pysmt.shortcuts.BVULT(left, right)[source]

Returns the Unsigned Less-Than comparison of the two BVs.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The Unsigned Less-Than comparison of the two BVs

Return type:

FNode

pysmt.shortcuts.BVUGT(left, right)[source]

Returns the Unsigned Greater-Than comparison of the two BVs.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The Unsigned Greater-Than comparison of the two BVs

Return type:

FNode

pysmt.shortcuts.BVULE(left, right)[source]

Returns the Unsigned Less-Equal comparison of the two BVs.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The Unsigned Less-Equal comparison of the two BVs

Return type:

FNode

pysmt.shortcuts.BVUGE(left, right)[source]

Returns the Unsigned Greater-Equal comparison of the two BVs.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The Unsigned Greater-Equal comparison of the two BVs

Return type:

FNode

pysmt.shortcuts.BVNeg(formula)[source]

Returns the arithmetic negation of the BV.

Parameters:formula – The target formula
Returns:The arithmetic negation of the formula
Return type:FNode
pysmt.shortcuts.BVAdd(left, right)[source]

Returns the sum of two BV.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The sum of the two BVs.

Return type:

FNode

pysmt.shortcuts.BVSub(left, right)[source]

Returns the difference of two BV.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The difference of the two BV

Return type:

FNode

pysmt.shortcuts.BVMul(left, right)[source]

Returns the product of two BV.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The product of the two BV

Return type:

FNode

pysmt.shortcuts.BVUDiv(left, right)[source]

Returns the Unsigned division of the two BV.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The Unsigned division of the two BV

Return type:

FNode

pysmt.shortcuts.BVURem(left, right)[source]

Returns the Unsigned remainder of the two BV.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The Unsigned remainder of the two BV

Return type:

FNode

pysmt.shortcuts.BVLShl(left, right)[source]

Returns the logical left shift the BV.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The logical left shift the BV

Return type:

FNode

pysmt.shortcuts.BVLShr(left, right)[source]

Returns the logical right shift the BV.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The logical right shift the BV

Return type:

FNode

pysmt.shortcuts.BVAShr(left, right)[source]
Returns the RIGHT arithmetic rotation of the left BV by the number
of steps specified by the right BV.
Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The RIGHT arithmetic rotation of the left BV by the number of steps specified by the right BV

Return type:

FNode

pysmt.shortcuts.BVRol(formula, steps)[source]

Returns the LEFT rotation of the BV by the number of steps.

Parameters:
  • formula – The target formula
  • steps – Specify the number of steps.
Returns:

The LEFT rotation of the BV by the number of steps

Return type:

FNode

pysmt.shortcuts.BVRor(formula, steps)[source]

Returns the RIGHT rotation of the BV by the number of steps.

Parameters:
  • formula – The target formula
  • steps – Specify the number of steps.
Returns:

The RIGHT rotation of the BV by the number of steps

Return type:

FNode

pysmt.shortcuts.BVZExt(formula, increase)[source]

Returns the zero-extension of the BV.

New bits are set to zero.

Parameters:
  • formula – The target formula
  • increase – Specify the increase
Returns:

The extension of the BV

Return type:

FNode

pysmt.shortcuts.BVSExt(formula, increase)[source]

Returns the signed-extension of the BV.

New bits are set according to the most-significant-bit.

Parameters:
  • formula – The target formula
  • increase – Specify the ‘increase’ value
Returns:

The signed-extension of the BV.

Return type:

FNode

pysmt.shortcuts.BVSLT(left, right)[source]

Returns the Signed Less-Than comparison of the two BVs.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The Signed Less-Than comparison of the two BVs

Return type:

FNode

pysmt.shortcuts.BVSLE(left, right)[source]

Returns the Signed Less-Equal comparison of the two BVs.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The Signed Less-Than-Equal comparison of the two BVs

Return type:

FNode

pysmt.shortcuts.BVSGT(left, right)[source]

Returns the Signed Greater-Than comparison of the two BVs.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The Signed Greater-Than comparison of the two BVs

Return type:

FNode

pysmt.shortcuts.BVSGE(left, right)[source]

Returns the Signed Greater-Equal comparison of the two BVs.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The Signed Greater-Equal comparison of the two BVs.

Return type:

FNode

pysmt.shortcuts.BVSDiv(left, right)[source]

Returns the Signed division of the two BVs.

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The the Signed division of left by right

Return type:

FNode

pysmt.shortcuts.BVSRem(left, right)[source]

Returns the Signed remainder of the two BVs

Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

The Signed remainder of left divided by right

Return type:

FNode

pysmt.shortcuts.BVComp(left, right)[source]
Returns a BV of size 1 equal to 0 if left is equal to right,
otherwise equal to 1.
Parameters:
  • left – Specify the left bitvector
  • right – Specify the right bitvector
Returns:

A BV of size 1 equal to 0 if left is equal to right, otherwise 1

Return type:

FNode

pysmt.shortcuts.Select(array, index)[source]

Returns a SELECT application on the array at the given index

Parameters:
  • array – Specify the array
  • index – Specify the index
Returns:

A SELECT application on array at index

Return type:

FNode

pysmt.shortcuts.Store(array, index, value)[source]

Returns a STORE application with given value on array at the given index

Parameters:
  • array – Specify the array
  • index – Specify the index
Returns:

A STORE on the array at the given index with the given value

Return type:

FNode

pysmt.shortcuts.Array(idx_type, default, assigned_values=None)[source]

Returns an Array with the given index type and initialization.

If assigned_values is specified, then it must be a map from constants of type idx_type to values of the same type as default and the array is initialized correspondingly.

Parameters:
  • idx_type – Specify the index type
  • default – Specify the default values
  • assigned_values – Specify the assigned values
Returns:

A node representing an array having index type equal to idx_type, initialized with default values. If assigned_values is specified, then it must be a map from constants of type idx_type to values of the same type as default and the array is initialized correspondingly.

Return type:

FNode

pysmt.shortcuts.Solver(name=None, logic=None, **kwargs)[source]

Returns a solver.

Parameters:
  • name – Specify the name of the solver
  • logic – Specify the logic that is going to be used.
Return type:

Solver

pysmt.shortcuts.UnsatCoreSolver(name=None, logic=None, unsat_cores_mode='all')[source]

Returns a solver supporting unsat core extraction.

Parameters:
  • name – Specify the name of the solver
  • logic – Specify the logic that is going to be used.
  • unsat_cores_mode – Specify the unsat cores mode.
Returns:

A solver supporting unsat core extraction.

Return type:

Solver

pysmt.shortcuts.QuantifierEliminator(name=None, logic=None)[source]

Returns a quantifier eliminator.

Parameters:
  • name – Specify the name of the solver
  • logic – Specify the logic that is going to be used.
Returns:

A quantifier eliminator with the specified name and logic

Return type:

QuantifierEliminator

pysmt.shortcuts.Interpolator(name=None, logic=None)[source]

Returns an interpolator

Parameters:
  • name – Specify the name of the solver
  • logic – Specify the logic that is going to be used.
Returns:

An interpolator

Return type:

Interpolator

pysmt.shortcuts.is_sat(formula, solver_name=None, logic=None, portfolio=None)[source]

Returns whether a formula is satisfiable.

Parameters:
  • formula (FNode) – The formula to check satisfiability
  • solver_name (string) – Specify the name of the solver to be used
  • logic – Specify the logic that is going to be used
  • portfolio (An iterable of solver names) – A list of solver names to perform portfolio solving.
Returns:

Whether the formula is SAT or UNSAT.

Return type:

bool

pysmt.shortcuts.get_model(formula, solver_name=None, logic=None)[source]

Similar to is_sat() but returns a model if the formula is satisfiable, otherwise None

Parameters:
  • formula – The target formula
  • solver_name – Specify the name of the solver
Param:

logic: Specify the logic that is going to be used

Returns:

A model if the formula is satisfiable

Return type:

Model

pysmt.shortcuts.get_implicant(formula, solver_name=None, logic=None)[source]

Returns a formula f_i such that Implies(f_i, formula) is valid or None if formula is unsatisfiable.

if complete is set to true, all the variables appearing in the formula are forced to appear in f_i. :param formula: The target formula :param solver_name: Specify the name of the solver :param: logic: Specify the logic that is going to be used :returns: A formula f_i such that Implies(f_i, formula) is valid or None

if formula is unsatisfiable.
Return type:FNode
pysmt.shortcuts.get_unsat_core(clauses, solver_name=None, logic=None)[source]

Similar to get_model() but returns the unsat core of the conjunction of the input clauses

Parameters:
  • clauses – Specify the list of input clauses
  • solver_name – Specify the name of the solver_name
  • logic – Specify the logic that is going to be used
Returns:

The unsat core of the conjunction of the input clauses

pysmt.shortcuts.is_valid(formula, solver_name=None, logic=None, portfolio=None)[source]

Similar to is_sat() but checks validity.

Parameters:
  • formula (FNode) – The target formula
  • solver_name – Specify the name of the solver to be used
  • logic – Specify the logic that is going to be used
  • portfolio – A list of solver names to perform portfolio solving.
Returns:

Whether the formula is SAT or UNSAT but checks validity

Return type:

bool

pysmt.shortcuts.is_unsat(formula, solver_name=None, logic=None, portfolio=None)[source]

Similar to is_sat() but checks unsatisfiability.

Parameters:
  • formula (FNode) – The target formula
  • solver_name – Specify the name of the solver to be used
  • logic – Specify the logic that is going to be used
  • portfolio – A list of solver names to perform portfolio solving.
Returns:

Whether the formula is UNSAT or not

Return type:

bool

pysmt.shortcuts.qelim(formula, solver_name=None, logic=None)[source]

Performs quantifier elimination of the given formula.

Parameters:
  • formula – The target formula
  • solver_name – Specify the name of the solver to be used
  • logic – Specify the logic that is going to be used
Returns:

A formula after performing quantifier elimination

Return type:

FNode

pysmt.shortcuts.binary_interpolant(formula_a, formula_b, solver_name=None, logic=None)[source]

Computes an interpolant of (formula_a, formula_b).

Returns None if the conjunction is satisfiable

Parameters:
  • formula_a – Specify formula_a
  • formula_b – Specify formula_b
  • solver_name – Specify the name of the solver to be used
  • logic – Specify the logic that is going to be used
Returns:

An interpolant of (formula_a, formula_b); None if the conjunction is satisfiable

Return type:

FNode or None

pysmt.shortcuts.sequence_interpolant(formulas, solver_name=None, logic=None)[source]

Computes a sequence interpolant of the formulas.

Returns None if the conjunction is satisfiable.

Parameters:
  • formulas – The target formulas
  • solver_name – Specify the name of the solver to be used
  • logic – Specify the logic that is going to be used
Returns:

A sequence intepolant of the formulas; None if the conjunction is satisfiable

Return type:

FNode or None

pysmt.shortcuts.read_configuration(config_filename, environment=None)[source]

Reads the pysmt configuration of the given file path and applies it on the specified environment. If no environment is specified, the top-level environment will be used.

Parameters:
  • config_filename – Specify the name of the config file
  • environment – Specify the environment
pysmt.shortcuts.write_configuration(config_filename, environment=None)[source]

Dumps the current pysmt configuration to the specified file path

Parameters:
  • config_filename – Specify the name of the config file
  • environment – Specify the environment
pysmt.shortcuts.read_smtlib(fname)[source]

Reads the SMT formula from the given file.

This supports compressed files, if the fname ends in .bz2 .

Parameters:fname – Specify the filename
Returns:An SMT formula
Return type:FNode
pysmt.shortcuts.write_smtlib(formula, fname)[source]

Reads the SMT formula from the given file.

Parameters:
  • formula – Specify the SMT formula to look for
  • fname – Specify the filename
pysmt.shortcuts.to_smtlib(formula, 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

Solver, Model, QuantifierEliminator, Interpolator, and UnsatCoreSolver

class pysmt.solvers.solver.Solver(environment, logic, **options)[source]

Represents a generic SMT Solver.

OptionsClass

alias of SolverOptions

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.

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.

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 funtion 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.

converter

Get the Converter associated with the Solver.

class pysmt.solvers.qelim.QuantifierEliminator[source]
eliminate_quantifiers(formula)[source]

Returns a quantifier-free equivalent formula of the given formula

If explicit_vars is specified, an explicit enumeration of all the possible models for such variables is computed and quantifier elimination is performed on each disjunct separately.

exit()[source]

Destroys the solver and closes associated resources.

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 unsatisfaiable, 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

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.

class pysmt.environment.Environment[source]

The Environment provides global singleton instances of various objects.

FormulaManager and the TypeChecker are among the most commonly used ones.

Subclasses of Environment should take care of adjusting the list of classes for the different services, by changing the class attributes.

FormulaManagerClass

alias of FormulaManager

SimplifierClass

alias of Simplifier

SubstituterClass

alias of MGSubstituter

HRSerializerClass

alias of HRSerializer

SizeOracleClass

alias of SizeOracle

AtomsOracleClass

alias of AtomsOracle

stc

Get the Simple Type Checker

qfo

Get the Quantifier Oracle

ao

Get the Atoms Oracle

theoryo

Get the Theory Oracle

typeso

Get the Types Oracle

fvo

Get the FreeVars Oracle

sizeo

Get the Size Oracle

add_dynamic_walker_function(nodetype, walker, function)[source]

Dynamically bind the given function to the walker for the nodetype.

This function enables the extension of walkers for new nodetypes. When introducing a new nodetype, we link a new function to a given walker, so that the walker will be able to handle the new nodetype.

See pysmt.walkers.generic.Walker.walk_error() for more information.

pysmt.environment.get_env()[source]

Returns the Environment at the head of the stack.

pysmt.environment.push_env(env=None)[source]

Push a env in the stack. If env is None, a new Environment is created.

pysmt.environment.pop_env()[source]

Pop an env from the stack.

pysmt.environment.reset_env()[source]

Destroys and recreate the head environment.

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 defintion 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

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.

class pysmt.factory.Factory(environment, solver_preference_list=None, qelim_preference_list=None, interpolation_preference_list=None)[source]

Factory used to build Solver, QuantifierEliminators, Interpolators etc.

This class contains the logic to magically select the correct solver. Moreover, this is the class providing the shortcuts is_sat, is_unsat etc.

set_solver_preference_list(preference_list)[source]

Defines the order in which to pick the solvers.

The list is not required to contain all the solvers. It is possible to define a subsets of the solvers, or even just one. The impact of this, is that the solver will never be selected automatically. Note, however, that the solver can still be selected by calling it by name.

set_qelim_preference_list(preference_list)[source]

Defines the order in which to pick the solvers.

set_interpolation_preference_list(preference_list)[source]

Defines the order in which to pick the solvers.

all_solvers(logic=None)[source]

Returns a dict <solver_name, solver_class> including all and only the solvers directly or indirectly supporting the given logic. A solver supports a logic if either the given logic is declared in the LOGICS class field or if a logic subsuming the given logic is declared in the LOGICS class field.

If logic is None, the map will contain all the known solvers

has_solvers(logic=None)[source]

Returns true if self.all_solvers(logic) is non-empty

all_quantifier_eliminators(logic=None)[source]

Returns a dict <qelim_name, qelim_class> including all and only the quantifier eliminators directly or indirectly supporting the given logic. A qelim supports a logic if either the given logic is declared in the LOGICS class field or if a logic subsuming the given logic is declared in the LOGICS class field.

If logic is None, the map will contain all the known quantifier eliminators

all_unsat_core_solvers(logic=None)[source]

Returns a dict <solver_name, solver_class> including all and only the solvers supporting unsat core extraction and directly or indirectly supporting the given logic. A solver supports a logic if either the given logic is declared in the LOGICS class field or if a logic subsuming the given logic is declared in the LOGICS class field.

If logic is None, the map will contain all the known solvers

all_interpolators(logic=None)[source]

Returns a dict <solver_name, solver_class> including all and only the solvers supporting interpolation and directly or indirectly supporting the given logic. A solver supports a logic if either the given logic is declared in the LOGICS class field or if a logic subsuming the given logic is declared in the LOGICS class field.

If logic is None, the map will contain all the known solvers

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

Return a formula in which subformula have been substituted.

subs is a dictionary mapping terms to be subtituted with their substitution.

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_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_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(*args, **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_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.

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.

class pysmt.formula.FormulaManager(env=None)[source]

FormulaManager is responsible for the creation of all formulae.

ForAll(variables, formula)[source]
Creates an expression of the form:
Forall variables. formula(variables)
Restrictions:
  • Formula must be of boolean type
  • Variables must be BOOL, REAL or INT
Exists(variables, formula)[source]
Creates an expression of the form:
Exists variables. formula(variables)
Restrictions:
  • Formula must be of boolean type
  • Variables must be BOOL, REAL or INT
Function(vname, params)[source]

Returns the function application of vname to params.

Note: Applying a 0-arity function returns the function itself.

Not(formula)[source]
Creates an expression of the form:
not formula

Restriction: Formula must be of boolean type

Implies(left, right)[source]
Creates an expression of the form:
left -> right

Restriction: Left and Right must be of boolean type

Iff(left, right)[source]
Creates an expression of the form:
left <-> right

Restriction: Left and Right must be of boolean type

Minus(left, right)[source]
Creates an expression of the form:
left - right

Restriction: Left and Right must be both INT or REAL type

Times(*args)[source]

Creates a multiplication of terms

This function has polimorphic n-arguments:
  • Times(a,b,c)
  • Times([a,b,c])
Restriction:
  • Arguments must be all of the same type
  • Arguments must be INT or REAL
Pow(base, exponent)[source]

Creates the n-th power of the base.

The exponent must be a constant.

Div(left, right)[source]

Creates an expression of the form: left / right

Equals(left, right)[source]

Creates an expression of the form: left = right

Restriction: Left and Right must be both REAL or INT type

GE(left, right)[source]
Creates an expression of the form:
left >= right

Restriction: Left and Right must be both REAL or INT type

GT(left, right)[source]
Creates an expression of the form:
left > right

Restriction: Left and Right must be both REAL or INT type

LE(left, right)[source]
Creates an expression of the form:
left <= right

Restriction: Left and Right must be both REAL or INT type

LT(left, right)[source]
Creates an expression of the form:
left < right

Restriction: Left and Right must be both REAL or INT type

Ite(iff, left, right)[source]
Creates an expression of the form:
if( iff ) then left else right
Restriction:
  • Iff must be BOOL
  • Left and Right must be both of the same type
Real(value)[source]

Returns a Real-type constant of the given value.

value can be:
  • A Fraction(n,d)
  • A tuple (n,d)
  • A long or int n
  • A float
  • (Optionally) a mpq or mpz object
Int(value)[source]

Return a constant of type INT.

TRUE()[source]

Return the boolean constant True.

FALSE()[source]

Return the boolean constant False.

And(*args)[source]

Returns a conjunction of terms.

This function has polimorphic arguments:
  • And(a,b,c)
  • And([a,b,c])

Restriction: Arguments must be boolean

Or(*args)[source]

Returns an disjunction of terms.

This function has polimorphic n-arguments:
  • Or(a,b,c)
  • Or([a,b,c])

Restriction: Arguments must be boolean

Plus(*args)[source]

Returns an sum of terms.

This function has polimorphic n-arguments:
  • Plus(a,b,c)
  • Plus([a,b,c])
Restriction:
  • Arguments must be all of the same type
  • Arguments must be INT or REAL
ToReal(formula)[source]

Cast a formula to real type.

AtMostOne(*args)[source]

At most one of the bool expressions can be true at anytime.

This using a quadratic encoding:
A -> !(B / C) B -> !(C)
ExactlyOne(*args)[source]

Encodes an exactly-one constraint on the boolean symbols.

This using a quadratic encoding:
A / B / C A -> !(B / C) B -> !(C)
AllDifferent(*args)[source]

Encodes the ‘all-different’ constraint using two possible encodings.

AllDifferent(x, y, z) := (x != y) & (x != z) & (y != z)

Xor(left, right)[source]

Returns the xor of left and right: left XOR right

Min(*args)[source]

Returns the encoding of the minimum expression within args

Max(*args)[source]

Returns the encoding of the maximum expression within args

EqualsOrIff(left, right)[source]

Returns Equals() or Iff() depending on the type of the arguments.

This can be used to deal with ambiguous cases where we might be dealing with both Theory and Boolean atoms.

BV(value, width=None)[source]

Return a constant of type BitVector.

value can be either: - a string of 0s and 1s - a string starting with “#b” followed by a sequence of 0s and 1s - an integer number s.t. 0 <= value < 2**width

In order to create the BV representation of a signed integer, the SBV() method shall be used.

SBV(value, width=None)[source]

Returns a constant of type BitVector interpreting the sign.

If the specified value is an integer, it is converted in the 2-complement representation of the given number, otherwise the behavior is the same as BV().

BVOne(width)[source]

Returns the bit-vector representing the unsigned one.

BVZero(width)[source]

Returns the bit-vector with all bits set to zero.

BVNot(formula)[source]

Returns the bitvector Not(bv)

BVAnd(left, right)[source]

Returns the Bit-wise AND of two bitvectors of the same size.

BVOr(left, right)[source]

Returns the Bit-wise OR of two bitvectors of the same size.

BVXor(left, right)[source]

Returns the Bit-wise XOR of two bitvectors of the same size.

BVConcat(left, right)[source]

Returns the Concatenation of the two BVs

BVExtract(formula, start=0, end=None)[source]

Returns the slice of formula from start to end (inclusive).

BVULT(left, right)[source]

Returns the formula left < right.

BVUGT(left, right)[source]

Returns the formula left > right.

BVULE(left, right)[source]

Returns the formula left <= right.

BVUGE(left, right)[source]

Returns the formula left >= right.

BVNeg(formula)[source]

Returns the arithmetic negation of the BV.

BVAdd(left, right)[source]

Returns the sum of two BV.

BVSub(left, right)[source]

Returns the difference of two BV.

BVMul(left, right)[source]

Returns the product of two BV.

BVUDiv(left, right)[source]

Returns the division of the two BV.

BVURem(left, right)[source]

Returns the reminder of the two BV.

BVLShl(left, right)[source]

Returns the logical left shift the BV.

BVLShr(left, right)[source]

Returns the logical right shift the BV.

BVRol(formula, steps)[source]

Returns the LEFT rotation of the BV by the number of steps.

BVRor(formula, steps)[source]

Returns the RIGHT rotation of the BV by the number of steps.

BVZExt(formula, increase)[source]

Returns the extension of the BV with ‘increase’ additional bits

New bits are set to zero.

BVSExt(formula, increase)[source]

Returns the signed extension of the BV with ‘increase’ additional bits

New bits are set according to the most-significant-bit.

BVSLT(left, right)[source]

Returns the SIGNED LOWER-THAN comparison for BV.

BVSLE(left, right)[source]

Returns the SIGNED LOWER-THAN-OR-EQUAL-TO comparison for BV.

BVComp(left, right)[source]

Returns a BV of size 1 equal to 0 if left is equal to right, otherwise 1 is returned.

BVSDiv(left, right)[source]

Returns the SIGNED DIVISION of left by right

BVSRem(left, right)[source]

Returns the SIGNED REMAINDER of left divided by right

BVAShr(left, right)[source]

Returns the RIGHT arithmetic rotation of the left BV by the number of steps specified by the right BV.

BVNand(left, right)[source]

Returns the NAND composition of left and right.

BVNor(left, right)[source]

Returns the NOR composition of left and right.

BVXnor(left, right)[source]

Returns the XNOR composition of left and right.

BVSGT(left, right)[source]

Returns the SIGNED GREATER-THAN comparison for BV.

BVSGE(left, right)[source]

Returns the SIGNED GREATER-THAN-OR-EQUAL-TO comparison for BV.

BVSMod(left, right)[source]

Returns the SIGNED MODULUS of left divided by right.

BVRepeat(formula, count=1)[source]

Returns the concatenation of count copies of formula.

Select(arr, idx)[source]

Creates a node representing an array selection.

Store(arr, idx, val)[source]

Creates a node representing an array update.

Array(idx_type, default, assigned_values=None)[source]

Creates a node representing an array having index type equal to idx_type, initialized with default values.

If assigned_values is specified, then it must be a map from constants of type idx_type to values of the same type as default and the array is initialized correspondingly.

normalize(formula)[source]

Returns the formula normalized to the current Formula Manager.

This method is useful to contextualize a formula coming from another formula manager.

E.g., f_a is defined with the FormulaManager a, and we want to
obtain f_b that is the formula f_a expressed on the FormulaManager b : f_b = b.normalize(f_a)
class pysmt.formula.FormulaContextualizer(env=None)[source]

Helper class to recreate a formula within a new environment.

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)[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)[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.

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
class pysmt.oracles.SizeOracle(env=None)[source]

Evaluates the size of a formula

get_size(formula, measure=None)[source]

Return the size of the formula according to the specified measure.

The default measure is MEASURE_TREE_NODES.

class pysmt.oracles.AtomsOracle(env=None, invalidate_memoization=False)[source]

This class returns the set of Boolean atoms involved in a formula A boolean atom is either a boolean variable or a theory atom

get_atoms(formula)[source]

Returns the set of atoms appearing 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

class pysmt.printers.HRPrinter(stream, env=None)[source]

Performs serialization of a formula in a human-readable way.

E.g., Implies(And(Symbol(x), Symbol(y)), Symbol(z)) ~> ‘(x * y) -> z’

printer(f, threshold=None)[source]

Performs the serialization of ‘f’.

Thresholding can be used to define how deep in the formula to go. After reaching the thresholded value, ”...” will be printed instead. This is mainly used for debugging.

class pysmt.printers.HRSerializer(environment=None)[source]

Return the serialized version of the formula as a string.

PrinterClass

alias of HRPrinter

serialize(formula, printer=None, threshold=None)[source]

Returns a string with the human-readable version of the formula.

‘printer’ is the printer to call to perform the serialization. ‘threshold’ is the thresholding value for the printing function.

class pysmt.printers.SmartPrinter(stream, subs=None)[source]

Better serialization allowing special printing of subformula.

The formula is serialized according to the format defined in the HRPrinter. However, everytime a formula that is present in ‘subs’ is found, this is replaced.

E.g., subs = {And(a,b): “ab”}

Everytime that the subformula And(a,b) is found, “ab” will be printed instead of “a & b”. This makes it possible to rename big subformulae, and provide better human-readable representation.

pysmt.printers.smart_serialize(formula, subs=None, threshold=None)[source]

Creates and calls a SmartPrinter to perform smart serialization.

Simplifier

class pysmt.simplifier.Simplifier(env=None)[source]

Perform basic simplifications of the input formula.

simplify(formula)[source]

Performs simplification of the given formula.

class pysmt.simplifier.BddSimplifier(env=None, static_ordering=None, bool_abstraction=False)[source]

A simplifier relying on BDDs.

The formula is translated into a BDD and then translated back into a pySMT formula. This is a much more expensive simplification process, and might not work with formulas with thousands of boolean variables.

The option static_ordering can be used to provide a variable ordering for the underlying bdd.

The option bool_abstraction controls how to behave if the input formula contains Theory terms (i.e., is not purely boolean). If this option is False (default) an exception will be thrown when a Theory atom is found. If it is set to True, the Theory part is abstracted, and the simplification is performed only on the boolean structure of the formula.

SMT-LIB

pysmt.smtlib.parser.open_(fname)[source]

Transparently handle .bz2 files.

pysmt.smtlib.parser.get_formula(script_stream, environment=None)[source]

Returns the formula asserted at the end of the given script

script_stream is a file descriptor.

pysmt.smtlib.parser.get_formula_strict(script_stream, environment=None)[source]

Returns the formula defined in the SMTScript.

This function assumes that only one formula is defined in the SMTScript. It will raise an exception if commands such as pop and push are present in the script, or if check-sat is called more than once.

pysmt.smtlib.parser.get_formula_fname(script_fname, environment=None, strict=True)[source]

Returns the formula asserted at the end of the given script.

class pysmt.smtlib.parser.SmtLibExecutionCache[source]

Execution environment for SMT2 script execution

bind(name, value)[source]

Binds a symbol in this environment

unbind(name)[source]

Unbinds the last binding of this symbol

get(name)[source]

Returns the last binding for ‘name’

update(value_map)[source]

Binds all the symbols in ‘value_map’

unbind_all(values)[source]

UnBinds all the symbols in ‘values’

class pysmt.smtlib.parser.Tokenizer(handle, interactive=False)[source]

Takes a file-like object and produces a stream of tokens following the LISP rules.

If interative is True, the file reading proceeds char-by-char with no buffering. This is useful for interactive use for example with a SMT-Lib2-compliant solver

The method add_extra_token allows to “push-back” a token, so that it will be returned by the next call to consume_token, instead of reading from the actual generator.

static create_generator(reader)[source]

Takes a file-like object and produces a stream of tokens following the LISP rules.

This is the method doing the heavy-lifting of tokenization.

class pysmt.smtlib.parser.SmtLibParser(environment=None, interactive=False)[source]

Parse an SmtLib file and builds an SmtLibScript object.

The main function is get_script (and its wrapper get_script_fname). This function relies on the tokenizer function (to split the inputs in token) that is consumed by the get_command function that returns a SmtLibCommand for each command in the original file.

If the interactive flag is True, the file reading proceeds char-by-char with no buffering. This is useful for interactive use for example with a SMT-Lib2-compliant solver

atom(token, mgr)[source]

Given a token and a FormulaManager, returns the pysmt representation of the token

get_expression(tokens)[source]

Returns the pysmt representation of the given parsed expression

get_script(script)[source]

Takes a file object and returns a SmtLibScript object representing the file

get_command_generator(script)[source]

Returns a python generator of SmtLibCommand’s given a file object to read from

This function can be used interactively, and blocks until a whole command is read from the script.

get_script_fname(script_fname)[source]

Given a filename and a Solver, executes the solver on the file.

parse_atoms(tokens, command, min_size, max_size=None)[source]

Parses a sequence of N atoms (min_size <= N <= max_size) consuming the tokens

parse_type(tokens, command, type_params=None, additional_token=None)[source]

Parses a single type name from the tokens

parse_atom(tokens, command)[source]

Parses a single name from the tokens

parse_params(tokens, command)[source]

Parses a list of types from the tokens

parse_named_params(tokens, command)[source]

Parses a list of names and type from the tokens

parse_expr_list(tokens, command)[source]

Parses a list of expressions form the tokens

consume_opening(tokens, command)[source]

Consumes a single ‘(‘

consume_closing(tokens, command)[source]

Consumes a single ‘)’

get_assignment_list(script)[source]

Parse an assignment list produced by get-model and get-value commands in SmtLib

get_command(tokens)[source]

Builds an SmtLibCommand instance out of a parsed term.

class pysmt.smtlib.parser.SmtLib20Parser(environment=None, interactive=False)[source]

Parser for SMT-LIB 2.0.

class pysmt.smtlib.parser.SmtLibZ3Parser(environment=None, interactive=False)[source]

Parses extended Z3 SmtLib Syntax

pysmt.smtlib.printers.to_smtlib(formula, 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

pysmt.smtlib.script.check_sat_filter(log)[source]

Returns the result of the check-sat command from a log.

Raises errors in case a unique check-sat command cannot be located.

class pysmt.smtlib.solver.SmtLibOptions(**base_options)[source]

Options for the SmtLib Solver.

  • debug_interaction: True, False Print the communication between pySMT and the wrapped executable
class pysmt.smtlib.solver.SmtLibSolver(args, environment, logic, LOGICS=None, **options)[source]

Wrapper for using a solver via textual SMT-LIB interface.

The solver is launched in a subprocess using args as arguments of the executable. Interaction with the solver occurs via pipe.

OptionsClass

alias of SmtLibOptions

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.

Substituter

class pysmt.substituter.Substituter(env)[source]

Performs substitution of a set of terms within a formula.

Let f be a formula ans subs be a map from formula to formula. Substitution returns a formula f’ in which all occurrences of the keys of the map have been replaced by their value.

There are a few considerations to take into account:
  • In which order to apply the substitution
  • How to deal with quantified subformulas

The order in which we apply the substitutions gives raise to two different approaches: Most General Substitution and Most Specific Substitution. Lets consider the example:

f = (a & b) subs = {a -> c, (c & b) -> d, (a & b) -> c}
With the Most General Substitution (MGS) we obtain:
f’ = c
with the Most Specific Substitution (MSS) we obtain:
f’ = d

The default behavior before version 0.5 was MSS. However, this leads to unexpected results when dealing with literals, i.e., substitutions in which both x and Not(x) appear, do not work as expected. In case of doubt, it is recommended to issue two separate calls to the substitution procedure.

substitute(formula, subs)[source]

Replaces any subformula in formula with the definition in subs.

class pysmt.substituter.MGSubstituter(env)[source]

Performs Most Generic Substitution.

This is the default behavior since version 0.5

walk_identity_or_replace(formula, args, **kwargs)[source]

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_algebraic_constant(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_and(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_array_select(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_array_store(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_array_value(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bool_constant(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_add(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_and(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_ashr(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_comp(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_concat(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_constant(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_extract(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_lshl(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_lshr(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_mul(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_neg(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_not(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_or(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_rol(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_ror(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_sdiv(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_sext(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_sle(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_slt(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_srem(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_sub(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_udiv(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_ule(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_ult(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_urem(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_xor(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_bv_zext(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_div(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_equals(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_function(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_iff(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_implies(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_int_constant(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_ite(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_le(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_lt(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_minus(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_not(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_or(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_plus(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_pow(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_real_constant(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_symbol(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_times(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

walk_toreal(formula, args, **kwargs)

If the formula appears in the substitution, return the substitution. Otherwise, rebuild the formula by calling the IdentityWalker.

class pysmt.substituter.MSSubstituter(env)[source]

Performs Most Specific Substitution.

This was the default beahvior before version 0.5

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.
pysmt.type_checker.assert_no_boolean_in_args(args)[source]

Enforces that the elements in args are not of BOOL type.

pysmt.type_checker.assert_boolean_args(args)[source]

Enforces that the elements in args are of BOOL type.

pysmt.type_checker.assert_same_type_args(args)[source]

Enforces that all elements in args have the same type.

pysmt.type_checker.assert_args_type_in(args, allowed_types)[source]

Enforces that the type of the arguments is an allowed type

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).

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.

iter_walk(formula, **kwargs)[source]

Performs an iterative walk of the DAG

walk_true(formula, args, **kwargs)[source]

Returns True, independently from the children’s value.

walk_false(formula, args, **kwargs)[source]

Returns False, independently from the children’s value.

walk_none(formula, args, **kwargs)[source]

Returns None, independently from the children’s value.

walk_identity(formula, **kwargs)[source]

Returns formula, independently from the childrens’s value.

walk_any(formula, args, **kwargs)[source]

Returns True if any of the children returned True.

walk_all(formula, args, **kwargs)[source]

Returns True if all the children returned True.

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.

walk(formula, threshold=None)[source]

Generic walk method, will apply the function defined by the map self.functions.

If threshold parameter is specified, the walk_threshold function will be called for all nodes with depth >= threshold.

walk_skip(formula)[source]

Default function to skip a node and process the children

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.