search

sosy-lab / java-smt

JavaSMT - Unified Java API for SMT solvers.
Apache License 2.0
180 stars 46 forks source link

Add a swig build script for the bitwuzla backend #353

Closed daniel-raffler closed 6 months ago

daniel-raffler commented 8 months ago

Hello everyone, this patch set removes all auto generated code and adds a new swig script instead. This will help simplify upgrades to new Bitwuzla versions as changes to the API don't have to be patched in manually. There are still some phantom reference issues with the new JNI bindings and because of this memory reallocation is currently disabled.

The patch also includes a number of upgrades to the FloatingPointFormulaManager for Bitwuzla. Most importantly the swig script includes code that allows us to convert floating point values to their decimal representation. This was needed to build a model for formulas over floating point variables and can't be done with the Bitwuzla API alone.

baierd commented 8 months ago

We should split the 2 matters and include the FP fixes in the add_bitwuzla branch and PR.

And we need to check/discuss if we want auto-generated wrappers. They are quite useful for updates, but do not allow us custom modification and simplification for the wrapper. Which can be even a security problem, e.g. for generated files.

daniel-raffler commented 8 months ago

I've now opened a second pull request with just the floating point changes here.

daniel-raffler commented 7 months ago

I've updated this branch to use the new TermManager interface from Bitwuzla (see here).

daniel-raffler commented 6 months ago

Updated to the latest git version. Bitwuzla now has a new method to read back variables/functions that were defined during a parser run (see here). This helps us fix some issues we had when using the parser with variables that were defined through the API earlier.