public class LexPathOrdering extends java.lang.Object implements TermOrdering
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)
|
int |
compare(Term p_a,
Term p_b)
Compare the two given terms
|
static java.math.BigInteger |
divide(java.math.BigInteger a,
java.math.BigInteger c) |
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 classpublic 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 integersCopyright © 2003-2019 The KeY-Project.