我想知道是否可以让 Z3 “记住”数组的更新。
例如，以下输入是可以满足的:
(declare-const x Int)
(declare-const a1 (Array Int Int))
(assert (= (select (store a1 x 2) x) 2))
(assert (not (= (select a1 x) 2)))
(check-sat)
第一个断言中的“store”不会影响第二个断言。 我可以对数组进行存储操作，从而导致数组发生永久更改吗？ 我的意思是，如果我在数组上使用存储，那么数组就会永远改变。 例如，如果我使用“(store a1 x 2)”之后，那么每次 (select a1 x) 都等于 2。 有人知道这个吗？ 谢谢。
最佳答案
表达式(= (select (store a1 x 2) x) 2) 等价于true。这是一个空洞的断言，因为数组理论公理之一是forall a,i,v: select(store(a,i,v), i) = v。因此，这个表达式只是公理(内置于 Z3 中)的一个实例，因此它是多余的。
也许，您打算断言(assert (= (select a1 x) 2))。此断言表示位置 x 处的数组值为 2。也就是说，Z3 生成的任何解决方案都必须将 2 分配给数组 a1 的该位置。
请注意，Z3 中没有断言“之前”和“之后”的概念或副作用。
例如，表达式a = a + 1相当于Z3中的false。用于将编程语言赋值编码到 Z3 中的一种常见技术对每个程序变量使用多个变量。每个“程序位置”有一个变量。例如，代码块a = a + 1; b = 2*a； a = b + 1 编码为 a_1 = a_0 + 1 和 b_1 = 2*a_0 和 a_2 = b_1 + 1。
以下文章包含更多示例/详细信息:http://dl.acm.org/citation.cfm?id=1995394
如果您打算对程序中使用的数组更新进行编码，则应该有一个数组 a1 代表更新前的数组，以及一个数组 a2 代表更新后的数组更新后。
也就是说，我们编写:(assert (= a2 (store a1 x 2)))，并将最后一个断言替换为 (assert (not (= (select a2 x) 2)) )
关于arrays - 关于Z3中的数组理论，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/12532627/