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.termfeature |
Modifier and Type | Method and Description |
---|---|
protected static TermFeature |
StaticFeatureCollection.eq(TermBuffer t) |
protected Feature |
AbstractFeatureStrategy.forEach(TermBuffer x,
TermGenerator gen,
Feature body) |
protected static Feature |
StaticFeatureCollection.let(TermBuffer x,
ProjectionToTerm value,
Feature body) |
protected static Feature |
StaticFeatureCollection.sum(TermBuffer x,
TermGenerator gen,
Feature body) |
Modifier and Type | Method and Description |
---|---|
static Feature |
LetFeature.create(TermBuffer var,
ProjectionToTerm value,
Feature body) |
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 | Method and Description |
---|---|
static TermFeature |
EqTermFeature.create(TermBuffer pattern) |
Copyright © 2003-2019 The KeY-Project.