IFunApp

final def !=(arg0: Any): Boolean

final def ##(): Int

def *(that: ITerm): ITerm

Product of two terms (only defined if at least one of the terms is constant).

def *(coeff: IdealInt): ITerm

Product of term with an integer.

def ***(coeff: IdealInt): ITerm

Product of two terms.

def +(that: ITerm): ITerm

Sum of two terms.

def +++(that: ITerm): ITerm

Sum of two terms.

def -(that: ITerm): ITerm

Difference between two terms.

def ---(that: ITerm): ITerm

Difference of two terms.

def <(that: ITerm): IFormula

Inequality between two terms.

def <=(that: ITerm): IFormula

Inequality between two terms.

def =/=(that: ITerm): IFormula

Dis-equation between two terms.

final def ==(arg0: Any): Boolean

def ===(that: ITerm): IFormula

Equation between two terms.

def >(that: ITerm): IFormula

Inequality between two terms.

def >=(that: ITerm): IFormula

Inequality between two terms.

def apply(i: Int): ITerm

Return the ith sub-expression.

val args: Seq[ITerm]

final def asInstanceOf[T0]: T0

def clone(): AnyRef

final def eq(arg0: AnyRef): Boolean

def equals(that: Any): Boolean

val fun: IFunction

final def getClass(): Class[_]

val hashCode: Int

final def isInstanceOf[T0]: Boolean

def iterator: Iterator[IExpression]

Iterator over the sub-expressions of this expression.

def length: Int

Number of sub-expressions.

def minusSimplify: ITerm

Negation of a term.

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

def subExpressions: IndexedSeq[IExpression]

The sub-expressions of this expression.

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

def toString(): String

def unary_-: ITerm

Negation of a term.

def update(newSubExprs: Seq[IExpression]): IFunApp

Replace the subexpressions of this node with new expressions

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

final def wait(arg0: Long): Unit

final def wait(): Unit

def finalize(): Unit