de.uka.ilkd.key.logic

Class LexPathOrdering.Weighter

java.lang.Object

de.uka.ilkd.key.logic.LexPathOrdering.Weighter

Direct Known Subclasses:

LexPathOrdering.FunctionWeighter, LexPathOrdering.LiteralWeighter

Enclosing class:

LexPathOrdering

private abstract static class LexPathOrdering.Weighter
extends java.lang.Object

Base class for metrics on symbols that are used to construct an ordering

Constructor Summary

Constructors

Modifier	Constructor and Description
private	Weighter()

Method Summary

Modifier and Type	Method and Description
int	compareWeights(Operator p_a, Operator p_b) Compare the weights of two symbols using the function getWeight.
protected abstract java.lang.Integer	getWeight(Operator p_op)

Methods inherited from class java.lang.Object

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

Constructor Detail

Weighter

private Weighter()

Method Detail

compareWeights

public int compareWeights(Operator p_a,
                          Operator p_b)

Compare the weights of two symbols using the function getWeight.

Returns:

a number negative, zero or a number positive if the weight of p_a is less than, equal, or greater than the weight of p_b

getWeight

protected abstract java.lang.Integer getWeight(Operator p_op)