public abstract class ReducibleMonomialsFeature extends BinaryTacletAppFeature
dividendSV
can be made smaller
(in the polynomial reduction ordering) by adding or subtracting
divisorSV
Modifier and Type | Field and Description |
---|---|
private ProjectionToTerm |
dividend |
private ProjectionToTerm |
divisor |
TOP_COST, ZERO_COST
Modifier | Constructor and Description |
---|---|
private |
ReducibleMonomialsFeature(ProjectionToTerm dividend,
ProjectionToTerm divisor) |
Modifier and Type | Method and Description |
---|---|
protected abstract boolean |
checkReducibility(Monomial mDividend,
Monomial mDivisor) |
static Feature |
createDivides(ProjectionToTerm dividend,
ProjectionToTerm divisor) |
static Feature |
createReducible(ProjectionToTerm dividend,
ProjectionToTerm divisor) |
protected boolean |
filter(TacletApp app,
PosInOccurrence pos,
Goal goal)
Compute whether the result of the feature is zero (
true )
or infinity (false ) |
filter
computeCost
private final ProjectionToTerm dividend
private final ProjectionToTerm divisor
private ReducibleMonomialsFeature(ProjectionToTerm dividend, ProjectionToTerm divisor)
public static Feature createReducible(ProjectionToTerm dividend, ProjectionToTerm divisor)
public static Feature createDivides(ProjectionToTerm dividend, ProjectionToTerm divisor)
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 applied