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

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

pysmt.shortcuts.
reset_env
()[source]¶ Resets the global environment, and returns the new one.
Returns: A new environment after resetting the global environment Return type: Environment

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

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

pysmt.shortcuts.
substitute
(formula, subs)[source]¶ Applies the substitutions defined in the dictionary to the formula.
Parameters:  formula (FNode) – The target formula
 subs (A dictionary from FNode to FNode) – Specify the substitutions to apply to the formula
Returns: Formula after applying the substitutions
Return type: Fnode

pysmt.shortcuts.
serialize
(formula, threshold=None)[source]¶ Provides a string representing the formula.
Parameters:  formula (Integer) – The target formula
 threshold – Specify the threshold
Returns: A string representing the formula
Return type: string

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

pysmt.shortcuts.
get_atoms
(formula)[source]¶ Returns the set of atoms of the formula.
Parameters: formula (FNode) – The target formula Returns: the set of atoms of the formula

pysmt.shortcuts.
get_formula_size
(formula, measure=None)[source]¶ Returns the size of the formula as measured by the given counting type.
See pysmt.oracles.SizeOracle for details.
Parameters:  formula (FNode) – The target formula
 measure – Specify the measure/counting type
Returns: The size of the formula as measured by the given counting type.

pysmt.shortcuts.
ForAll
(variables, formula)[source]¶  \[\forall v_1, \cdots, v_n . \varphi(v_1, \cdots, v_n)\]

pysmt.shortcuts.
Exists
(variables, formula)[source]¶  \[\exists v_1, \cdots, v_n . \varphi(v_1, \cdots, v_n)\]

pysmt.shortcuts.
Symbol
(name, typename=Bool)[source]¶ Returns a symbol with the given name and type.
Parameters:  name – Specify the name
 typename – Specify the typename
Returns: A symbol with the given name and type

pysmt.shortcuts.
FreshSymbol
(typename=Bool, template=None)[source]¶ Returns a symbol with a fresh name and given type.
Parameters:  typename – Specify the typename
 template – Specify the template
Returns: A symbol with a fresh name and a given type

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

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

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

pysmt.shortcuts.
TRUE
()[source]¶ Returns the Boolean constant TRUE.
returns: The Boolean constant TRUE

pysmt.shortcuts.
FALSE
()[source]¶ Returns the Boolean constant FALSE.
returns: The Boolean constant FALSE

pysmt.shortcuts.
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 nonboolean 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: Returns: The XOR of left and right

pysmt.shortcuts.
EqualsOrIff
(left, right)[source]¶ Returns Equals() or Iff() depending on the type of the arguments.
This can be used to deal with ambiguous cases where we might be dealing with both Theory and Boolean atoms.

pysmt.shortcuts.
BV
(value, width=None)[source]¶ Returns a constant of type BitVector.
value can be either:  a string of 0s and 1s  a string starting with “#b” followed by a sequence of 0s and 1s  an integer number s.t. 0 <= value < 2**width
In order to create the BV representation of a signed integer, the SBV() method shall be used.
Parameters:  value – Specify the value
 width – Specify the width
Returns: A constant of type BitVector
Return type:

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 2complement representation of the given number, otherwise the behavior is the same as BV().
Parameters:  value – Specify the value
 width – Specify the width of the BV
Returns: A constant of type BitVector interpreting the sign.
Return type:

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

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

pysmt.shortcuts.
BVNot
(formula)[source]¶ Returns the bitwise negation of the bitvector
Parameters: formula – The target formula Returns: The bitvector Not(bv) Return type: FNode

pysmt.shortcuts.
BVAnd
(left, right)[source]¶ Returns the Bitwise AND of two bitvectors of the same size.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The bitwise AND of left and right
Return type:

pysmt.shortcuts.
BVOr
(left, right)[source]¶ Returns the Bitwise OR of two bitvectors of the same size.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The bitwise OR of left and right
Return type:

pysmt.shortcuts.
BVXor
(left, right)[source]¶ Returns the Bitwise XOR of two bitvectors of the same size.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The bitwise XOR of left and right
Return type:

pysmt.shortcuts.
BVConcat
(left, right)[source]¶ Returns the Concatenation of the two BVs
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The concatenation of the two BVs
Return type:

pysmt.shortcuts.
BVExtract
(formula, start=0, end=None)[source]¶ Returns the slice of formula from start to end (inclusive).
Parameters:  formula – The target formula
 start – Specify the start index
 end – Specify the end index
Returns: The slice of formula from start to end (inclusive)
Return type: Fnode

pysmt.shortcuts.
BVULT
(left, right)[source]¶ Returns the Unsigned LessThan comparison of the two BVs.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The Unsigned LessThan comparison of the two BVs
Return type:

pysmt.shortcuts.
BVUGT
(left, right)[source]¶ Returns the Unsigned GreaterThan comparison of the two BVs.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The Unsigned GreaterThan comparison of the two BVs
Return type:

pysmt.shortcuts.
BVULE
(left, right)[source]¶ Returns the Unsigned LessEqual comparison of the two BVs.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The Unsigned LessEqual comparison of the two BVs
Return type:

pysmt.shortcuts.
BVUGE
(left, right)[source]¶ Returns the Unsigned GreaterEqual comparison of the two BVs.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The Unsigned GreaterEqual comparison of the two BVs
Return type:

pysmt.shortcuts.
BVNeg
(formula)[source]¶ Returns the arithmetic negation of the BV.
Parameters: formula – The target formula Returns: The arithmetic negation of the formula Return type: FNode

pysmt.shortcuts.
BVAdd
(left, right)[source]¶ Returns the sum of two BV.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The sum of the two BVs.
Return type:

pysmt.shortcuts.
BVSub
(left, right)[source]¶ Returns the difference of two BV.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The difference of the two BV
Return type:

pysmt.shortcuts.
BVMul
(left, right)[source]¶ Returns the product of two BV.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The product of the two BV
Return type:

pysmt.shortcuts.
BVUDiv
(left, right)[source]¶ Returns the Unsigned division of the two BV.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The Unsigned division of the two BV
Return type:

pysmt.shortcuts.
BVURem
(left, right)[source]¶ Returns the Unsigned remainder of the two BV.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The Unsigned remainder of the two BV
Return type:

pysmt.shortcuts.
BVLShl
(left, right)[source]¶ Returns the logical left shift the BV.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The logical left shift the BV
Return type:

pysmt.shortcuts.
BVLShr
(left, right)[source]¶ Returns the logical right shift the BV.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The logical right shift the BV
Return type:

pysmt.shortcuts.
BVAShr
(left, right)[source]¶  Returns the RIGHT arithmetic shift of the left BV by the number
 of steps specified by the right BV.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The RIGHT arithmetic shift of the left BV by the number of steps specified by the right BV
Return type:

pysmt.shortcuts.
BVRol
(formula, steps)[source]¶ Returns the LEFT rotation of the BV by the number of steps.
Parameters:  formula – The target formula
 steps – Specify the number of steps.
Returns: The LEFT rotation of the BV by the number of steps
Return type:

pysmt.shortcuts.
BVRor
(formula, steps)[source]¶ Returns the RIGHT rotation of the BV by the number of steps.
Parameters:  formula – The target formula
 steps – Specify the number of steps.
Returns: The RIGHT rotation of the BV by the number of steps
Return type:

pysmt.shortcuts.
BVZExt
(formula, increase)[source]¶ Returns the zeroextension of the BV.
New bits are set to zero.
Parameters:  formula – The target formula
 increase – Specify the increase
Returns: The extension of the BV
Return type:

pysmt.shortcuts.
BVSExt
(formula, increase)[source]¶ Returns the signedextension of the BV.
New bits are set according to the mostsignificantbit.
Parameters:  formula – The target formula
 increase – Specify the ‘increase’ value
Returns: The signedextension of the BV.
Return type:

pysmt.shortcuts.
BVSLT
(left, right)[source]¶ Returns the Signed LessThan comparison of the two BVs.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The Signed LessThan comparison of the two BVs
Return type:

pysmt.shortcuts.
BVSLE
(left, right)[source]¶ Returns the Signed LessEqual comparison of the two BVs.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The Signed LessThanEqual comparison of the two BVs
Return type:

pysmt.shortcuts.
BVSGT
(left, right)[source]¶ Returns the Signed GreaterThan comparison of the two BVs.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The Signed GreaterThan comparison of the two BVs
Return type:

pysmt.shortcuts.
BVSGE
(left, right)[source]¶ Returns the Signed GreaterEqual comparison of the two BVs.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The Signed GreaterEqual comparison of the two BVs.
Return type:

pysmt.shortcuts.
BVSDiv
(left, right)[source]¶ Returns the Signed division of the two BVs.
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The the Signed division of left by right
Return type:

pysmt.shortcuts.
BVSRem
(left, right)[source]¶ Returns the Signed remainder of the two BVs
Parameters:  left – Specify the left bitvector
 right – Specify the right bitvector
Returns: The Signed remainder of left divided by right
Return type:

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

pysmt.shortcuts.
BVToNatural
(formula)[source]¶ Returns the Natural number represented by the BitVector.
Parameters: formula – Bitvector to be converted Returns: An integer between 0 and 2^m1 Return type: FNode

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 nonnegative 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 nonempty.

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
Returns: A SELECT application on array at index
Return type:

pysmt.shortcuts.
Store
(array, index, value)[source]¶ Returns a STORE application with given value on array at the given index
Parameters:  array – Specify the array
 index – Specify the index
Returns: A STORE on the array at the given index with the given value
Return type:

pysmt.shortcuts.
Array
(idx_type, default, assigned_values=None)[source]¶ Returns an Array with the given index type and initialization.
If assigned_values is specified, then it must be a map from constants of type idx_type to values of the same type as default and the array is initialized correspondingly.
Parameters:  idx_type – Specify the index type
 default – Specify the default values
 assigned_values – Specify the assigned values
Returns: A node representing an array having index type equal to idx_type, initialized with default values. If assigned_values is specified, then it must be a map from constants of type idx_type to values of the same type as default and the array is initialized correspondingly.
Return type:

pysmt.shortcuts.
Solver
(name=None, logic=None, **kwargs)[source]¶ Returns a solver.
Parameters:  name – Specify the name of the solver
 logic – Specify the logic that is going to be used.
Return type:

pysmt.shortcuts.
UnsatCoreSolver
(name=None, logic=None, unsat_cores_mode='all')[source]¶ Returns a solver supporting unsat core extraction.
Parameters:  name – Specify the name of the solver
 logic – Specify the logic that is going to be used.
 unsat_cores_mode – Specify the unsat cores mode.
Returns: A solver supporting unsat core extraction.
Return type:

pysmt.shortcuts.
QuantifierEliminator
(name=None, logic=None)[source]¶ Returns a quantifier eliminator.
Parameters:  name – Specify the name of the solver
 logic – Specify the logic that is going to be used.
Returns: A quantifier eliminator with the specified name and logic
Return type:

pysmt.shortcuts.
Interpolator
(name=None, logic=None)[source]¶ Returns an interpolator
Parameters:  name – Specify the name of the solver
 logic – Specify the logic that is going to be used.
Returns: An interpolator
Return type:

pysmt.shortcuts.
Portfolio
(solvers_set, logic, **options)[source]¶ Creates a portfolio using the specified solvers.
 Solver_set is an iterable. Elements of solver_set can be
 a name of a solver
 a tuple containing a name of a solver and dict of options
 E.g.,
 Portfolio([“msat”, “z3”], incremental=True)
 or
 Porfolio([(“msat”, {“random_seed”: 1}), (“msat”, {“random_seed”: 2})],
 incremental=True)
Options specified in the Portfolio are shared among all solvers, e.g., in the first example all solvers will receive the option ‘incremental=True’.
One process will be used for each of the solvers.
Parameters:  solvers_set – Specify set of solvers to be used in the portfolio.
 logic – Specify the logic that is going to be used, this might restrict the set of solvers in the portfolio.
Returns: A portfolio solver
Return type: Portfolio

pysmt.shortcuts.
is_sat
(formula, solver_name=None, logic=None, portfolio=None)[source]¶ Returns whether a formula is satisfiable.
Parameters:  formula (FNode) – The formula to check satisfiability
 solver_name (string) – Specify the name of the solver to be used
 logic – Specify the logic that is going to be used
 portfolio (An iterable of solver names) – A list of solver names to perform portfolio solving.
Returns: Whether the formula is SAT or UNSAT.
Return type: bool

pysmt.shortcuts.
get_model
(formula, solver_name=None, logic=None)[source]¶ Similar to
is_sat()
but returns a model if the formula is satisfiable, otherwise NoneParameters:  formula – The target formula
 solver_name – Specify the name of the solver
Param: logic: Specify the logic that is going to be used
Returns: A model if the formula is satisfiable
Return type:

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 clausesParameters:  clauses – Specify the list of input clauses
 solver_name – Specify the name of the solver_name
 logic – Specify the logic that is going to be used
Returns: The unsat core of the conjunction of the input clauses

pysmt.shortcuts.
is_valid
(formula, solver_name=None, logic=None, portfolio=None)[source]¶ Similar to
is_sat()
but checks validity.Parameters:  formula (FNode) – The target formula
 solver_name – Specify the name of the solver to be used
 logic – Specify the logic that is going to be used
 portfolio – A list of solver names to perform portfolio solving.
Returns: Whether the formula is SAT or UNSAT but checks validity
Return type: bool

pysmt.shortcuts.
is_unsat
(formula, solver_name=None, logic=None, portfolio=None)[source]¶ Similar to
is_sat()
but checks unsatisfiability.Parameters:  formula (FNode) – The target formula
 solver_name – Specify the name of the solver to be used
 logic – Specify the logic that is going to be used
 portfolio – A list of solver names to perform portfolio solving.
Returns: Whether the formula is UNSAT or not
Return type: bool

pysmt.shortcuts.
qelim
(formula, solver_name=None, logic=None)[source]¶ Performs quantifier elimination of the given formula.
Parameters:  formula – The target formula
 solver_name – Specify the name of the solver to be used
 logic – Specify the logic that is going to be used
Returns: A formula after performing quantifier elimination
Return type:

pysmt.shortcuts.
binary_interpolant
(formula_a, formula_b, solver_name=None, logic=None)[source]¶ Computes an interpolant of (formula_a, formula_b).
Returns None if the conjunction is satisfiable
Parameters:  formula_a – Specify formula_a
 formula_b – Specify formula_b
 solver_name – Specify the name of the solver to be used
 logic – Specify the logic that is going to be used
Returns: An interpolant of (formula_a, formula_b); None if the conjunction is satisfiable
Return type: FNode or None

pysmt.shortcuts.
sequence_interpolant
(formulas, solver_name=None, logic=None)[source]¶ Computes a sequence interpolant of the formulas.
Returns None if the conjunction is satisfiable.
Parameters:  formulas – The target formulas
 solver_name – Specify the name of the solver to be used
 logic – Specify the logic that is going to be used
Returns: A sequence intepolant of the formulas; None if the conjunction is satisfiable
Return type: FNode or None

pysmt.shortcuts.
read_configuration
(config_filename, environment=None)[source]¶ Reads the pysmt configuration of the given file path and applies it on the specified environment. If no environment is specified, the toplevel environment will be used.
Parameters:  config_filename – Specify the name of the config file
 environment – Specify the environment

pysmt.shortcuts.
write_configuration
(config_filename, environment=None)[source]¶ Dumps the current pysmt configuration to the specified file path
Parameters:  config_filename – Specify the name of the config file
 environment – Specify the environment

pysmt.shortcuts.
read_smtlib
(fname)[source]¶ Reads the SMT formula from the given file.
This supports compressed files, if the fname ends in .bz2 .
Parameters: fname – Specify the filename Returns: An SMT formula Return type: FNode

pysmt.shortcuts.
write_smtlib
(formula, fname)[source]¶ Writes the given formula in SmtLib 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 SmtLib string representation of the formula.
The daggify parameter can be used to switch from a linearsize 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 Return type: bool

is_valid
(formula)[source]¶ Checks validity of the formula w.r.t. the current state of the solver.
Previous assertions are taken into account. See
is_sat()
Returns: Whether formula is valid Return type: bool

is_unsat
(formula)[source]¶ Checks unsatisfiability of the formula w.r.t. the current state of the solver.
Previous assertions are taken into account. See
is_sat()
Returns: Whether formula is unsatisfiable Return type: bool

get_values
(formulae)[source]¶ Returns the value of the expressions if a model was found.
Requires option generate_models to be set to true (default) and can be called only after
solve()
(or to one of the derived methods) returned sat or unknown, if no change to the assertion set occurred.Returns: A dictionary associating to each expr a value Return type: dict

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 SMTLIB function get_values


class
pysmt.solvers.solver.
Model
(environment)[source]¶ An abstract Model for a Solver.
This class provides basic services to operate on a model returned by a solver. This class is used as superclass for more specific Models, that are solver dependent or by the EagerModel class.

get_value
(formula, model_completion=True)[source]¶ Returns the value of formula in the current model (if one exists).
If model_completion is True, then variables not appearing in the assignment are given a default value, otherwise an error is generated.
This is a simplified version of the SMTLIB 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]¶

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.

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
¶ alias of
pysmt.type_checker.SimpleTypeChecker

FormulaManagerClass
¶ alias of
pysmt.formula.FormulaManager

SimplifierClass
¶ alias of
pysmt.simplifier.Simplifier

SubstituterClass
¶ alias of
pysmt.substituter.MGSubstituter

HRSerializerClass
¶ alias of
pysmt.printers.HRSerializer

QuantifierOracleClass
¶ alias of
pysmt.oracles.QuantifierOracle

TheoryOracleClass
¶ alias of
pysmt.oracles.TheoryOracle

FreeVarsOracleClass
¶ alias of
pysmt.oracles.FreeVarsOracle

SizeOracleClass
¶ alias of
pysmt.oracles.SizeOracle

AtomsOracleClass
¶ alias of
pysmt.oracles.AtomsOracle

TypesOracleClass
¶ alias of
pysmt.oracles.TypesOracle

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.

Exceptions¶
This module contains all custom exceptions of pySMT.

exception
pysmt.exceptions.
UnknownSmtLibCommandError
[source]¶ Raised when the parser finds an unknown command.

exception
pysmt.exceptions.
SolverReturnedUnknownResultError
[source]¶ This exception is raised if a solver returns ‘unknown’ as a result

exception
pysmt.exceptions.
UnknownSolverAnswerError
[source]¶ Raised when the a solver returns an invalid response.

exception
pysmt.exceptions.
NoSolverAvailableError
[source]¶ No solver is available for the selected Logic.

exception
pysmt.exceptions.
UndefinedLogicError
[source]¶ This exception is raised if an undefined Logic is attempted to be used.

exception
pysmt.exceptions.
InternalSolverError
[source]¶ Generic exception to capture errors provided by a solver.

exception
pysmt.exceptions.
NoLogicAvailableError
[source]¶ Generic exception to capture errors caused by missing support for logics.

exception
pysmt.exceptions.
SolverRedefinitionError
[source]¶ Exception representing errors caused by multiple 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.
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_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

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.

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 TypeChecker.
See
SimpleTypeChecker

is_constant
(_type=None, value=None)[source]¶ Test whether the formula is a constant.
Optionally, check that the constant is of the given type and value.

is_bool_constant
(value=None)[source]¶ Test whether the formula is a Boolean constant.
Optionally, check that the constant has the given value.

is_real_constant
(value=None)[source]¶ Test whether the formula is a Real constant.
Optionally, check that the constant has the given value.

is_int_constant
(value=None)[source]¶ Test whether the formula is an Integer constant.
Optionally, check that the constant has the given value.

is_bv_constant
(value=None, width=None)[source]¶ Test whether the formula is a BitVector constant.
Optionally, check that the constant has the given value.

is_string_constant
(value=None)[source]¶ Test whether the formula is a String constant.
Optionally, check that the constant has the given value.

is_symbol
(type_=None)[source]¶ Test whether the formula is a Symbol.
Optionally, check that the symbol has the given type.

is_literal
()[source]¶ Test whether the formula is a literal.
A literal is a positive or negative Boolean symbol.

is_lira_op
(**kwargs)¶ Test whether the node is a IRA operator.

serialize
(threshold=None)[source]¶ Returns a human readable representation of the formula.
The threshold parameter can be used to limit the amount of the formula that will be printed. See
HRSerializer

to_smtlib
(daggify=True)[source]¶ Returns a SmtLib string representation of the formula.
The daggify parameter can be used to switch from a linearsize representation that uses ‘let’ operators to represent the formula as a dag or a simpler (but possibly exponential) representation that expands the formula as a tree.
See
SmtPrinter

is_term
()[source]¶ Test whether the node is a term.
All nodes are terms, except for function definitions.

bv_str
(fmt='b')[source]¶ Return a string representation of the BitVector.
 fmt: ‘b’ : Binary
 ‘d’ : Decimal ‘x’ : Hexadecimal
The representation is always unsigned

bv_bin_str
(reverse=False)[source]¶ Return the binary representation of the BitVector as string.
The reverse option is provided to deal with MSB/LSB.

array_value_get
(index)[source]¶ Returns the value of this Array Value at the given index. The index must be a constant of the correct type.
This function is equivalent (but possibly faster) than the following code:
m = self.array_value_assigned_values_map() try: return m[index] except KeyError: return self.array_value_default()

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 0arity 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 narguments:
 Times(a,b,c)
 Times([a,b,c])
 Restriction:
 Arguments must be all of the same type
 Arguments must be INT or REAL

Equals
(left, right)[source]¶ Creates an expression of the form: left = right
For the boolean case use Iff

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

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 narguments:
 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 narguments:
 Plus(a,b,c)
 Plus([a,b,c])
 Restriction:
 Arguments must be all of the same type
 Arguments must be INT or REAL

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 exactlyone constraint on the boolean symbols.
 This using a quadratic encoding:
 A / B / C A > !(B / C) B > !(C)

AllDifferent
(*args)[source]¶ Encodes the ‘alldifferent’ constraint using two possible encodings.
AllDifferent(x, y, z) := (x != y) & (x != z) & (y != z)

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 2complement representation of the given number, otherwise the behavior is the same as BV().

BVExtract
(formula, start=0, end=None)[source]¶ Returns the slice of formula from start to end (inclusive).

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

BVComp
(left, right)[source]¶ Returns a BV of size 1 equal to 0 if left is equal to right, otherwise 1 is returned.

BVAShr
(left, right)[source]¶ Returns the RIGHT arithmetic rotation of the left BV by the number of steps specified by the right BV.

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 nonnegative 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 nonempty.

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^m1

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.

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

class
pysmt.logics.
Theory
(arrays=None, arrays_const=None, bit_vectors=None, floating_point=None, integer_arithmetic=None, real_arithmetic=None, integer_difference=None, real_difference=None, linear=None, uninterpreted=None, custom_type=None, strings=None)[source]¶ Describes a theory similarly to the SMTLIB 2.0.

class
pysmt.logics.
Logic
(name, description, quantifier_free=False, theory=None, **theory_kwargs)[source]¶ Describes a Logic similarly to the way they are defined in the SMTLIB 2.0
Note: We define more Logics than the ones defined in the SMTLib 2.0. See LOGICS for a list of all the logics and SMTLIB2_LOGICS for the restriction to the ones defined in SMTLIB2.0

pysmt.logics.
convert_logic_from_string
(name)[source]¶ Helper function to parse function arguments.
This takes a logic or a string or None, and returns a logic or None.

pysmt.logics.
get_logic_name
(**logic_kwargs)[source]¶ Returns the name of the Logic that matches the given properties.
See get_logic for the list of parameters.

pysmt.logics.
get_logic
(quantifier_free=False, arrays=False, arrays_const=False, bit_vectors=False, floating_point=False, integer_arithmetic=False, real_arithmetic=False, integer_difference=False, real_difference=False, linear=True, uninterpreted=False, custom_type=False, strings=False)[source]¶ Returns the Logic that matches the given properties.
Equivalent (but better) to executing get_logic_by_name(get_logic_name(…))

pysmt.logics.
most_generic_logic
(logics)[source]¶ Given a set of logics, return the most generic one.
If a unique most generic logic does not exists, throw an error.

pysmt.logics.
get_closer_logic
(supported_logics, logic)[source]¶ Returns the smaller supported logic that is greater or equal to the given logic. Raises NoLogicAvailableError if the solver does not support the given logic.
Operators¶
This module defines all the operators used internally by pySMT.
Note that other expressions can be built in the FormulaManager, but they will be rewritten (during construction) in order to only use these operators.
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.
QuantifierOracle
(env=None, invalidate_memoization=False)[source]¶ 

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]¶ 

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_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_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_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]¶

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

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.


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

Printers¶

class
pysmt.printers.
HRPrinter
(stream, env=None)[source]¶ Performs serialization of a formula in a humanreadable 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.

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 humanreadable representation.
Simplifier¶

class
pysmt.simplifier.
Simplifier
(env=None)[source]¶ Perform basic simplifications of the input 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.
SMTLIB¶

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

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.


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.


pysmt.smtlib.printers.
to_smtlib
(formula, daggify=True)[source]¶ Returns a SmtLib string representation of the formula.
The daggify parameter can be used to switch from a linearsize representation that uses ‘let’ operators to represent the formula as a dag or a simpler (but possibly exponential) representation that expands the formula as a tree.
See
SmtPrinter

pysmt.smtlib.script.
check_sat_filter
(log)[source]¶ Returns the result of the checksat command from a log.
Raises errors in case a unique checksat 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 SMTLIB 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.

get_value
(item)[source]¶ Returns the value of formula in the current model (if one exists).
This is a simplified version of the SMTLIB function get_values

Defines constants for the commands of the SMTLIB

class
pysmt.smtlib.annotations.
Annotations
(initial_annotations=None)[source]¶ Handles and stores (key,value) annotations for formulae

add
(formula, annotation, value=None)[source]¶ Adds an annotation for the given formula, possibly with the specified value

remove_value
(formula, annotation, value)[source]¶ Removes the given annotation for the given formula

has_annotation
(formula, annotation, value=None)[source]¶ Returns True iff the given formula has the given annotation. If Value is specified, True is returned only if the value is matching.

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.

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
TypeChecker¶
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]¶ 

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.
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 SMTLIB “definesort” command.

pysmt.typing.
FunctionType
(return_type, param_types)[source]¶ Returns Function Type with the given arguments.
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.

walk_false
(formula, args, **kwargs)[source]¶ Returns False, independently from the children’s value.


class
pysmt.walkers.
TreeWalker
(env=None)[source]¶ TreeWalker treats the formula as a Tree and does not perform memoization.
This should be used when applying a the function to the same formula is expected to yield different results, for example, serialization. If the operations are functions, consider using the DagWalker instead.
The recursion within walk_ methods is obtained by using the ‘yield’ keyword. In practice, each walk_ method is a generator that yields its arguments. If the generator returns None, no recursion will be performed.

class
pysmt.walkers.
IdentityDagWalker
(env=None, invalidate_memoization=None)[source]¶ This class traverses a formula and rebuilds it recursively identically.
This could be useful when only some nodes needs to be rewritten but the structure of the formula has to be kept.

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.
