de.uka.ilkd.key.logic

Class BoundVarsVisitor

java.lang.Object

de.uka.ilkd.key.logic.DefaultVisitor

de.uka.ilkd.key.logic.BoundVarsVisitor

All Implemented Interfaces:

Visitor

public class BoundVarsVisitor
extends DefaultVisitor

Visitor traversing a term and collecting all variables that occur bound. The visitor implements also a continuation on sequents, traversing all of the formulas occuring in the sequent.

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableSet<QuantifiableVariable>	bdVars

Constructor Summary

Constructors

Constructor and Description
BoundVarsVisitor() creates a Visitor that collects all bound variables for the subterms of the term it is called from.

Method Summary

Modifier and Type	Method and Description
ImmutableSet<QuantifiableVariable>	getBoundVariables() returns all the bound variables that have been stored
void	visit(Sequent visited) visits a sequent
void	visit(Term visited) only called by execPostOrder in Term.

Methods inherited from class de.uka.ilkd.key.logic.DefaultVisitor

subtreeEntered, subtreeLeft, visitSubtree

Methods inherited from class java.lang.Object

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

Field Detail

bdVars

private ImmutableSet<QuantifiableVariable> bdVars

Constructor Detail

BoundVarsVisitor

public BoundVarsVisitor()

creates a Visitor that collects all bound variables for the subterms of the term it is called from.

Method Detail

visit

public void visit(Term visited)

only called by execPostOrder in Term.

Parameters:

visited - the Term to be visited

visit

public void visit(Sequent visited)

visits a sequent

getBoundVariables

public ImmutableSet<QuantifiableVariable> getBoundVariables()

returns all the bound variables that have been stored