SMT_visitor

(class from pyomo.contrib.satsolver.satsolver)

class pyomo.contrib.satsolver.satsolver.SMT_visitor(varmap)

Bases: StreamBasedExpressionVisitor

Creates an SMT expression from the corresponding Pyomo expression.

This class walks a pyomo expression tree and builds up the corresponding SMT string representation of an equivalent expression

__init__(varmap)

Methods

__init__(varmap)
beforeChild(node, child, child_idx)
exitNode(node, data)
finalizeResult(node_result)
walk_expression(expr)	Walk an expression, calling registered callbacks.
walk_expression_nonrecursive(expr)	Nonrecursively walk an expression, calling registered callbacks.

Attributes

client_methods

Member Documentation

walk_expression(expr)

Walk an expression, calling registered callbacks.

This is the standard interface for running the visitor. It defaults to using an efficient recursive implementation of the visitor, falling back on walk_expression_nonrecursive() if the recursion stack gets too deep.

walk_expression_nonrecursive(expr)

Nonrecursively walk an expression, calling registered callbacks.

This routine is safer than the recursive walkers for deep (or unbalanced) trees. It is, however, slightly slower than the recursive implementations.