Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
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 |
Modifier and Type | Method and Description |
---|---|
IntegerLDT |
TypeConverter.getIntegerLDT() |
Modifier and Type | Method and Description |
---|---|
protected static Feature |
StaticFeatureCollection.atomSmallerThan(java.lang.String smaller,
java.lang.String bigger,
IntegerLDT numbers) |
protected static Feature |
StaticFeatureCollection.literalsSmallerThan(java.lang.String smaller,
java.lang.String bigger,
IntegerLDT numbers) |
protected static Feature |
StaticFeatureCollection.monSmallerThan(java.lang.String smaller,
java.lang.String bigger,
IntegerLDT numbers) |
Modifier and Type | Method and Description |
---|---|
static Feature |
FindRightishFeature.create(IntegerLDT numbers) |
static Feature |
MonomialsSmallerThanFeature.create(ProjectionToTerm left,
ProjectionToTerm right,
IntegerLDT numbers) |
static Feature |
AtomsSmallerThanFeature.create(ProjectionToTerm left,
ProjectionToTerm right,
IntegerLDT numbers) |
Constructor and Description |
---|
AbstractMonomialSmallerThanFeature(IntegerLDT numbers) |
Modifier and Type | Method and Description |
---|---|
static Feature |
LiteralsSmallerThanFeature.create(ProjectionToTerm left,
ProjectionToTerm right,
IntegerLDT numbers) |
static Feature |
ClausesSmallerThanFeature.create(ProjectionToTerm left,
ProjectionToTerm right,
IntegerLDT numbers) |
Copyright © 2003-2019 The KeY-Project.