trait TheorySort extends Sort
Trait for sorts that belong to a specific theory.
- Alphabetic
- By Inheritance
- TheorySort
- Sort
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Abstract Value Members
- abstract 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
assignmentmap. Alternatively, a sort can add indexes to thedefinedTermsset 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
- Sort
- abstract val cardinality: Option[IdealInt]
The cardinality of sorts with fixed-size, finite domain.
The cardinality of sorts with fixed-size, finite domain.
- Definition Classes
- Sort
- abstract def individuals: Stream[ITerm]
Terms representing elements of the sort.
Terms representing elements of the sort.
- Definition Classes
- Sort
- abstract def membershipConstraint(t: Term)(implicit order: TermOrder): Formula
Constraints defining the range of the sort.
Constraints defining the range of the sort.
- Definition Classes
- Sort
- abstract val name: String
- Definition Classes
- Sort
- abstract def theory: Theory
Query the theory that the sort belongs to.
Concrete Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- 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
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- 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 boundVariable(index: Int): IVariable
The variable with given de Bruijn index and
thissort.The variable with given de Bruijn index and
thissort.- Definition Classes
- Sort
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- 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
- 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
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- 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
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def getSubTerms(ids: Seq[Term], sorts: Seq[Sort], terms: Map[(IdealInt, Sort), ITerm]): Either[Seq[ITerm], Seq[(IdealInt, Sort)]]
- Attributes
- protected
- Definition Classes
- Sort
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def newConstant(name: String): ConstantTerm
Allocation of a new constant with
thissort.Allocation of a new constant with
thissort.- Definition Classes
- Sort
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- Sort → AnyRef → Any
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- 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
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)