de.uni_freiburg.informatik.ultimate.logic

Class ComputeFreeVariables

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.NonRecursive.TermWalker

de.uni_freiburg.informatik.ultimate.logic.ComputeFreeVariables

All Implemented Interfaces:

NonRecursive.Walker

public class ComputeFreeVariables
extends NonRecursive.TermWalker

Helper to compute the free variables contained in a term. This class uses memoization in the terms to compute the free variables efficiently on DAGs.

Author:

hoenicke

Field Summary

Fields inherited from class de.uni_freiburg.informatik.ultimate.logic.NonRecursive.TermWalker

mTerm

Constructor Summary

Constructors

Constructor and Description
ComputeFreeVariables(Term term)

Method Summary

Modifier and Type	Method and Description
void	walk(NonRecursive walker) Do one step of the recursive algorithm.
void	walk(NonRecursive walker, AnnotatedTerm annot)
void	walk(NonRecursive walker, ApplicationTerm term)
void	walk(NonRecursive walker, ConstantTerm term)
void	walk(NonRecursive walker, LetTerm letTerm)
void	walk(NonRecursive walker, QuantifiedFormula quant)
void	walk(NonRecursive walker, TermVariable term)

Methods inherited from class de.uni_freiburg.informatik.ultimate.logic.NonRecursive.TermWalker

getTerm, toString

Methods inherited from class java.lang.Object

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

Constructor Detail

ComputeFreeVariables

public ComputeFreeVariables(Term term)

Method Detail

walk

public void walk(NonRecursive walker)

Description copied from interface: NonRecursive.Walker

Do one step of the recursive algorithm. This may enqueue new walkers that do the remaining steps.

Specified by:

walk in interface NonRecursive.Walker

Overrides:

walk in class NonRecursive.TermWalker

Parameters:

walker - The non recursive engine where new walkers can be enqueued.

walk

public void walk(NonRecursive walker,
                 AnnotatedTerm annot)

Specified by:

walk in class NonRecursive.TermWalker

walk

public void walk(NonRecursive walker,
                 ApplicationTerm term)

Specified by:

walk in class NonRecursive.TermWalker

walk

public void walk(NonRecursive walker,
                 ConstantTerm term)

Specified by:

walk in class NonRecursive.TermWalker

walk

public void walk(NonRecursive walker,
                 LetTerm letTerm)

Specified by:

walk in class NonRecursive.TermWalker

walk

public void walk(NonRecursive walker,
                 QuantifiedFormula quant)

Specified by:

walk in class NonRecursive.TermWalker

walk

public void walk(NonRecursive walker,
                 TermVariable term)

Specified by:

walk in class NonRecursive.TermWalker