| java.lang.Object
 de.uka.ilkd.key.strategy.AbstractFeatureStrategy
All known Subclasses: de.uka.ilkd.key.strategy.SimplificationOfOCLStrategy, de.uka.ilkd.key.strategy.JavaCardDLStrategy, de.uka.ilkd.key.strategy.FOLStrategy,
| AbstractFeatureStrategy | | abstract public class AbstractFeatureStrategy implements Strategy(Code) | | |
| Method Summary | |
| protected Feature | add(Feature a, Feature b)
| | protected Feature | add(Feature a, Feature b, Feature c)
| | protected TermFeature | add(TermFeature a, TermFeature b)
| | protected TermFeature | add(TermFeature a, TermFeature b, TermFeature c)
| | protected TermFeature | any()
| | protected Feature | applyTF(String schemaVar, TermFeature tf)
Invoke the term feature tf on the term that instantiation
of schemaVar. | | protected Feature | applyTF(ProjectionToTerm term, TermFeature tf)
Evaluate the term feature tf for the term described by the
projection term. | | protected Feature | applyTFNonStrict(String schemaVar, TermFeature tf)
Invoke the term feature tf on the term that instantiation
of schemaVar. | | protected Feature | applyTFNonStrict(ProjectionToTerm term, TermFeature tf)
Evaluate the term feature tf for the term described by the
projection term. | | protected void | bindRuleSet(RuleSetDispatchFeature d, RuleSet ruleSet, Feature f)
| | protected void | bindRuleSet(RuleSetDispatchFeature d, RuleSet ruleSet, long cost)
| | protected void | bindRuleSet(RuleSetDispatchFeature d, String ruleSet, Feature f)
| | protected void | bindRuleSet(RuleSetDispatchFeature d, String ruleSet, long cost)
| | protected void | clearRuleSetBindings(RuleSetDispatchFeature d, RuleSet ruleSet)
| | protected void | clearRuleSetBindings(RuleSetDispatchFeature d, String ruleSet)
| | protected Feature | contains(ProjectionToTerm bigTerm, ProjectionToTerm searchedTerm)
| | protected void | disableInstantiate()
| | protected void | enableInstantiate()
| | protected Feature | eq(Feature a, Feature b)
| | protected TermFeature | eq(TermBuffer t)
| | protected Feature | eq(ProjectionToTerm t1, ProjectionToTerm t2)
| | protected TermFeature | extendsTrans(Sort s)
| | protected Feature | forEach(TermBuffer x, TermGenerator gen, Feature body)
| | protected BackTrackingManager | getBtManager()
| | protected TacletFilter | getFilterFor(String[] p_names)
| | protected RuleSet | getHeuristic(String p_name)
| | protected Proof | getProof()
| | protected Feature | ifHeuristics(String[] heuristics, Feature thenFeature)
| | protected Feature | ifHeuristics(String[] heuristics, Feature thenFeature, Feature elseFeature)
| | protected Feature | ifHeuristics(String[] names, int priority)
| | protected Feature | ifZero(Feature cond, Feature thenFeature)
| | protected Feature | ifZero(Feature cond, Feature thenFeature, Feature elseFeature)
| | protected TermFeature | ifZero(TermFeature cond, TermFeature thenFeature)
| | protected TermFeature | ifZero(TermFeature cond, TermFeature thenFeature, TermFeature elseFeature)
| | protected Feature | implicitCastNecessary(ProjectionToTerm s1)
| | protected Feature | inftyConst()
| | protected TermFeature | inftyTermConst()
| | protected ProjectionToTerm | instOf(String schemaVar)
Create a projection of taclet applications to the instantiation of the
schema variables schemaVar. | | protected ProjectionToTerm | instOfNonStrict(String schemaVar)
Create a projection of taclet applications to the instantiation of the
schema variables schemaVar. | | protected Feature | instantiate(Name sv, ProjectionToTerm value)
| | protected Feature | instantiate(String sv, ProjectionToTerm value)
| | final public void | instantiateApp(RuleApp app, PosInOccurrence pio, Goal goal, RuleAppCostCollector collector)
| | abstract protected RuleAppCost | instantiateApp(RuleApp app, PosInOccurrence pio, Goal goal)
| | protected Feature | isInstantiated(String schemaVar)
| | protected Feature | isSubSortFeature(ProjectionToTerm s1, ProjectionToTerm s2)
| | protected Feature | leq(Feature a, Feature b)
| | protected Feature | less(Feature a, Feature b)
| | protected Feature | let(TermBuffer x, ProjectionToTerm value, Feature body)
| | protected Feature | longConst(long a)
| | protected TermFeature | longTermConst(long a)
| | protected Feature | not(Feature f)
| | protected TermFeature | not(TermFeature f)
| | protected Feature | oneOf(Feature[] features)
| | protected Feature | oneOf(Feature feature0, Feature feature1)
| | protected TermFeature | op(Operator op)
| | protected TermFeature | opSub(Operator op, TermFeature sub0)
| | protected TermFeature | opSub(Operator op, TermFeature sub0, TermFeature sub1)
| | protected ProjectionToTerm | opTerm(Operator op, ProjectionToTerm[] subTerms)
| | protected ProjectionToTerm | opTerm(Operator op, ProjectionToTerm subTerm)
| | protected ProjectionToTerm | opTerm(Operator op, ProjectionToTerm subTerm0, ProjectionToTerm subTerm1)
| | protected TermFeature | or(TermFeature a, TermFeature b)
| | protected TermFeature | or(TermFeature a, TermFeature b, TermFeature c)
| | protected Feature | or(Feature a, Feature b)
| | protected Feature | or(Feature a, Feature b, Feature c)
| | protected Feature | println(ProjectionToTerm t)
| | protected TermFeature | rec(TermFeature cond, TermFeature summand)
| | protected Feature | selectSimplifier(long priority)
| | protected ProjectionToTerm | sub(ProjectionToTerm t, int index)
| | protected TermFeature | sub(TermFeature sub0)
| | protected TermFeature | sub(TermFeature sub0, TermFeature sub1)
| | protected ProjectionToTerm | subAt(ProjectionToTerm t, PosInTerm pit)
| | protected Feature | sum(TermBuffer x, TermGenerator gen, Feature body)
|
| AbstractFeatureStrategy | | protected AbstractFeatureStrategy(Proof proof)(Code) | | |
| applyTF | | protected Feature applyTF(String schemaVar, TermFeature tf)(Code) | | Invoke the term feature tf on the term that instantiation
of schemaVar. This is the strict/safe version that raises an
error of schemaVar is not instantiated for a particular
taclet app
|
| applyTF | | protected Feature applyTF(ProjectionToTerm term, TermFeature tf)(Code) | | Evaluate the term feature tf for the term described by the
projection term. If term is undefined for
a particular rule app, an exception is raised
|
| applyTFNonStrict | | protected Feature applyTFNonStrict(String schemaVar, TermFeature tf)(Code) | | Invoke the term feature tf on the term that instantiation
of schemaVar. This is the non-strict/unsafe version that
simply returns zero if schemaVar is not instantiated for a
particular taclet app
|
| applyTFNonStrict | | protected Feature applyTFNonStrict(ProjectionToTerm term, TermFeature tf)(Code) | | Evaluate the term feature tf for the term described by the
projection term. If term is undefined for
a particular rule app, zero is returned
|
| disableInstantiate | | protected void disableInstantiate()(Code) | | |
| enableInstantiate | | protected void enableInstantiate()(Code) | | |
| getProof | | protected Proof getProof()(Code) | | Returns the proof. |
| ifHeuristics | | protected Feature ifHeuristics(String[] heuristics, Feature thenFeature)(Code) | |
Parameters:
heuristics -
Parameters:
thenFeature - |
| ifHeuristics | | protected Feature ifHeuristics(String[] heuristics, Feature thenFeature, Feature elseFeature)(Code) | |
Parameters:
heuristics -
Parameters:
thenFeature -
Parameters:
elseFeature - |
| ifHeuristics | | protected Feature ifHeuristics(String[] names, int priority)(Code) | |
Parameters:
names -
Parameters:
priority - |
| instOf | | protected ProjectionToTerm instOf(String schemaVar)(Code) | | Create a projection of taclet applications to the instantiation of the
schema variables schemaVar. If schemaVar
is not instantiated for a particular taclet app, an error will be raised
|
| instOfNonStrict | | protected ProjectionToTerm instOfNonStrict(String schemaVar)(Code) | | Create a projection of taclet applications to the instantiation of the
schema variables schemaVar. The projection will be
partial and undefined for those taclet applications that do not
instantiate schemaVar
|
| selectSimplifier | | protected Feature selectSimplifier(long priority)(Code) | |
Parameters:
priority - |
|
|