public class ConstraintAwareSyntacticalReplaceVisitor extends SyntacticalReplaceVisitor
applicationPosInOccurrence, goal, labelHint, rule, ruleApp, services, SUBSTITUTION_WITH_LABELS_HINT, svInst, tb, termLabelState
Constructor and Description |
---|
ConstraintAwareSyntacticalReplaceVisitor(TermLabelState termLabelState,
Services services,
Constraint metavariableInst,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Taclet.TacletLabelHint labelHint,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
protected Term |
toTerm(Term t)
the method is only still invoked to allow the
ConstraintAwareSyntacticalReplaceVisitor
to recursively replace meta variables |
void |
visited(Term visited) |
getSVInstantiations, getTerm, pushNew, subtreeEntered, subtreeLeft, visit
visitSubtree
public ConstraintAwareSyntacticalReplaceVisitor(TermLabelState termLabelState, Services services, Constraint metavariableInst, PosInOccurrence applicationPosInOccurrence, Rule rule, RuleApp ruleApp, Taclet.TacletLabelHint labelHint, Goal goal)
protected Term toTerm(Term t)
SyntacticalReplaceVisitor
ConstraintAwareSyntacticalReplaceVisitor
to recursively replace meta variablestoTerm
in class SyntacticalReplaceVisitor
public void visited(Term visited)
Copyright © 2003-2019 The KeY-Project.