case classCombinatorSpec(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
Serializable, Serializable, Product, Equals, AnyRef, Any
Specification of an array combinator. The indexes of argument and result sorts refer to the
ExtArray
theories specified as part of theCombArray
theory. The fielddefinition
of ann
-ary combinator defines the operation as a relation on the array objects; the defining formula can contain free variables_0, _1, ..., _n
, representing then-1
arguments objects and the result object, respectively.