ADT

Type Members

class ADTException extends Exception
class ADTProxySort extends ProxySort

Class representing the types/sorts defined by this ADT theory
case class ADTSort(num: Int) extends CtorArgSort with Product with Serializable
sealed abstract class CtorArgSort extends AnyRef
case class CtorSignature(arguments: Seq[(String, CtorArgSort)], result: ADTSort) extends Product with Serializable
case class OtherSort(sort: Sort) extends CtorArgSort with Product with Serializable

Value Members

final def !=(arg0: Any): Boolean

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

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

Definition Classes
AnyRef → Any
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.
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.
object CtorId

Extractor recognising the X_ctor functions of any ADT theory.
Extractor recognising the X_ctor functions of any ADT theory.
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.
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.
object TermMeasure extends Enumeration
object TermSize

Extractor recognising the X_size functions of any ADT theory.
Extractor recognising the X_size functions of any ADT theory.
final def asInstanceOf[T0]: T0

Definition Classes
Any
def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate() @throws( ... )
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.
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.
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.
def depthSortedVectors(sorts: List[Sort]): Stream[List[ITerm]]

Attributes
protected[ap.theories]
final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
def equals(arg0: Any): Boolean

Definition Classes
AnyRef → Any
final def getClass(): Class[_]

Definition Classes
AnyRef → Any
Annotations
@HotSpotIntrinsicCandidate()
def hashCode(): Int

Definition Classes
AnyRef → Any
Annotations
@HotSpotIntrinsicCandidate()
final def isInstanceOf[T0]: Boolean

Definition Classes
Any
final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
final def notify(): Unit

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

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

Definition Classes
AnyRef
def toString(): String

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

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

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

Definition Classes
AnyRef
Annotations
@throws( ... )

Deprecated Value Members

def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
Deprecated
(Since version ) see corresponding Javadoc for more information.

Related Docs: class ADT | package theories

object ADT

Type Members

class ADTException extends Exception

class ADTProxySort extends ProxySort

case class ADTSort(num: Int) extends CtorArgSort with Product with Serializable

sealed abstract class CtorArgSort extends AnyRef

case class CtorSignature(arguments: Seq[(String, CtorArgSort)], result: ADTSort) extends Product with Serializable

case class OtherSort(sort: Sort) extends CtorArgSort with Product with Serializable

Value Members

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

object BoolADT extends ADT

object Constructor

object CtorId

object CtorIdRewriter extends CollectingVisitor[Unit, IExpression]

object Selector

object TermMeasure extends Enumeration

object TermSize

final def asInstanceOf[T0]: T0

def clone(): AnyRef

def createEnumType(name: String, cases: Seq[String]): (Sort, IndexedSeq[ITerm])

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

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

def depthSortedVectors(sorts: List[Sort]): Stream[List[ITerm]]

final def eq(arg0: AnyRef): Boolean

def equals(arg0: Any): Boolean

final def getClass(): Class[_]

def hashCode(): Int

final def isInstanceOf[T0]: Boolean

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

final def synchronized[T0](arg0: ⇒ T0): T0

def toString(): String

final def wait(arg0: Long, arg1: Int): Unit

final def wait(arg0: Long): Unit

final def wait(): Unit

Deprecated Value Members

def finalize(): Unit

Inherited from AnyRef

Inherited from Any

Ungrouped