Array Constraints in Z3
I have two questions about how Z3 works with arrays.
1) In models, arrays have an "else" element along with the corresponding value. Is there a way to specify constraints on the "else" element in an array in a formula? For example, can we indicate that the first element of the array is greater than 5 and all other elements are less than 5?
2) After checking the following formula via z3 on the command line
(set-logic QF_AX)
(declare-sort Index 0)
(declare-sort Element 0)
(declare-fun a1 () (Array Index Element))
(declare-fun i0 () Index)
(declare-fun i1 () Index)
(assert
(let
(
(?v_1 (select a1 i0))
(?v_2 (select a1 i1))
)
(
not(= ?v_1 ?v_2)
)
)
)
Z3 generates the following output.
sat
(model
;; universe for Index:
;; Index!val!1 Index!val!0
;; -----------
;; definitions for universe elements:
(declare-fun Index!val!1 () Index)
(declare-fun Index!val!0 () Index)
;; cardinality constraint:
(forall ((x Index)) (or (= x Index!val!1) (= x Index!val!0)))
;; -----------
;; universe for Element:
;; Element!val!1 Element!val!0
;; -----------
;; definitions for universe elements:
(declare-fun Element!val!1 () Element)
(declare-fun Element!val!0 () Element)
;; cardinality constraint:
(forall ((x Element)) (or (= x Element!val!1) (= x Element!val!0)))
;; -----------
(define-fun i1 () Index
Index!val!1)
(define-fun a1 () (Array Index Element)
(_ as-array k!0))
(define-fun i0 () Index
Index!val!0)
(define-fun k!0 ((x!1 Index)) Element
(ite (= x!1 Index!val!0) Element!val!0
(ite (= x!1 Index!val!1) Element!val!1
Element!val!0)))
)
After checking the same formula through Z3py, the following model is generated.
[i1 = Index!val!1,
a1 = [Index!val!0 -> Element!val!0,
Index!val!1 -> Element!val!1,
else -> Element!val!0],
i0 = Index!val!0,
k!0 = [Index!val!0 -> Element!val!0,
Index!val!1 -> Element!val!1,
else -> Element!val!0]]
Interestingly, the reference to k!0
in is a1
"dereferenced" in Z3py; a1
refers to the object FuncInterp
. It's always like that? In particular, if the program follows the model provided by Z3py, is it safe to assume that all expressions as_array
will be resolved to the base function definition?
source to share
Arrays are a special case as they have func_interp. In the Python API we can rely on this dereferenced
, this is the function get_interp
that does it for us:
def get_interp(self, decl):
...
if decl.arity() == 0:
r = _to_expr_ref(Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast), self.ctx)
if is_as_array(r):
return self.get_interp(get_as_array_func(r)) # <-- Here.
else:
return r
source to share