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
The term order that cannot sort anything apart from
Constant.ONE
and variables
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 operations.
constantSeq
is the list of constants that are totally ordered by thisTermOrder
, starting with the biggest constant. In addition, variable terms are by default ordered as bigger as all constants. We use theList
datatype for the constant order, so that new large constants can efficiently be added.