public class LexPathOrdering extends java.lang.Object implements TermOrdering
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::
|
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
|
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 and Description |
---|
LexPathOrdering() |
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) |
private static final LexPathOrdering.CompRes UNCOMPARABLE
private static final LexPathOrdering.CompRes EQUALS
private static final LexPathOrdering.CompRes GREATER
private static final LexPathOrdering.CompRes LESS
private final java.util.HashMap<LexPathOrdering.CacheKey,LexPathOrdering.CompRes> cache
private final java.util.WeakHashMap<Sort,java.lang.Integer> sortDepthCache
Sort
to Integer
, storing the
lengths of maximal paths from a sort to the top element of the sort
lattice.private final LexPathOrdering.Weighter literalWeighter
private final LexPathOrdering.Weighter functionWeighter
public int compare(Term p_a, Term p_b)
TermOrdering
compare
in interface TermOrdering
p_a
is less than, equal, or greater than
p_b
regarding the ordering given by the
implementing classprivate 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)
private int compare(Operator aOp, Sort aSort, ImmutableArray<TermLabel> aLabels, Operator bOp, Sort bSort, ImmutableArray<TermLabel> bLabels)
p_a
is less than, equal, or greater than p_b
private int getSortDepth(Sort s)
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 ideaprivate int getSortDepthHelp(Sort s)
private boolean isVar(Operator op)
op
is a logic variablepublic static int compare(java.math.BigInteger a, java.math.BigInteger b)
a
is smaller, equal to or greater than b
public static java.math.BigInteger divide(java.math.BigInteger a, java.math.BigInteger c)
a
by c
,
such that the remainder becomes minimal in the reduction ordering
LexPathOrdering.compare
on integers