 # 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): IQuantified

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 terms from a model.

Extract terms from a model. Such terms will always be encoded as integers, and integers can have different meaning depending on the considered sort.

Definition Classes
UninterpretedSortSort
13. #### 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
14. #### def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( ... )
15. #### 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
16. #### def eps(f: (ITerm) ⇒ IFormula): IEpsilon

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
17. #### def eps(f: IFormula): IEpsilon

Generate an epsilon-expression.

Generate an epsilon-expression.

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

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

Definition Classes
AnyRef → Any
20. #### 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
21. #### 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
22. #### 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
23. #### 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
24. #### 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
25. #### def ex(f: IFormula): IQuantified

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
26. #### def finalize(): Unit

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

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

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

Definition Classes
AnyRef → Any
30. #### 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
31. #### final def isInstanceOf[T0]: Boolean

Definition Classes
Any
32. #### 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
33. #### def membershipConstraint(t: ITerm): IFormula

Constraints defining the range of the sort.

Constraints defining the range of the sort.

Definition Classes
UninterpretedSortSort
34. #### val name: String

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

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

Allocation of a new constant with `this` sort.

Allocation of a new constant with `this` sort.

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

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

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

Definition Classes
AnyRef

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

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

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

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

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