de.uka.ilkd.key.logic

Class LexPathOrdering

java.lang.Object

de.uka.ilkd.key.logic.LexPathOrdering

All Implemented Interfaces:

TermOrdering

public class LexPathOrdering
extends java.lang.Object
implements TermOrdering

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	LexPathOrdering.CacheKey
private static class	LexPathOrdering.CompRes
private static class	LexPathOrdering.FunctionWeighter Explicit ordering for different kinds of function symbols; symbols like C:: or C.
private static class	LexPathOrdering.LiteralWeighter Explicit ordering of literals (symbols assigned a weight by this class are regarded as smaller than all other symbols)
private static class	LexPathOrdering.Weighter Base class for metrics on symbols that are used to construct an ordering

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.HashMap<LexPathOrdering.CacheKey,LexPathOrdering.CompRes>	cache
private static LexPathOrdering.CompRes	EQUALS
private LexPathOrdering.Weighter	functionWeighter
private static LexPathOrdering.CompRes	GREATER
private static LexPathOrdering.CompRes	LESS
private LexPathOrdering.Weighter	literalWeighter
private java.util.WeakHashMap<Sort,java.lang.Integer>	sortDepthCache Hashmap from Sort to Integer, storing the lengths of maximal paths from a sort to the top element of the sort lattice.
private static LexPathOrdering.CompRes	UNCOMPARABLE

Constructor Summary

Constructors

Constructor and Description
LexPathOrdering()

Method Summary

Modifier and Type	Method and Description
static int	compare(java.math.BigInteger a, java.math.BigInteger b) TODO: this should also be used when comparing terms The reduction ordering on integers that is described in "A critical-pair/completion algorithm for finitely generated ideals in rings", with the difference that positive numbers are here considered as smaller than negative numbers (with the same absolute value)
private int	compare(Operator aOp, Sort aSort, ImmutableArray<TermLabel> aLabels, Operator bOp, Sort bSort, ImmutableArray<TermLabel> bLabels) Compare the two given symbols
int	compare(Term p_a, Term p_b) Compare the two given terms
private LexPathOrdering.CompRes	compareHelp(Term p_a, Term p_b)
private LexPathOrdering.CompRes	compareHelp2(Term p_a, Term p_b)
private LexPathOrdering.CompRes	compareSubsLex(Term p_a, Term p_b)
static java.math.BigInteger	divide(java.math.BigInteger a, java.math.BigInteger c)
private int	getSortDepth(Sort s)
private int	getSortDepthHelp(Sort s)
private boolean	greaterThanSubs(Term p_a, Term p_b, int firstSub)
private boolean	isVar(Operator op)
private boolean	oneSubGeq(Term p_a, Term p_b)

Methods inherited from class java.lang.Object

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

Field Detail

UNCOMPARABLE

private static final LexPathOrdering.CompRes UNCOMPARABLE

EQUALS

private static final LexPathOrdering.CompRes EQUALS

GREATER

private static final LexPathOrdering.CompRes GREATER

LESS

private static final LexPathOrdering.CompRes LESS

cache

private final java.util.HashMap<LexPathOrdering.CacheKey,LexPathOrdering.CompRes> cache

sortDepthCache

private final java.util.WeakHashMap<Sort,java.lang.Integer> sortDepthCache

Hashmap from Sort to Integer, storing the lengths of maximal paths from a sort to the top element of the sort lattice.

literalWeighter

private final LexPathOrdering.Weighter literalWeighter

functionWeighter

private final LexPathOrdering.Weighter functionWeighter

Constructor Detail

LexPathOrdering

public LexPathOrdering()

Method Detail

compare

public int compare(Term p_a,
                   Term p_b)

Description copied from interface: TermOrdering

Compare the two given terms

Specified by:

compare in interface TermOrdering

Returns:

a number negative, zero or a number positive if p_a is less than, equal, or greater than p_b regarding the ordering given by the implementing class

compareHelp

private LexPathOrdering.CompRes compareHelp(Term p_a,
                                            Term p_b)

compareHelp2

private LexPathOrdering.CompRes compareHelp2(Term p_a,
                                             Term p_b)

compareSubsLex

private LexPathOrdering.CompRes compareSubsLex(Term p_a,
                                               Term p_b)

greaterThanSubs

private boolean greaterThanSubs(Term p_a,
                                Term p_b,
                                int firstSub)

oneSubGeq

private boolean oneSubGeq(Term p_a,
                          Term p_b)

compare

private int compare(Operator aOp,
                    Sort aSort,
                    ImmutableArray<TermLabel> aLabels,
                    Operator bOp,
                    Sort bSort,
                    ImmutableArray<TermLabel> bLabels)

Compare the two given symbols

Returns:

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

getSortDepth

private int getSortDepth(Sort s)

Returns:

the length of the longest path from s to the top element of the sort lattice. Probably this length is not computed correctly here, because the representation of sorts in key is completely messed up, but you get the idea

getSortDepthHelp

private int getSortDepthHelp(Sort s)

isVar

private boolean isVar(Operator op)

Returns:

true iff op is a logic variable

compare

public static int compare(java.math.BigInteger a,
                          java.math.BigInteger b)

TODO: this should also be used when comparing terms The reduction ordering on integers that is described in "A critical-pair/completion algorithm for finitely generated ideals in rings", with the difference that positive numbers are here considered as smaller than negative numbers (with the same absolute value)

Returns:

a negative number, zero, or a positive number, if a is smaller, equal to or greater than b

divide

public static java.math.BigInteger divide(java.math.BigInteger a,
                                          java.math.BigInteger c)

Returns:

the result of dividing a by c, such that the remainder becomes minimal in the reduction ordering LexPathOrdering.compare on integers