SMTLIB数组理论在Z3中的奇怪之处

Question

在使用SMTLIB数组时，我注意到Z3对该理论的理解与我的不同。我使用的是SMTLIB数组理论，可以在官方网站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 1

Answer 1

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