case class ITermITE(cond: IFormula, left: ITerm, right: ITerm) extends ITerm with Product with Serializable
If-then-else term.
- Alphabetic
- By Inheritance
- ITermITE
- Serializable
- Product
- Equals
- ITerm
- IExpression
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- def *(that: ITerm): ITerm
Product of two terms (only defined if at least one of the terms is constant).
Product of two terms (only defined if at least one of the terms is constant).
- Definition Classes
- ITerm
- def *(coeff: IdealInt): ITerm
Product of term with an integer.
Product of term with an integer.
- Definition Classes
- ITerm
- def ***(coeff: IdealInt): ITerm
Product of two terms.
Product of two terms. The resulting expression is simplified immediately if one of the terms is constant.
- Definition Classes
- ITerm
- def +(that: ITerm): ITerm
Sum of two terms.
Sum of two terms.
- Definition Classes
- ITerm
- def +++(that: ITerm): ITerm
Sum of two terms.
Sum of two terms. The resulting expression is simplified immediately if one of the terms disappears.
- Definition Classes
- ITerm
- def -(that: ITerm): ITerm
Difference between two terms.
Difference between two terms.
- Definition Classes
- ITerm
- def ---(that: ITerm): ITerm
Difference of two terms.
Difference of two terms. The resulting expression is simplified immediately if one of the terms disappears.
- Definition Classes
- ITerm
- def <(that: ITerm): IFormula
Inequality between two terms.
Inequality between two terms.
- Definition Classes
- ITerm
- def <=(that: ITerm): IFormula
Inequality between two terms.
Inequality between two terms.
- Definition Classes
- ITerm
- def =/=(that: ITerm): IFormula
Dis-equation between two terms.
Dis-equation between two terms.
- Definition Classes
- ITerm
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- def ===(that: ITerm): IFormula
Equation between two terms.
Equation between two terms.
- Definition Classes
- ITerm
- def >(that: ITerm): IFormula
Inequality between two terms.
Inequality between two terms.
- Definition Classes
- ITerm
- def >=(that: ITerm): IFormula
Inequality between two terms.
Inequality between two terms.
- Definition Classes
- ITerm
- def apply(i: Int): IExpression
Return the
ith sub-expression.Return the
ith sub-expression.- Definition Classes
- ITermITE → IExpression
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- val cond: IFormula
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- val hashCode: Int
- Definition Classes
- ITermITE → AnyRef → Any
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def iterator: Iterator[IExpression]
Iterator over the sub-expressions of this expression.
Iterator over the sub-expressions of this expression.
- Definition Classes
- IExpression
- val left: ITerm
- def length: Int
Number of sub-expressions.
Number of sub-expressions.
- Definition Classes
- ITermITE → IExpression
- def minusSimplify: ITerm
Negation of a term.
Negation of a term. The resulting expression is simplified immediately if one of the terms is constant.
- Definition Classes
- ITerm
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def productElementNames: Iterator[String]
- Definition Classes
- Product
- val right: ITerm
- def subExpressions: IndexedSeq[IExpression]
The sub-expressions of this expression.
The sub-expressions of this expression.
- Definition Classes
- IExpression
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- ITermITE → AnyRef → Any
- def unary_-: ITerm
Negation of a term.
Negation of a term.
- Definition Classes
- ITerm
- def update(newSubExprs: Seq[IExpression]): ITermITE
Replace the subexpressions of this node with new expressions
Replace the subexpressions of this node with new expressions
- Definition Classes
- ITermITE → ITerm → IExpression
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)