de.uka.ilkd.key.strategy.feature

Class SortComparisonFeature

java.lang.Object

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

de.uka.ilkd.key.strategy.feature.SortComparisonFeature

All Implemented Interfaces:

Feature

public class SortComparisonFeature
extends BinaryFeature

Field Summary

Fields

Modifier and Type	Field and Description
private int	comparator
private ProjectionToTerm	s1
private ProjectionToTerm	s2
static int	SUBSORT

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

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
private	SortComparisonFeature(ProjectionToTerm s1, ProjectionToTerm s2, int comparator) creates a new comparision term feature

Method Summary

Modifier and Type	Method and Description
protected boolean	compare(Sort sort1, Sort sort2)
static Feature	create(ProjectionToTerm s1, ProjectionToTerm s2, int cmp)
protected boolean	filter(RuleApp 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.BinaryFeature

computeCost

Methods inherited from class java.lang.Object

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

Field Detail

SUBSORT

public static final int SUBSORT

See Also:

Constant Field Values

s1

private final ProjectionToTerm s1

s2

private final ProjectionToTerm s2

comparator

private final int comparator

Constructor Detail

SortComparisonFeature

private SortComparisonFeature(ProjectionToTerm s1,
                              ProjectionToTerm s2,
                              int comparator)

creates a new comparision term feature

Method Detail

create

public static Feature create(ProjectionToTerm s1,
                             ProjectionToTerm s2,
                             int cmp)

filter

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

Description copied from class: BinaryFeature

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

Specified by:

filter in class BinaryFeature

Parameters:

app - the RuleApp

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 boolean compare(Sort sort1,
                          Sort sort2)

Parameters:

sort1 -

sort2 -