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.
- Alphabetic
- By Inheritance
- ModSort
- Serializable
- Product
- Equals
- TheorySort
- ProxySort
- Sort
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Value Members
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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 thedefinedTerms
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. - 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
- val cardinality: Option[IdealInt]
The cardinality of sorts with fixed-size, finite domain.
- def decodeToTerm(d: IdealInt, assignment: Map[(IdealInt, Sort), ITerm]): Option[ITerm]
Extract a term representation of some value in the sort.
- 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
- def eps(f: IFormula): ISortedEpsilon
Generate an epsilon-expression.
Generate an epsilon-expression.
- Definition Classes
- Sort
- 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
- 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
- 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
- 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
- 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
- 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
- val individuals: Stream[ITerm]
Terms representing elements of the sort.
- val lower: IdealInt
- def membershipConstraint(t: Term)(implicit order: TermOrder): Formula
Constraints defining the range of the sort.
- val modulus: IdealInt
- val name: String
- def newConstant(name: String): ConstantTerm
Allocation of a new constant with
this
sort.Allocation of a new constant with
this
sort.- Definition Classes
- Sort
- def productElementNames: Iterator[String]
- Definition Classes
- Product
- val theory: ModuloArithmetic.type
Query the theory that the sort belongs to.
Query the theory that the sort belongs to.
- Definition Classes
- ModSort → TheorySort
- def toString(): String
- Definition Classes
- Sort → AnyRef → Any
- val upper: IdealInt
- 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