Z3 中的 SMTLIB 阵列理论奇点

Question

在使用 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

Answer 1

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