de.uni_freiburg.informatik.ultimate.logic

Class NonRecursive

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.NonRecursive

Direct Known Subclasses:

CheckClosedTerm, FormulaLet, TermEquivalence, TermTransformer

public class NonRecursive
extends java.lang.Object

This class does a recursive algorithm by using an explicit stack on the heap. If you need a stateless walker, you can just implement Walker. If your goal is to walk terms, then TermWalker may help you, as it already dispatches the walk function based on the type of the term. A simple term walker can be created as:

 class MyWalker extends TermWalker {
    MyWalker(Term term) { super(term) }
    walk(NonRecursiveWalker walker, final ApplicationTerm appTerm) {
       walker.addWorkItem(new NonRecursive.Walker() {
          public void walk(NonRecursiveWalker walker) {
             // ... code that should run after parameters are processed
          }
       }
       for (Term param : appTerm.getParameters()) {
          walker.enqueueWalker(new MyWalker(param));
       }
    }
    walk(... // handle other term classes...
 

For stateful walker you need to extend the class NonRecursive. In addition you still need a Walker class that does the job. It can access the state by casting NonRecursive. Results can be added in a stateful walker to an additional result stack. See FormulaUnLet as an example.

Author:

Jochen Hoenicke

See Also:

ComputeFreeVariables, FormulaUnLet

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	NonRecursive.TermWalker Walker that walks non-recursively over terms.
protected static interface	NonRecursive.Walker Walker that does some piece of work.

Constructor Summary

Constructors

Constructor and Description
NonRecursive()

Method Summary

Modifier and Type	Method and Description
void	enqueueWalker(NonRecursive.Walker item) Enqueues a walker on the todo stack.
protected void	reset() Manually reset this walker.
void	run() The main work horse.
void	run(NonRecursive.Walker item) The main work horse.
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

NonRecursive

public NonRecursive()

Method Detail

reset

protected void reset()

Manually reset this walker. This function can be used to clear the todo stack when an exception is raised by a walker. This exception will terminate the non-recursive walk but will leave some walker in the todo stack.

enqueueWalker

public void enqueueWalker(NonRecursive.Walker item)

Enqueues a walker on the todo stack.

Parameters:

item - the walker to enqueue.

run

public void run(NonRecursive.Walker item)

The main work horse. This will repeat doing work items until the todo stack is empty.

Parameters:

item - the walker to execute initially.

run

public void run()

The main work horse. This will repeat doing work items until the todo stack is empty. This method expects that some Walker are on the todo stack.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object