SMTLineariser

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

def apply(benchmarkName: String, logic: String, status: String, constsToDeclare: Seq[ConstantTerm], predsToDeclare: Seq[Predicate], formulas: Seq[IFormula]): Unit

def apply(formulas: Seq[IFormula], signature: Signature, logic: String, status: String, benchmarkName: String): Unit

def apply(formulas: Seq[IFormula], signature: Signature, benchmarkName: String): Unit

def apply(term: ITerm): Unit

def apply(formula: IFormula, constantType: (ConstantTerm) ⇒ Option[SMTType], functionType: (IFunction) ⇒ Option[SMTFunctionType], predType: (Predicate) ⇒ Option[SMTFunctionType], prettyBitvectors: Boolean = true): Unit

def apply(formula: IFormula): Unit

def apply(expr: IExpression): Unit

def applyNoPrettyBitvectors(term: ITerm): Unit

def applyNoPrettyBitvectors(formula: IFormula): Unit

final def asInstanceOf[T0]: T0

def asString(t: ITerm): String

def asString(formula: IFormula): String

def asString(t: IExpression): String

def clone(): AnyRef

final def eq(arg0: AnyRef): Boolean

def equals(arg0: Any): Boolean

def escapeSQString(str: String): String

Unescape a single-quoted string; the only recognised escape sequence is

def escapeString(str: String): String

val functionTypeFromSort: (IFunction) ⇒ Option[SMTFunctionType]

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

val predTypeFromSort: (Predicate) ⇒ Option[SMTFunctionType]

def printADTDeclaration(adt: ADT): Unit

def printADTDeclarations(adts: Seq[ADT]): Unit

def printArguments(argSorts: Seq[Sort], formalArgs: Seq[ConstantTerm]): Unit

def printDefineFun(f: IFunction, functionType: (Seq[Sort], Sort), formalArgs: Seq[ConstantTerm], body: IExpression): Unit

def printHeapDeclaration(heap: Heap): Unit

def printHeapDeclarations(heaps: Seq[Heap]): Unit

def printModel(model: IFormula): Unit

def printSMTType(t: SMTType): Unit

def quoteIdentifier(str: String): String

def simpleUnescapeIt(it: Iterator[Int]): Seq[Int]

Unescaping strictly following the SMT-LIB standard.

def smtTypeAsString(t: SMTType): String

def sort2SMTString(sort: Sort): String

def sort2SMTType(sort: Sort): (SMTType, Option[(ITerm) ⇒ IFormula])

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

def toSMTExpr(value: IdealInt): String

def toString(): String

def unescapeIt(it: Iterator[Int]): Seq[Int]

def unescapeSQString(str: String): String

Unescape a single-quoted string; the only recognised escape sequence is

def unescapeString(str: String): String

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

final def wait(arg0: Long): Unit

final def wait(): Unit

def finalize(): Unit