(theory BitVector_ArraysEx :written_by {Clark Barrett} :date {May 7, 2007} :sorts_description { All sort symbols of the form BitVec[m], where m is a numeral greater than 0. All sort symbols of the form Array[m:n], where m and n are numerals with m > 0 and n > 0. } :funs_description { All functions from the theory Fixed_Size_Bitvectors. } :funs_description { All function symbols with arity of the form (select Array[m:n] BitVec[m] BitVec[n]) where - m,n are numerals - m > 0, n > 0 } :funs_description { All function symbols with arity of the form (store Array[m:n] BitVec[m] BitVec[n] Array[m:n]) where - m,n are numerals - m > 0, n > 0 } :preds_description { All predicates from the theory Fixed_Size_Bitvectors. } :definition "This is a theory containing an infinite number of copies of the theory of functional arrays with extensionality: one for each pair of bitvector sorts. It can be formally defined as the union of the SMT-LIB theory Fixed_Size_Bitvectors and an infinite number of variants of the SMT-LIB theory ArraysEx: one for each distinct signature morphism mapping the sort Index to BitVec[m] and the sort Element to Bitvec[n] where m and n range over all positive numerals. In each of the copies of ArraysEx, the sort Array is renamed to Array[m:n] and each copy of ArraysEx contributes exactly one select function and one store function to the infinite polymorphic family of select and store functions described above. " :notes "As in the theory Fixed_Size_Bitvectors, this theory does not provide a value for the formal attributes :sorts, :funs, and :preds because there are an infinite number of them. See the notes in theory Fixed_Size_Bitvectors for details. If for i=1,2, T_i is an SMT-LIB theory with sorts S_i, function symbols F_i, predicate symbols P_i, and axioms A_i, by \"union\" of T_1 and T_2 we mean the theory T with sorts S_1 U S_2, function symbols F_1 U F_2, predicate symbols P_1 U P_2, and axioms A_1 U A_2 (where U stands for set theoretic union). The theory T is a well-defined SMT-LIB theory whenever S_1, S_2, F_1, F_2, P_1, P_2 are all pairwise disjoint, as is the case for the component theories considered here. " )