case class CombinatorSpec(name: String, argsSorts: Seq[Int], resSort: Int, definition: IFormula) extends Product with Serializable
Specification of an array combinator. The indexes of argument and
result sorts refer to the ExtArray theories
specified as part of the CombArray theory. The field
definition of an n-ary combinator
defines the operation as a relation on the array objects; the
defining formula can contain free variables _0, _1, ...,
_n, representing the n-1 arguments objects
and the result object, respectively.
Linear Supertypes
Ordering
- Alphabetic
 - By Inheritance
 
Inherited
- CombinatorSpec
 - Serializable
 - Product
 - Equals
 - AnyRef
 - Any
 
- Hide All
 - Show All
 
Visibility
- Public
 - Protected
 
Instance Constructors
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 argsSorts: Seq[Int]
 -   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 definition: IFormula
 -   final  def eq(arg0: AnyRef): Boolean
- Definition Classes
 - AnyRef
 
 -   final  def getClass(): Class[_ <: AnyRef]
- Definition Classes
 - AnyRef → Any
 - Annotations
 - @HotSpotIntrinsicCandidate() @native()
 
 -   final  def isInstanceOf[T0]: Boolean
- Definition Classes
 - Any
 
 -  val name: String
 -   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 resSort: Int
 -   final  def synchronized[T0](arg0: => T0): T0
- Definition Classes
 - AnyRef
 
 -   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)