Packages

object ADT

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. ADT
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. class ADTException extends Exception
  2. class ADTProxySort extends ProxySort with TheorySort

    Class representing the types/sorts defined by this ADT theory

  3. case class ADTSort(num: Int) extends CtorArgSort with Product with Serializable
  4. sealed abstract class CtorArgSort extends AnyRef
  5. case class CtorSignature(arguments: Seq[(String, CtorArgSort)], result: ADTSort) extends Product with Serializable
  6. case class OtherSort(sort: Sort) extends CtorArgSort with Product with Serializable

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. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  6. def createEnumType(name: String, cases: Seq[String]): (Sort, IndexedSeq[ITerm])

    Create an ADT that implements an enumeration, and return the corresponding sort and the terms representing the cases.

  7. def createListType(name: String, elementSort: Sort, withSize: Boolean = false): (Sort, IFunction, IFunction, IFunction, IFunction, Option[IFunction])

    Create an ADT that implements lists.

    Create an ADT that implements lists. The return tuple provides the list sort, and the functions for nil, cons, head, tail. If the withSize option is set, the last returned function is the size function of the ADT; it computes the number of constructor symbols of a term.

  8. def createRecordType(name: String, fields: Seq[(String, Sort)]): (Sort, IFunction, IndexedSeq[IFunction])

    Create an ADT that implements a record type, and return the corresponding sort, the constructor symbol, and the selectors.

  9. def depthSortedVectors(sorts: List[Sort]): Stream[List[ITerm]]
    Attributes
    protected[theories]
  10. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  11. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  12. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  13. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  14. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  15. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  16. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  17. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  18. def printSMTCtorDeclaration(ctor: MonoSortedIFunction, selectors: Seq[MonoSortedIFunction]): Unit
    Attributes
    protected[theories]
  19. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  20. def toString(): String
    Definition Classes
    AnyRef → Any
  21. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  22. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  23. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  24. object BoolADT extends ADT

    The ADT of Booleans, with truth values true, false as only constructors.

    The ADT of Booleans, with truth values true, false as only constructors. The ADT is a simple enumeration, and preprocessing will map true to value 0, and false to value 1.

  25. object Constructor

    Extractor recognising the constructors of any ADT theory.

    Extractor recognising the constructors of any ADT theory. The extractor will produce the adt, and the index of the constructor.

  26. object CtorId

    Extractor recognising the X_ctor functions of any ADT theory.

  27. object CtorIdRewriter extends CollectingVisitor[Unit, IExpression]

    The preprocessor can sometimes cause solution formulas that are illegal according to SMT-LIB because they contain the ADT.CtorId functions in wrong places.

    The preprocessor can sometimes cause solution formulas that are illegal according to SMT-LIB because they contain the ADT.CtorId functions in wrong places. This class rewrites such formulas to only use CtorId functions in equations ctorId(t) = num.

  28. object Selector

    Extractor recognising the selectors of any ADT theory.

    Extractor recognising the selectors of any ADT theory. The extractor will produce the adt, the index of the constructor, and the index of the selected constructor argument.

  29. object TermMeasure extends Enumeration
  30. object TermSize

    Extractor recognising the X_size functions of any ADT theory.

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