| java.lang.Object
 de.uka.ilkd.key.logic.Visitor
de.uka.ilkd.key.rule.SVNameCorrespondenceCollector
| SVNameCorrespondenceCollector | | public class SVNameCorrespondenceCollector extends Visitor (Code) | | This visitor is used to collect information about schema variable
pairs occurring within the same substitution operator within a
taclet. This information is used to choose names of metavariables
or skolem functions.
|
| getCorrespondences | | public MapFromSchemaVariableToSchemaVariable getCorrespondences()(Code) | | the found correspondences as a map, mapping schema variable aonto schema variables b if b is replaced with a somewhere in thistaclet |
| visit | | public void visit(Term t)(Code) | | is called by the execPostOrder-method of a term
Parameters:
Term - if the toplevel operator of this term is asubstitution of schema variables, then this pair is added tothe map "nameCorrespondences" |
| visit | | public void visit(Sequent seq)(Code) | | collects all correspondences in a sequent
Parameters:
seq - the Sequent to visit |
| visit | | public void visit(Taclet taclet, boolean visitAddrules)(Code) | | collects all correspondences in a taclet
Parameters:
taclet - the Taclet where the correspondences have to becollected
Parameters:
visitAddRules - a boolean that contols if the addrule sections areto be ignored (iff false) or if the visitor descends into them (iff true) |
|
|