Package

ap.theories

nia

Permalink

package nia

Visibility
  1. Public
  2. All

Type Members

  1. class Basis extends AnyRef

    Permalink

    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

    Permalink
  3. class Gaussian extends AnyRef

    Permalink
  4. class GlexOrdering extends MonomialOrdering

    Permalink

    Graded Lexicographical ordering

  5. class GrevlexOrdering extends MonomialOrdering

    Permalink

    Graded Reverse Lexicographical ordering (Using the termOrdering!)

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

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

    Permalink
  8. abstract class IntervalInt extends AnyRef

    Permalink
  9. class IntervalPropagator extends AnyRef

    Permalink

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

  10. class IntervalSet extends AnyRef

    Permalink

    Main class for interval constraint propagation.

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

    Permalink
  12. class LexOrdering extends MonomialOrdering

    Permalink
  13. class ListOrdering extends Ordering[ConstantTerm]

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

    Permalink

    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]

    Permalink

    Monomial orderings

  16. class PartitionOrdering extends MonomialOrdering

    Permalink

    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

    Permalink

    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

  1. object Gaussian

    Permalink
  2. object GroebnerMultiplication extends MulTheory

    Permalink

    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.

  3. object InconsistentIntervalsException extends IntervalException

    Permalink
  4. object Interval extends Serializable

    Permalink
  5. object IntervalNegInf extends IntervalInt with Product with Serializable

    Permalink
  6. object IntervalPosInf extends IntervalInt with Product with Serializable

    Permalink
  7. object IntervalPropagator

    Permalink
  8. object Monomial extends Serializable

    Permalink
  9. object PartitionOrdering extends Serializable

    Permalink
  10. object Polynomial extends Serializable

    Permalink
  11. object StringOrdering extends Ordering[ConstantTerm]

    Permalink

    ConstantTerm orderings

Ungrouped