Most efficient way to represent memory buffers in Z3

Question

I would like to model fixed-size memory buffers and their access operations in Z3. The size of the buffers can be anywhere from a couple of bytes to hundreds of bytes. The standard way employed by several existing tools (e.g., KLEE) is to create array variables over the domain and range of bitvectors. Each memory buffer gets such an array and memory reads/writes are encoded using select/store operations.

Alas, in my benchmarks, when using this approach, Z3(*) appears to be consistently slower than STP. Before analyzing the queries in more detail to figure out what's going on, I wanted to make sure I'm using the "right" approach to encoding memory operations in Z3 (since, admittedly, STP was specifically designed to be used with arrays and bitvectors).

So what is the most efficient way of representing memory buffers in Z3? I'm considering a couple of alternatives thus far:

1. Use assertions to specify the initial values of the memory buffer, instead of using nested store-s. However, in my preliminary tests, this appears to slow down Z3 even more.
2. Use bitvectors to encode the buffers. However, the resulting bitvectors can get quite large (~1000s of bits), and I'm not sure Z3 or any other solver could handle that efficiently.
3. Create individual bitvector variables for each memory byte and use nested ite expressions to route memory accesses to corresponding variables. However, I'm afraid this would complicate the model quite a lot and introduce the need for quantifiers.
4. Use uninterpreted functions instead of arrays, but this requires redefining the array axioms in a way that may be less efficient than Z3's own built-in array theory.

Are there any better approaches that I'm missing?

(*) Default non-incremental solver, Z3 branch unstable@aba79802cfb5

Answer 1

There is one point about using arrays for KLEE style applications. Z3 does not work well if you initialize an array using an equation:

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

It is much more efficient to formulate such constraints as:

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

(which works when the indices are different constants or known to be different)

You can also turn off extensionality for arrays. Arrays are treated as extensional by default. It should not matter for KLEE style applications.