Package | Description |
---|---|
de.uka.ilkd.key.informationflow.macros | |
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.macros | |
de.uka.ilkd.key.strategy |
This package contains classes implementing the proof search strategies of KeY.
|
de.uka.ilkd.key.strategy.feature | |
de.uka.ilkd.key.strategy.feature.instantiator | |
de.uka.ilkd.key.strategy.quantifierHeuristics | |
de.uka.ilkd.key.strategy.termfeature |
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
UseInformationFlowContractMacro.PropExpansionStrategy.computeCost(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
LRUCache<PosInOccurrence,RuleAppCost> |
ServiceCaches.getIfThenElseMalusCache() |
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
FilterStrategy.computeCost(RuleApp app,
PosInOccurrence pio,
Goal goal) |
RuleAppCost |
PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy.computeCost(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal) |
protected RuleAppCost |
PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal) |
Modifier and Type | Class and Description |
---|---|
class |
NumberRuleAppCost |
class |
TopRuleAppCost
Singleton implementation of the
RuleAppCost interface, which
denotes a maximum cost (rule applications with this cost can't be afforded
at all) |
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
NumberRuleAppCost.add(NumberRuleAppCost cost2) |
RuleAppCost |
RuleAppCost.add(RuleAppCost cost2)
Add the given costs to the costs that are represented by this object
|
RuleAppCost |
NumberRuleAppCost.add(RuleAppCost cost2) |
RuleAppCost |
TopRuleAppCost.add(RuleAppCost cost2) |
protected static RuleAppCost |
StaticFeatureCollection.c(long p) |
RuleAppCost |
SimpleFilteredStrategy.computeCost(RuleApp app,
PosInOccurrence pio,
Goal goal)
Evaluate the cost of a
RuleApp . |
RuleAppCost |
FIFOStrategy.computeCost(RuleApp app,
PosInOccurrence pio,
Goal goal)
Evaluate the cost of a
RuleApp . |
RuleAppCost |
IsInRangeProvable.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
JavaCardDLStrategy.computeCost(RuleApp app,
PosInOccurrence pio,
Goal goal)
Evaluate the cost of a
RuleApp . |
static RuleAppCost |
NumberRuleAppCost.create(int p_cost) |
static RuleAppCost |
NumberRuleAppCost.create(long p_cost) |
RuleAppCost |
RuleAppContainer.getCost() |
static RuleAppCost |
NumberRuleAppCost.getZeroCost() |
protected abstract RuleAppCost |
AbstractFeatureStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal) |
protected RuleAppCost |
JavaCardDLStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
RuleAppCost.add(RuleAppCost cost2)
Add the given costs to the costs that are represented by this object
|
RuleAppCost |
NumberRuleAppCost.add(RuleAppCost cost2) |
RuleAppCost |
TopRuleAppCost.add(RuleAppCost cost2) |
void |
RuleAppCostCollector.collect(RuleApp app,
RuleAppCost cost) |
int |
RuleAppCost.compareTo(RuleAppCost o) |
int |
NumberRuleAppCost.compareTo(RuleAppCost o) |
int |
TopRuleAppCost.compareTo(RuleAppCost o) |
Constructor and Description |
---|
RuleAppContainer(RuleApp p_app,
RuleAppCost p_cost) |
TacletAppContainer(RuleApp p_app,
RuleAppCost p_cost,
long p_age) |
Modifier and Type | Field and Description |
---|---|
static RuleAppCost |
BinaryFeature.TOP_COST
Constant that represents the boolean value false
|
static RuleAppCost |
ContainsTermFeature.TOP_COST
Constant that represents the boolean value false
|
static RuleAppCost |
QueryExpandCost.TOP_COST
Constant that represents the boolean value false
|
static RuleAppCost |
BinaryFeature.ZERO_COST
Constant that represents the boolean value true
|
static RuleAppCost |
ContainsTermFeature.ZERO_COST
Constant that represents the boolean value true
|
static RuleAppCost |
QueryExpandCost.ZERO_COST
Constant that represents the boolean value true
|
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
CountBranchFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal)
Compute the cost of a RuleApp.
|
RuleAppCost |
AgeFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
BinaryFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
ConstFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
FocusIsSubFormulaOfInfFlowContractAppFeature.computeCost(RuleApp ruleApp,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
LetFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
IfThenElseMalusFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
FindDepthFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
ComprehendedSumFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
PrintFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
SimplifyReplaceKnownCandidateFeature.computeCost(RuleApp ruleApp,
PosInOccurrence pos,
Goal goal)
Compute the cost of a RuleApp.
|
RuleAppCost |
Feature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal)
Evaluate the cost of a
RuleApp . |
RuleAppCost |
ShannonFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
RuleSetDispatchFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
ContainsTermFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
SumFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
FindRightishFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
DeleteMergePointRuleFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
ConditionalFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
MergeRuleFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
AbstractBetaFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal)
Compute the cost of a RuleApp.
|
RuleAppCost |
InfFlowContractAppFeature.computeCost(RuleApp ruleApp,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
QueryExpandCost.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
ApplyTFFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected RuleAppCost |
ContainsQuantifierFeature.doComputation(PosInOccurrence pos,
Term findTerm,
ServiceCaches caches) |
protected RuleAppCost |
PurePosDPathFeature.doComputation(PosInOccurrence pos,
Term findTerm,
ServiceCaches caches) |
protected RuleAppCost |
CountMaxDPathFeature.doComputation(PosInOccurrence pos,
Term findTerm,
ServiceCaches caches) |
protected RuleAppCost |
LeftmostNegAtomFeature.doComputation(PosInOccurrence pos,
Term findTerm,
ServiceCaches caches) |
protected RuleAppCost |
SimplifyBetaCandidateFeature.doComputation(PosInOccurrence pos,
Term findTerm,
ServiceCaches caches) |
protected RuleAppCost |
CountPosDPathFeature.doComputation(PosInOccurrence pos,
Term findTerm,
ServiceCaches caches) |
protected abstract RuleAppCost |
AbstractBetaFeature.doComputation(PosInOccurrence pos,
Term findTerm,
ServiceCaches caches) |
RuleAppCost |
ConstFeature.getValue() |
Modifier and Type | Method and Description |
---|---|
static Feature |
ScaleFeature.createAffine(Feature f,
RuleAppCost dom0,
RuleAppCost dom1,
RuleAppCost img0,
RuleAppCost img1)
Create a feature that applies an affine transformation to the result of
the base feature.
|
static Feature |
ShannonFeature.createConditional(Feature cond,
RuleAppCost trueCost,
Feature thenFeature) |
static Feature |
ShannonFeature.createConditional(Feature cond,
RuleAppCost trueCost,
Feature thenFeature,
Feature elseFeature) |
static Feature |
ShannonFeature.createConditional(Feature cond,
RuleAppCost trueCost,
Feature thenFeature,
RuleAppCost elseValue) |
static Feature |
ShannonFeature.createConditional(Feature cond,
RuleAppCost trueCost,
RuleAppCost thenValue) |
static Feature |
ShannonFeature.createConditional(Feature cond,
RuleAppCost trueCost,
RuleAppCost thenValue,
RuleAppCost elseValue) |
static Feature |
ConditionalFeature.createConditional(RuleFilter cond,
Feature thenFeature,
RuleAppCost elseValue) |
static Feature |
ConditionalFeature.createConditional(RuleFilter cond,
RuleAppCost thenValue) |
static Feature |
ConditionalFeature.createConditional(RuleFilter cond,
RuleAppCost thenValue,
RuleAppCost elseValue) |
static Feature |
ShannonFeature.createConditionalBinary(Feature cond,
Feature thenFeature,
RuleAppCost elseValue) |
static Feature |
ShannonFeature.createConditionalBinary(Feature cond,
RuleAppCost thenValue) |
static Feature |
ShannonFeature.createConditionalBinary(Feature cond,
RuleAppCost thenValue,
RuleAppCost elseValue) |
static Feature |
ConstFeature.createConst(RuleAppCost p_val) |
static Feature |
ApplyTFFeature.createNonStrict(ProjectionToTerm proj,
TermFeature tf,
RuleAppCost noInstCost) |
protected static void |
ScaleFeature.illegalCostError(RuleAppCost cost) |
static Feature |
ScaleFeature.realAffine(Feature f,
RuleAppCost dom0,
RuleAppCost dom1,
RuleAppCost img0,
RuleAppCost img1) |
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
ForEachCP.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
OneOfCP.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
SVInstantiationCP.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
InstantiationCostScalerFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
InstantiationCost.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal)
Compute the cost of a RuleApp.
|
Modifier and Type | Field and Description |
---|---|
static RuleAppCost |
BinaryTermFeature.TOP_COST
Constant that represents the boolean value false
|
static RuleAppCost |
BinaryTermFeature.ZERO_COST
Constant that represents the boolean value true
|
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
SubTermFeature.compute(Term term,
Services services) |
RuleAppCost |
BinarySumTermFeature.compute(Term term,
Services services) |
RuleAppCost |
RecSubTermFeature.compute(Term term,
Services services) |
RuleAppCost |
ConstTermFeature.compute(Term term,
Services services) |
RuleAppCost |
ShannonTermFeature.compute(Term term,
Services services) |
RuleAppCost |
BinaryTermFeature.compute(Term term,
Services services) |
RuleAppCost |
PrintTermFeature.compute(Term term,
Services services) |
RuleAppCost |
TermFeature.compute(Term term,
Services services) |
Modifier and Type | Method and Description |
---|---|
static TermFeature |
SubTermFeature.create(TermFeature[] fs,
RuleAppCost arityMismatchCost) |
static TermFeature |
ConstTermFeature.createConst(RuleAppCost p_val) |
Copyright © 2003-2019 The KeY-Project.