case class ISortedVariable(index: Int, sort: Sort) extends IVariable with Product with Serializable
Bound variables, represented using their de Bruijn index and the sort.
- Alphabetic
- By Inheritance
- ISortedVariable
- Serializable
- Product
- Equals
- IVariable
- 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
- 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()
- 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
- ISortedVariable → AnyRef → Any
- val index: Int
The index of the bound variable.
The index of the bound variable.
- Definition Classes
- ISortedVariable → IVariable
- 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
- 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
- def shiftedBy(shift: Int): IVariable
Increase the index of this variable by
shift(which can have any sign).Increase the index of this variable by
shift(which can have any sign).- Definition Classes
- ISortedVariable → IVariable
- val sort: Sort
The sort of the bound variable.
The sort of the bound variable.
- Definition Classes
- ISortedVariable → IVariable
- 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
- ISortedVariable → AnyRef → Any
- def unary_-: ITerm
Negation of a term.
Negation of a term.
- Definition Classes
- ITerm
- def update(newSubExprs: Seq[IExpression]): ITerm
Replace the subexpressions of this node with new expressions
Replace the subexpressions of this node with new expressions
- Definition Classes
- 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)