public class LiteralsSmallerThanFeature extends SmallerThanFeature
Modifier and Type | Class and Description |
---|---|
private class |
LiteralsSmallerThanFeature.LiteralCollector |
private class |
LiteralsSmallerThanFeature.MonomialIterator |
SmallerThanFeature.Collector
Modifier and Type | Field and Description |
---|---|
private ProjectionToTerm |
left |
private IntegerLDT |
numbers |
private QuanEliminationAnalyser |
quanAnalyser |
private ProjectionToTerm |
right |
TOP_COST, ZERO_COST
Modifier | Constructor and Description |
---|---|
private |
LiteralsSmallerThanFeature(ProjectionToTerm left,
ProjectionToTerm right,
IntegerLDT numbers) |
Modifier and Type | Method and Description |
---|---|
private int |
comparePolynomials(Term t1,
Term t2) |
protected boolean |
compareTerms(Term leftTerm,
Term rightTerm,
PosInOccurrence pos,
Goal goal) |
static Feature |
create(ProjectionToTerm left,
ProjectionToTerm right,
IntegerLDT numbers) |
private Term |
discardNegation(Term t) |
protected boolean |
filter(TacletApp app,
PosInOccurrence pos,
Goal goal)
Compute whether the result of the feature is zero (
true )
or infinity (false ) |
private int |
formulaKind(Term t) |
private boolean |
isBinaryIntRelation(Term t) |
protected boolean |
lessThan(Term t1,
Term t2,
PosInOccurrence focus,
Goal goal)
this overwrites the method of
SmallerThanFeature |
compare, lessThan
filter
computeCost
private final ProjectionToTerm left
private final ProjectionToTerm right
private final IntegerLDT numbers
private final QuanEliminationAnalyser quanAnalyser
private LiteralsSmallerThanFeature(ProjectionToTerm left, ProjectionToTerm right, IntegerLDT numbers)
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
private boolean isBinaryIntRelation(Term t)
private int formulaKind(Term t)