Trait for classes providing term alias information.
Trait that can be used to track the computation taking place in systems of equations, inequalities, etc.
Class for representing constants.
Class for representing constants. This is not a case class, two constants are the same iff the object that they are represented by are the same.
Various infix operators terms and linear combinations
Various functions to work with vectors of terms
A few functions to work with predicates
Trait for objects that can be sorted by a TermOrder
.
Trait for objects that can be sorted by a TermOrder
. It is a
design decision that the used order cannot be queried from an object (so that
it must not be stored in the object). It can be checked whether an object is
consistent with a certain given order, however.
Extension of Sorted
where also the actual TermOrder
can be queried
Extension of Sorted
where also the actual TermOrder
can be queried
Some methods for generating random conjunctions
Enumeration to represent whether two terms cannot, may, or must have the same value.
Enumeration to represent whether two terms cannot, may, or must have
the same value. The value CannotDueToFreedom
expresses that
the free-constant heuristic tells that the terms can be assumed to be
different
The term representing the literal 1
Collection of functions that makes it easier to use the term/formula datastructures by adding lots of syntactic sugar
Class for representing total orderings on constants (and variables), and their extension to arbitrary terms.
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
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.
Trait that can be used to track the computation taking place in systems of equations, inequalities, etc. This is used to produce proofs.