module Array: sig end
Operation on function symbols of the theory
Th.arr
of
functional arrays.
- Constants
mk_create, mk_select, mk_update for representing
Create, Select, Update, respectively.
get f returns the function symbol in Th.arr represented by f,
or raises Not_found. - The test
is_create f (is_select f, is_update f) succeeds iff f
represents some Create (Select, Update).
pp p fmt (op, al) pretty-prints the appliation of op to the
argument list al depending on the value of Pretty.flag. See
also Pretty.apply. It assumes applications to Create to be
unary, Select is binary, and Update is ternary.
val get : Sym.t -> Sym.arrays
val mk_create : Sym.t
val mk_select : Sym.t
val mk_update : Sym.t
val is : Sym.t -> bool
val is_create : Sym.t -> bool
val is_select : Sym.t -> bool
val is_update : Sym.t -> bool
val pp : 'a Pretty.printer -> (Sym.arrays * 'a list) Pretty.printer