de.uka.ilkd.key.strategy.feature

Class SmallerThanFeature

java.lang.Object

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

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

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

All Implemented Interfaces:

Feature

Direct Known Subclasses:

AbstractMonomialSmallerThanFeature, ClausesSmallerThanFeature, LiteralsSmallerThanFeature, SetsSmallerThanFeature, TermSmallerThanFeature

public abstract class SmallerThanFeature
extends BinaryTacletAppFeature

Abstract superclass for features comparing terms (in particular polynomials or monomials) using the term ordering

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
protected static class	SmallerThanFeature.Collector

Field Summary

Fields

Modifier and Type	Field and Description
private TermOrdering	termOrdering

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

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Constructor and Description
SmallerThanFeature()

Method Summary

Modifier and Type	Method and Description
protected int	compare(Term t1, Term t2)
protected boolean	lessThan(ImmutableList<Term> list1, ImmutableList<Term> list2, PosInOccurrence focus, Goal currentGoal)
protected boolean	lessThan(Term t1, Term t2, PosInOccurrence focus, Goal currentGoal)

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

filter, 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

termOrdering

private final TermOrdering termOrdering

Constructor Detail

SmallerThanFeature

public SmallerThanFeature()

Method Detail

lessThan

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

compare

protected final int compare(Term t1,
                            Term t2)

lessThan

protected final boolean lessThan(ImmutableList<Term> list1,
                                 ImmutableList<Term> list2,
                                 PosInOccurrence focus,
                                 Goal currentGoal)

Returns:

true iff each element of list1 is strictly smaller than all elements of list2