search

epfl-lara / ScalaZ3

DSL in Scala for Constraint Solving with Z3 SMT Solver
Apache License 2.0
123 stars 34 forks source link

Z3 4.8.14 #80

Closed mario-bucev closed 2 years ago

mario-bucev commented 2 years ago

To get getAbsFuncDecl working, we savagely apply a patch on the Z3 sources to export mkAbs. The other changes are mostly whitespace trimming (done by the editor...) and putting () to methods expecting them to address the warnings when cross-compiling to Scala 2.13

samarion commented 2 years ago

To get getAbsFuncDecl working, we savagely apply a patch on the Z3 sources to export mkAbs.

So much violence! :)

If the tests pass, this LGTM. It would probably be worth updating the unmanaged jars in Inox and Stainless as well.

mario-bucev commented 2 years ago

I had a quick glance at updating the unmanaged jars in Inox and some tests fail, but it should not be too hard to update them.

samarion commented 2 years ago

Hmm, failing tests don't sound too good. Is 4.8.12 a stable Z3 version? Which version are we shipping in the z3 binary?

mario-bucev commented 2 years ago

It seems so; what's weird is that all tests (in the master branch) that communicate with Z3 through SMT-LIB use the 4.8.12 version and all pass.

samarion commented 2 years ago

Which Inox tests are failing with this version? Maybe there's been a subtle API change in the native version which we have to take into account?

Maybe you can try a different Z3 version otherwise?

mario-bucev commented 2 years ago

The Z3 Set Extraction test (in SemanticsSuite, for nativez3 and unrollz3 only) as well as the Model Extraction test (in SolversSuite, only for nativez3). I'll investigate the issue and try your suggestion as well.

samarion commented 2 years ago

Ah, then it's fairly likely that we're running into bugs in Inox if it's only about model extraction.

mario-bucev commented 2 years ago

Z3 is returning a lambda which Z3Native does not currently support. Maybe we can do something similar to what is done in Z3Target: https://github.com/epfl-lara/inox/blob/efd76f30e486a89fc4fc33c073a69f3bf2bfd052/src/main/scala/inox/solvers/smtlib/Z3Target.scala#L187-L209 (or try with a different Z3 version)

samarion commented 2 years ago

Adapting Z3Native to handle lambdas like Z3Target sounds like a plan.

mario-bucev commented 2 years ago

Upgrading to 4.8.14 resolves the problem with the set extraction, as Z3 no longer returns lambdas (seems to be related to the fix of https://github.com/Z3Prover/z3/issues/5604). There are some integration tests that fail though (I did not run 4.8.12 on the integration tests, but they are likely to fail as well).

mario-bucev commented 2 years ago

With some small changes, all Inox tests pass. Stainless does not need any adaptations (except for its dependencies of course), and one Bolts benchmark, gcd, needs one tiny change.

samarion commented 2 years ago

That sounds reasonable. Can you please open a PR with the Inox changes too?

mario-bucev commented 2 years ago

Sure! Here it is: https://github.com/epfl-lara/inox/pull/175