# 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 Environment
pysmt.shortcuts.reset_env()[source]

Resets the global environment, and returns the new one.

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

Returns the type of the formula.

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

Returns the simplified version of the formula.

Parameters: formula (FNode) – The target formula The simplified version of the formula 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 Formula after applying the substitutions Fnode
pysmt.shortcuts.serialize(formula, threshold=None)[source]

Provides a string representing the formula.

Parameters: formula (Integer) – The target formula threshold – Specify the threshold A string representing the formula string
pysmt.shortcuts.get_free_variables(formula)[source]

Returns the free variables of the formula.

Parameters: formula (FNode) – The target formula 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 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 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.NotEquals(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 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 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 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 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 A Real constant with the given value
pysmt.shortcuts.String(value)[source]

Returns a String 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 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 A constant of type BitVector 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 A constant of type BitVector interpreting the sign. FNode
pysmt.shortcuts.BVOne(width=None)[source]

Returns the unsigned one constant BitVector.

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

Returns the zero constant BitVector.

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

Returns the bitwise negation of the bitvector

Parameters: formula – The target formula The bitvector Not(bv) 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 The bit-wise AND of left and right 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 The bit-wise OR of left and right 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 The bit-wise XOR of left and right 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 The concatenation of the two BVs 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 The slice of formula from start to end (inclusive) 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 The Unsigned Less-Than comparison of the two BVs 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 The Unsigned Greater-Than comparison of the two BVs 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 The Unsigned Less-Equal comparison of the two BVs 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 The Unsigned Greater-Equal comparison of the two BVs FNode
pysmt.shortcuts.BVNeg(formula)[source]

Returns the arithmetic negation of the BV.

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

Returns the sum of two BV.

Parameters: left – Specify the left bitvector right – Specify the right bitvector The sum of the two BVs. FNode
pysmt.shortcuts.BVSub(left, right)[source]

Returns the difference of two BV.

Parameters: left – Specify the left bitvector right – Specify the right bitvector The difference of the two BV FNode
pysmt.shortcuts.BVMul(left, right)[source]

Returns the product of two BV.

Parameters: left – Specify the left bitvector right – Specify the right bitvector The product of the two BV 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 The Unsigned division of the two BV 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 The Unsigned remainder of the two BV 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 The logical left shift the BV 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 The logical right shift the BV 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 The RIGHT arithmetic rotation of the left BV by the number of steps specified by the right BV 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. The LEFT rotation of the BV by the number of steps 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. The RIGHT rotation of the BV by the number of steps 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 The extension of the BV 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 The signed-extension of the BV. 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 The Signed Less-Than comparison of the two BVs 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 The Signed Less-Than-Equal comparison of the two BVs 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 The Signed Greater-Than comparison of the two BVs 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 The Signed Greater-Equal comparison of the two BVs. 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 The the Signed division of left by right 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 The Signed remainder of left divided by right 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 A BV of size 1 equal to 0 if left is equal to right, otherwise 1 FNode
pysmt.shortcuts.BVToNatural(formula)[source]

Returns the Natural number represented by the BitVector.

Parameters: formula – Bitvector to be converted An integer between 0 and 2^m-1 FNode
pysmt.shortcuts.StrLength(string)[source]

Returns the length of a formula resulting a String

pysmt.shortcuts.StrCharAt(string, index)[source]

Returns a single character String at position i.

s is a string term and i is an integer term. i is the position.

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

Returns the concatenation of n Strings.

s1, s2, …, and sn are String terms. String concatenation takes at least 2 arguments.

pysmt.shortcuts.StrContains(string, target)[source]

Returns wether string contains the target.

s and t are String terms.

pysmt.shortcuts.StrIndexOf(string, target, offset)[source]

Returns the position of the first occurrence of target in string after the offset.

s and t being a non empty strings and i a non-negative integer. It returns -1 if the value to search for never occurs.

pysmt.shortcuts.StrReplace(s, t1, t2)[source]

Returns a new string where the first occurrence of t1 is replace by t2.

where s, t1 and t2 are string terms, t1 is non-empty.

pysmt.shortcuts.StrSubstr(s, i, j)[source]

Returns a substring of s starting at i and ending at j+i.

where s is a string term and i, j are integer terms.

pysmt.shortcuts.StrPrefixOf(s, t)[source]

Returns whether the s is a prefix of the string t.

where s and t are string terms.

pysmt.shortcuts.StrSuffixOf(s, t)[source]

Returns whether the string s is a suffix of the string t.

where s and t are string terms.

pysmt.shortcuts.StrToInt(x)[source]

Returns the corresponding natural number of s is valid;

If s is not valid, it returns -1.

pysmt.shortcuts.IntToStr(x)[source]

Returns the corresponding String representing the natural number x.

where x is an integer term. If x is not a natural number it returns the empty String.

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 A SELECT application on array at index 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 A STORE on the array at the given index with the given value 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 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. 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. 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. A solver supporting unsat core extraction. 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. A quantifier eliminator with the specified name and logic 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. An interpolator 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. Whether the formula is SAT or UNSAT. 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 logic: Specify the logic that is going to be used A model if the formula is satisfiable 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 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. Whether the formula is SAT or UNSAT but checks validity 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. Whether the formula is UNSAT or not 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 A formula after performing quantifier elimination 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 An interpolant of (formula_a, formula_b); None if the conjunction is satisfiable 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 A sequence intepolant of the formulas; None if the conjunction is satisfiable 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 An SMT formula FNode
pysmt.shortcuts.write_smtlib(formula, fname)[source]

Writes the given formula in Smt-Lib format to the given file.

Parameters: formula – Specify the SMT formula to be written 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 pysmt.solvers.options.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 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 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 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 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.

TypeCheckerClass
FormulaManagerClass
SimplifierClass
SubstituterClass
HRSerializerClass
QuantifierOracleClass
TheoryOracleClass
FreeVarsOracleClass
SizeOracleClass
AtomsOracleClass
TypesOracleClass
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

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]

## 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_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_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_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

For the boolean case use Iff

NotEquals(left, right)[source]

Creates an expression of the form: left != right

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.

String(value)[source]

Return a constant of type STRING.

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.

StrLength(formula)[source]

Returns the length of a formula resulting a String

StrConcat(*args)[source]

Returns the concatenation of n Strings.

s1, s2, …, and sn are String terms. String concatenation takes at least 2 arguments.

StrContains(s, t)[source]

Returns wether the String s contains the String t.

s and t are String terms.

StrIndexOf(s, t, i)[source]

Returns the position of the first occurrence of t in s after the index i.

s and t being a non empty strings and i a non-negative integer. It returns -1 if the value to search for never occurs.

StrReplace(s, t1, t2)[source]

Returns a new string where the first occurrence of t1 is replace by t2.

where s, t1 and t2 are string terms, t1 is non-empty.

StrSubstr(s, i, j)[source]

Returns a substring of s starting at i and ending at j+i.

where s is a string term and i, j are integer terms.

StrPrefixOf(s, t)[source]

Returns whether the s is a prefix of the string t.

where s and t are string terms.

StrSuffixOf(s, t)[source]

Returns whether the string s is a suffix of the string t.

where s and t are string terms.

StrToInt(s)[source]

Returns the corresponding natural number of s.

If s does not represent a natural number, it returns -1.

IntToStr(x)[source]

Returns the corresponding String representing the natural number x.

where x is an integer term. If x is not a natural number it returns the empty String.

StrCharAt(s, i)[source]

Returns a single character String at position i.

s is a string term and i is an integer term. i is the position.

BVToNatural(formula)[source]

Returns the Natural number represented by the BitVector.

Given a BitVector of width m returns an integer between 0 and 2^m-1

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.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

## 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.QuantifierOracle(env=None, invalidate_memoization=False)[source]
is_qf(formula)[source]

Returns whether formula is Quantifier Free.

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

Returns True if all the children returned True.

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

Returns False, independently from the children’s value.

walk_algebraic_constant(formula, args, **kwargs)

Returns True if all the children returned True.

walk_and(formula, args, **kwargs)

Returns True if all the children returned True.

walk_array_select(formula, args, **kwargs)

Returns True if all the children returned True.

walk_array_store(formula, args, **kwargs)

Returns True if all the children returned True.

walk_array_value(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bool_constant(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_add(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_and(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_ashr(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_comp(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_concat(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_constant(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_extract(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_lshl(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_lshr(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_mul(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_neg(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_not(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_or(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_rol(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_ror(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_sdiv(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_sext(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_sle(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_slt(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_srem(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_sub(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_tonatural(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_udiv(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_ule(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_ult(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_urem(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_xor(formula, args, **kwargs)

Returns True if all the children returned True.

walk_bv_zext(formula, args, **kwargs)

Returns True if all the children returned True.

walk_div(formula, args, **kwargs)

Returns True if all the children returned True.

walk_equals(formula, args, **kwargs)

Returns True if all the children returned True.

walk_exists(formula, args, **kwargs)

Returns False, independently from the children’s value.

walk_forall(formula, args, **kwargs)

Returns False, independently from the children’s value.

walk_function(formula, args, **kwargs)

Returns True if all the children returned True.

walk_iff(formula, args, **kwargs)

Returns True if all the children returned True.

walk_implies(formula, args, **kwargs)

Returns True if all the children returned True.

walk_int_constant(formula, args, **kwargs)

Returns True if all the children returned True.

walk_int_to_str(formula, args, **kwargs)

Returns True if all the children returned True.

walk_ite(formula, args, **kwargs)

Returns True if all the children returned True.

walk_le(formula, args, **kwargs)

Returns True if all the children returned True.

walk_lt(formula, args, **kwargs)

Returns True if all the children returned True.

walk_minus(formula, args, **kwargs)

Returns True if all the children returned True.

walk_not(formula, args, **kwargs)

Returns True if all the children returned True.

walk_or(formula, args, **kwargs)

Returns True if all the children returned True.

walk_plus(formula, args, **kwargs)

Returns True if all the children returned True.

walk_pow(formula, args, **kwargs)

Returns True if all the children returned True.

walk_real_constant(formula, args, **kwargs)

Returns True if all the children returned True.

walk_str_charat(formula, args, **kwargs)

Returns True if all the children returned True.

walk_str_concat(formula, args, **kwargs)

Returns True if all the children returned True.

walk_str_constant(formula, args, **kwargs)

Returns True if all the children returned True.

walk_str_contains(formula, args, **kwargs)

Returns True if all the children returned True.

walk_str_indexof(formula, args, **kwargs)

Returns True if all the children returned True.

walk_str_length(formula, args, **kwargs)

Returns True if all the children returned True.

walk_str_prefixof(formula, args, **kwargs)

Returns True if all the children returned True.

walk_str_replace(formula, args, **kwargs)

Returns True if all the children returned True.

walk_str_substr(formula, args, **kwargs)

Returns True if all the children returned True.

walk_str_suffixof(formula, args, **kwargs)

Returns True if all the children returned True.

walk_str_to_int(formula, args, **kwargs)

Returns True if all the children returned True.

walk_symbol(formula, args, **kwargs)

Returns True if all the children returned True.

walk_times(formula, args, **kwargs)

Returns True if all the children returned True.

walk_toreal(formula, args, **kwargs)

Returns True if all the children returned True.

class pysmt.oracles.TheoryOracle(env=None, invalidate_memoization=False)[source]
get_theory(formula)[source]

Returns the thoery for the formula.

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

Combines the current theory value of the children

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

Returns a new theory object with the type of the constant.

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

Returns a new theory object with the type of the symbol.

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

Extends the Theory with UF.

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

Extends the Theory with LIRA.

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

Extends the Theory with Integer.

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

Extends the Theory with Non-Linear, if needed.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Extends the Theory with Strings.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Extends the Theory with Non-Linear, if needed.

walk_and(formula, args, **kwargs)

Combines the current theory value of the children

walk_array_select(formula, args, **kwargs)

Combines the current theory value of the children

walk_array_store(formula, args, **kwargs)

Combines the current theory value of the children

walk_bool_constant(formula, args, **kwargs)

Returns a new theory object with the type of the constant.

walk_bv_add(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_and(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_ashr(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_comp(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_concat(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_constant(formula, args, **kwargs)

Returns a new theory object with the type of the constant.

walk_bv_extract(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_lshl(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_lshr(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_mul(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_neg(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_not(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_or(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_rol(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_ror(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_sdiv(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_sext(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_sle(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_slt(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_srem(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_sub(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_udiv(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_ule(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_ult(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_urem(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_xor(formula, args, **kwargs)

Combines the current theory value of the children

walk_bv_zext(formula, args, **kwargs)

Combines the current theory value of the children

walk_equals(formula, args, **kwargs)

Combines the current theory value of the children

walk_exists(formula, args, **kwargs)

Combines the current theory value of the children

walk_forall(formula, args, **kwargs)

Combines the current theory value of the children

walk_iff(formula, args, **kwargs)

Combines the current theory value of the children

walk_implies(formula, args, **kwargs)

Combines the current theory value of the children

walk_int_constant(formula, args, **kwargs)

Returns a new theory object with the type of the constant.

walk_int_to_str(formula, args, **kwargs)

Combines the current theory value of the children

walk_ite(formula, args, **kwargs)

Combines the current theory value of the children

walk_le(formula, args, **kwargs)

Combines the current theory value of the children

walk_lt(formula, args, **kwargs)

Combines the current theory value of the children

walk_minus(formula, args, **kwargs)

Combines the current theory value of the children

walk_not(formula, args, **kwargs)

Combines the current theory value of the children

walk_or(formula, args, **kwargs)

Combines the current theory value of the children

walk_real_constant(formula, args, **kwargs)

Returns a new theory object with the type of the constant.

walk_str_charat(formula, args, **kwargs)

Combines the current theory value of the children

walk_str_concat(formula, args, **kwargs)

Combines the current theory value of the children

walk_str_constant(formula, args, **kwargs)

Returns a new theory object with the type of the constant.

walk_str_contains(formula, args, **kwargs)

Combines the current theory value of the children

walk_str_prefixof(formula, args, **kwargs)

Combines the current theory value of the children

walk_str_replace(formula, args, **kwargs)

Combines the current theory value of the children

walk_str_substr(formula, args, **kwargs)

Combines the current theory value of the children

walk_str_suffixof(formula, args, **kwargs)

Combines the current theory value of the children

class pysmt.oracles.FreeVarsOracle(env=None, invalidate_memoization=False)[source]
get_free_variables(formula)[source]

Returns the set of Symbols appearing free in the formula.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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.

walk_symbol(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_function(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

class pysmt.oracles.TypesOracle(env=None, invalidate_memoization=False)[source]
get_types(formula, custom_only=False)[source]

Returns the types appearing in the formula.

custom_only: filter the result by excluding base SMT-LIB types.

expand_types(types)[source]

Recursively look into composite types.

Note: This returns a list. The list is ordered (by construction) by having simpler types first)

walk_symbol(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_function(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

walk_not(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_symbol(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_function(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_real_constant(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_int_constant(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bool_constant(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_constant(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_algebraic_constant(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_extract(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_neg(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_ror(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_rol(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_zext(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_sext(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_ite(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_forall(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_exists(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_toreal(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_constant(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_length(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_charat(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_concat(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_contains(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_indexof(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_replace(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_substr(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_prefixof(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_suffixof(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_to_int(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_int_to_str(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_array_select(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_array_store(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_array_value(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_tonatural(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_and(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_or(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_plus(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_times(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_div(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_pow(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_iff(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_implies(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_minus(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_equals(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_le(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_lt(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_xor(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_concat(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_udiv(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_urem(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_sdiv(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_srem(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_sle(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_slt(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_ule(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_ult(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_lshl(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_lshr(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_ashr(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_comp(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_and(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_or(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_not(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_add(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_mul(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_sub(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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.

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.

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.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Returns formula, independently from the childrens’s value.

walk_algebraic_constant(formula, args, **kwargs)

Returns formula, independently from the childrens’s value.

walk_bool_constant(formula, args, **kwargs)

Returns formula, independently from the childrens’s value.

walk_bv_constant(formula, args, **kwargs)

Returns formula, independently from the childrens’s value.

walk_int_constant(formula, args, **kwargs)

Returns formula, independently from the childrens’s value.

walk_real_constant(formula, args, **kwargs)

Returns formula, independently from the childrens’s value.

walk_str_constant(formula, args, **kwargs)

Returns formula, independently from the childrens’s value.

walk_symbol(formula, args, **kwargs)

Returns formula, independently from the childrens’s value.

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.

simplify(formula)[source]

Performs simplification of the given formula.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

## SMT-LIB¶

class pysmt.smtlib.printers.SmtPrinter(stream)[source]
walk_threshold(formula)[source]

This is a complete printer

walk_and(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_or(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_not(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_implies(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_iff(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_plus(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_minus(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_times(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_equals(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_le(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_lt(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_ite(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_toreal(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_div(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_pow(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_and(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_or(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_not(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_xor(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_add(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_sub(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_neg(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_mul(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_udiv(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_urem(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_lshl(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_lshr(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_ult(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_ule(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_slt(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_sle(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_concat(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_comp(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_ashr(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_sdiv(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_srem(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_tonatural(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_array_select(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_array_store(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_symbol(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_function(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_int_constant(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_real_constant(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bool_constant(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_constant(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_constant(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_forall(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_exists(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_extract(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_length(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_charat(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_concat(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_contains(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_indexof(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_replace(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_substr(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_prefixof(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_suffixof(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_to_int(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_int_to_str(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_array_value(formula)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

class pysmt.smtlib.printers.SmtDagPrinter(stream, template='.def_%d')[source]
walk_and(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_or(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_not(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_implies(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_iff(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_plus(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_minus(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_times(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_equals(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_le(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_lt(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_ite(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_toreal(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_div(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_pow(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_and(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_or(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_not(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_xor(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_add(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_sub(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_neg(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_mul(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_udiv(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_urem(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_lshl(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_lshr(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_ult(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_ule(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_slt(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_sle(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_concat(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_comp(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_ashr(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_sdiv(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_srem(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_tonatural(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_array_select(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_array_store(formula, args)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_symbol(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_int_constant(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_real_constant(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_constant(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bool_constant(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_constant(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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.

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.script.SmtLibCommand[source]
serialize(outstream=None, printer=None, daggify=True)[source]

Serializes the SmtLibCommand into outstream using the given printer.

Exactly one of outstream or printer must be specified. When specifying the printer, the associated outstream will be used. If printer is not specified, daggify controls the printer to be created. If true a daggified formula is produced, otherwise a tree printing is done.

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

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.

reset_assertions()[source]

Removes all defined assertions.

add_assertion(formula, named=None)[source]

Add assertion to the solver.

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.

get_value(item)[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

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

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_forall(formula, args, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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_tonatural(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_int_to_str(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_str_charat(formula, args, **kwargs)

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

walk_str_concat(formula, args, **kwargs)

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

walk_str_constant(formula, args, **kwargs)

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

walk_str_contains(formula, args, **kwargs)

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

walk_str_indexof(formula, args, **kwargs)

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

walk_str_length(formula, args, **kwargs)

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

walk_str_prefixof(formula, args, **kwargs)

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

walk_str_replace(formula, args, **kwargs)

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

walk_str_substr(formula, args, **kwargs)

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

walk_str_suffixof(formula, args, **kwargs)

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

walk_str_to_int(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

substitute(formula, subs)[source]

Replaces any subformula in formula with the definition in subs.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

## 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.
class pysmt.type_checker.SimpleTypeChecker(env=None)[source]
get_type(formula)[source]

Returns the pysmt.types type of the formula

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_length(formula, args, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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.

class pysmt.typing.StringType[source]
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.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_constant(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_constant(formula, **kwargs)[source]

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

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

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.