Add new SMT solver: Bitwuzla

[kfriedberger]

The team of Boolector developed a new SMT solver Bitwuzla that seems to be quite fast for bitvector logic (see results of SMT-COMP 2020). Bitwuzla seems to be the successor of Boolector (which has some reported limitations in its API) and might be maintained for longer.

Currently, Bitwuzla is not yet publicly available, and API documentation is missing. Implementing suppport for this new solver into JavaSMT might be a nice student project.

TODO:

• [x] ask the developers of Bitwuzla to publish their solver under a decent license (Apache or LGPL would be preferred, GPL itself is not ideal).
• [ ] optional: ask the developers of Bitwuzla to support Linux and Windows in their build scripts, because we would like to also have a Windows version of each solver. We aim for (cross-)compiling everything via GCC or MinGW on a Linux host.
• [x] implement the JNI and Java bindings for the solver (maybe they are similar to Boolector's bindings, from where we could copy some parts)
• [x] test it (several JUnit already available)
• [x] evaluate it (e.g. benchmarks with CPAchecker)

[baierd]

Bitwuzla currently has no API to traverse formulas or parse formulas without solving them right away. Also it does not mention any form of reentrant mode/compiliation process currently.

Since those are rather important for us, i've asked the devs for all of this in the discussion board of their GutHub presence:

• Term traversal and term parsing
• Reentrant Bitwuzla

[baierd]

The Devs answered and term traversal is possible, the API was just not publicly stated in the API website, but its useable and fits our purposes. Also, Bitwuzla is already reentrant.

They are very interested in adding term parsing and i provided an example.

[baierd]

The license under which Bitwuzla is published is the MIT license.