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.feature.instantiator | |
de.uka.ilkd.key.strategy.quantifierHeuristics | |
de.uka.ilkd.key.strategy.termgenerator | |
de.uka.ilkd.key.symbolic_execution.strategy |
Modifier and Type | Method and Description |
---|---|
protected Feature |
AbstractFeatureStrategy.forEach(TermBuffer x,
TermGenerator gen,
Feature body) |
protected static Feature |
StaticFeatureCollection.sum(TermBuffer x,
TermGenerator gen,
Feature body) |
Modifier and Type | Method and Description |
---|---|
static Feature |
ComprehendedSumFeature.create(TermBuffer var,
TermGenerator generator,
Feature body) |
Modifier and Type | Method and Description |
---|---|
static Feature |
ForEachCP.create(TermBuffer var,
TermGenerator generator,
Feature body,
BackTrackingManager manager) |
Modifier and Type | Class and Description |
---|---|
class |
HeuristicInstantiation |
Modifier and Type | Field and Description |
---|---|
static TermGenerator |
HeuristicInstantiation.INSTANCE |
Modifier and Type | Class and Description |
---|---|
class |
AllowedCutPositionsGenerator
Enumerate potential subformulas of a formula that could be used for a cut
(taclet cut_direct).
|
class |
HeapGenerator
The heap generator returns an iterator over all terms of sort heap
that
can be found in the sequent
are top level in the sense that they are not part of a larger term expression
depending on the mode: heaps just occurring in updates are included or ignored
|
class |
MultiplesModEquationsGenerator
Try to rewrite a monomial (term)
source so that it becomes a
multiple of another monomial target , using the integer
equations of the antecedent. |
class |
RootsGenerator
Term generator for inferring the range of values that a variable can have from
a given non-linear (in)equation.
|
class |
SequentFormulasGenerator
Term generator that enumerates the formulas of the current
sequent/antecedent/succedent.
|
class |
SubtermGenerator
Term generator that enumerates the subterms or subformulas of a given term.
|
class |
SuperTermGenerator |
class |
TriggeredInstantiations |
Modifier and Type | Field and Description |
---|---|
static TermGenerator |
HeapGenerator.INSTANCE |
static TermGenerator |
AllowedCutPositionsGenerator.INSTANCE |
static TermGenerator |
HeapGenerator.INSTANCE_EXCLUDE_UPDATES |
Modifier and Type | Method and Description |
---|---|
static TermGenerator |
TriggeredInstantiations.create(boolean skipConditions) |
static TermGenerator |
MultiplesModEquationsGenerator.create(ProjectionToTerm source,
ProjectionToTerm target) |
static TermGenerator |
RootsGenerator.create(ProjectionToTerm powerRelation,
TermServices services) |
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) |
Modifier and Type | Class and Description |
---|---|
class |
CutHeapObjectsTermGenerator
This
TermGenerator is used by the SymbolicExecutionStrategy
to add early alias checks of used objects as target of store operations
on heaps. |
Copyright © 2003-2019 The KeY-Project.