 # nia

Visibility
1. Public
2. All

### Type Members

1. #### class Basis extends AnyRef

Represents a collection of polynomials

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

5. #### class GrevlexOrdering extends MonomialOrdering

Graded Reverse Lexicographical ordering (Using the termOrdering!)

9. #### class IntervalPropagator extends AnyRef

Simple class to derive interval bounds for the constants in a proof goal

10. #### class IntervalSet extends AnyRef

Main class for interval constraint propagation.

14. #### case class Monomial(pairs: PairList)(implicit ordering: MonomialOrdering) extends Product with Serializable

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")

15. #### abstract class MonomialOrdering extends Ordering[Monomial]

Monomial orderings

16. #### class PartitionOrdering extends MonomialOrdering

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

17. #### case class Polynomial(terms: CoeffMonomialList)(implicit ordering: MonomialOrdering = new DegenOrdering) extends Product with Serializable

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

### Value Members

2. #### object GroebnerMultiplication extends MulTheory

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.

11. #### object StringOrdering extends Ordering[ConstantTerm]

ConstantTerm orderings