object ExtArray
- Alphabetic
- By Inheritance
- ExtArray
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Type Members
- case class ArraySort(theory: ExtArray) extends ProxySort with TheorySort with Product with Serializable
Sort representing arrays.
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- val AC: AC_ARRAY.type
- def aliasChecker(goal: Goal): (LinearCombination, LinearCombination) => Boolean
- Attributes
- protected[arrays]
- def apply(indexSorts: Seq[Sort], objSort: Sort): ExtArray
Get a unique instance of the array theory with the given index and element sorts.
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def bidirChecker(atoms: Iterable[Atom], goal: Goal): (Atom) => Boolean
- Attributes
- protected[arrays]
- 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
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- 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()
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- AnyRef → Any
- 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])
- object Const
Extractor recognising the
const
function of any array theory. - object Lambda
Constructor and extractor of lambda expressions, encoded using epsilon terms and quantifiers.
Constructor and extractor of lambda expressions, encoded using epsilon terms and quantifiers. The body of the expression is expected to contain free variables
_0, _1, ...
corresponding to the variables bound by the lambda. - object Select
Extractor recognising the
select
function of any array theory. - object Store
Extractor recognising the
store
function of any array theory.
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)