Package | Description |
---|---|
de.uka.ilkd.key.informationflow.macros | |
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.findprefix | |
de.uka.ilkd.key.strategy.feature.instantiator | |
de.uka.ilkd.key.strategy.quantifierHeuristics | |
de.uka.ilkd.key.strategy.termfeature | |
de.uka.ilkd.key.symbolic_execution.strategy |
Modifier and Type | Class and Description |
---|---|
protected class |
UseInformationFlowContractMacro.PropExpansionStrategy
This strategy accepts all rule apps for which the rule name starts with a
string in the admitted set and rejects everything else.
|
Modifier and Type | Class and Description |
---|---|
class |
FilterStrategy |
protected class |
PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy
This strategy accepts all rule apps for which the rule name starts with a
string in the admitted set and rejects everything else.
|
Modifier and Type | Interface and Description |
---|---|
interface |
Strategy
Generic interface for evaluating the cost of
a RuleApp with regard to a specific strategy
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractFeatureStrategy |
class |
FIFOStrategy
Trivial implementation of the Strategy interface
that uses only the goal time to determine the cost
of a RuleApp.
|
class |
IntroducedSymbolBy |
class |
IsInRangeProvable
Feature used to check if the value of a given term with
moduloXXX
(with XXX being Long, Int, etc.) is in the range of Long, Integer etc. |
class |
JavaCardDLStrategy
Strategy tailored to be used as long as a java program can be found in the
sequent.
|
class |
SimpleFilteredStrategy
Trivial implementation of the Strategy interface
that uses only the goal time to determine the cost
of a RuleApp.
|
Modifier and Type | Method and Description |
---|---|
protected static Feature |
StaticFeatureCollection.add(Feature... features) |
protected static Feature |
StaticFeatureCollection.add(Feature a,
Feature b) |
protected static Feature |
StaticFeatureCollection.add(Feature a,
Feature b,
Feature c) |
protected static Feature |
StaticFeatureCollection.applyTF(ProjectionToTerm term,
TermFeature tf)
Evaluate the term feature
tf for the term described by the projection
term . |
protected static Feature |
StaticFeatureCollection.applyTF(java.lang.String schemaVar,
TermFeature tf)
Invoke the term feature
tf on the term that instantiation of
schemaVar . |
protected static Feature |
StaticFeatureCollection.applyTFNonStrict(ProjectionToTerm term,
TermFeature tf)
Evaluate the term feature
tf for the term described by the projection
term . |
protected static Feature |
StaticFeatureCollection.applyTFNonStrict(java.lang.String schemaVar,
TermFeature tf)
Invoke the term feature
tf on the term that instantiation of
schemaVar . |
protected static Feature |
StaticFeatureCollection.atomSmallerThan(java.lang.String smaller,
java.lang.String bigger,
IntegerLDT numbers) |
protected static Feature |
StaticFeatureCollection.blockContractExternalFeature(Feature cost) |
protected static Feature |
StaticFeatureCollection.blockContractInternalFeature(Feature cost) |
protected static Feature |
StaticFeatureCollection.contains(ProjectionToTerm bigTerm,
ProjectionToTerm searchedTerm) |
protected static Feature |
StaticFeatureCollection.countOccurrences(ProjectionToTerm cutFormula) |
static Feature |
IntroducedSymbolBy.create(ProjectionToTerm termWithTopLevelOpToCheck,
java.lang.String ruleSetName,
java.lang.String schemaVar) |
protected static Feature |
StaticFeatureCollection.eq(Feature a,
Feature b) |
protected static Feature |
StaticFeatureCollection.eq(ProjectionToTerm t1,
ProjectionToTerm t2) |
protected Feature |
AbstractFeatureStrategy.forEach(TermBuffer x,
TermGenerator gen,
Feature body) |
protected Feature |
AbstractFeatureStrategy.ifHeuristics(java.lang.String[] heuristics,
Feature thenFeature) |
protected Feature |
AbstractFeatureStrategy.ifHeuristics(java.lang.String[] heuristics,
Feature thenFeature,
Feature elseFeature) |
protected Feature |
AbstractFeatureStrategy.ifHeuristics(java.lang.String[] names,
int priority) |
protected static Feature |
StaticFeatureCollection.ifZero(Feature cond,
Feature thenFeature) |
protected static Feature |
StaticFeatureCollection.ifZero(Feature cond,
Feature thenFeature,
Feature elseFeature) |
protected static Feature |
StaticFeatureCollection.implicitCastNecessary(ProjectionToTerm s1) |
protected static Feature |
StaticFeatureCollection.inftyConst() |
protected Feature |
AbstractFeatureStrategy.instantiate(Name sv,
ProjectionToTerm value) |
protected Feature |
AbstractFeatureStrategy.instantiate(java.lang.String sv,
ProjectionToTerm value) |
protected Feature |
AbstractFeatureStrategy.instantiateTriggeredVariable(ProjectionToTerm value) |
protected static Feature |
StaticFeatureCollection.isInstantiated(java.lang.String schemaVar) |
protected static Feature |
StaticFeatureCollection.isSubSortFeature(ProjectionToTerm s1,
ProjectionToTerm s2) |
protected static Feature |
StaticFeatureCollection.isTriggerVariableInstantiated() |
protected static Feature |
StaticFeatureCollection.leq(Feature a,
Feature b) |
protected static Feature |
StaticFeatureCollection.less(Feature a,
Feature b) |
protected static Feature |
StaticFeatureCollection.let(TermBuffer x,
ProjectionToTerm value,
Feature body) |
protected static Feature |
StaticFeatureCollection.literalsSmallerThan(java.lang.String smaller,
java.lang.String bigger,
IntegerLDT numbers) |
protected static Feature |
StaticFeatureCollection.longConst(long a) |
protected static Feature |
StaticFeatureCollection.loopContractApplyHead(Feature cost) |
protected static Feature |
StaticFeatureCollection.loopContractExternalFeature(Feature cost) |
protected static Feature |
StaticFeatureCollection.loopContractInternalFeature(Feature cost) |
protected static Feature |
StaticFeatureCollection.loopInvFeature(Feature costStdInv) |
protected static Feature |
StaticFeatureCollection.mergeRuleFeature(Feature cost) |
protected static Feature |
StaticFeatureCollection.methodSpecFeature(Feature cost) |
protected static Feature |
StaticFeatureCollection.monSmallerThan(java.lang.String smaller,
java.lang.String bigger,
IntegerLDT numbers) |
protected static Feature |
StaticFeatureCollection.not(Feature f) |
protected Feature |
AbstractFeatureStrategy.oneOf(Feature[] features) |
protected Feature |
AbstractFeatureStrategy.oneOf(Feature feature0,
Feature feature1) |
protected static Feature |
StaticFeatureCollection.or(Feature... features) |
protected static Feature |
StaticFeatureCollection.or(Feature a,
Feature b) |
protected static Feature |
StaticFeatureCollection.or(Feature a,
Feature b,
Feature c) |
protected static Feature |
StaticFeatureCollection.println(ProjectionToTerm t) |
protected static Feature |
StaticFeatureCollection.querySpecFeature(Feature cost) |
protected static Feature |
StaticFeatureCollection.sequentContainsNoPrograms() |
protected Feature |
JavaCardDLStrategy.setupApprovalF() |
protected Feature |
JavaCardDLStrategy.setupGlobalF(Feature dispatcher) |
protected static Feature |
StaticFeatureCollection.sum(TermBuffer x,
TermGenerator gen,
Feature body) |
protected static Feature |
StaticFeatureCollection.termSmallerThan(java.lang.String smaller,
java.lang.String bigger) |
Modifier and Type | Method and Description |
---|---|
protected static Feature |
StaticFeatureCollection.add(Feature... features) |
protected static Feature |
StaticFeatureCollection.add(Feature a,
Feature b) |
protected static Feature |
StaticFeatureCollection.add(Feature a,
Feature b,
Feature c) |
protected void |
AbstractFeatureStrategy.bindRuleSet(RuleSetDispatchFeature d,
RuleSet ruleSet,
Feature f) |
protected void |
AbstractFeatureStrategy.bindRuleSet(RuleSetDispatchFeature d,
java.lang.String ruleSet,
Feature f) |
protected static Feature |
StaticFeatureCollection.blockContractExternalFeature(Feature cost) |
protected static Feature |
StaticFeatureCollection.blockContractInternalFeature(Feature cost) |
protected static Feature |
StaticFeatureCollection.eq(Feature a,
Feature b) |
protected Feature |
AbstractFeatureStrategy.forEach(TermBuffer x,
TermGenerator gen,
Feature body) |
protected Feature |
AbstractFeatureStrategy.ifHeuristics(java.lang.String[] heuristics,
Feature thenFeature) |
protected Feature |
AbstractFeatureStrategy.ifHeuristics(java.lang.String[] heuristics,
Feature thenFeature,
Feature elseFeature) |
protected static Feature |
StaticFeatureCollection.ifZero(Feature cond,
Feature thenFeature) |
protected static Feature |
StaticFeatureCollection.ifZero(Feature cond,
Feature thenFeature,
Feature elseFeature) |
protected static Feature |
StaticFeatureCollection.leq(Feature a,
Feature b) |
protected static Feature |
StaticFeatureCollection.less(Feature a,
Feature b) |
protected static Feature |
StaticFeatureCollection.let(TermBuffer x,
ProjectionToTerm value,
Feature body) |
protected static Feature |
StaticFeatureCollection.loopContractApplyHead(Feature cost) |
protected static Feature |
StaticFeatureCollection.loopContractExternalFeature(Feature cost) |
protected static Feature |
StaticFeatureCollection.loopContractInternalFeature(Feature cost) |
protected static Feature |
StaticFeatureCollection.loopInvFeature(Feature costStdInv) |
protected static Feature |
StaticFeatureCollection.mergeRuleFeature(Feature cost) |
protected static Feature |
StaticFeatureCollection.methodSpecFeature(Feature cost) |
protected static Feature |
StaticFeatureCollection.not(Feature f) |
protected Feature |
AbstractFeatureStrategy.oneOf(Feature[] features) |
protected Feature |
AbstractFeatureStrategy.oneOf(Feature feature0,
Feature feature1) |
protected static Feature |
StaticFeatureCollection.or(Feature... features) |
protected static Feature |
StaticFeatureCollection.or(Feature a,
Feature b) |
protected static Feature |
StaticFeatureCollection.or(Feature a,
Feature b,
Feature c) |
protected static Feature |
StaticFeatureCollection.querySpecFeature(Feature cost) |
protected Feature |
JavaCardDLStrategy.setupGlobalF(Feature dispatcher) |
protected static Feature |
StaticFeatureCollection.sum(TermBuffer x,
TermGenerator gen,
Feature body) |
Modifier and Type | Class and Description |
---|---|
class |
AbstractBetaFeature
This abstract class contains some auxiliary methods for the selection of
beta rules that are supposed to be applied.
|
class |
AbstractMonomialSmallerThanFeature |
class |
AbstractNonDuplicateAppFeature |
class |
AgeFeature
Feature that computes the age of the goal (i.e.
|
class |
AllowedCutPositionFeature
Feature that returns zero iff the application focus of a rule is a potential
cut position (taclet cut_direct).
|
class |
ApplyTFFeature
Feature for invoking a term feature on the instantiation of a schema variable
|
class |
AtomsSmallerThanFeature
Feature that returns zero iff each variable/atom of one monomial is smaller
than all variables of a second monomial
|
class |
AutomatedRuleFeature
This feature checks if a rule may be applied automatically.
|
class |
BinaryFeature
Abstract superclass for features that have either zero cost or top cost.
|
class |
BinaryTacletAppFeature
Abstract superclass for features of TacletApps that have either zero or top
cost.
|
class |
CheckApplyEqFeature
This feature checks that an equation is not applied to itself.
|
class |
CompareCostsFeature |
class |
ComprehendedSumFeature
A feature that computes the sum of the values of a feature term when a given
variable ranges over a sequence of terms
|
class |
ConditionalFeature
A feature that evaluates one of two given features, depending on the result
of a
RuleFilter |
class |
ConstFeature
A feature that returns a constant value
|
class |
ContainsQuantifierFeature
Binary feature that returns zero iff the focus of a rule contains a
quantifier
NB: this can nowadays be done more nicely using term features
|
class |
ContainsTermFeature
Feature for checking if the term of the first projection contains the
term of the second projection.
|
class |
CountBranchFeature
Feature that returns the number of branches for a given taclet application
Size of "assumes" sequents is currently not considered
|
class |
CountMaxDPathFeature
Feature that returns the maximum number of literals occurring within a d-path
of the find-formula as a formula of the antecedent.
|
class |
CountPosDPathFeature
Feature that returns the maximum number of positive literals occurring within
a d-path of the find-formula as a formula of the antecedent.
|
class |
DeleteMergePointRuleFeature
Costs for the
DeleteMergePointRule ; incredibly cheap if the previous
rule application was a MergeRule app, infinitely expensive otherwise. |
class |
DependencyContractFeature |
class |
DiffFindAndIfFeature
Binary feature that returns zero iff the \assumes- and find-formula
of a Taclet are matched to different members of the sequent.
|
class |
DiffFindAndReplacewithFeature
Binary feature that returns zero iff the replacewith- and find-parts
of a Taclet are matched to different terms.
|
class |
DirectlyBelowFeature
This feature returns zero if and only if the focus of the given rule
application exists, is not top-level and the symbol immediately above the
focus is
badSymbol . |
class |
DirectlyBelowSymbolFeature
This feature returns zero if and only if the focus of the given rule
application exists, is not top-level and the symbol immediately above the
focus is
badSymbol . |
class |
EqNonDuplicateAppFeature
Binary feature that returns zero iff a certain Taclet app has not already
been performed.
|
class |
FindDepthFeature
A feature that computes the depth of the find-position of a taclet (top-level
positions have depth zero or if not a find taclet)
TODO: eliminate this class and use term features instead
|
class |
FindRightishFeature
Walking from the root of a formula down to the focus of a rule application,
count how often we choose the left branch (subterm) and how the right
branches.
|
class |
FocusInAntecFeature |
class |
FocusIsSubFormulaOfInfFlowContractAppFeature
Checks whether the focus of the ruleApp is contained in one of the formulas
added by information flow contract applications.
|
class |
FormulaAddedByRuleFeature
Binary feature that returns zero iff the find-formula of the concerned rule
app was introduced by a certain kind rule of rule (described via a
RuleFilter ) |
class |
IfThenElseMalusFeature
Feature that counts the IfThenElse operators above the focus of a rule
application.
|
class |
ImplicitCastNecessary |
class |
InEquationMultFeature
Feature that decides whether the multiplication of two inequations (using
rules of set inEqSimp_nonLin_multiply) is allowed.
|
class |
InfFlowContractAppFeature |
class |
InstantiatedSVFeature
Feature that returns zero iff a certain schema variable is instantiated.
|
class |
LeftmostNegAtomFeature
Feature that returns zero if there is no atom with negative polarity on a
common d-path and on the left of the find-position within the find-formula as
a formula of the antecedent.
|
class |
LetFeature
Feature for locally binding a
TermBuffer to a certain value,
namely to a term that is generated by a ProjectionToTerm . |
class |
MatchedIfFeature
Binary features that returns zero iff the if-formulas of a Taclet are
instantiated or the Taclet does not have any if-formulas.
|
class |
MergeRuleFeature
Costs for the
MergeRule ; cheap if the first statement in the chosen
top-level formula is a MergePointStatement , otherwise, infinitely
expensive. |
class |
MonomialsSmallerThanFeature
Feature that returns zero iff each monomial of one polynomial is smaller than
all monomials of a second polynomial
|
class |
NonDuplicateAppFeature
Binary feature that returns zero iff a certain Taclet app has not already
been performed
|
class |
NonDuplicateAppModPositionFeature
Binary feature that returns zero iff a certain Taclet app has not already
been performed
|
class |
NoSelfApplicationFeature
This feature checks that the position of application is not contained in the
if-formulas.
|
class |
NotBelowBinderFeature
Returns zero iff the position of a rule application is not below any
operators that bind variables
|
class |
NotBelowQuantifierFeature
Binary feature that returns zero iff the position of the given rule app is
not within the scope of a quantifier
|
class |
NotInScopeOfModalityFeature
Returns zero iff the position of a rule application is not in the scope of a
modal operator (a program block or an update).
|
class |
OnlyInScopeOfQuantifiersFeature
BinaryFeature that return zero if all the operator is quantifier from root
to position it point to.
|
class |
PolynomialValuesCmpFeature
Return zero only if the value of one (left) polynomial always will be (less
or equal) or (less) than the value of a second (right) polynomial.
|
class |
PrintFeature
For debugging purposes.
|
class |
PurePosDPathFeature
Binary feature that returns zero iff the find-formula of a rule contains a
d-path consisting only of positive literals (as a formula of the antecedent).
|
class |
QueryExpandCost
A Feature that computes the cost for using the query expand rule.
|
class |
ReducibleMonomialsFeature
Return zero iff the monomial
dividendSV can be made smaller
(in the polynomial reduction ordering) by adding or subtracting
divisorSV |
class |
RuleSetDispatchFeature
Feature for relating rule sets with feature terms.
|
class |
ScaleFeature
A feature that applies an affine transformation to the result of
a given feature.
|
class |
SeqContainsExecutableCodeFeature |
class |
SetsSmallerThanFeature |
class |
ShannonFeature
A conditional feature, in which the condition itself is a (binary) feature.
|
class |
SimplifyBetaCandidateFeature
Binary feature that returns zero iff the hyper-tableaux simplification method
approves the given application (which is supposed to be the application of a
beta rule).
|
class |
SimplifyReplaceKnownCandidateFeature
Binary feature that returns true iff the hyper-tableaux simplification method
approves the given application (which is supposed to be the application of a
replace-known rule).
|
class |
SmallerThanFeature
Abstract superclass for features comparing terms (in particular polynomials
or monomials) using the term ordering
|
class |
SortComparisonFeature |
class |
SumFeature
A feature that computes the sum of a given list (vector) of features
|
class |
SVNeedsInstantiation |
class |
TacletRequiringInstantiationFeature
Feature that returns zero iff the given rule app is a taclet app that needs
explicit instantiation of schema variables (which has not been done yet)
|
class |
TermSmallerThanFeature
Feature that returns zero iff one term is smaller than another term in the
current term ordering
|
class |
ThrownExceptionFeature |
class |
TopLevelFindFeature
Feature for investigating whether the focus of a rule application is a
top-level formula, a top-level formula of the antecedent or a top-level
formula of the succedent
|
class |
TriggerVarInstantiatedFeature |
class |
TrivialMonomialLCRFeature
Return zero of the least common reducible of two monomials is so trivial that
it is not necessary to do the critical pair completion
"A critical-pair/completion algorithm for finitely generated ideals in rings"
|
Modifier and Type | Field and Description |
---|---|
protected Feature |
CompareCostsFeature.a |
static Feature |
TopLevelFindFeature.ANTEC |
static Feature |
TopLevelFindFeature.ANTEC_OR_SUCC |
static Feature |
TopLevelFindFeature.ANTEC_OR_SUCC_WITH_UPDATE |
static Feature |
TopLevelFindFeature.ANTEC_WITH_UPDATE |
protected Feature |
CompareCostsFeature.b |
static Feature |
CountBranchFeature.INSTANCE |
static Feature |
TriggerVarInstantiatedFeature.INSTANCE |
static Feature |
FocusInAntecFeature.INSTANCE |
static Feature |
MatchedIfFeature.INSTANCE |
static Feature |
TacletRequiringInstantiationFeature.INSTANCE |
static Feature |
ContainsQuantifierFeature.INSTANCE |
static Feature |
OnlyInScopeOfQuantifiersFeature.INSTANCE |
static Feature |
AgeFeature.INSTANCE |
static Feature |
AutomatedRuleFeature.INSTANCE |
static Feature |
FocusIsSubFormulaOfInfFlowContractAppFeature.INSTANCE |
static Feature |
IfThenElseMalusFeature.INSTANCE |
static Feature |
FindDepthFeature.INSTANCE |
static Feature |
NoSelfApplicationFeature.INSTANCE |
static Feature |
DiffFindAndIfFeature.INSTANCE
the single instance of this feature
|
static Feature |
PurePosDPathFeature.INSTANCE |
static Feature |
CountMaxDPathFeature.INSTANCE |
static Feature |
LeftmostNegAtomFeature.INSTANCE |
static Feature |
NotInScopeOfModalityFeature.INSTANCE |
static Feature |
AllowedCutPositionFeature.INSTANCE |
static Feature |
SimplifyReplaceKnownCandidateFeature.INSTANCE |
static Feature |
SimplifyBetaCandidateFeature.INSTANCE |
static Feature |
NonDuplicateAppFeature.INSTANCE |
static Feature |
CountPosDPathFeature.INSTANCE |
static Feature |
NotBelowBinderFeature.INSTANCE |
static Feature |
DeleteMergePointRuleFeature.INSTANCE |
static Feature |
NonDuplicateAppModPositionFeature.INSTANCE |
static Feature |
EqNonDuplicateAppFeature.INSTANCE |
static Feature |
DiffFindAndReplacewithFeature.INSTANCE
the single instance of this feature
|
static Feature |
MergeRuleFeature.INSTANCE |
static Feature |
InfFlowContractAppFeature.INSTANCE |
static Feature |
NotBelowQuantifierFeature.INSTANCE |
static Feature |
CheckApplyEqFeature.INSTANCE |
static Feature |
SeqContainsExecutableCodeFeature.PROGRAMS |
static Feature |
SeqContainsExecutableCodeFeature.PROGRAMS_OR_QUERIES |
static Feature |
TopLevelFindFeature.SUCC |
static Feature |
TopLevelFindFeature.SUCC_WITH_UPDATE |
Modifier and Type | Method and Description |
---|---|
static Feature |
FindRightishFeature.create(IntegerLDT numbers) |
static Feature |
InstantiatedSVFeature.create(Name svName) |
static Feature |
DirectlyBelowSymbolFeature.create(Operator badSymbol) |
static Feature |
DirectlyBelowSymbolFeature.create(Operator badSymbol,
int index) |
static Feature |
ImplicitCastNecessary.create(ProjectionToTerm s1) |
static Feature |
TermSmallerThanFeature.create(ProjectionToTerm left,
ProjectionToTerm right) |
static Feature |
ContainsTermFeature.create(ProjectionToTerm proj1,
ProjectionToTerm proj2) |
static Feature |
TrivialMonomialLCRFeature.create(ProjectionToTerm a,
ProjectionToTerm b) |
static Feature |
SortComparisonFeature.create(ProjectionToTerm s1,
ProjectionToTerm s2,
int cmp) |
static Feature |
MonomialsSmallerThanFeature.create(ProjectionToTerm left,
ProjectionToTerm right,
IntegerLDT numbers) |
static Feature |
AtomsSmallerThanFeature.create(ProjectionToTerm left,
ProjectionToTerm right,
IntegerLDT numbers) |
static Feature |
SetsSmallerThanFeature.create(ProjectionToTerm left,
ProjectionToTerm right,
LocSetLDT locSetLDT) |
static Feature |
ApplyTFFeature.create(ProjectionToTerm proj,
TermFeature tf) |
static Feature |
FormulaAddedByRuleFeature.create(RuleFilter p_filter) |
static Feature |
SVNeedsInstantiation.create(java.lang.String svName) |
static Feature |
ThrownExceptionFeature.create(java.lang.String[] blockedExceptions,
Services services) |
static Feature |
LetFeature.create(TermBuffer var,
ProjectionToTerm value,
Feature body) |
static Feature |
ComprehendedSumFeature.create(TermBuffer var,
TermGenerator generator,
Feature body) |
static Feature |
ScaleFeature.createAffine(Feature f,
double coeff,
long offset)
Create a feature that applies an affine transformation to the result of
the base feature.
|
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) |
static Feature |
ConditionalFeature.createConditional(RuleFilter cond,
Feature thenFeature,
Feature elseFeature) |
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) |
static Feature |
ShannonFeature.createConditionalBinary(Feature cond,
Feature thenFeature,
Feature elseFeature) |
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 |
ReducibleMonomialsFeature.createDivides(ProjectionToTerm dividend,
ProjectionToTerm divisor) |
static Feature |
ApplyTFFeature.createNonStrict(ProjectionToTerm proj,
TermFeature tf,
RuleAppCost noInstCost) |
static Feature |
ReducibleMonomialsFeature.createReducible(ProjectionToTerm dividend,
ProjectionToTerm divisor) |
static Feature |
ScaleFeature.createScaled(Feature f,
double coeff)
Create a feature that scales the result of the base feature.
|
static Feature |
SumFeature.createSum(Feature... fs) |
static Feature |
PolynomialValuesCmpFeature.divides(ProjectionToTerm left,
ProjectionToTerm right) |
static Feature |
PolynomialValuesCmpFeature.divides(ProjectionToTerm left,
ProjectionToTerm right,
ProjectionToTerm leftCoeff,
ProjectionToTerm rightCoeff) |
static Feature |
CompareCostsFeature.eq(Feature a,
Feature b) |
static Feature |
PolynomialValuesCmpFeature.eq(ProjectionToTerm left,
ProjectionToTerm right) |
static Feature |
PolynomialValuesCmpFeature.eq(ProjectionToTerm left,
ProjectionToTerm right,
ProjectionToTerm leftCoeff,
ProjectionToTerm rightCoeff) |
static Feature |
InEquationMultFeature.exactlyBounded(ProjectionToTerm mult1Candidate,
ProjectionToTerm mult2Candidate,
ProjectionToTerm targetCandidate)
Return zero iff the product of mult1 and mult2 is target
|
Feature |
RuleSetDispatchFeature.get(RuleSet ruleSet)
|
protected Feature |
ScaleFeature.getFeature() |
static Feature |
CompareCostsFeature.leq(Feature a,
Feature b) |
static Feature |
PolynomialValuesCmpFeature.leq(ProjectionToTerm left,
ProjectionToTerm right) |
static Feature |
PolynomialValuesCmpFeature.leq(ProjectionToTerm left,
ProjectionToTerm right,
ProjectionToTerm leftCoeff,
ProjectionToTerm rightCoeff) |
static Feature |
CompareCostsFeature.less(Feature a,
Feature b) |
static Feature |
PolynomialValuesCmpFeature.lt(ProjectionToTerm left,
ProjectionToTerm right) |
static Feature |
PolynomialValuesCmpFeature.lt(ProjectionToTerm left,
ProjectionToTerm right,
ProjectionToTerm leftCoeff,
ProjectionToTerm rightCoeff) |
static Feature |
InEquationMultFeature.partiallyBounded(ProjectionToTerm mult1Candidate,
ProjectionToTerm mult2Candidate,
ProjectionToTerm targetCandidate)
Return zero iff the multiplication of mult1 and mult2 is allowed,
because the resulting product is partially covered by target.
|
static Feature |
ScaleFeature.realAffine(Feature f,
RuleAppCost dom0,
RuleAppCost dom1,
RuleAppCost img0,
RuleAppCost img1) |
static Feature |
InEquationMultFeature.totallyBounded(ProjectionToTerm mult1Candidate,
ProjectionToTerm mult2Candidate,
ProjectionToTerm targetCandidate)
Return zero iff the product of mult1 and mult2 is a factor of target
|
Modifier and Type | Method and Description |
---|---|
void |
RuleSetDispatchFeature.add(RuleSet ruleSet,
Feature f)
Bind feature
f to the rule set ruleSet . |
static Feature |
LetFeature.create(TermBuffer var,
ProjectionToTerm value,
Feature body) |
static Feature |
ComprehendedSumFeature.create(TermBuffer var,
TermGenerator generator,
Feature body) |
static Feature |
ScaleFeature.createAffine(Feature f,
double coeff,
long offset)
Create a feature that applies an affine transformation to the result of
the base feature.
|
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) |
static Feature |
ConditionalFeature.createConditional(RuleFilter cond,
Feature thenFeature,
Feature elseFeature) |
static Feature |
ConditionalFeature.createConditional(RuleFilter cond,
Feature thenFeature,
RuleAppCost elseValue) |
static Feature |
ShannonFeature.createConditionalBinary(Feature cond,
Feature thenFeature) |
static Feature |
ShannonFeature.createConditionalBinary(Feature cond,
Feature thenFeature,
Feature elseFeature) |
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 |
ScaleFeature.createScaled(Feature f,
double coeff)
Create a feature that scales the result of the base feature.
|
static Feature |
SumFeature.createSum(Feature... fs) |
static Feature |
CompareCostsFeature.eq(Feature a,
Feature b) |
static Feature |
CompareCostsFeature.leq(Feature a,
Feature b) |
static Feature |
CompareCostsFeature.less(Feature a,
Feature b) |
static Feature |
ScaleFeature.realAffine(Feature f,
RuleAppCost dom0,
RuleAppCost dom1,
RuleAppCost img0,
RuleAppCost img1) |
Constructor and Description |
---|
PrintFeature(Feature f) |
PrintFeature(java.lang.String prefix,
Feature f) |
ScaleFeature(Feature p_feature) |
Modifier and Type | Class and Description |
---|---|
class |
FindPrefixRestrictionFeature
Feature for investigating whether some restrictions to the prefix of the
find formula apply.
|
Modifier and Type | Class and Description |
---|---|
class |
ForEachCP
Feature representing a
ChoicePoint that iterates over the
terms returned by a TermGenerator . |
class |
OneOfCP |
class |
SVInstantiationCP
Feature representing a
ChoicePoint for instantiating a schema
variable of a taclet with the term that is returned by a
ProjectionToTerm . |
Modifier and Type | Method and Description |
---|---|
static Feature |
OneOfCP.create(Feature[] features,
BackTrackingManager manager) |
static Feature |
SVInstantiationCP.create(Name svToInstantiate,
ProjectionToTerm value,
BackTrackingManager manager) |
static Feature |
ForEachCP.create(TermBuffer var,
TermGenerator generator,
Feature body,
BackTrackingManager manager) |
static Feature |
SVInstantiationCP.createTriggeredVarCP(ProjectionToTerm value,
BackTrackingManager manager) |
Modifier and Type | Method and Description |
---|---|
static Feature |
OneOfCP.create(Feature[] features,
BackTrackingManager manager) |
static Feature |
ForEachCP.create(TermBuffer var,
TermGenerator generator,
Feature body,
BackTrackingManager manager) |
Modifier and Type | Class and Description |
---|---|
class |
ClausesSmallerThanFeature
Ordering used to sort the clauses in a quantified formula.
|
class |
ExistentiallyConnectedFormulasFeature
Binary feature that return zero if two given projection term is CS-Releated.
|
class |
InstantiationCost
Feature that returns the number of branches after instantiated the quantifier
formula.
|
class |
InstantiationCostScalerFeature |
class |
LiteralsSmallerThanFeature |
class |
SplittableQuantifiedFormulaFeature |
Modifier and Type | Field and Description |
---|---|
static Feature |
SplittableQuantifiedFormulaFeature.INSTANCE |
Modifier and Type | Method and Description |
---|---|
static Feature |
InstantiationCostScalerFeature.create(Feature costFeature,
Feature allowSplitting) |
static Feature |
InstantiationCost.create(ProjectionToTerm varInst) |
static Feature |
ExistentiallyConnectedFormulasFeature.create(ProjectionToTerm for0,
ProjectionToTerm for1) |
static Feature |
LiteralsSmallerThanFeature.create(ProjectionToTerm left,
ProjectionToTerm right,
IntegerLDT numbers) |
static Feature |
ClausesSmallerThanFeature.create(ProjectionToTerm left,
ProjectionToTerm right,
IntegerLDT numbers) |
Modifier and Type | Method and Description |
---|---|
static Feature |
InstantiationCostScalerFeature.create(Feature costFeature,
Feature allowSplitting) |
Modifier and Type | Class and Description |
---|---|
class |
ContainsLabelFeature |
class |
ContainsLabelNameFeature |
Modifier and Type | Class and Description |
---|---|
class |
CutHeapObjectsFeature
This
BinaryFeature checks if a cut with an equality for
an alias check should be done or not. |
class |
SimplifyTermStrategy
|
class |
SymbolicExecutionStrategy
Strategy to use for symbolic execution. |
Modifier and Type | Method and Description |
---|---|
protected Feature |
SymbolicExecutionStrategy.modalitySideProofFeature()
Computes the cost
Feature for the ModalitySideProofRule . |
protected Feature |
SymbolicExecutionStrategy.querySideProofFeature()
Computes the cost
Feature for the QuerySideProofRule . |
protected Feature |
SymbolicExecutionStrategy.setupApprovalF() |
protected Feature |
SimplifyTermStrategy.setupApprovalF() |
protected Feature |
SymbolicExecutionStrategy.setupGlobalF(Feature dispatcher) |
Modifier and Type | Method and Description |
---|---|
protected Feature |
SymbolicExecutionStrategy.setupGlobalF(Feature dispatcher) |
Copyright © 2003-2019 The KeY-Project.