(logic QF_A

 :written_by {Silvio Ranise and Cesare Tinelli}
 :date {08/04/05}
 :updated {01/05/07}

 :history {
   Bug fix in the :notes field below, pointed out by Albert Oliveras.
 }

 :theory Arrays

 :language 
 "Closed quantifier-free formulas built over an arbitrary expansion of
  the Arrays signature with free constant symbols.

  Note that the formulas can contain term (resp., formula) variables 
  as long as they are bound by a let (resp., flet) construct.
  Also, formulas in ite terms must be themselves quantifier-free.
 "
 :notes
 "If F is a formula in the language it is possible to pre-process F
  so that F is satisfiable in the theory Arrays iff the resulting
  formula F' is satisfiable in the theory Empty.
  The pre-processing step goes as follows: conjoin to the formula F,
  all formulas of the form

    (= (select (store t_a t_i t_e) t_j)
       (ite (= t_i t_j) t_e (read t_a t_j)))

  for all terms t_a of sort Array, all terms t_e of sort Element, and
  pairs of terms t_i, t_j of sort Index occurring in F.
  This is far from being efficient since it may generate a lot of
  possibly useless instances. But it suggests the key intuition
  underlying the theory of arrays, i.e., the semantics of select and
  store encapsulate case-splitting.
 "
)