public abstract class InEquationMultFeature extends BinaryTacletAppFeature
Modifier and Type | Field and Description |
---|---|
protected ProjectionToTerm |
mult1Candidate |
protected ProjectionToTerm |
mult2Candidate |
protected ProjectionToTerm |
targetCandidate |
TOP_COST, ZERO_COST
Modifier | Constructor and Description |
---|---|
protected |
InEquationMultFeature(ProjectionToTerm mult1Candidate,
ProjectionToTerm mult2Candidate,
ProjectionToTerm targetCandidate) |
Modifier and Type | Method and Description |
---|---|
static Feature |
exactlyBounded(ProjectionToTerm mult1Candidate,
ProjectionToTerm mult2Candidate,
ProjectionToTerm targetCandidate)
Return zero iff the product of mult1 and mult2 is target
|
protected abstract boolean |
filter(Monomial targetM,
Monomial mult1M,
Monomial mult2M) |
protected boolean |
filter(TacletApp app,
PosInOccurrence pos,
Goal goal)
Compute whether the result of the feature is zero (
true )
or infinity (false ) |
static Feature |
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 |
totallyBounded(ProjectionToTerm mult1Candidate,
ProjectionToTerm mult2Candidate,
ProjectionToTerm targetCandidate)
Return zero iff the product of mult1 and mult2 is a factor of target
|
filter
computeCost
protected final ProjectionToTerm targetCandidate
protected final ProjectionToTerm mult1Candidate
protected final ProjectionToTerm mult2Candidate
protected InEquationMultFeature(ProjectionToTerm mult1Candidate, ProjectionToTerm mult2Candidate, ProjectionToTerm targetCandidate)
public static Feature partiallyBounded(ProjectionToTerm mult1Candidate, ProjectionToTerm mult2Candidate, ProjectionToTerm targetCandidate)
mult1Candidate
- the left side of the first inequation to be multipliedmult2Candidate
- the left side of the second inequation to be multipliedtargetCandidate
- the left side of the inequation that is supposed to bound the
other two inequationspublic static Feature totallyBounded(ProjectionToTerm mult1Candidate, ProjectionToTerm mult2Candidate, ProjectionToTerm targetCandidate)
public static Feature exactlyBounded(ProjectionToTerm mult1Candidate, ProjectionToTerm mult2Candidate, ProjectionToTerm targetCandidate)
protected final 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