# Integer

### Related Doc: package Sort

#### object Integer extends Sort

The sort of integers, which is also the default sort whenever no sort is specified.

Linear Supertypes
Sort, AnyRef, Any
Ordering
1. Alphabetic
2. By Inheritance
Inherited
1. Integer
2. Sort
3. AnyRef
4. 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
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
IntegerSort
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
IntegerSort
15. #### def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate() @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
IntegerSort
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. #### final def getClass(): Class[_]

Definition Classes
AnyRef → Any
Annotations
@HotSpotIntrinsicCandidate()
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
Annotations
@HotSpotIntrinsicCandidate()
30. #### val individuals: Stream[ITerm]

Terms representing elements of the sort.

Terms representing elements of the sort.

Definition Classes
IntegerSort
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
IntegerSort
33. #### val name: String

Definition Classes
IntegerSort
34. #### final def ne(arg0: AnyRef): Boolean

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

Allocation of a new constant with `this` sort.

Allocation of a new constant with `this` sort.

Definition Classes
IntegerSort
36. #### final def notify(): Unit

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

Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate()
38. #### final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
39. #### def toString(): String

Definition Classes
Sort → AnyRef → Any
40. #### final def wait(arg0: Long, arg1: Int): Unit

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

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

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

1. #### def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
Deprecated