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

Question

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

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

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

Use assertions指定内存缓冲区的初始值，而不是使用嵌套 store -s。然而，在我的初步测试中，这似乎更能减慢 Z3 的速度。

使用位向量对缓冲区进行编码。但是，生成的位向量可能会变得非常大(约 1000 位)，我不确定 Z3 或任何其他求解器是否可以有效地处理它。

为每个内存字节和 use nested ite expressions 创建单独的位向量变量将内存访问路由到相应的变量。但是，我担心这会使模型复杂化并引入对量词的需求。

使用未解释的函数而不是数组，但这需要以可能比 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 风格的应用程序，这应该无关紧要。