case class ISortedEpsilon(sort: Sort, cond: IFormula) extends IEpsilon with Product with Serializable
Epsilon term, which is defined to evaluate to an arbitrary value
satisfying the formula cond. cond is expected
to contain a bound variable with de Bruijn index 0 and the given sort.
- Alphabetic
- By Inheritance
- ISortedEpsilon
- Serializable
- Product
- Equals
- IEpsilon
- IVariableBinder
- 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
- ISortedEpsilon → 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
The body of the epsilon term.
The body of the epsilon term.
- Definition Classes
- ISortedEpsilon → IEpsilon
- 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
- ISortedEpsilon → 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
- def length: Int
Number of sub-expressions.
Number of sub-expressions.
- Definition Classes
- ISortedEpsilon → 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 sort: Sort
The sort of the bound variable.
The sort of the bound variable.
- Definition Classes
- ISortedEpsilon → IEpsilon → IVariableBinder
- 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
- ISortedEpsilon → AnyRef → Any
- def unary_-: ITerm
Negation of a term.
Negation of a term.
- Definition Classes
- ITerm
- def update(newSubExprs: Seq[IExpression]): ISortedEpsilon
Replace the subexpressions of this node with new expressions
Replace the subexpressions of this node with new expressions
- Definition Classes
- ISortedEpsilon → 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)