module Funarr: sig end
Theory of arrays.
Author(s): Harald Ruess
Terms in the theory of arrays are
- creation
create(a) of a constant array
- selection
a[j] of element at position j in the array a, and
- updating
a[i := x] array a at position i with value x.
Given an equality relation =E and a disequality relation <>D, the
theory of arrays is specified by
create(a)[j] = aa[i:=x][j] = x when i =E ja[i:=x][j] = a[j] when i <>D ja[i:=x][i:=y] = a[i:=y]a[j:=y][i:=x] = a[i:=x][j:=y] if i <>D j and Term.(<<<)i j.
val d_interp : Term.t -> Sym.arrays * Term.t list
val d_update : Term.t -> Term.t * Term.t * Term.t
val d_select : Term.t -> Term.t * Term.t
val d_create : Term.t -> Term.t
val d_select_update : Term.t -> Term.t * Term.t * Term.t * Term.t
d_select a returns (b, i, x, j) if a is of the form a[i:=x][j].
type equalRel = Term.t -> Term.t -> Three.t
val is_interp : Term.t -> bool
val mk_create : Term.t -> Term.t
Creating constant array.
val mk_select : equalRel -> Term.t -> Term.t -> Term.t
mk_select a j constructs a canonical term equivalent
to App(select, [a; j]).
val mk_update : equalRel -> Term.t -> Term.t -> Term.t -> Term.t
mk_update a x i constructs a canonical term equivalent
to App(update, [a;x;i]).
val sigma : equalRel -> Sym.arrays -> Term.t list -> Term.t
Array canonizer.
val map : equalRel -> (Term.t -> Term.t) -> Term.t -> Term.t
Applying a term transformer at all uninterpreted positions
map f (mk_select a j) equals mk_select (map f a) (map f j)map f (mk_update a i x) equals mk_select (map f a) (map f i) (map f x)- Otherwise,
map f x equals f x
module Flat: sig end