de.uka.ilkd.key.strategy.feature

Class ReducibleMonomialsFeature

java.lang.Object

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

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

de.uka.ilkd.key.strategy.feature.ReducibleMonomialsFeature

All Implemented Interfaces:

Feature

public abstract class ReducibleMonomialsFeature
extends BinaryTacletAppFeature

Return zero iff the monomial dividendSV can be made smaller (in the polynomial reduction ordering) by adding or subtracting divisorSV

Field Summary

Fields

Modifier and Type	Field and Description
private ProjectionToTerm	dividend
private ProjectionToTerm	divisor

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

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
private	ReducibleMonomialsFeature(ProjectionToTerm dividend, ProjectionToTerm divisor)

Method Summary

Modifier and Type	Method and Description
protected abstract boolean	checkReducibility(Monomial mDividend, Monomial mDivisor)
static Feature	createDivides(ProjectionToTerm dividend, ProjectionToTerm divisor)
static Feature	createReducible(ProjectionToTerm dividend, ProjectionToTerm divisor)
protected boolean	filter(TacletApp app, PosInOccurrence pos, Goal goal) Compute whether the result of the feature is zero (true) or infinity (false)

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

dividend

private final ProjectionToTerm dividend

divisor

private final ProjectionToTerm divisor

Constructor Detail

ReducibleMonomialsFeature

private ReducibleMonomialsFeature(ProjectionToTerm dividend,
                                  ProjectionToTerm divisor)

Method Detail

createReducible

public static Feature createReducible(ProjectionToTerm dividend,
                                      ProjectionToTerm divisor)

createDivides

public static Feature createDivides(ProjectionToTerm dividend,
                                    ProjectionToTerm divisor)

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.

checkReducibility

protected abstract boolean checkReducibility(Monomial mDividend,
                                             Monomial mDivisor)