Object

ap.types.Sort

MultipleValueBool

Related Doc: package Sort

Permalink

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.

See also

Bool

ap.theories.ADT.BoolADT

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

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

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

    Permalink
    Definition Classes
    AnyRef → Any
  4. val False: IFunApp

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink
    Definition Classes
    Any
  13. val asTerm: Decoder[Option[ITerm]]

    Permalink

    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

    Permalink

    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
    MultipleValueBoolProxySortSort
  15. def boundVariable(index: Int): IVariable

    Permalink

    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]

    Permalink

    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

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  18. def decodeToTerm(d: IdealInt, assign: Map[(IdealInt, Sort), ITerm]): Option[ITerm]

    Permalink

    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

    Permalink

    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

    Permalink

    Generate an epsilon-expression.

    Generate an epsilon-expression.

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

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

    Permalink
    Definition Classes
    AnyRef → Any
  23. def ex(f: (ITerm, ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    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

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

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

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

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

    Permalink

    Terms representing elements of the sort.

    Terms representing elements of the sort.

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

    Permalink

    Construct a tester for false.

    Construct a tester for false.

  35. final def isInstanceOf[T0]: Boolean

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

    Permalink

    Construct a tester for true.

    Construct a tester for true.

  37. def membershipConstraint(t: Term)(implicit order: TermOrder): Formula

    Permalink

    Constraints defining the range of the sort.

    Constraints defining the range of the sort.

    Definition Classes
    ProxySortSort
  38. val name: String

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

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

    Permalink

    Allocation of a new constant with this sort.

    Allocation of a new constant with this sort.

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

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

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

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

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

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

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

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  48. def witness: Option[ITerm]

    Permalink

    A witness term proving that the sort is inhabited.

    A witness term proving that the sort is inhabited.

    Definition Classes
    Sort

Inherited from ProxySort

Inherited from Sort

Inherited from AnyRef

Inherited from Any

Ungrouped