public class LiteralsSmallerThanFeature extends SmallerThanFeature
SmallerThanFeature.Collector
TOP_COST, ZERO_COST
Modifier and Type | Method and Description |
---|---|
protected boolean |
compareTerms(Term leftTerm,
Term rightTerm,
PosInOccurrence pos,
Goal goal) |
static Feature |
create(ProjectionToTerm left,
ProjectionToTerm right,
IntegerLDT numbers) |
protected boolean |
filter(TacletApp app,
PosInOccurrence pos,
Goal goal)
Compute whether the result of the feature is zero (
true )
or infinity (false ) |
protected boolean |
lessThan(Term t1,
Term t2,
PosInOccurrence focus,
Goal goal)
this overwrites the method of
SmallerThanFeature |
compare, lessThan
filter
computeCost
public static Feature create(ProjectionToTerm left, ProjectionToTerm right, IntegerLDT numbers)
protected boolean filter(TacletApp app, PosInOccurrence pos, Goal goal)
BinaryTacletAppFeature
true
)
or infinity (false
)filter
in class BinaryTacletAppFeature
app
- the TacletApppos
- position where app
is to be appliedgoal
- the goal on which app
is to be appliedprotected boolean compareTerms(Term leftTerm, Term rightTerm, PosInOccurrence pos, Goal goal)
protected boolean lessThan(Term t1, Term t2, PosInOccurrence focus, Goal goal)
SmallerThanFeature
lessThan
in class SmallerThanFeature
Copyright © 2003-2019 The KeY-Project.