| java.lang.Object
 de.uka.ilkd.key.strategy.feature.BinaryFeature
de.uka.ilkd.key.strategy.feature.BinaryTacletAppFeature
de.uka.ilkd.key.strategy.feature.InEquationMultFeature
| InEquationMultFeature | | abstract public class InEquationMultFeature extends BinaryTacletAppFeature (Code) | | Feature that decides whether the multiplication of two inequations (using
rules of set inEqSimp_nonLin_multiply) is allowed. We only do this if the
product of the left sides of the inequations has factors in common with the
left side of some other inequation, similarly to how it is decided in the
Buchberger algorithm.
|
| Method Summary | |
| public static Feature | exactlyBounded(ProjectionToTerm mult1Candidate, ProjectionToTerm mult2Candidate, ProjectionToTerm targetCandidate)
| | final protected boolean | filter(TacletApp app, PosInOccurrence pos, Goal goal)
| | abstract protected boolean | filter(Monomial targetM, Monomial mult1M, Monomial mult2M)
| | public 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. | | public static Feature | totallyBounded(ProjectionToTerm mult1Candidate, ProjectionToTerm mult2Candidate, ProjectionToTerm targetCandidate)
|
| partiallyBounded | | public static Feature partiallyBounded(ProjectionToTerm mult1Candidate, ProjectionToTerm mult2Candidate, ProjectionToTerm targetCandidate)(Code) | | Return zero iff the multiplication of mult1 and mult2 is allowed,
because the resulting product is partially covered by target.
Parameters:
mult1Candidate - the left side of the first inequation to be multiplied
Parameters:
mult2Candidate - the left side of the second inequation to be multiplied
Parameters:
targetCandidate - the left side of the inequation that is supposed to bound theother two inequations |
|
|