关于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