public abstract class PolynomialValuesCmpFeature extends BinaryTacletAppFeature
TOP_COST, ZERO_COST
Modifier | Constructor and Description |
---|---|
protected |
PolynomialValuesCmpFeature(ProjectionToTerm left,
ProjectionToTerm right,
ProjectionToTerm leftCoeff,
ProjectionToTerm rightCoeff) |
filter
computeCost
protected PolynomialValuesCmpFeature(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)
public static Feature leq(ProjectionToTerm left, ProjectionToTerm right)
public static Feature leq(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)
public static Feature divides(ProjectionToTerm left, ProjectionToTerm right)
public static Feature divides(ProjectionToTerm left, ProjectionToTerm right, ProjectionToTerm leftCoeff, ProjectionToTerm rightCoeff)
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 abstract boolean compare(Polynomial leftPoly, Polynomial rightPoly)
Copyright © 2003-2019 The KeY-Project.