SMTParser2InputAbsy

Type Members

case class BoundVariable(varType: SMTType) extends VariableType with Product with Serializable
case class SMTADT(adt: ADT, sortNum: Int) extends SMTType with Product with Serializable
case class SMTArray(arguments: List[SMTType], result: SMTType) extends SMTType with Product with Serializable
case class SMTBitVec(width: Int) extends SMTType with Product with Serializable
case class SMTChar(sort: Sort) extends SMTType with Product with Serializable
class SMTCommandTerminator extends Reader

Class for adding parentheses () after each SMT-LIB command; this is necessary in the interactive/incremental mode, because otherwise the parser always waits for the next token to arrive before forwarding a command.
Class for adding parentheses () after each SMT-LIB command; this is necessary in the interactive/incremental mode, because otherwise the parser always waits for the next token to arrive before forwarding a command. This also removes all CR-characters in a stream (necessary because the lexer seems to dislike CRs in comments), and adds an LF in the end, because the lexer does not allow inputs that end with a //-comment line either.
case class SMTFunctionType(arguments: List[SMTType], result: SMTType) extends Product with Serializable
case class SMTHeap(heap: Heap) extends SMTType with Product with Serializable
case class SMTHeapAddress(heap: Heap) extends SMTType with Product with Serializable
case class SMTReal(sort: Sort) extends SMTType with Product with Serializable
case class SMTRegLan(sort: Sort) extends SMTType with Product with Serializable
case class SMTSeq(theory: SeqTheory, elementType: SMTType) extends SMTType with Product with Serializable
case class SMTString(sort: Sort) extends SMTType with Product with Serializable
abstract class SMTType extends AnyRef
case class SMTUnint(sort: Sort) extends SMTType with Product with Serializable
case class SubstExpression(e: IExpression, t: SMTType) extends VariableType with Product with Serializable
sealed abstract class VariableType extends AnyRef

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
val BVDecLiteral: Regex
object CastSymbol
val DecLiteral: Regex
val HexLiteral: Regex
object IndexedIdentifier
object IndexedSymbol
object NatLiteral
object NumIndexedSymbol1
object NumIndexedSymbol2
object PlainIdentifier
object PlainSymbol
object SMTADT extends Serializable
object SMTBool extends SMTType with Product with Serializable
val SMTBoolVariableType: SMTFunctionType
object SMTInteger extends SMTType with Product with Serializable
def apply(settings: ParserSettings, prover: api.SimpleAPI): SMTParser2InputAbsy
def apply(settings: ParserSettings): SMTParser2InputAbsy
final def asInstanceOf[T0]: T0

Definition Classes
Any
def asString(s: Sort): String
def asString(s: Symbol): String
def asString(id: Identifier): String
def asString(id: IndexC): String
def asString(s: SymbolRef): String
def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate() @throws( ... )
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 SMTParser2InputAbsy | package parser

object SMTParser2InputAbsy

Type Members

case class BoundVariable(varType: SMTType) extends VariableType with Product with Serializable

case class SMTADT(adt: ADT, sortNum: Int) extends SMTType with Product with Serializable

case class SMTArray(arguments: List[SMTType], result: SMTType) extends SMTType with Product with Serializable

case class SMTBitVec(width: Int) extends SMTType with Product with Serializable

case class SMTChar(sort: Sort) extends SMTType with Product with Serializable

class SMTCommandTerminator extends Reader

case class SMTFunctionType(arguments: List[SMTType], result: SMTType) extends Product with Serializable

case class SMTHeap(heap: Heap) extends SMTType with Product with Serializable

case class SMTHeapAddress(heap: Heap) extends SMTType with Product with Serializable

case class SMTReal(sort: Sort) extends SMTType with Product with Serializable

case class SMTRegLan(sort: Sort) extends SMTType with Product with Serializable

case class SMTSeq(theory: SeqTheory, elementType: SMTType) extends SMTType with Product with Serializable

case class SMTString(sort: Sort) extends SMTType with Product with Serializable

abstract class SMTType extends AnyRef

case class SMTUnint(sort: Sort) extends SMTType with Product with Serializable

case class SubstExpression(e: IExpression, t: SMTType) extends VariableType with Product with Serializable

sealed abstract class VariableType extends AnyRef

Value Members

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

val BVDecLiteral: Regex

object CastSymbol

val DecLiteral: Regex

val HexLiteral: Regex

object IndexedIdentifier

object IndexedSymbol

object NatLiteral

object NumIndexedSymbol1

object NumIndexedSymbol2

object PlainIdentifier

object PlainSymbol

object SMTADT extends Serializable

object SMTBool extends SMTType with Product with Serializable

val SMTBoolVariableType: SMTFunctionType

object SMTInteger extends SMTType with Product with Serializable

def apply(settings: ParserSettings, prover: api.SimpleAPI): SMTParser2InputAbsy

def apply(settings: ParserSettings): SMTParser2InputAbsy

final def asInstanceOf[T0]: T0

def asString(s: Sort): String

def asString(s: Symbol): String

def asString(id: Identifier): String

def asString(id: IndexC): String

def asString(s: SymbolRef): String

def clone(): AnyRef

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