public class SVNameCorrespondenceCollector extends DefaultVisitor
Modifier and Type | Method and Description |
---|---|
ImmutableMap<SchemaVariable,SchemaVariable> |
getCorrespondences() |
void |
visit(Sequent seq)
collects all correspondences in a sequent
|
void |
visit(Taclet taclet,
boolean visitAddrules)
collects all correspondences in a taclet
|
void |
visit(Term t)
is called by the execPostOrder-method of a term
|
subtreeEntered, subtreeLeft, visitSubtree
public void visit(Term t)
t
- the Term if the toplevel operator of this term is a
substitution of schema variables, then this pair is added to
the map "nameCorrespondences"public ImmutableMap<SchemaVariable,SchemaVariable> getCorrespondences()
public void visit(Sequent seq)
seq
- the Sequent to visitpublic void visit(Taclet taclet, boolean visitAddrules)
taclet
- the Taclet where the correspondences have to be
collectedvisitAddrules
- a boolean that contols if the addrule sections are
to be ignored (iff false) or if the visitor descends into them (iff true)Copyright © 2003-2019 The KeY-Project.