de.uka.ilkd.key.strategy.quantifierHeuristics

Class ConstraintAwareSyntacticalReplaceVisitor

java.lang.Object

de.uka.ilkd.key.logic.DefaultVisitor

de.uka.ilkd.key.rule.SyntacticalReplaceVisitor

de.uka.ilkd.key.strategy.quantifierHeuristics.ConstraintAwareSyntacticalReplaceVisitor

All Implemented Interfaces:

Visitor

public class ConstraintAwareSyntacticalReplaceVisitor
extends SyntacticalReplaceVisitor

In KeY 1.x we supported a free variable calculus based on meta variables. This feature has been abandoned in KeY 2.0. Until the strategy for quantifier instantiations is adapted, we cannot get rid of them completely (they are used to determine triggers).

Field Summary

Fields

Modifier and Type	Field and Description
private Constraint	metavariableInst Deprecated.

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

applicationPosInOccurrence, goal, labelHint, rule, ruleApp, services, SUBSTITUTION_WITH_LABELS_HINT, svInst, tb, termLabelState

Constructor Summary

Constructors

Constructor and Description
ConstraintAwareSyntacticalReplaceVisitor(TermLabelState termLabelState, Services services, Constraint metavariableInst, PosInOccurrence applicationPosInOccurrence, Rule rule, RuleApp ruleApp, Taclet.TacletLabelHint labelHint, Goal goal)

Method Summary

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)

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

getSVInstantiations, getTerm, pushNew, subtreeEntered, subtreeLeft, visit

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

visitSubtree

Methods inherited from class java.lang.Object

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

Field Detail

metavariableInst

@Deprecated
private final Constraint metavariableInst

Deprecated.

Constructor Detail

ConstraintAwareSyntacticalReplaceVisitor

public ConstraintAwareSyntacticalReplaceVisitor(TermLabelState termLabelState,
                                                Services services,
                                                Constraint metavariableInst,
                                                PosInOccurrence applicationPosInOccurrence,
                                                Rule rule,
                                                RuleApp ruleApp,
                                                Taclet.TacletLabelHint labelHint,
                                                Goal goal)

Method Detail

toTerm

protected Term toTerm(Term t)

Description copied from class: SyntacticalReplaceVisitor

the method is only still invoked to allow the ConstraintAwareSyntacticalReplaceVisitor to recursively replace meta variables

Overrides:

toTerm in class SyntacticalReplaceVisitor

visited

public void visited(Term visited)