Packages

trait Sort extends AnyRef

Trait representing sorts of individuals in the logic.

Linear Supertypes
AnyRef, Any
Known Subclasses
ADTProxySort, AddressSort, HeapSort, TheorySort, ArraySort, ArraySort, ModSort, FractionSort, SeqSort, AbstractStringSort, ProxySort, Integer, Interval, MultipleValueBool, Nat, InfUninterpretedSort, UninterpretedSort
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Sort
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Abstract Value Members

  1. abstract 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.

  2. abstract val cardinality: Option[IdealInt]

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

  3. abstract def individuals: Stream[ITerm]

    Terms representing elements of the sort.

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

    Constraints defining the range of the sort.

  5. abstract val name: String

Concrete 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)).

  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)).

  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)).

  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)).

  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)).

  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.

  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.

  12. def boundVariable(index: Int): IVariable

    The variable with given de Bruijn index and this sort.

  13. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  14. 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

  15. 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)).

  16. def eps(f: IFormula): ISortedEpsilon

    Generate an epsilon-expression.

  17. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  18. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  19. 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)).

  20. 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)).

  21. 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)).

  22. 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)).

  23. 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)).

  24. def ex(f: IFormula): ISortedQuantified

    Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.

  25. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  26. def getSubTerms(ids: Seq[Term], sorts: Seq[Sort], terms: Map[(IdealInt, Sort), ITerm]): Either[Seq[ITerm], Seq[(IdealInt, Sort)]]
    Attributes
    protected
  27. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  28. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  29. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  30. def newConstant(name: String): ConstantTerm

    Allocation of a new constant with this sort.

  31. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  32. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  33. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  34. def toString(): String
    Definition Classes
    Sort → AnyRef → Any
  35. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  36. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  37. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  38. def witness: Option[ITerm]

    A witness term proving that the sort is inhabited.

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated

    (Since version 9)

Inherited from AnyRef

Inherited from Any

Ungrouped