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.

Each 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.

val mk_array_ext : context -> Expr.expr -> Expr.expr -> Expr.expr

Create array extensionality index given two arrays with the same sort.

The meaning is given by the axiom: (=> (= (select A (array-ext A B)) (select B (array-ext A B))) (= A B))