Package | Description |
---|---|
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.quantifierHeuristics | |
de.uka.ilkd.key.strategy.termfeature | |
de.uka.ilkd.key.strategy.termgenerator |
Modifier and Type | Method and Description |
---|---|
protected static TermFeature |
StaticFeatureCollection.add(TermFeature a,
TermFeature b) |
protected static TermFeature |
StaticFeatureCollection.add(TermFeature a,
TermFeature b,
TermFeature c) |
protected static TermFeature |
StaticFeatureCollection.any() |
protected static TermFeature |
StaticFeatureCollection.eq(TermBuffer t) |
protected static TermFeature |
StaticFeatureCollection.extendsTrans(Sort s) |
protected static TermFeature |
StaticFeatureCollection.ifZero(TermFeature cond,
TermFeature thenFeature) |
protected static TermFeature |
StaticFeatureCollection.ifZero(TermFeature cond,
TermFeature thenFeature,
TermFeature elseFeature) |
protected static TermFeature |
StaticFeatureCollection.inftyTermConst() |
protected static TermFeature |
StaticFeatureCollection.longTermConst(long a) |
protected static TermFeature |
StaticFeatureCollection.not(TermFeature f) |
protected static TermFeature |
StaticFeatureCollection.op(Operator op) |
protected static TermFeature |
StaticFeatureCollection.opSub(Operator op,
TermFeature sub0) |
protected static TermFeature |
StaticFeatureCollection.opSub(Operator op,
TermFeature sub0,
TermFeature sub1) |
protected static TermFeature |
StaticFeatureCollection.or(TermFeature a,
TermFeature b) |
protected static TermFeature |
StaticFeatureCollection.or(TermFeature a,
TermFeature b,
TermFeature c) |
protected static TermFeature |
StaticFeatureCollection.rec(TermFeature cond,
TermFeature summand) |
protected static TermFeature |
StaticFeatureCollection.sub(TermFeature sub0) |
protected static TermFeature |
StaticFeatureCollection.sub(TermFeature sub0,
TermFeature sub1) |
Modifier and Type | Method and Description |
---|---|
protected static TermFeature |
StaticFeatureCollection.add(TermFeature a,
TermFeature b) |
protected static TermFeature |
StaticFeatureCollection.add(TermFeature a,
TermFeature b,
TermFeature 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 TermFeature |
StaticFeatureCollection.ifZero(TermFeature cond,
TermFeature thenFeature) |
protected static TermFeature |
StaticFeatureCollection.ifZero(TermFeature cond,
TermFeature thenFeature,
TermFeature elseFeature) |
protected static TermFeature |
StaticFeatureCollection.not(TermFeature f) |
protected static TermFeature |
StaticFeatureCollection.opSub(Operator op,
TermFeature sub0) |
protected static TermFeature |
StaticFeatureCollection.opSub(Operator op,
TermFeature sub0,
TermFeature sub1) |
protected static TermFeature |
StaticFeatureCollection.or(TermFeature a,
TermFeature b) |
protected static TermFeature |
StaticFeatureCollection.or(TermFeature a,
TermFeature b,
TermFeature c) |
protected static TermFeature |
StaticFeatureCollection.rec(TermFeature cond,
TermFeature summand) |
protected static TermFeature |
StaticFeatureCollection.sub(TermFeature sub0) |
protected static TermFeature |
StaticFeatureCollection.sub(TermFeature sub0,
TermFeature sub1) |
Modifier and Type | Method and Description |
---|---|
static Feature |
ApplyTFFeature.create(ProjectionToTerm proj,
TermFeature tf) |
static Feature |
ApplyTFFeature.createNonStrict(ProjectionToTerm proj,
TermFeature tf,
RuleAppCost noInstCost) |
Modifier and Type | Class and Description |
---|---|
class |
EliminableQuantifierTF |
class |
RecAndExistentiallyConnectedClausesFeature
Binary Term Feature return zero if root is a CNF quantifier formula with several
clauses.
|
Modifier and Type | Field and Description |
---|---|
static TermFeature |
RecAndExistentiallyConnectedClausesFeature.INSTANCE |
static TermFeature |
EliminableQuantifierTF.INSTANCE |
Modifier and Type | Class and Description |
---|---|
class |
AnonHeapTermFeature |
class |
AtomTermFeature |
class |
BinarySumTermFeature
A feature that computes the sum of two given features (faster than the more
general class
SumFeature ) |
class |
BinaryTermFeature
Abstract superclass for features that have either zero cost or top cost.
|
class |
ClosedExpressionTermFeature
return zero cost if given term does not contain any free variables.
|
class |
ConstantTermFeature |
class |
ConstTermFeature
A feature that returns a constant value
|
class |
ContainsExecutableCodeTermFeature
Returns zero iff a term contains a program or (optionally) a query expression
|
class |
EqTermFeature
Term feature for testing equality of two terms.
|
class |
IsHeapFunctionTermFeature |
class |
IsInductionVariable
The comment below was the description used in the variable condition:
In the taclet language the variable condition is called "\isInductVar". |
class |
IsNonRigidTermFeature
this termfeature returns ZERO costs if the given term
is non-rigid
|
class |
IsPostConditionTermFeature
Term has the post condition term label.
|
class |
IsSelectSkolemConstantTermFeature
A schema variable that is used as placeholder for auxiliary heap skolem
constants.
|
class |
OperatorClassTF
Term feature for checking whether the top operator of a term has an instance
of a certain class
|
class |
OperatorTF
Term feature for checking whether the top operator of a term is
identical to a given one
|
class |
PrimitiveHeapTermFeature |
class |
PrintTermFeature |
class |
RecSubTermFeature
Feature for invoking a term feature recursively on all subterms of a term.
|
class |
ShannonTermFeature
A conditional feature, in which the condition itself is a (binary) feature.
|
class |
SimplifiedSelectTermFeature |
class |
SortExtendsTransTermFeature
Term feature for testing whether the sort of a term is a subsort of a given
sort (or exactly the given sort).
|
class |
SubTermFeature
Feature for invoking a list of term features on the direct subterms of a
given term.
|
class |
TermLabelTermFeature
A termfeature that can be used to check whether a term has a specific label
TermLabelTermFeature.create(TermLabel)
or any label {TermLabelTermFeature.HAS_ANY_LABEL at all. |
Modifier and Type | Field and Description |
---|---|
static TermFeature |
TermLabelTermFeature.HAS_ANY_LABEL |
static TermFeature |
AtomTermFeature.INSTANCE |
static TermFeature |
IsInductionVariable.INSTANCE |
static TermFeature |
IsNonRigidTermFeature.INSTANCE |
static TermFeature |
ClosedExpressionTermFeature.INSTANCE |
static TermFeature |
ConstantTermFeature.INSTANCE |
static TermFeature |
PrintTermFeature.INSTANCE |
static TermFeature |
ContainsExecutableCodeTermFeature.PROGRAMS |
static TermFeature |
ContainsExecutableCodeTermFeature.PROGRAMS_OR_QUERIES |
Modifier and Type | Method and Description |
---|---|
static TermFeature |
OperatorClassTF.create(java.lang.Class<? extends Operator> op) |
static TermFeature |
SimplifiedSelectTermFeature.create(HeapLDT heapLDT) |
static TermFeature |
OperatorTF.create(Operator op) |
static TermFeature |
SortExtendsTransTermFeature.create(Sort sort) |
static TermFeature |
EqTermFeature.create(TermBuffer pattern) |
static TermFeature |
SubTermFeature.create(TermFeature[] fs) |
static TermFeature |
SubTermFeature.create(TermFeature[] fs,
RuleAppCost arityMismatchCost) |
static TermFeature |
RecSubTermFeature.create(TermFeature cond,
TermFeature summand) |
static TermFeature |
TermLabelTermFeature.create(TermLabel label) |
static TermFeature |
ShannonTermFeature.createConditionalBinary(TermFeature cond,
TermFeature thenFeature) |
static TermFeature |
ShannonTermFeature.createConditionalBinary(TermFeature cond,
TermFeature thenFeature,
TermFeature elseFeature) |
static TermFeature |
ConstTermFeature.createConst(RuleAppCost p_val) |
static TermFeature |
BinarySumTermFeature.createSum(TermFeature f0,
TermFeature f1) |
Modifier and Type | Method and Description |
---|---|
static TermFeature |
SubTermFeature.create(TermFeature[] fs) |
static TermFeature |
SubTermFeature.create(TermFeature[] fs,
RuleAppCost arityMismatchCost) |
static TermFeature |
RecSubTermFeature.create(TermFeature cond,
TermFeature summand) |
static TermFeature |
ShannonTermFeature.createConditionalBinary(TermFeature cond,
TermFeature thenFeature) |
static TermFeature |
ShannonTermFeature.createConditionalBinary(TermFeature cond,
TermFeature thenFeature,
TermFeature elseFeature) |
static TermFeature |
BinarySumTermFeature.createSum(TermFeature f0,
TermFeature f1) |
Modifier and Type | Method and Description |
---|---|
static TermGenerator |
SubtermGenerator.leftTraverse(ProjectionToTerm cTerm,
TermFeature cond)
Left-traverse the subterms of a term in depth-first order.
|
static TermGenerator |
SubtermGenerator.rightTraverse(ProjectionToTerm cTerm,
TermFeature cond)
Right-traverse the subterms of a term in depth-first order.
|
static TermGenerator |
SuperTermGenerator.upwards(TermFeature cond,
Services services) |
static TermGenerator |
SuperTermGenerator.upwardsWithIndex(TermFeature cond,
Services services) |
Constructor and Description |
---|
SuperTermGenerator(TermFeature cond) |
Copyright © 2003-2019 The KeY-Project.