Update Yices to version 2.8.0

[daniel-raffler]

Hello,
this PR updates Yices to version 2.7.0 and closes #402. Other than that the new version mainly includes improvements to the MCSat solver, which we're not using at the moment. Here is a full changelog.

Yices2 has some additional features that we may want to include:

• Nonlinear arithmetic is supported with the MCSat solver
• MCSat also support interpolation (link), but not unsat core (yet?)
• Dpll (which we currently use) has unsat core, but no interpolation or non-linear arithmetic
• Only Dpll can be compiled with the --thread-safety option that allows multiple solver instances to run in parallel
• Arrays have been added separately, see here for the other pull request
• Yices can use Cadical/Kissat/CryptoMiniSat as backend for SAT solving. This could be significantly faster, but is currently limited to QF_BV logic

In this PR I stuck with Dpll as solver and just enabled the --thread-safety option. We could still add MCSat support and maybe even the external SAT solvers. Yices then picks the solver based on the logic, which would give us the best feature set. The big downside is that MCSat is not compatible with --thread-safety, which means that multiple parallel solver instances are not possible

Update

The thread-safety issues in MCSAT have been fixed, and unsat core is now also supported in MCSAT. We therefore switched to MCSAT as the default solver

• A new option solver.yices2.solverType=dpllt has been added to use dpllt instead
• Interpolation is now supported, thanks to the MCSAT solver
• Nonlinear arithmetics and division by zero are also working now

We also switched the entire backend to the official Java bindings for Yices. In addition, a new build script has been added, and Windows binaries are now available

This PR is currently waiting on SRI-CSL/yices2#614, but should be ready to merge otherwise

Linked issues:

• MC-SAT and thread safety SRI-CSL/yices2#608
• MCSAT crashes when generating models for curried functions SRI-CSL/yices2#613
• Yices crashes during interpolation SRI-CSL/yices2#615
• Rare crashes while popping a solver frame SRI-CSL/yices2#616
• Update Yices bindings and add some missing features SRI-CSL/yices2_java_bindings#8

[daniel-raffler]

@kfriedberger
I can try uploading the binaries this time. What architecture should I compile for? Yices2 seems to use --march=znver3 when I compile it on my laptop. Is that OK, or should I try to pick something else?

[kfriedberger]

@daniel-raffler
We did use the Ubuntu docker image (18.04 if possible without further overhead, else the 22.04) for building binary solvers.
The steps for publication are documented in https://github.com/sosy-lab/java-smt/blob/master/doc/Developers-How-to-Release-into-Ivy.md#publishing-yices2 ... wait ... that seems quite outdated for Yices2. I will have a deeper look the next days.

[kfriedberger]

Overall looks good. I will make a deeper test the next days.

[kfriedberger]

We could maybe add BOOL_RETURN for such methods.

[daniel-raffler]

@daniel-raffler We did use the Ubuntu docker image (18.04 if possible without further overhead, else the 22.04) for building binary solvers. The steps for publication are documented in https://github.com/sosy-lab/java-smt/blob/master/doc/Developers-How-to-Release-into-Ivy.md#publishing-yices2 ... wait ... that seems quite outdated for Yices2. I will have a deeper look the next days.

Thanks! I've been able to build the binaries in the 18.04 image

Should I build with --thread-safety or --enable-mcsat? Unfortunately these options can't be combined and I'm not quite sure which one is more important to us

[disteph]

Yices2 has some additional features that we may want to include:

* Nonlinear arithmetic is supported with the MCSat solver

* MCSat also support interpolation ([link](https://yices.csl.sri.com/doc/context-operations.html#c.yices_check_context_with_interpolation)), but not `unsat core` ([yet?](https://github.com/SRI-CSL/yices2/pull/578))

Just FYI, support for unsat cores in MCSAT has been merged into master (both through SMTLib2 input and through API calls): SRI-CSL/yices2#578.

It will be part of the upcoming Yices release 2.8.

[baierd]

Thank you for that info! Both features are actually requested by users that i talk to a lot currently!
@daniel-raffler we should focus on finishing this PR. It will most likely not make 6.0.0, but we can just publish 6.1 once this is done.

[daniel-raffler]

Some benchmark results:

From left to right: Yices old, Yices new (with dpllt), MathSAT (for reference)

Comparison between dpllt and mcsat:

We get significantly better results with dpllt (light brown), then with mcsat. Part of this is due to some open issues that cause segfaults in mcsat. However, this can't explain the difference entirely, and dpllt does currently seem to outperform mcsat at least on some tasks. (Note that interpolation always has to be done with mcsat, even when the dpllt option is used. So the comparison isn't entirely fair, and we would get much worse results for dpllt if it wasn't for this fallback)

[daniel-raffler]

I've added binaries for Windows. They seem to be working in Wine, but we may need some more testing

Yices has github actions (link) to build the solver on MacOS. We could probably start from there if we also want to support that platform

[daniel-raffler]

@kfriedberger Just a heads up: If you want to build the binaries, we need the issue-613-mcsat-curried-function-model branch

You can download yices like this:

ant download-yices2

Then go to downloads/yices2 and change the branch:

cd downloads/yices2
git checkout issue-613-mcsat-curried-function-model

After that, just follow the build instructions

[kfriedberger]

Is there a plan to integrate https://github.com/daniel-raffler/yices2_java_bindings.git into its original? Just asking, not urgent.

[daniel-raffler]

Is there a plan to integrate https://github.com/daniel-raffler/yices2_java_bindings.git into its original? Just asking, not urgent.

Yes, I've open a PR last week: SRI-CSL/yices2_java_bindings#8

[ThomasHaas]

Yices has github actions (link) to build the solver on MacOS. We could probably start from there if we also want to support that platform

I would love Yices2 support on MacOS (ARM). It usually outperforms Z3 (and others) by quite a lot on our QF_BV encoding in Dartagnan (sometimes by a whole order of magnitude). It seems to do some serious black magic there :)

[daniel-raffler]

Hello Thomas,

I've been able to build the MacOS (Arm) binaries with a github runner. We still have to figure out to sign and ship the binaries, but I can at least include the build script. It's not too complicated to run and the binaries can then just be copied over

Yices has github actions (link) to build the solver on MacOS. We could probably start from there if we also want to support that platform

I would love Yices2 support on MacOS (ARM). It usually outperforms Z3 (and others) by quite a lot on our QF_BV encoding in Dartagnan (sometimes by a whole order of magnitude). It seems to do some serious black magic there :)

Is this with the default solver, or would we need one of these delegates? So far we only have the internal solver, but we might still add one of the delegates

[ThomasHaas]

I've been able to build the MacOS (Arm) binaries with a github runner. We still have to figure out to sign and ship the binaries, but I can at least include the build script. It's not too complicated to run and the binaries can then just be copied over

Sounds great.

I would love Yices2 support on MacOS (ARM). It usually outperforms Z3 (and others) by quite a lot on our QF_BV encoding in Dartagnan (sometimes by a whole order of magnitude). It seems to do some serious black magic there :)

Is this with the default solver, or would we need one of these delegates? So far we only have the internal solver, but we might still add one of the delegates

The default internal solver. Funnily enough, that one outpeforms Kissat and Cadical on our benchmarks.
To test that, we generated QF_BV encodings, used Yices2 to bitblast them into DIMACS and then re-parsed the file with Yices2 but different SAT solver backends (internal/kissat/cadical). The internal SAT solver was the fastest!
Also, Kissat does not support incremental solving, so it's not so interesting in the first place I think.
Similarly, MCSAT is extremely bad on bitvector arithmetic and I think multi-threaded solving is also quite bad...
Basically, we only care about the default setting for now :)

[kfriedberger]

Thanks for the input, everyone. A couple of thoughts on the direction of the latest discussion here:

First, I think it's important that we keep JavaSMT vendor-independent when it comes to our build process. We should avoid being tied too closely to GitHub Actions for publishing; the goal is to ensure any user can still build the library reliably on their own local machine. Apple is kind of special here, maybe we find a way with tools like osxcross/ldid/rcodesign in the future.

Regarding the macOS-specific points, there are multiple solvers waiting for macOS:

• Yices2 (maybe outdated PR): Yices2 MacOS Support #400
• MathSAT (integrated, but maybe only used once): Extend compile.sh for libmathsat5j for macOS dylib #430

Should we move that conversation over to a separate issue? It feels like it deserves its own space for discussion and debugging without cluttering the Yices update.

[kfriedberger]

@daniel-raffler :
The current state looks good. 👍
Do you see anything blocking a merge? If not, let's merge. ⏩
Further updates can be applied in another PR, e.g., after merging SRI-CSL/yices2_java_bindings#8 and the "final" release of Yices 2.8.0. Version 2.7.0+X is sufficient for today.
You have done great work in updating these solver bindings. 🥇