de.uka.ilkd.key.strategy.feature

Class InEquationMultFeature

java.lang.Object

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

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

de.uka.ilkd.key.strategy.feature.InEquationMultFeature

All Implemented Interfaces:

Feature

public abstract class InEquationMultFeature
extends BinaryTacletAppFeature

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.

Field Summary

Fields

Modifier and Type	Field and Description
protected ProjectionToTerm	mult1Candidate
protected ProjectionToTerm	mult2Candidate
protected ProjectionToTerm	targetCandidate

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

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	InEquationMultFeature(ProjectionToTerm mult1Candidate, ProjectionToTerm mult2Candidate, ProjectionToTerm targetCandidate)

Method Summary

Modifier and Type	Method and Description
static Feature	exactlyBounded(ProjectionToTerm mult1Candidate, ProjectionToTerm mult2Candidate, ProjectionToTerm targetCandidate) Return zero iff the product of mult1 and mult2 is target
protected abstract boolean	filter(Monomial targetM, Monomial mult1M, Monomial mult2M)
protected boolean	filter(TacletApp app, PosInOccurrence pos, Goal goal) Compute whether the result of the feature is zero (true) or infinity (false)
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.
static Feature	totallyBounded(ProjectionToTerm mult1Candidate, ProjectionToTerm mult2Candidate, ProjectionToTerm targetCandidate) Return zero iff the product of mult1 and mult2 is a factor of target

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

targetCandidate

protected final ProjectionToTerm targetCandidate

mult1Candidate

protected final ProjectionToTerm mult1Candidate

mult2Candidate

protected final ProjectionToTerm mult2Candidate

Constructor Detail

InEquationMultFeature

protected InEquationMultFeature(ProjectionToTerm mult1Candidate,
                                ProjectionToTerm mult2Candidate,
                                ProjectionToTerm targetCandidate)

Method Detail

partiallyBounded

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.

Parameters:

mult1Candidate - the left side of the first inequation to be multiplied

mult2Candidate - the left side of the second inequation to be multiplied

targetCandidate - the left side of the inequation that is supposed to bound the other two inequations

totallyBounded

public static Feature totallyBounded(ProjectionToTerm mult1Candidate,
                                     ProjectionToTerm mult2Candidate,
                                     ProjectionToTerm targetCandidate)

Return zero iff the product of mult1 and mult2 is a factor of target

exactlyBounded

public static Feature exactlyBounded(ProjectionToTerm mult1Candidate,
                                     ProjectionToTerm mult2Candidate,
                                     ProjectionToTerm targetCandidate)

Return zero iff the product of mult1 and mult2 is target

filter

protected final 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.

filter

protected abstract boolean filter(Monomial targetM,
                                  Monomial mult1M,
                                  Monomial mult2M)