nia

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. class BufferingIntervalStore extends IntervalStore

   

3. case class CoeffMonomial(coeff: IdealInt, monomial: Monomial)(implicit ordering: MonomialOrdering) extends Product with Serializable

   

4. class Gaussian extends AnyRef

   

5. class GlexOrdering extends MonomialOrdering

   

   Graded Lexicographical ordering

6. class GrevlexOrdering extends MonomialOrdering

   

   Graded Reverse Lexicographical ordering (Using the termOrdering!)

7. case class Interval(lower: IntervalInt, upper: IntervalInt, gap: Option[(IdealInt, IdealInt)] = None) extends Product with Serializable

   

8. case class IntervalException(smth: String) extends Exception with Product with Serializable

   

9. abstract class IntervalInt extends AnyRef

   

10. class IntervalPropagator extends AnyRef

    

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

11. class IntervalSet extends AnyRef

    

    Main class for interval constraint propagation.

12. trait IntervalStore extends AnyRef

    

13. case class IntervalVal(value: IdealInt) extends IntervalInt with Product with Serializable

    

14. class LexOrdering extends MonomialOrdering

    

15. class ListOrdering extends Ordering[ConstantTerm]

    

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

17. abstract class MonomialOrdering extends Ordering[Monomial]

    

    Monomial orderings

18. class NIASplitter extends TheoryProcedure

    

    Splitter handles the splitting when no new information can be deduced

19. 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

20. 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