Module S.Ax

type t
type sort
val sort : idx:int -> int -> sort

sort ~idx elm creates a new array kind that maps idx-bit bitvector indexes to elm-bit bitvector values.

val const : sort -> string -> t

const sort name creates the (first-order) constant array named name.

val store : t -> Bv.t -> Bv.t -> t

store a i x creates the array store operation of the byte x at index i in the array a.

val select : t -> Bv.t -> Bv.t

select a i creates the array select operation of one byte at index i in the array a.

val equal : t -> t -> Bl.t

equal x y creates the array = operation between x and y.

val diff : t -> t -> Bl.t

diff x y creates the array <> operation between x and y.

val ite : Bl.t -> t -> t -> t

ite x y z creates the array ite operation between y and z according to x.