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.strategy.termProjection |
Modifier and Type | Method and Description |
---|---|
protected static ProjectionToTerm |
StaticFeatureCollection.instOf(java.lang.String schemaVar)
Create a projection of taclet applications to the instantiation of the schema variables
schemaVar . |
protected static ProjectionToTerm |
StaticFeatureCollection.instOfNonStrict(java.lang.String schemaVar)
Create a projection of taclet applications to the instantiation of the schema variables
schemaVar . |
protected static ProjectionToTerm |
StaticFeatureCollection.instOfTriggerVariable()
Create a projection of taclet applications to the instantiation of the trigger variable of a
taclet.
|
protected static ProjectionToTerm |
StaticFeatureCollection.opTerm(Operator op,
ProjectionToTerm subTerm) |
protected static ProjectionToTerm |
StaticFeatureCollection.opTerm(Operator op,
ProjectionToTerm[] subTerms) |
protected static ProjectionToTerm |
StaticFeatureCollection.opTerm(Operator op,
ProjectionToTerm subTerm0,
ProjectionToTerm subTerm1) |
protected static ProjectionToTerm |
StaticFeatureCollection.sub(ProjectionToTerm t,
int index) |
protected static ProjectionToTerm |
StaticFeatureCollection.subAt(ProjectionToTerm t,
PosInTerm pit) |
Modifier and Type | Method and Description |
---|---|
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.applyTFNonStrict(ProjectionToTerm term,
TermFeature tf)
Evaluate the term feature
tf for the term described by the projection
term . |
protected static Feature |
StaticFeatureCollection.contains(ProjectionToTerm bigTerm,
ProjectionToTerm searchedTerm) |
protected static Feature |
StaticFeatureCollection.countOccurrences(ProjectionToTerm cutFormula) |
static Feature |
IntroducedSymbolBy.create(ProjectionToTerm termWithTopLevelOpToCheck,
java.lang.String ruleSetName,
java.lang.String schemaVar) |
protected static Feature |
StaticFeatureCollection.eq(ProjectionToTerm t1,
ProjectionToTerm t2) |
protected static Feature |
StaticFeatureCollection.implicitCastNecessary(ProjectionToTerm s1) |
protected Feature |
AbstractFeatureStrategy.instantiate(Name sv,
ProjectionToTerm value) |
protected Feature |
AbstractFeatureStrategy.instantiate(java.lang.String sv,
ProjectionToTerm value) |
protected Feature |
AbstractFeatureStrategy.instantiateTriggeredVariable(ProjectionToTerm value) |
protected static Feature |
StaticFeatureCollection.isSubSortFeature(ProjectionToTerm s1,
ProjectionToTerm s2) |
protected static Feature |
StaticFeatureCollection.let(TermBuffer x,
ProjectionToTerm value,
Feature body) |
protected static ProjectionToTerm |
StaticFeatureCollection.opTerm(Operator op,
ProjectionToTerm subTerm) |
protected static ProjectionToTerm |
StaticFeatureCollection.opTerm(Operator op,
ProjectionToTerm[] subTerms) |
protected static ProjectionToTerm |
StaticFeatureCollection.opTerm(Operator op,
ProjectionToTerm subTerm0,
ProjectionToTerm subTerm1) |
protected static Feature |
StaticFeatureCollection.println(ProjectionToTerm t) |
protected static ProjectionToTerm |
StaticFeatureCollection.sub(ProjectionToTerm t,
int index) |
protected static ProjectionToTerm |
StaticFeatureCollection.subAt(ProjectionToTerm t,
PosInTerm pit) |
Constructor and Description |
---|
IntroducedSymbolBy(ProjectionToTerm termWithTopLevelOpToCheck,
Name ruleSetName,
Name schemaVar) |
Modifier and Type | Field and Description |
---|---|
protected ProjectionToTerm |
InEquationMultFeature.mult1Candidate |
protected ProjectionToTerm |
InEquationMultFeature.mult2Candidate |
protected ProjectionToTerm |
InEquationMultFeature.targetCandidate |
Modifier and Type | Method and Description |
---|---|
static Feature |
ImplicitCastNecessary.create(ProjectionToTerm s1) |
static Feature |
TermSmallerThanFeature.create(ProjectionToTerm left,
ProjectionToTerm right) |
static Feature |
ContainsTermFeature.create(ProjectionToTerm proj1,
ProjectionToTerm proj2) |
static Feature |
TrivialMonomialLCRFeature.create(ProjectionToTerm a,
ProjectionToTerm b) |
static Feature |
SortComparisonFeature.create(ProjectionToTerm s1,
ProjectionToTerm s2,
int cmp) |
static Feature |
MonomialsSmallerThanFeature.create(ProjectionToTerm left,
ProjectionToTerm right,
IntegerLDT numbers) |
static Feature |
AtomsSmallerThanFeature.create(ProjectionToTerm left,
ProjectionToTerm right,
IntegerLDT numbers) |
static Feature |
SetsSmallerThanFeature.create(ProjectionToTerm left,
ProjectionToTerm right,
LocSetLDT locSetLDT) |
static Feature |
ApplyTFFeature.create(ProjectionToTerm proj,
TermFeature tf) |
static Feature |
LetFeature.create(TermBuffer var,
ProjectionToTerm value,
Feature body) |
static Feature |
ReducibleMonomialsFeature.createDivides(ProjectionToTerm dividend,
ProjectionToTerm divisor) |
static Feature |
ApplyTFFeature.createNonStrict(ProjectionToTerm proj,
TermFeature tf,
RuleAppCost noInstCost) |
static Feature |
ReducibleMonomialsFeature.createReducible(ProjectionToTerm dividend,
ProjectionToTerm divisor) |
static Feature |
PolynomialValuesCmpFeature.divides(ProjectionToTerm left,
ProjectionToTerm right) |
static Feature |
PolynomialValuesCmpFeature.divides(ProjectionToTerm left,
ProjectionToTerm right,
ProjectionToTerm leftCoeff,
ProjectionToTerm rightCoeff) |
static Feature |
PolynomialValuesCmpFeature.eq(ProjectionToTerm left,
ProjectionToTerm right) |
static Feature |
PolynomialValuesCmpFeature.eq(ProjectionToTerm left,
ProjectionToTerm right,
ProjectionToTerm leftCoeff,
ProjectionToTerm rightCoeff) |
static Feature |
InEquationMultFeature.exactlyBounded(ProjectionToTerm mult1Candidate,
ProjectionToTerm mult2Candidate,
ProjectionToTerm targetCandidate)
Return zero iff the product of mult1 and mult2 is target
|
static Feature |
PolynomialValuesCmpFeature.leq(ProjectionToTerm left,
ProjectionToTerm right) |
static Feature |
PolynomialValuesCmpFeature.leq(ProjectionToTerm left,
ProjectionToTerm right,
ProjectionToTerm leftCoeff,
ProjectionToTerm rightCoeff) |
static Feature |
PolynomialValuesCmpFeature.lt(ProjectionToTerm left,
ProjectionToTerm right) |
static Feature |
PolynomialValuesCmpFeature.lt(ProjectionToTerm left,
ProjectionToTerm right,
ProjectionToTerm leftCoeff,
ProjectionToTerm rightCoeff) |
static Feature |
InEquationMultFeature.partiallyBounded(ProjectionToTerm mult1Candidate,
ProjectionToTerm mult2Candidate,
ProjectionToTerm targetCandidate)
Return zero iff the multiplication of mult1 and mult2 is allowed,
because the resulting product is partially covered by target.
|
static Feature |
InEquationMultFeature.totallyBounded(ProjectionToTerm mult1Candidate,
ProjectionToTerm mult2Candidate,
ProjectionToTerm targetCandidate)
Return zero iff the product of mult1 and mult2 is a factor of target
|
Constructor and Description |
---|
InEquationMultFeature(ProjectionToTerm mult1Candidate,
ProjectionToTerm mult2Candidate,
ProjectionToTerm targetCandidate) |
PolynomialValuesCmpFeature(ProjectionToTerm left,
ProjectionToTerm right,
ProjectionToTerm leftCoeff,
ProjectionToTerm rightCoeff) |
Modifier and Type | Method and Description |
---|---|
static Feature |
SVInstantiationCP.create(Name svToInstantiate,
ProjectionToTerm value,
BackTrackingManager manager) |
static Feature |
SVInstantiationCP.createTriggeredVarCP(ProjectionToTerm value,
BackTrackingManager manager) |
Modifier and Type | Method and Description |
---|---|
static Feature |
InstantiationCost.create(ProjectionToTerm varInst) |
static Feature |
ExistentiallyConnectedFormulasFeature.create(ProjectionToTerm for0,
ProjectionToTerm for1) |
static Feature |
LiteralsSmallerThanFeature.create(ProjectionToTerm left,
ProjectionToTerm right,
IntegerLDT numbers) |
static Feature |
ClausesSmallerThanFeature.create(ProjectionToTerm left,
ProjectionToTerm right,
IntegerLDT numbers) |
Modifier and Type | Method and Description |
---|---|
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.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractDividePolynomialsProjection |
class |
AssumptionProjection
Term projection that delivers the assumptions of a taclet application
(the formulas that the \assumes clause of the taclet refers to).
|
class |
CoeffGcdProjection
Given a monomial and a polynomial, this projection computes the gcd of all
numerical coefficients.
|
class |
DividePolynomialsProjection |
class |
FocusFormulaProjection |
class |
FocusProjection
Projection of a rule application to its focus (the term or formula that the
rule operates on, that for taclets is described using
\find ,
and that can be modified by the rule). |
class |
MonomialColumnOp |
class |
ReduceMonomialsProjection
Projection for dividing one monomial by another.
|
class |
SubtermProjection
Projection for computing a subterm of a given term.
|
class |
SVInstantiationProjection
Projection of taclet apps to the instantiation of a schema variable.
|
class |
TermBuffer
Projection that can store and returns an arbitrary term or formula.
|
class |
TermConstructionProjection
Term projection for constructing a bigger term from a sequence of direct
subterms and an operator.
|
class |
TriggerVariableInstantiationProjection |
Modifier and Type | Field and Description |
---|---|
static ProjectionToTerm |
FocusProjection.INSTANCE |
static ProjectionToTerm |
FocusFormulaProjection.INSTANCE |
Modifier and Type | Method and Description |
---|---|
static ProjectionToTerm |
AssumptionProjection.create(int no) |
static ProjectionToTerm |
FocusProjection.create(int stepsUpwards) |
static ProjectionToTerm |
TermConstructionProjection.create(Operator op,
ProjectionToTerm[] subTerms) |
static ProjectionToTerm |
SubtermProjection.create(ProjectionToTerm completeTerm,
PosInTerm pit) |
static ProjectionToTerm |
MonomialColumnOp.create(ProjectionToTerm leftCoefficient,
ProjectionToTerm polynomial) |
static ProjectionToTerm |
CoeffGcdProjection.create(ProjectionToTerm monomialLeft,
ProjectionToTerm polynomialRight) |
static ProjectionToTerm |
ReduceMonomialsProjection.create(ProjectionToTerm dividend,
ProjectionToTerm divisor) |
static ProjectionToTerm |
DividePolynomialsProjection.createRoundingDown(ProjectionToTerm leftCoefficient,
ProjectionToTerm polynomial) |
static ProjectionToTerm |
DividePolynomialsProjection.createRoundingUp(ProjectionToTerm leftCoefficient,
ProjectionToTerm polynomial) |
Modifier and Type | Method and Description |
---|---|
static ProjectionToTerm |
TermConstructionProjection.create(Operator op,
ProjectionToTerm[] subTerms) |
static ProjectionToTerm |
SubtermProjection.create(ProjectionToTerm completeTerm,
PosInTerm pit) |
static ProjectionToTerm |
MonomialColumnOp.create(ProjectionToTerm leftCoefficient,
ProjectionToTerm polynomial) |
static ProjectionToTerm |
CoeffGcdProjection.create(ProjectionToTerm monomialLeft,
ProjectionToTerm polynomialRight) |
static ProjectionToTerm |
ReduceMonomialsProjection.create(ProjectionToTerm dividend,
ProjectionToTerm divisor) |
static ProjectionToTerm |
DividePolynomialsProjection.createRoundingDown(ProjectionToTerm leftCoefficient,
ProjectionToTerm polynomial) |
static ProjectionToTerm |
DividePolynomialsProjection.createRoundingUp(ProjectionToTerm leftCoefficient,
ProjectionToTerm polynomial) |
Constructor and Description |
---|
AbstractDividePolynomialsProjection(ProjectionToTerm leftCoefficient,
ProjectionToTerm polynomial) |
Copyright © 2003-2019 The KeY-Project.