module Z3Array:sig
..end
val mk_sort : context -> Sort.sort -> Sort.sort -> Sort.sort
val is_store : Expr.expr -> bool
val is_select : Expr.expr -> bool
val is_constant_array : Expr.expr -> bool
val is_default_array : Expr.expr -> bool
val is_array_map : Expr.expr -> bool
f
(a1,..,a_n)i
= f(a1i
,...,a_ni
) for every i.val is_as_array : Expr.expr -> bool
val is_array : Expr.expr -> bool
val get_domain : Sort.sort -> Sort.sort
val get_range : Sort.sort -> Sort.sort
val mk_const : context ->
Symbol.symbol -> Sort.sort -> Sort.sort -> Expr.expr
val mk_const_s : context -> string -> Sort.sort -> Sort.sort -> Expr.expr
val mk_select : context -> Expr.expr -> Expr.expr -> Expr.expr
The argument a
is the array and i
is the index
of the array that gets read.
The node a
must have an array sort [domain -> range]
,
and i
must have the sort domain
.
The sort of the result is range
.
Z3Array.mk_sort
Z3Array.mk_store
val mk_store : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
The node a
must have an array sort [domain -> range]
,
i
must have sort domain
,
v
must have sort range. The sort of the result is [domain -> range]
.
The semantics of this function is given by the theory of arrays described in the SMT-LIB
standard. See http://smtlib.org for more details.
The result of this function is an array that is equal to a
(with respect to select
)
on all indices except for i
, where it maps to v
(and the select
of a
with
respect to i
may be a different value).
Z3Array.mk_sort
Z3Array.mk_select
val mk_const_array : context -> Sort.sort -> Expr.expr -> Expr.expr
The resulting term is an array, such that a select
on an arbitrary index
produces the value v
.
Z3Array.mk_sort
Z3Array.mk_select
val mk_map : context -> FuncDecl.func_decl -> Expr.expr list -> Expr.expr
Eeach element of args
must be of an array sort [domain_i -> range_i]
.
The function declaration f
must have type range_1 .. range_n -> range
.
v
must have sort range. The sort of the result is [domain_i -> range]
.
Z3Array.mk_sort
Z3Array.mk_select
Z3Array.mk_store
val mk_term_array : context -> Expr.expr -> Expr.expr
Produces the default range value, for arrays that can be represented as
finite maps with a default range value.