在 Z3 中表示内存缓冲区的最有效方法

Question

我想在 Z3 中对固定大小的内存缓冲区及其访问操作进行建模。缓冲区的大小可以从几个字节到数百个字节不等。几个现有工具（例如，KLEE）采用的标准方法是在位向量的域和范围内创建数组变量。每个内存缓冲区都会获得这样一个数组，并且内存读/写使用select/store操作进行编码。

唉，在我的基准测试中，使用这种方法时，Z3(*) 似乎始终比 STP 慢。在更详细地分析查询以弄清楚发生了什么之前，我想确保我使用了“正确”的方法来编码 Z3 中的内存操作（因为，无可否认，STP 专门设计用于数组和位向量）。

那么在 Z3 中表示内存缓冲区的最有效方法是什么？到目前为止，我正在考虑几个替代方案：

1. 使用断言来指定内存缓冲区的初始值，而不是使用嵌套的store-s。然而，在我的初步测试中，这似乎更能减慢 Z3 的速度。
2. 使用位向量对缓冲区进行编码。但是，生成的位向量可能会变得非常大（约 1000 位），我不确定 Z3 或任何其他求解器是否可以有效地处理它。
3. 为每个内存字节创建单独的位向量变量，并使用嵌套ite表达式将内存访问路由到相应的变量。但是，我担心这会使模型复杂化并引入对量词的需求。
4. 使用未解释的函数而不是数组，但这需要以可能比 Z3 自己的内置数组理论效率低的方式重新定义数组公理。

有没有更好的方法我错过了？

(*) 默认非增量求解器，Z3 分支 unstable@aba79802cfb5

Answer 1

关于在 KLEE 风格的应用程序中使用数组有一点。如果您使用等式初始化数组，则 Z3 无法正常工作：

  (assert (= A (store (store (store .. (store A0 i1 v1) ..) i4 v4) i5 v5)))

制定以下约束要有效得多：

  (assert (= (select A i1) v1))
  (assert (= (select A i2) v2))

（当指数是不同的常数或已知不同时有效）

您还可以关闭数组的扩展性。默认情况下，数组被视为可扩展的。对于 KLEE 风格的应用程序，这应该无关紧要。