Sort

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 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.
abstract val cardinality: Option[IdealInt]

The cardinality of sorts with fixed-size, finite domain.
abstract def individuals: Stream[ITerm]

Terms representing elements of the sort.
abstract def membershipConstraint(t: Term)(implicit order: TermOrder): Formula

Constraints defining the range of the sort.
abstract val name: String

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)).
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)).
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)).
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)).
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)).
def all(f: IFormula): ISortedQuantified

Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.
final def asInstanceOf[T0]: T0

Definition Classes
Any
val asTerm: Decoder[Option[ITerm]]

Extract a term representation of some value in the sort.
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.
def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate() @throws( ... )
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
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)).
def eps(f: IFormula): ISortedEpsilon

Generate an epsilon-expression.
final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
def equals(arg0: Any): 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)).
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)).
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)).
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)).
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)).
def ex(f: IFormula): ISortedQuantified

Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.
final def getClass(): Class[_]

Definition Classes
AnyRef → Any
Annotations
@HotSpotIntrinsicCandidate()
def getSubTerms(ids: Seq[Term], sorts: Seq[Sort], terms: Map[(IdealInt, Sort), ITerm]): Either[Seq[ITerm], Seq[(IdealInt, Sort)]]

Attributes
protected
def hashCode(): Int

Definition Classes
AnyRef → Any
Annotations
@HotSpotIntrinsicCandidate()
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 this sort.
Allocation of a new constant with this sort.
final def notify(): Unit

Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate()
final def notifyAll(): Unit

Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate()
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( ... )
final def wait(arg0: Long): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
def witness: Option[ITerm]

A witness term proving that the sort is inhabited.

Deprecated Value Members

def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
Deprecated
(Since version ) see corresponding Javadoc for more information.

Related Docs: object Sort | package types

trait Sort extends AnyRef

Abstract Value Members

abstract def augmentModelTermSet(model: Conjunction, assignment: Map[(IdealInt, Sort), ITerm], allTerms: Set[(IdealInt, Sort)], definedTerms: Set[(IdealInt, Sort)]): Unit

abstract val cardinality: Option[IdealInt]

abstract def individuals: Stream[ITerm]

abstract def membershipConstraint(t: Term)(implicit order: TermOrder): Formula

abstract val name: String

Concrete Value Members

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

def all(f: (ITerm, ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

def all(f: (ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

def all(f: (ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

def all(f: (ITerm, ITerm) ⇒ IFormula): IFormula

def all(f: (ITerm) ⇒ IFormula): IFormula

def all(f: IFormula): ISortedQuantified

final def asInstanceOf[T0]: T0

val asTerm: Decoder[Option[ITerm]]

def boundVariable(index: Int): IVariable

def clone(): AnyRef

def decodeToTerm(d: IdealInt, assignment: Map[(IdealInt, Sort), ITerm]): Option[ITerm]

def eps(f: (ITerm) ⇒ IFormula): ISortedEpsilon

def eps(f: IFormula): ISortedEpsilon

final def eq(arg0: AnyRef): Boolean

def equals(arg0: Any): Boolean

def ex(f: (ITerm, ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

def ex(f: (ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

def ex(f: (ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

def ex(f: (ITerm, ITerm) ⇒ IFormula): IFormula

def ex(f: (ITerm) ⇒ IFormula): IFormula

def ex(f: IFormula): ISortedQuantified

final def getClass(): Class[_]

def getSubTerms(ids: Seq[Term], sorts: Seq[Sort], terms: Map[(IdealInt, Sort), ITerm]): Either[Seq[ITerm], Seq[(IdealInt, Sort)]]

def hashCode(): Int

final def isInstanceOf[T0]: Boolean

final def ne(arg0: AnyRef): Boolean

def newConstant(name: String): ConstantTerm

final def notify(): Unit

final def notifyAll(): Unit

final def synchronized[T0](arg0: ⇒ T0): T0

def toString(): String

final def wait(arg0: Long, arg1: Int): Unit

final def wait(arg0: Long): Unit

final def wait(): Unit

def witness: Option[ITerm]

Deprecated Value Members

def finalize(): Unit

Inherited from AnyRef

Inherited from Any

Ungrouped