Package | Description |
---|---|
de.uka.ilkd.key.strategy.quantifierHeuristics | |
de.uka.ilkd.key.strategy.termfeature |
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 | Class and Description |
---|---|
class |
AnonHeapTermFeature |
class |
AtomTermFeature |
class |
ClosedExpressionTermFeature
return zero cost if given term does not contain any free variables.
|
class |
ConstantTermFeature |
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 |
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 |
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. |
Copyright © 2003-2019 The KeY-Project.