# Source code for pysmt.walkers.tree

#
# This file is part of pySMT.
#
#   Copyright 2014 Andrea Micheli and Marco Gario
#
#   you may not use this file except in compliance with the License.
#   You may obtain a copy of the License at
#
#
#   Unless required by applicable law or agreed to in writing, software
#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
#   See the License for the specific language governing permissions and
#
from pysmt.walkers.generic import Walker

[docs]class TreeWalker(Walker):
"""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

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.

"""

def __init__(self, env=None):
Walker.__init__(self, env)
return

[docs]    def walk(self, formula, threshold=None):
"""Generic walk method, will apply the function defined by the map
self.functions.

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

try:
f = self.functions[formula.node_type()]
except KeyError:
f = self.walk_error

iterator = f(formula)
if iterator is None:
return

stack = [iterator]
while stack:
f = stack[-1]
try:
child = next(f)
if threshold and len(stack) >= threshold:
iterator = self.walk_threshold(child)
if iterator is not None:
stack.append(iterator)
else:
try:
cf = self.functions[child.node_type()]
except KeyError:
cf = self.walk_error
iterator = cf(child)
if iterator is not None:
stack.append(iterator)
except StopIteration:
stack.pop()
return

def walk_threshold(self, formula):
raise NotImplementedError

[docs]    def walk_skip(self, formula):
""" Default function to skip a node and process the children """
for s in formula.args():
yield s
return

# EOC TreeWalker