# MultipleValueBool

### Related Doc: package Sort

#### object MultipleValueBool extends ProxySort

The sort of integers reinterpreted as Booleans. Integer `0true`, every non-zero number as `false`. For symbolic representation the same terms as in sort `Bool` are used.

Bool

Linear Supertypes
ProxySort, Sort, AnyRef, Any
Ordering
1. Alphabetic
2. By inheritance
Inherited
1. MultipleValueBool
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
4. #### val False: IFunApp

Term representing the Boolean value `false`, and mapped to integer `1`.

Term representing the Boolean value `false`, and mapped to integer `1`. (But note that every non-zero number is interpreted as `false`).

5. #### val True: IFunApp

Term representing the Boolean value `true`, and mapped to integer `0`.

Term representing the Boolean value `true`, and mapped to integer `0`.

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

Definition Classes
Any
13. #### 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
14. #### 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
MultipleValueBoolProxySortSort
15. #### 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
16. #### 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
17. #### def clone(): AnyRef

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

Generate an epsilon-expression.

Generate an epsilon-expression.

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

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

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

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

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

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

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

Terms representing elements of the sort.

Terms representing elements of the sort.

Definition Classes
MultipleValueBoolProxySortSort
34. #### def isFalse(t: ITerm): IFormula

Construct a tester for `false`.

Construct a tester for `false`.

35. #### final def isInstanceOf[T0]: Boolean

Definition Classes
Any
36. #### def isTrue(t: ITerm): IFormula

Construct a tester for `true`.

Construct a tester for `true`.

37. #### 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
38. #### val name: String

Definition Classes
MultipleValueBoolProxySortSort
39. #### final def ne(arg0: AnyRef): Boolean

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

Allocation of a new constant with `this` sort.

Allocation of a new constant with `this` sort.

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

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

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

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

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

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

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

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