SMTParsingUtils

Type Members

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.

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 FFDecLiteral: Regex
val HexLiteral: Regex
object IndexedIdentifier
object IndexedSymbol
object NatLiteral
object NumIndexedSymbol1
object NumIndexedSymbol2
object PlainIdentifier
object PlainSymbol
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 asTerm(expr: (IExpression, SMTType), expectedSort: SMTType): ITerm
def asTerm(expr: (IExpression, SMTType)): ITerm
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()
def parseWithEntry[T](input: Reader, entry: (parser) ⇒ T): T

Parse starting at an arbitrarily specified entry point
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 Doc: package parser

object SMTParsingUtils

Type Members

class SMTCommandTerminator extends Reader

Value Members

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

val BVDecLiteral: Regex

object CastSymbol

val DecLiteral: Regex

val FFDecLiteral: Regex

val HexLiteral: Regex

object IndexedIdentifier

object IndexedSymbol

object NatLiteral

object NumIndexedSymbol1

object NumIndexedSymbol2

object PlainIdentifier

object PlainSymbol

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 asTerm(expr: (IExpression, SMTType), expectedSort: SMTType): ITerm

def asTerm(expr: (IExpression, SMTType)): ITerm

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

def parseWithEntry[T](input: Reader, entry: (parser) ⇒ T): T

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