Add bitwuzla

[kfriedberger]

[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. #330
• 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.

[baierd]

Update on the formula dump: I've added the "proper" printout (which adds all that is needed to parse it as SMTLIB2), but it still does fail in changing the symbol names. I've reported it to the Bitwuzla devs.

I also noticed some things that are problematic. Firstly, when trying to parse a query that is in some form malformed or incomplete, the parser crashes the program in a non-recoverable state. I will construct a program showcasing this and send it to the devs. Also, parsing (check-sat) results in an automatic SAT check, even if disabled in the parser. It also rewrites formulas, which can not be stopped by options. I remove all (check-sat) Strings from queries that are parsed for now. Besides that, parsing and dumping is now working.

[baierd]

I've temporarily disabled the tests for quantifiers, FP and some singular ones for parsing/symbol names. Besides that, the PR is ready for review.

[baierd]

Quantifiers are now fixed and seem to work properly. Elimination is not possible because Bitwuzla does not support this feature.

[daniel-raffler]

I've opened a new discussion about our issues with the parser on the Bitwuzla bugtracker: https://github.com/bitwuzla/bitwuzla/discussions/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.