# UninterpretedSort

### Related Doc: package UninterpretedSortTheory

#### class UninterpretedSort extends Sort

Linear Supertypes
Sort, AnyRef, Any
Ordering
1. Alphabetic
2. By inheritance
Inherited
1. UninterpretedSort
2. Sort
3. AnyRef
4. Any
1. Hide All
2. Show all
Visibility
1. Public
2. All

### Instance Constructors

1. #### new UninterpretedSort(name: String, theory: UninterpretedSortTheory)

Attributes
protected[ap.types]

### Value Members

1. #### final def !=(arg0: Any): Boolean

Definition Classes
AnyRef → Any
2. #### final def ##(): Int

Definition Classes
AnyRef → Any
3. #### final def ==(arg0: Any): Boolean

Definition Classes
AnyRef → Any
4. #### 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
5. #### 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
6. #### 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
7. #### 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
8. #### 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
9. #### 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
10. #### final def asInstanceOf[T0]: T0

Definition Classes
Any
11. #### 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
12. #### 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
UninterpretedSortSort
13. #### 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
14. #### val cardinality: Option[IdealInt]

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

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

Definition Classes
UninterpretedSortSort
15. #### def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( ... )
16. #### def decodeToTerm(d: IdealInt, assign: 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
UninterpretedSortSort
17. #### 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
18. #### def eps(f: IFormula): ISortedEpsilon

Generate an epsilon-expression.

Generate an epsilon-expression.

Definition Classes
Sort
19. #### final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
20. #### def equals(arg0: Any): Boolean

Definition Classes
AnyRef → Any
21. #### 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
22. #### 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
23. #### 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
24. #### 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
25. #### 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
26. #### 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
27. #### def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( classOf[java.lang.Throwable] )
28. #### final def getClass(): Class[_]

Definition Classes
AnyRef → Any
29. #### def getSubTerms(ids: Seq[Term], sorts: Seq[Sort], terms: Map[(IdealInt, Sort), ITerm]): Either[Seq[ITerm], Seq[(IdealInt, Sort)]]

Attributes
protected
Definition Classes
Sort
30. #### def hashCode(): Int

Definition Classes
AnyRef → Any
31. #### val individuals: Stream[ITerm]

We just create numbered constants to represent the individuals.

We just create numbered constants to represent the individuals.

Definition Classes
UninterpretedSortSort
32. #### final def isInstanceOf[T0]: Boolean

Definition Classes
Any
33. #### def membershipConstraint(t: Term)(implicit order: TermOrder): Formula

Constraints defining the range of the sort.

Constraints defining the range of the sort.

Definition Classes
UninterpretedSortSort

35. #### val name: String

Definition Classes
UninterpretedSortSort
36. #### final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
37. #### def newConstant(name: String): ConstantTerm

Allocation of a new constant with `this` sort.

Allocation of a new constant with `this` sort.

Definition Classes
Sort
38. #### final def notify(): Unit

Definition Classes
AnyRef
39. #### final def notifyAll(): Unit

Definition Classes
AnyRef
40. #### final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef

42. #### def toString(): String

Definition Classes
Sort → AnyRef → Any
43. #### final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
44. #### final def wait(arg0: Long, arg1: Int): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
45. #### final def wait(arg0: Long): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
46. #### 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