SMTParser2InputAbsy

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

def addAxiom(f: IFormula): Unit

def addTheory(t: Theory): Unit

def apply(input: Reader): (IFormula, List[IInterpolantSpec], Signature)

Parse a problem from a character stream.

def asFormula(expr: (IExpression, SMTType)): IFormula

final def asInstanceOf[T0]: T0

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

def checkArgNum(op: String, expected: Int, args: Seq[Term]): Unit

def clone(): AnyRef

def collectSubExpressions(f: GrammarExpression, cont: (GrammarExpression) ⇒ Boolean, Connective: ASTConnective): Seq[GrammarExpression]

def constantTypeMap: Map[ConstantTerm, SMTType]

def ensureEnvironmentCopy: Unit

Make sure that the current settings frame contains a local copy of the Environment.

def env: Environment[SMTType, VariableType, SMTFunctionType, SMTFunctionType, SMTType]

final def eq(arg0: AnyRef): Boolean

def equals(arg0: Any): Boolean

def extractAssertions(input: Reader): Seq[IFormula]

def extractHeap(args: Seq[Term]): Option[(Option[ITerm], Heap)]

def functionTypeMap: Map[IFunction, SMTFunctionType]

def genSignature(completeFor: IExpression): Signature

def getAxioms: IFormula

final def getClass(): Class[_]

def hashCode(): Int

def incrementalityMessage(thing: String, warnOnly: Boolean): String

final def isInstanceOf[T0]: Boolean

lazy val mulTheory: MulTheory

def mult(t1: ITerm, t2: ITerm): ITerm

final def ne(arg0: AnyRef): Boolean

def neverInline(expr: IExpression): Boolean

Check whether the given expression should never be inlined, e.g., because it is too big.

final def notify(): Unit

final def notifyAll(): Unit

def objectType(heapTheory: Heap): SMTType

def parseExpression(str: String): IExpression

def parseIgnoreCommand(input: Reader): IExpression

Parse an SMT-LIB script of the form (ignore expression).

def pop: Unit

Pop a frame from the settings stack.

def popState: (Map[IFunction, (IExpression, SMTType)], AnyRef, Int, Map[PartName, Int])

Pop a frame from the settings stack.

def predicateTypeMap: Map[Predicate, SMTFunctionType]

def processIncrementally(input: Reader, timeout: Int, _timeoutPer: Int, userDefStoppingCond: ⇒ Boolean): Unit

def push: Unit

Add a new frame to the settings stack; this in particular affects the Environment.

def pushState(state: (Map[IFunction, (IExpression, SMTType)], AnyRef, Int, Map[PartName, Int])): Unit

Add a new frame to the settings stack; this in particular affects the Environment.

def registerRecFunctions(funs: Seq[(IFunction, (IExpression, SMTType))]): Unit

def reset: Unit

Erase all stored information.

def symApp(sym: SymbolRef, args: Seq[Term], polarity: Int): (IExpression, SMTType)

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

def toString(): String

def translateHeapFun(funF: (Heap) ⇒ IFunction, args: Seq[Term], argTypesF: (Heap) ⇒ Seq[SMTType], resTypeF: (Heap) ⇒ SMTType): Option[(IExpression, SMTType)]

def translateSort(s: Sort): SMTType

def translateSpecConstant(c: SpecConstant): (ITerm, SMTType)

def translateTerm(t: Term, polarity: Int): (IExpression, SMTType)

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

final def wait(arg0: Long): Unit

final def wait(): Unit

def finalize(): Unit