-
Notifications
You must be signed in to change notification settings - Fork 1.5k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Performance issue with bitvectors combined with datatypes #6930
Comments
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. |
You can try the option sat.smt=true, which allows incremental pre-processing. It helps |
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. |
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). |
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 We made some progress by fiddling with Z3 options and other aspects of the setup. Unfortunately we have struggled to benefit directly from the Thanks for your help, and sorry this is turning out more difficult than expected. |
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):
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
The text was updated successfully, but these errors were encountered: