Performance issue with bitvectors combined with datatypes

[talsewell]

I'm experimenting with adjusting a Z3-based tool to produce bitvector encodings of its problems rather than integer encodings. This is producing surprising performance regressions.

The tool I'm working on is called CN, and it does analysis and verification of C programs, and can be found here https://github.com/rems-project/cerberus as part of the Cerberus project, in case that is of interest.

This example illustrates the problem (also attached as match_z3_2.smt2.txt):

(declare-datatypes ((i32 0)) (((i32 (unsigned_32 (_ BitVec 32))))))
(declare-fun x () i32)
(declare-datatypes ((kv_tree 0)) (((Empty)
  (Node (node_k i32) (node_l kv_tree)
  (node_r kv_tree) (node_v i32)))))
(declare-fun tr () kv_tree)
(assert (= tr (Node (i32 #x00000001) Empty
    (Node (i32 #x00000003) Empty Empty (i32 #x00000000)) x)))
(declare-fun defaulti32 () i32)

(define-fun tree_k_v_sum () i32
    (i32 (bvadd (unsigned_32 (node_k tr)) (unsigned_32 (node_v tr)))))
(define-fun x_plus_1 () i32
    (i32 (bvadd (unsigned_32 x) #x00000001)))
(define-fun fetch_tree_k_v_sum () i32
    (ite (and ((_ is (Empty () kv_tree)) tr)) (i32 #x00000000)
        (ite ((_ is (Node (i32 kv_tree kv_tree i32) kv_tree)) tr) tree_k_v_sum defaulti32)))

(check-sat)
(check-sat (not (= fetch_tree_k_v_sum x_plus_1)))

This declares a tree datatype, names a value tr which is asserted equal to a concrete tree shape of 2 nodes, and does a simple pattern match on it. The pattern match is encoded via the (_ is ...) expressions, and the encoding might not be ideal. I've constructed this example by reducing and cleaning up an example produced by CN.

The additional i32 datatype is used to wrap 32-bit bitvectors into an isomorphic type. The idea was to have different types for encoding signed and unsigned bitvectors, which are different types at our end.

This problem takes Z3 a few seconds to solve. This is a major performance regression. Replacing bitvectors with integers creates a variant problem (attached as match_z3_3.smt2.txt) which solves in milliseconds. I've tested this on my local machine for Z3 versions 4.10.2, 4.8.12 and 4.12.2. Version 4.12.2 was about 50% faster, but still much slower than for integers.

This is all a bit surprising. No doubt bitvectors are generally a little more difficult than integers. However, I've had good experience with Z3 on bitvector problems in the past, and CN works well enough with datatypes and integers. Is there something special about the combination of datatypes and bitvectors which we should watch out for?

The wrapping i32 datatype in this example is unnecessary. If we remove it, we get the version attached as match_z3_4.smt2.txt, which Z3 solves in milliseconds. We've now removed the use of these wrapping datatypes in the encoding, which has improved performance a bit, but has not eliminated the worst performance issues.

Unfortunately, there is still a bigger example that is timing out, and issue we haven't had with our integer version. One version of this example is attached as mut_tree_z3.smt2.txt. We haven't yet tried to minimise or clean up that particular example problem.

Hopefully you have some insight for us! We'd be happy for any of these examples to be used as test cases.

match_z3_2.smt2.txt match_z3_3.smt2.txt match_z3_4.smt2.txt mut_tree_z3.smt2.txt

[talsewell]

After discussion with colleagues, we note that Z3 4.12 does seem to solve the most challenging of these (mut_tree_z3.smt2.txt) whereas previous Z3 versions seemed to time out on it entirely.

This probably gives us a way to proceed, but we'd still like to know more about the performance questions here.

[NikolajBjorner]

You can try the option sat.smt=true, which allows incremental pre-processing. It helps

[talsewell]

Thanks for that hint. It does indeed seem to solve the performance problem, when processing this problem as a standalone instance. It doesn't seem to make much difference when using the solve in incremental mode via the API. We'll keep experimenting with how we call the solver.

[NikolajBjorner]

sat.smt=true solver remains still a bit hidden. It has other issues, but for the first sample it shows that incremental pre-processing helps a lot. The assumption can be simplified modulo assertions. The example also suggested that I pre-process all assertions before processing the assumption (which could require replaying some simplified assertions).

[talsewell]

We've continued with this, have a new example, and some more questions.

We now have a smaller example that clearly demonstrates the timeout. This example is, essentially, a simple identity on bitvectors, wrapped in some repeated construction and destruction of wrapper tuple types. With sat.smt=true it solves instantly, without that setting it times out. I'm not sure if that's useful.

small_z3_timeout.smt2.txt

We made some progress by fiddling with Z3 options and other aspects of the setup. Unfortunately we have struggled to benefit directly from the sat.smt=true setting. While that seems to completely fix the performance issues when Z3 is called on the command line, we've been using Z3 via the OCaml API. It seems that solver variants documented as incremental are insensitive to sat.smt. Is that expected? We seem to be able to use sat.smt=true via the from-tactic Solver.mk_solver_t or the combined solver, which seem have their own downsides. I'll try to report an actual crash we've been seeing separately, for instance.

Thanks for your help, and sorry this is turning out more difficult than expected.