arrays - 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。调用 select在索引 0 似乎证实了这一点:

(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) )。您可以通过不使用常量数组来解决该错误。我修复了这个错误，修复将在下一个版本中可用。