在使用 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
最佳答案
感谢您报告问题。这是数组预处理器中的一个错误。预处理器在调用实际求解器之前简化了数组表达式。该错误仅影响使用常量数组的问题(例如, ((as const (Array Int Int)) 0)
)。您可以通过不使用常量数组来解决该错误。我修复了这个错误,修复将在下一个版本中可用。
关于arrays - Z3 中的 SMTLIB 阵列理论奇怪,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/9431739/