java-smt icon indicating copy to clipboard operation
java-smt copied to clipboard

Add a swig build script for the bitwuzla backend

Open daniel-raffler opened this issue 2 years ago • 3 comments

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.

daniel-raffler avatar Jan 30 '24 03:01 daniel-raffler

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.

baierd avatar Jan 31 '24 16:01 baierd

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

daniel-raffler avatar Feb 01 '24 15:02 daniel-raffler

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

daniel-raffler avatar Feb 28 '24 21:02 daniel-raffler

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.

daniel-raffler avatar Mar 14 '24 16:03 daniel-raffler