Packages

case class ModSort(lower: IdealInt, upper: IdealInt) extends ProxySort with TheorySort with Product with Serializable

Modulo sorts, representing the interval [lower, upper] with wrap-around arithmetic.

Linear Supertypes
Serializable, Product, Equals, TheorySort, ProxySort, Sort, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. ModSort
  2. Serializable
  3. Product
  4. Equals
  5. TheorySort
  6. ProxySort
  7. Sort
  8. AnyRef
  9. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Instance Constructors

  1. new ModSort(lower: IdealInt, upper: IdealInt)

Value Members

  1. def all(f: (ITerm, ITerm, ITerm, ITerm, ITerm) => IFormula): IFormula

    Higher-order syntax for universal quantifiers.

    Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as Sort.all((a, b, c, d, e) => phi(a, b, c, d, e)).

    Definition Classes
    Sort
  2. def all(f: (ITerm, ITerm, ITerm, ITerm) => IFormula): IFormula

    Higher-order syntax for universal quantifiers.

    Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as Sort.all((a, b, c, d) => phi(a, b, c, d)).

    Definition Classes
    Sort
  3. def all(f: (ITerm, ITerm, ITerm) => IFormula): IFormula

    Higher-order syntax for universal quantifiers.

    Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as Sort.all((a, b, c) => phi(a, b, c)).

    Definition Classes
    Sort
  4. def all(f: (ITerm, ITerm) => IFormula): IFormula

    Higher-order syntax for universal quantifiers.

    Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as Sort.all((a, b) => phi(a, b)).

    Definition Classes
    Sort
  5. def all(f: (ITerm) => IFormula): IFormula

    Higher-order syntax for universal quantifiers.

    Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as Sort.all(a => phi(a)).

    Definition Classes
    Sort
  6. def all(f: IFormula): ISortedQuantified

    Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.

    Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.

    Definition Classes
    Sort
  7. val asTerm: Decoder[Option[ITerm]]

    Extract a term representation of some value in the sort.

    Extract a term representation of some value in the sort.

    Definition Classes
    Sort
  8. def augmentModelTermSet(model: Conjunction, assignment: Map[(IdealInt, Sort), ITerm], allTerms: Set[(IdealInt, Sort)], definedTerms: Set[(IdealInt, Sort)]): Unit

    Extract constructor terms from a model.

    Extract constructor terms from a model. Such terms will always be encoded as integers, and integers can have different meaning depending on the considered sort. Each sort can add the terms representing a model to the assignment map. Alternatively, a sort can add indexes to the definedTerms set to indicate a particular index is defined by a model, but the corresponding constructor term is not available yet because it refers to other terms that are not yet available.

    Definition Classes
    ProxySortSort
  9. def boundVariable(index: Int): IVariable

    The variable with given de Bruijn index and this sort.

    The variable with given de Bruijn index and this sort.

    Definition Classes
    Sort
  10. val cardinality: Option[IdealInt]

    The cardinality of sorts with fixed-size, finite domain.

    The cardinality of sorts with fixed-size, finite domain.

    Definition Classes
    ProxySortSort
  11. def decodeToTerm(d: IdealInt, assignment: Map[(IdealInt, Sort), ITerm]): Option[ITerm]

    Extract a term representation of some value in the sort.

    Extract a term representation of some value in the sort. This method can be overwritten in sub-classes to decode in a sort-specific way

    Definition Classes
    ModSortProxySortSort
  12. def eps(f: (ITerm) => IFormula): ISortedEpsilon

    Higher-order syntax for epsilon-expressions.

    Higher-order syntax for epsilon-expressions. This makes it possible to write things like Sort.eps(a => phi(a)).

    Definition Classes
    Sort
  13. def eps(f: IFormula): ISortedEpsilon

    Generate an epsilon-expression.

    Generate an epsilon-expression.

    Definition Classes
    Sort
  14. def ex(f: (ITerm, ITerm, ITerm, ITerm, ITerm) => IFormula): IFormula

    Higher-order syntax for existential quantifiers.

    Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as Sort.ex((a, b, c, d, e) => phi(a, b, c, d, e)).

    Definition Classes
    Sort
  15. def ex(f: (ITerm, ITerm, ITerm, ITerm) => IFormula): IFormula

    Higher-order syntax for existential quantifiers.

    Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as Sort.ex((a, b, c, d) => phi(a, b, c, d)).

    Definition Classes
    Sort
  16. def ex(f: (ITerm, ITerm, ITerm) => IFormula): IFormula

    Higher-order syntax for existential quantifiers.

    Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as Sort.ex((a, b, c) => phi(a, b, c)).

    Definition Classes
    Sort
  17. def ex(f: (ITerm, ITerm) => IFormula): IFormula

    Higher-order syntax for existential quantifiers.

    Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as Sort.ex((a, b) => phi(a, b)).

    Definition Classes
    Sort
  18. def ex(f: (ITerm) => IFormula): IFormula

    Higher-order syntax for existential quantifiers.

    Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as Sort.ex(a => phi(a)).

    Definition Classes
    Sort
  19. def ex(f: IFormula): ISortedQuantified

    Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.

    Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.

    Definition Classes
    Sort
  20. val individuals: Stream[ITerm]

    Terms representing elements of the sort.

    Terms representing elements of the sort.

    Definition Classes
    ModSortProxySortSort
  21. val lower: IdealInt
  22. def membershipConstraint(t: Term)(implicit order: TermOrder): Formula

    Constraints defining the range of the sort.

    Constraints defining the range of the sort.

    Definition Classes
    ProxySortSort
  23. val modulus: IdealInt
  24. val name: String
    Definition Classes
    ModSortProxySortSort
  25. def newConstant(name: String): ConstantTerm

    Allocation of a new constant with this sort.

    Allocation of a new constant with this sort.

    Definition Classes
    Sort
  26. def productElementNames: Iterator[String]
    Definition Classes
    Product
  27. val theory: ModuloArithmetic.type

    Query the theory that the sort belongs to.

    Query the theory that the sort belongs to.

    Definition Classes
    ModSortTheorySort
  28. def toString(): String
    Definition Classes
    Sort → AnyRef → Any
  29. val upper: IdealInt
  30. def witness: Option[ITerm]

    A witness term proving that the sort is inhabited.

    A witness term proving that the sort is inhabited.

    Definition Classes
    Sort