de.uka.ilkd.key.strategy.feature

Class MonomialsSmallerThanFeature

java.lang.Object

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

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

de.uka.ilkd.key.strategy.feature.SmallerThanFeature

de.uka.ilkd.key.strategy.feature.AbstractMonomialSmallerThanFeature

de.uka.ilkd.key.strategy.feature.MonomialsSmallerThanFeature

All Implemented Interfaces:

Feature

public class MonomialsSmallerThanFeature
extends AbstractMonomialSmallerThanFeature

Feature that returns zero iff each monomial of one polynomial is smaller than all monomials of a second polynomial

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	MonomialsSmallerThanFeature.MonomialCollector

Nested classes/interfaces inherited from class de.uka.ilkd.key.strategy.feature.SmallerThanFeature

SmallerThanFeature.Collector

Field Summary

Fields

Modifier and Type	Field and Description
private Function	add
private TermFeature	hasCoeff
private ProjectionToTerm	left
private Function	mul
private ProjectionToTerm	right
private Function	Z

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

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
private	MonomialsSmallerThanFeature(ProjectionToTerm left, ProjectionToTerm right, IntegerLDT numbers)

Method Summary

Modifier and Type	Method and Description
private int	compareLexNewSyms(ImmutableList<Term> atoms1, ImmutableList<Term> atoms2, Goal goal)
static Feature	create(ProjectionToTerm left, ProjectionToTerm right, IntegerLDT numbers)
(package private) static TermFeature	createHasCoeffTermFeature(IntegerLDT numbers)
private int	degree(Term t)
protected boolean	filter(TacletApp app, PosInOccurrence pos, Goal goal) Compute whether the result of the feature is zero (true) or infinity (false)
protected boolean	lessThan(Term t1, Term t2, PosInOccurrence focus, Goal goal) this overwrites the method of SmallerThanFeature

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

collectAtoms, introductionTime

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

compare, lessThan

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

hasCoeff

private final TermFeature hasCoeff

left

private final ProjectionToTerm left

right

private final ProjectionToTerm right

Z

private final Function Z

mul

private final Function mul

add

private final Function add

Constructor Detail

MonomialsSmallerThanFeature

private MonomialsSmallerThanFeature(ProjectionToTerm left,
                                    ProjectionToTerm right,
                                    IntegerLDT numbers)

Method Detail

createHasCoeffTermFeature

static TermFeature createHasCoeffTermFeature(IntegerLDT numbers)

create

public static Feature create(ProjectionToTerm left,
                             ProjectionToTerm right,
                             IntegerLDT numbers)

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.

lessThan

protected boolean lessThan(Term t1,
                           Term t2,
                           PosInOccurrence focus,
                           Goal goal)

this overwrites the method of SmallerThanFeature

Overrides:

lessThan in class SmallerThanFeature

compareLexNewSyms

private int compareLexNewSyms(ImmutableList<Term> atoms1,
                              ImmutableList<Term> atoms2,
                              Goal goal)

degree

private int degree(Term t)

Returns:

the degree of a monomial (number of terms that are connected multiplicatively) -1. To ensure that also cases like f(a*b)=a*b are handled properly, we simply count the total number of multiplication operators in the term.