protected class PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy extends AbstractFeatureStrategy
Constructor and Description |
---|
RemovePostStrategy(Proof proof) |
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
computeCost(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal)
Evaluate the cost of a
RuleApp . |
private java.lang.String |
getAppRuleName(Node parent) |
protected RuleAppCost |
instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal) |
boolean |
isApprovedApp(RuleApp app,
PosInOccurrence pio,
Goal goal)
Re-Evaluate a
RuleApp . |
boolean |
isStopAtFirstNonCloseableGoal()
|
Name |
name()
returns the name of this element
|
bindRuleSet, bindRuleSet, bindRuleSet, bindRuleSet, clearRuleSetBindings, clearRuleSetBindings, disableInstantiate, enableInstantiate, forEach, getFilterFor, getHeuristic, getProof, ifHeuristics, ifHeuristics, ifHeuristics, instantiate, instantiate, instantiateApp, instantiateTriggeredVariable, oneOf, oneOf
add, add, add, add, add, any, applyTF, applyTF, applyTFNonStrict, applyTFNonStrict, atomSmallerThan, blockContractExternalFeature, blockContractInternalFeature, c, contains, countOccurrences, eq, eq, eq, extendsTrans, ifZero, ifZero, ifZero, ifZero, implicitCastNecessary, inftyConst, inftyTermConst, instOf, instOfNonStrict, instOfTriggerVariable, isInstantiated, isSubSortFeature, isTriggerVariableInstantiated, leq, less, let, literalsSmallerThan, longConst, longTermConst, loopContractApplyHead, loopContractExternalFeature, loopContractInternalFeature, loopInvFeature, mergeRuleFeature, methodSpecFeature, monSmallerThan, not, not, op, opSub, opSub, opTerm, opTerm, opTerm, or, or, or, or, or, println, querySpecFeature, rec, sequentContainsNoPrograms, sub, sub, sub, subAt, sum, termSmallerThan
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
updateStrategySettings
private final Name NAME
public RemovePostStrategy(Proof proof)
public Name name()
Named
public RuleAppCost computeCost(RuleApp ruleApp, PosInOccurrence pio, Goal goal)
Feature
RuleApp
.ruleApp
- the RuleApppio
- position where app
is to be appliedgoal
- the goal on which app
is to be appliedRuleAppCost
object. TopRuleAppCost.INSTANCE
indicates that the rule shall not be applied at all (it is discarded by
the strategy).public boolean isApprovedApp(RuleApp app, PosInOccurrence pio, Goal goal)
Strategy
RuleApp
. This method is
called immediately before a rule is really appliedprivate java.lang.String getAppRuleName(Node parent)
protected RuleAppCost instantiateApp(RuleApp app, PosInOccurrence pio, Goal goal)
instantiateApp
in class AbstractFeatureStrategy