SMTLineariser

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

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 printArguments(argSorts: Seq[Sort], formalArgs: Seq[ConstantTerm]): Unit

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

def printModel(model: IFormula): Unit

def printSMTType(t: SMTType): Unit

def printWithDecls(formulas: Seq[IFormula], constsToDeclare: Seq[ConstantTerm] = List(), predsToDeclare: Seq[Predicate] = List(), funsToDeclare: Seq[IFunction] = List(), extraTheories: Seq[Theory] = List(), benchmarkName: String = "", logic: String = "AUFLIA", status: String = "unknown"): Unit

def printWithDeclsSig(formulas: Seq[IFormula], signature: Signature, extraTheories: Seq[Theory] = List(), benchmarkName: String = "", logic: String = "AUFLIA", status: String = "unknown"): 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])

def sortTheoryDeps(theories: Seq[Theory]): Seq[Theory]

Topologically sort theories to be declared: dependencies of a theory preceed the theory in the resulting list.

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