sosy-lab
Re-enable Z3 4.5.0 for better interpolation (continuation of #536)
This PR continues the work from PR536 with support from our CI etc.
Original PR description from @leventeBajczi: Old versions of z3 were really good at interpolation, and I want to add support for it in JavaSMT.
To this end, I've added the implementation of a Z3Legacy solver (to be renamed, as discussed with @baierd), which builds on the 4.5.0 release of z3, rebuilt to use com.microsoft.z3legacy as its package name to avoid name collisions with new z3.
Pre-built binaries with the modifications are available at https://github.com/leventeBajczi/z3/releases/tag/legacy-4.3.0-15644597379, which Theta already uses like this. This should be somehow integrated into the solver management of JavaSMT, which I have no experience with.
To demonstrate how good this version of Z3 is, I ran some preliminary tests in CPAchecker, and found that an NLA encoding of programs using Z3 as the interpolation solver in the predicate analysis configuration results in 510 successfully solved tasks, which are otherwise unsolved by the bitprecise encoding of the same tasks with mathsat5.
Also, I found that https://github.com/sosy-lab/java-smt/issues/381 (which I opened) is referenced in 3 of the tests, that now failed on this implementation. I removed the overly constraining line which expected the constraint IDs to be unique, which is not necessary IMO if the interpolation problem reported in that issue is otherwise handled - which it seems to be.
@kfriedberger: I see that in ac68cf89700ea8c4fbb1071cba6895e3d8dcf7f5, you re-enabled the assertions I commented out. My understanding is that these tests are checking if my issue in https://github.com/sosy-lab/java-smt/issues/381 applies to the solver, but I don't think the equivalence of the handle for the formulas is necessarily a good way to test this. The issue was that a repeated addition of formulas made interpolation not work, and I think that tests should test exactly that -- and in this case, legacy Z3 fails the current tests, but otherwise pass the original issue's tests. What do you think?
@leventeBajczi points for noticing ✔️ The tests were just a smaller issue: Please do not disable tests that are intended for all solvers, when just adding one new solver, but rather use an assume-is-not-statement for LegacyZ3, if required. Additionally, there were several compiler warnings from around the disabled code that were not fixed properly. As soon as we get a properly compiled and released version of LegacyZ3 v4.5.0 included into JavaSMT (which we currently do not yet have managed), we will take another look at the tests.
Thanks, great! (Just for the record -- I agree with not disabling tests in general, but in this case, I think that removing that assertion doesn't defeat the original purpose of the test IMO)
@leventeBajczi and @baierd : Is there any reason to use Z3 4.5.0 from 07-2016 instead of the latest version with interpolation support from around 05-2018? Was this just an example that provided interpolation support? The version from 2016 seems to suffer from parser issues (and some other issues :smile:), maybe related to a bug with signed/unsigned-int. We might not fix such bugs within JavaSMT, as the used version of Z3 is quite outdated.
@kfriedberger It's purely because this was the one version that we (in Theta) use, and therefore, I can attest to it being useful and usable in a lot of situations. I don't have any experience with the newer versions that could still interpolate.
I wouldn't have any problems this being ported over to the newest still-interpolating version of z3, but then we'd really need to test it thoroughly -- both for performance and for buggyness. Although I would expect the latter aspect to only improve.
Current status:
- Z3 legacy v4.5.0 is available in SVN as dev1-version (only for Linux x64, no Windows or MacOS support, no ARM support).
- JavaSMT contains sufficient bindings for LegacyZ3 and supports latest features, such as model and evaluator improvements.
Known bugs:
- LegacyZ3 does not support parsing SMTLIB. We might need an update of LegacyZ3 for that.
- String theory does not properly handle UTF8 or several String operations. Z3 is too old for that.
We simply disable support for theories/logics that are handled "better" in the up-to-date Z3 versions. The main purpose of the solver is interpolation support, so everything not included in that has little benefit.