| java.lang.Object de.uka.ilkd.key.strategy.feature.BinaryFeature de.uka.ilkd.key.strategy.feature.BinaryTacletAppFeature de.uka.ilkd.key.strategy.feature.PolynomialValuesCmpFeature
PolynomialValuesCmpFeature | abstract public class PolynomialValuesCmpFeature extends BinaryTacletAppFeature (Code) | | Return zero only if the value of one (left) polynomial always will be (less
or equal) or (less) than the value of a second (right) polynomial.
Both polynomials can optionally be multiplied with some constant before
comparison.
|
Method Summary | |
abstract protected boolean | compare(Polynomial leftPoly, Polynomial rightPoly) | public static Feature | divides(ProjectionToTerm left, ProjectionToTerm right) | public static Feature | divides(ProjectionToTerm left, ProjectionToTerm right, ProjectionToTerm leftCoeff, ProjectionToTerm rightCoeff) | public static Feature | eq(ProjectionToTerm left, ProjectionToTerm right) | public static Feature | eq(ProjectionToTerm left, ProjectionToTerm right, ProjectionToTerm leftCoeff, ProjectionToTerm rightCoeff) | protected boolean | filter(TacletApp app, PosInOccurrence pos, Goal goal) | public static Feature | leq(ProjectionToTerm left, ProjectionToTerm right) | public static Feature | leq(ProjectionToTerm left, ProjectionToTerm right, ProjectionToTerm leftCoeff, ProjectionToTerm rightCoeff) | public static Feature | lt(ProjectionToTerm left, ProjectionToTerm right) | public static Feature | lt(ProjectionToTerm left, ProjectionToTerm right, ProjectionToTerm leftCoeff, ProjectionToTerm rightCoeff) |
|
|