Ordering on atoms that lists large atoms last
Ordering on terms that lists large terms last
Determine whether this term order does not consider any constants as bigger than the given constants
Extend this ordering by inserting a further constant newConst
.
Extend this ordering by inserting a further constant newConst
.
This constant is inserted so that it gets as big as possible, but such that
it is smaller than all constants of the set biggerConstants
Extend this ordering by inserting further predicate newPreds
.
Extend this ordering by inserting further predicate newPreds
.
The predicates are inserted so that they get as big as possible
Extend this ordering by inserting a further predicate newPred
.
Extend this ordering by inserting a further predicate newPred
.
This predicate is inserted so that it gets as big as possible
Assuming that seq
is a sequence of linear combinations
sorted in descending order according to this
TermOrder
, find the index of the first element whose
leading term could be lt
Assuming that seq
is a sequence of linear combinations
sorted in descending order according to this
TermOrder
, find the index of the first element whose
leading term could be lt
Test whether x
is sorting by this TermOrder
, or
return true
if x
is not a sorted entity
Test whether x
is sorting by this TermOrder
, or
return true
if x
is not a sorted entity
Return true
iff the term order that
is an
extension of the order this
considering only the constants
consideredConstants
.
Return true
iff the term order that
is an
extension of the order this
considering only the constants
consideredConstants
. I.e., this
restricted to
the constants in consideredConstants
is a suborder of
that
.
Return true
iff the term order that
is an
extension of the order this
, i.e., when restricted to the
constants that are ordered by this
it describes the same
order.
Return true
iff the term order that
is an
extension of the order this
, i.e., when restricted to the
constants that are ordered by this
it describes the same
order.
Ordering on linear combinations that lists large linear combinations last
Change this ordering by making the constant const
as big as
possible, but still smaller than all constants of the set
biggerConstants
Change this ordering by making the constant const
as big as
possible, but still smaller than all constants of the set
biggerConstants
Return the set of all constants that are sorted by this
TermOrder
Return the set of all constants that are sorted by this
TermOrder
Return the set of all predicates that are sorted by this
TermOrder
Return the set of all predicates that are sorted by this
TermOrder
Ordering on predicates that lists large predicates last
Generate a new TermOrder
that coincides with this one, except
that all predicates have been removed
Generate a new TermOrder
that coincides with this one, except
that all predicates have been removed
Restrict this ordering to the given symbols
Ordering on atoms that lists large atoms first
Ordering on linear combinations that lists large linear combinations first
Ordering on predicates that lists large predicates first
Ordering on terms that lists large terms first
Sort the given constants in ascending order
Sort the given constants in ascending order
If x
is a sorted entity, sort it by this
TermOrder
, or otherwise return the unchanged x
If x
is a sorted entity, sort it by this
TermOrder
, or otherwise return the unchanged x
Sort the given predicates in ascending order
Ordering on terms that lists large terms last