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

2.  case class CoeffMonomial(coeff: IdealInt, monomial: Monomial)(implicit ordering: MonomialOrdering) extends Product with Serializable
3.  class Gaussian extends AnyRef
4.  class GlexOrdering extends MonomialOrdering

   Graded Lexicographical ordering

5.  class GrevlexOrdering extends MonomialOrdering

   Graded Reverse Lexicographical ordering (Using the termOrdering!)

6.  case class Interval(lower: IntervalInt, upper: IntervalInt, gap: Option[(Int, Int)] = None) extends Product with Serializable
7.  case class IntervalException(smth: String) extends Exception with Product with Serializable
8.  abstract class IntervalInt extends AnyRef
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.

11.  case class IntervalVal(value: IdealInt) extends IntervalInt with Product with Serializable
12.  class LexOrdering extends MonomialOrdering
13.  class ListOrdering extends Ordering[ConstantTerm]
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