de.uka.ilkd.key.strategy

Class NoFindTacletAppContainer

java.lang.Object

de.uka.ilkd.key.strategy.RuleAppContainer

de.uka.ilkd.key.strategy.TacletAppContainer

de.uka.ilkd.key.strategy.NoFindTacletAppContainer

All Implemented Interfaces:

java.lang.Comparable<RuleAppContainer>

public class NoFindTacletAppContainer
extends TacletAppContainer

Instances of this class are immutable

Constructor Summary

Constructors

Constructor and Description
NoFindTacletAppContainer(NoPosTacletApp p_app, RuleAppCost p_cost, long p_age)

Method Summary

Modifier and Type	Method and Description
protected boolean	isStillApplicable(Goal p_goal)

Methods inherited from class de.uka.ilkd.key.strategy.TacletAppContainer

completeRuleApp, createAppContainers, createAppContainers, createContainer, createFurtherApps, createInitialAppContainers, getAge, getPosInOccurrence, getTacletApp, ifFormulasStillValid

Methods inherited from class de.uka.ilkd.key.strategy.RuleAppContainer

compareTo, createAppContainer, createAppContainers, getCost, getRuleApp

Methods inherited from class java.lang.Object

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

Constructor Detail

NoFindTacletAppContainer

NoFindTacletAppContainer(NoPosTacletApp p_app,
                         RuleAppCost p_cost,
                         long p_age)

Method Detail

isStillApplicable

protected boolean isStillApplicable(Goal p_goal)

Specified by:

isStillApplicable in class TacletAppContainer

Returns:

true iff the stored rule app is applicable for the given sequent, i.e. always true since NoFindTaclets are not bound to a find-position (if-formulas are not considered)