public class JavaCardDLStrategy extends AbstractFeatureStrategy
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
JAVA_CARD_DL_STRATEGY |
protected StrategyProperties |
strategyProperties |
Modifier | Constructor and Description |
---|---|
protected |
JavaCardDLStrategy(Proof proof,
StrategyProperties strategyProperties) |
Modifier and Type | Method and Description |
---|---|
protected boolean |
arithDefOps() |
RuleAppCost |
computeCost(RuleApp app,
PosInOccurrence pio,
Goal goal)
Evaluate the cost of a
RuleApp . |
protected RuleSetDispatchFeature |
getCostComputationDispatcher() |
protected RuleSetDispatchFeature |
getInstantiationDispatcher() |
protected Services |
getServices() |
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
|
protected Feature |
setupApprovalF() |
protected Feature |
setupGlobalF(Feature dispatcher) |
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
public static final java.lang.String JAVA_CARD_DL_STRATEGY
protected final StrategyProperties strategyProperties
protected JavaCardDLStrategy(Proof proof, StrategyProperties strategyProperties)
protected final RuleSetDispatchFeature getCostComputationDispatcher()
protected final RuleSetDispatchFeature getInstantiationDispatcher()
protected boolean arithDefOps()
protected final Services getServices()
protected Feature setupApprovalF()
public Name name()
Named
public RuleAppCost computeCost(RuleApp app, PosInOccurrence pio, Goal goal)
RuleApp
.app
- rule applicationpio
- corresponding PosInOccurrence
goal
- corresponding goalRuleAppCost
object.
TopRuleAppCost.INSTANCE
indicates that the rule
shall not be applied at all (it is discarded by the strategy).public final boolean isApprovedApp(RuleApp app, PosInOccurrence pio, Goal goal)
RuleApp
. This method is called immediately
before a rule is really appliedapp
- the rule applicationpio
- the position in occurrencegoal
- the goalprotected RuleAppCost instantiateApp(RuleApp app, PosInOccurrence pio, Goal goal)
instantiateApp
in class AbstractFeatureStrategy
Copyright © 2003-2019 The KeY-Project.