 # ADTProxySort

### Related Doc: package ADT

#### class ADTProxySort extends ProxySort

Class representing the types/sorts defined by this ADT theory

Linear Supertypes
ProxySort, Sort, AnyRef, Any
Ordering
1. Alphabetic
2. By Inheritance
Inherited
1. ADTProxySort
2. ProxySort
3. Sort
4. AnyRef
5. Any
1. Hide All
2. Show All
Visibility
1. Public
2. All

### 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

5. #### 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
6. #### 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
7. #### 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
8. #### 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
9. #### 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
10. #### 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
11. #### final def asInstanceOf[T0]: T0

Definition Classes
Any
12. #### 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
13. #### def augmentModelTermSet(model: Conjunction, terms: 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
ADTProxySortProxySortSort
14. #### 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
15. #### val cardinality: Option[IdealInt]

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

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

Definition Classes
ProxySortSort
16. #### def clone(): AnyRef

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

Generate an epsilon-expression.

Generate an epsilon-expression.

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

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

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

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

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

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

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

Terms representing elements of the sort.

Terms representing elements of the sort.

Definition Classes
ADTProxySortProxySortSort
33. #### final def isInstanceOf[T0]: Boolean

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

Constraints defining the range of the sort.

Constraints defining the range of the sort.

Definition Classes
ProxySortSort
35. #### val name: String

Definition Classes
ProxySortSort
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

41. #### 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