de.uka.ilkd.key.strategy.feature

Class PolynomialValuesCmpFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.BinaryFeature

de.uka.ilkd.key.strategy.feature.BinaryTacletAppFeature

de.uka.ilkd.key.strategy.feature.PolynomialValuesCmpFeature

All Implemented Interfaces:

Feature

public abstract class PolynomialValuesCmpFeature
extends BinaryTacletAppFeature

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.

Field Summary

Fields

Modifier and Type	Field and Description
private ProjectionToTerm	left
private ProjectionToTerm	leftCoeff
private ProjectionToTerm	right
private ProjectionToTerm	rightCoeff

Fields inherited from class de.uka.ilkd.key.strategy.feature.BinaryFeature

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	PolynomialValuesCmpFeature(ProjectionToTerm left, ProjectionToTerm right, ProjectionToTerm leftCoeff, ProjectionToTerm rightCoeff)

Method Summary

Modifier and Type	Method and Description
protected abstract boolean	compare(Polynomial leftPoly, Polynomial rightPoly)
static Feature	divides(ProjectionToTerm left, ProjectionToTerm right)
static Feature	divides(ProjectionToTerm left, ProjectionToTerm right, ProjectionToTerm leftCoeff, ProjectionToTerm rightCoeff)
static Feature	eq(ProjectionToTerm left, ProjectionToTerm right)
static Feature	eq(ProjectionToTerm left, ProjectionToTerm right, ProjectionToTerm leftCoeff, ProjectionToTerm rightCoeff)
protected boolean	filter(TacletApp app, PosInOccurrence pos, Goal goal) Compute whether the result of the feature is zero (true) or infinity (false)
private Polynomial	getPolynomial(ProjectionToTerm polyProj, ProjectionToTerm coeffProj, TacletApp app, PosInOccurrence pos, Goal goal)
static Feature	leq(ProjectionToTerm left, ProjectionToTerm right)
static Feature	leq(ProjectionToTerm left, ProjectionToTerm right, ProjectionToTerm leftCoeff, ProjectionToTerm rightCoeff)
static Feature	lt(ProjectionToTerm left, ProjectionToTerm right)
static Feature	lt(ProjectionToTerm left, ProjectionToTerm right, ProjectionToTerm leftCoeff, ProjectionToTerm rightCoeff)

Methods inherited from class de.uka.ilkd.key.strategy.feature.BinaryTacletAppFeature

filter

Methods inherited from class de.uka.ilkd.key.strategy.feature.BinaryFeature

computeCost

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

left

private final ProjectionToTerm left

right

private final ProjectionToTerm right

leftCoeff

private final ProjectionToTerm leftCoeff

rightCoeff

private final ProjectionToTerm rightCoeff

Constructor Detail

PolynomialValuesCmpFeature

protected PolynomialValuesCmpFeature(ProjectionToTerm left,
                                     ProjectionToTerm right,
                                     ProjectionToTerm leftCoeff,
                                     ProjectionToTerm rightCoeff)

Method Detail

lt

public static Feature lt(ProjectionToTerm left,
                         ProjectionToTerm right)

lt

public static Feature lt(ProjectionToTerm left,
                         ProjectionToTerm right,
                         ProjectionToTerm leftCoeff,
                         ProjectionToTerm rightCoeff)

leq

public static Feature leq(ProjectionToTerm left,
                          ProjectionToTerm right)

leq

public static Feature leq(ProjectionToTerm left,
                          ProjectionToTerm right,
                          ProjectionToTerm leftCoeff,
                          ProjectionToTerm rightCoeff)

eq

public static Feature eq(ProjectionToTerm left,
                         ProjectionToTerm right)

eq

public static Feature eq(ProjectionToTerm left,
                         ProjectionToTerm right,
                         ProjectionToTerm leftCoeff,
                         ProjectionToTerm rightCoeff)

divides

public static Feature divides(ProjectionToTerm left,
                              ProjectionToTerm right)

divides

public static Feature divides(ProjectionToTerm left,
                              ProjectionToTerm right,
                              ProjectionToTerm leftCoeff,
                              ProjectionToTerm rightCoeff)

filter

protected boolean filter(TacletApp app,
                         PosInOccurrence pos,
                         Goal goal)

Description copied from class: BinaryTacletAppFeature

Compute whether the result of the feature is zero (true) or infinity (false)

Specified by:

filter in class BinaryTacletAppFeature

Parameters:

app - the TacletApp

pos - position where app is to be applied

goal - the goal on which app is to be applied

Returns:

true iff the the result of the feature is supposed to be zero.

compare

protected abstract boolean compare(Polynomial leftPoly,
                                   Polynomial rightPoly)

getPolynomial

private Polynomial getPolynomial(ProjectionToTerm polyProj,
                                 ProjectionToTerm coeffProj,
                                 TacletApp app,
                                 PosInOccurrence pos,
                                 Goal goal)