de.uka.ilkd.key.rule

Class TacletVariableSVCollector

java.lang.Object

de.uka.ilkd.key.logic.DefaultVisitor

de.uka.ilkd.key.rule.TacletSchemaVariableCollector

de.uka.ilkd.key.rule.TacletVariableSVCollector

All Implemented Interfaces:

Visitor

public class TacletVariableSVCollector
extends TacletSchemaVariableCollector

This class is used to collect all appearing SchemaVariables that are bound in a Taclet. Duplicates are not removed becaues the use of persistent datastructure and up to now we just have a SetAsList-implementaion causing to have O(sqr(n)) if it would used. The class is used by RuleApps to compute all non-instantiated variables.

Field Summary

Fields inherited from class de.uka.ilkd.key.rule.TacletSchemaVariableCollector

varList

Constructor Summary

Constructors

Constructor and Description
TacletVariableSVCollector()

Method Summary

Modifier and Type	Method and Description
void	visit(Term t) visits term t in post order (Term.execPostOrder(de.uka.ilkd.key.logic.Visitor)) and collects all bound schema variables

Methods inherited from class de.uka.ilkd.key.rule.TacletSchemaVariableCollector

collectSVInProgram, contains, size, varIterator, vars, visit, visit, visitFindPart, visitGoalTemplates, visitWithoutAddrule

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

Constructor Detail

TacletVariableSVCollector

public TacletVariableSVCollector()

Method Detail

visit

public void visit(Term t)

visits term t in post order (Term.execPostOrder(de.uka.ilkd.key.logic.Visitor)) and collects all bound schema variables

Specified by:

visit in interface Visitor

Overrides:

visit in class TacletSchemaVariableCollector

Parameters:

t - the Term to be visited (t must not be null