arrays - Z3中的SMTLIB阵列理论奇数

在使用SMTLIB阵列时，我注意到Z3对理论和我的理解之间的差异。我正在使用SMTLIB阵列理论[0]，该理论可以在官方网站[1]上找到。

我认为我的问题最好用一个简单的例子来说明。

(store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0)
       (store (store ((as const (Array Int Int)) 0) 0 1) 1 2)

第一个数组应在索引1处返回2，对于所有其他索引返回0，第二个数组应在索引0处返回1，在索引1处返回2，对于所有其他索引返回0。在索引0处调用select似乎可以确认这一点：

(assert
    (=
        (select (store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) 0)
        0
    )
)
(assert
    (=
        1
        (select        (store (store ((as const (Array Int Int)) 0) 0 1) 1 2)      0)
    )
)

Z3都返回sat。

(assert
    (=
        (select (store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) 0)
        (select        (store (store ((as const (Array Int Int)) 0) 0 1) 1 2)      0)
    )
)

不出所料，在这种情况下，Z3（在重要的情况下，我正在linux-amd64上使用3.2版）回答unsat。接下来，让我们比较这两个数组：

(assert
    (=
        (store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0)
               (store (store ((as const (Array Int Int)) 0) 0 1) 1 2)
    )
)

Z3告诉我sat，我将其解释为“这两个数组比较相等”。但是，我希望这些数组不能比较相等。我基于SMTLIB阵列理论，该理论说：

- (forall ((a (Array s1 s2)) (b (Array s1 s2)))
    (=> (forall ((i s1)) (= (select a i) (select b i)))
            (= a b)))

因此，用通俗的英语来说，这将意味着“两个数组在所有索引相等且相等时才相等”。有人可以向我解释吗？我是否缺少某些东西或对理论有误解？对于您对此问题的任何想法，我将不胜感激。

最好的祝福，
里昂

[0] http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2
[1] http://smtlib.org

最佳答案

感谢您报告问题。这是数组预处理器中的错误。在调用实际的求解器之前，预处理器会简化数组表达式。该错误仅影响使用常量数组（例如((as const (Array Int Int)) 0)）的问题。您可以通过不使用常量数组来解决该错误。我已修复该错误，该修复程序将在下一版本中提供。