Module Z3.Z3Array

module Z3Array: sig .. end
Functions to manipulate Array expressions

val mk_sort : context -> Sort.sort -> Sort.sort -> Sort.sort
Create a new array sort.
val is_store : Expr.expr -> bool
Indicates whether the term is an array store. It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j). Array store takes at least 3 arguments.
val is_select : Expr.expr -> bool
Indicates whether the term is an array select.
val is_constant_array : Expr.expr -> bool
Indicates whether the term is a constant array. For example, select(const(v),i) = v holds for every v and i. The function is unary.
val is_default_array : Expr.expr -> bool
Indicates whether the term is a default array. For example default(const(v)) = v. The function is unary.
val is_array_map : Expr.expr -> bool
Indicates whether the term is an array map. It satisfies mapf(a1,..,a_n)i = f(a1i,...,a_ni) for every i.
val is_as_array : Expr.expr -> bool
Indicates whether the term is an as-array term. An as-array term is n array value that behaves as the function graph of the function passed as parameter.
val is_array : Expr.expr -> bool
Indicates whether the term is of an array sort.
val get_domain : Sort.sort -> Sort.sort
The domain of the array sort.
val get_range : Sort.sort -> Sort.sort
The range of the array sort.
val mk_const : context ->
Symbol.symbol -> Sort.sort -> Sort.sort -> Expr.expr
Create an array constant.
val mk_const_s : context -> string -> Sort.sort -> Sort.sort -> Expr.expr
Create an array constant.
val mk_select : context -> Expr.expr -> Expr.expr -> Expr.expr
Array read.

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
Array update.

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
Create a constant array.

The resulting term is an array, such that a selecton 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
Maps f on the argument arrays.

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
Access the array default value.

Produces the default range value, for arrays that can be represented as finite maps with a default range value.