z3 - Z3 中的建模数组赋值

Question

我正在做一个程序验证项目。我有以下语句要在 Z3 中建模：

temp = a[i];
a[i] = a[j];
a[j] = temp;

所有变量都是整数类型。有人会给我一些关于如何建立约束来模拟上述语句的提示吗？

Answer 1

这是一个通用的“食谱”。

我们使用 表示数组更新(store a i v)。结果是一个等于 的新数组a，但在位置i包含值v。数组访问a[i]应编码为(select a i). 诸如此类的赋值i = i + 1通常是通过创建代表i赋值前后的值的 Z3 变量来编码的。也就是说，我们会将其编码为(= i1 (+ i0 1)). 请记住，公式(= i (+ i 1))等价于false。

这是上面以 SMT 2.0 格式编码的示例。

http://www.rise4fun.com/Z3/G5Zk

这是在上面的链接中找到的脚本。

(declare-const a0 (Array Int Int))
(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))
(declare-const temp0 Int)
(declare-const temp1 Int)
(declare-const i0 Int)
(declare-const j0 Int)

(assert (= temp0 (select a0 i0)))
(assert (= a1 (store a0 i0 (select a0 j0))))
(assert (= a2 (store a1 j0 temp0)))

(check-sat)
(get-model)