Class for representing total orderings on constants (and variables), and
their extension to arbitrary terms. For the time being, we do not consider
arbitrary (non-nullary) functions apart from the pre-defined arithmetic
constantSeq is the list of constants that are totally ordered by
this TermOrder, starting with the biggest constant. In
addition, variable terms are by default ordered as bigger as all constants.
We use the List datatype for the constant order, so that new
large constants can efficiently be added.
Weight objects that are used to abstract from the concrete terms.
Weight objects that are used to abstract from the concrete terms. There are
three types of weights: for variables, and for constants, and for the
literal 1. Variables are heavier that constants are heavier than literals.
The term order that cannot sort anything apart from
Constant.ONE and variables