Add bitwuzla

[kfriedberger]

No description provided.

[baierd]

Bitwuzla has several critical issues that need to be resolved before it can be merged:

• Bitwuzla does not add || around symbol names with non valid characters. Example: main::a should be returned as |main::a|. SMTLIB2.6 states that both symbols are equivalent. So this might be a non-issue in the end. But we should nevertheless decide if this is critical to us (in regard to CPAchecker for example) and if we want to solve this ourselfs.
• It is not possible to get a decimal value out of a Floating-Point value. (And this is extremely hard to solve in Java) I already requested help however.

There are also minor issues that can be resolved later:

• Bitwuzla changes existing terms when substituting subterms. I've created an issue for this and explained why this is a problem for quantifiers.
• Parsing equal queries with Bitwuzla results in non-equal formulas. Parsing equal queries with Bitwuzla results in non-equal formulas #330
• Bitwuzla crashes with SIGABRT on failed parse Bitwuzla crashes with SIGABRT on failed parse #329

[baierd]

@kfriedberger could you review the model, especially the ValueAssignments for UFs and Arrays for me please? I would like some feedback for my implementation.

[baierd]

It seems like trivial Boolean based formulas are rewritten/simplified by Bitwuzla even if the option BITWUZLA_OPT_REWRITE_LEVEL is set to no rewrites. However, since dumping of formulas is currently being done by a selfmade method in Java based on the visitor instead of the Bitwuzla native API call bitwuzla_print_formula(). I plan on wrapping bitwuzla_print_formula() in our JNI wrapper, such that we can use it and then test again. (bitwuzla_print_formula() wants a file to dump into, so it is significantly easier to handle this in the C wrapper directly.)

[baierd]

Update on the symbol naming: if there is a space in a symbol name, we expect that the symbol name will be wrapped in || (similar to the main::a problem described above, just that spaces need to be encased.). The dump of Bitwuzla does not do this currently. However, since we are not using Bitwuzlas dump mechanism, but a selfmade one, i will test this again after i added the native dump function.

[daniel-raffler]

I've opened a new discussion about our issues with the parser on the Bitwuzla bugtracker:
bitwuzla/bitwuzla#101

[baierd]

I've published the new version 0.3.1 and updated our code for it.
The only 2 issues are the parsing problem mentioned above and that we can't use formulas on stacks distinct to the creation stack. But both don't block a merge in my opinion.
There is a test failing because of the outdated CI. So we need to update that.

We should update the CI and then we can merge.

[baierd]

Formulas in the new version of Bitwutzla just released are now capable of being used thread independently.
We should update our wrapper and code before merging this.