關於Z3中數組的限制

Question

我有兩個關於Z3如何操作數組的問題。

1）在模型中，數組有一個「else」元素以及相應的值。有沒有一種方法來指定公式中數組上「else」元素的約束？例如，我們可以指定數組的第一個元素大於5，而其他所有元素都小於5？

2）當在命令行經由Z3檢查下列公式，

(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產生如下的輸出。

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))) 
) 

在通過Z3py檢查相同的公式時，會生成以下模型。

[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]] 

有趣的是，在a1提及k!0在Z3py 「引用」，即，a1指FuncInterp對象。情況總是如此嗎？特別是，如果一個程序在Z3py提供的模型上行走，假設所有的as_array表達式都將被解析爲底層函數定義是否安全？

Answer 1

數組有點特殊，因爲它們有一個func_interp模型。在Python API中，我們可以依賴dereferenced這是get_interp函數，它可以幫助我們：

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