Represents a collection of polynomials
Graded Lexicographical ordering
Graded Reverse Lexicographical ordering (Using the termOrdering!)
Simple class to derive interval bounds for the constants in a proof goal
Main class for interval constraint propagation.
The pairs withing the list of a monomial are sorted in descending order (e.g.
The pairs withing the list of a monomial are sorted in descending order (e.g. [(z,3), (y,2), (x,1)] instead of [(x,1), (y,2), (z,3)] for "xyyzzz")
Monomial orderings
The ConstantTerms in list are given highest order according to the sorting of list.
The ConstantTerms in list are given highest order according to the sorting of list. Falling back on ordering if not found in list
INVARIANT: If t1 is before t2 in list, then t1 > t2
INVARIANT: If t1 is before t2 in list, then t1 > t2
TODO: Fix zero-polynomial representation
Implementation of a theory of non-linear integer arithmetic.
Implementation of a theory of non-linear integer arithmetic. Currently the theory does Groebner basis calculation followed by interval propagation.
ConstantTerm orderings
Represents a collection of polynomials
By keeping a map and a priorityqueue in parallel, the data structure supports: -- Finding the smallest element (keeping it ordered) -- Finding all polynomials with a LT containing some variables