我想知道，我是否可以让 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 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 and b_1 = 2*a_0 and a_2 = b_1 + 1。
以下文章包含更多示例/详细信息：http://dl.acm.org/citation.cfm?id=1995394
如果您打算对程序中使用的数组更新进行编码，您应该有一个数组a1 代表更新前的数组，一个数组a2 代表更新后的数组。
也就是说，我们写：(assert (= a2 (store a1 x 2)))，并将最后一个断言替换为（断言(not (= (select a2 x) 2)))
【讨论】：