6

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

Z3sat为两者返回。

(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

4

1 回答 1

3

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

于 2012-02-24T16:39:09.543 回答