Adding missing features to the Bitwuzla bindings by daniel-raffler · Pull Request #369 · sosy-lab/java-smt

daniel-raffler · 2024-04-09T11:26:53Z

Hello everyone,
this pull request updates the Bitwuzla bindings with several features that have been added in the past few months:

Parsing is now fully supported. See Parsing in Bitwuzla bitwuzla/bitwuzla#101
All floating point test were re-enabled, and we implemented a workaround to allow casting from float to bitvector. See Casting a Bitwuzla term from float to bitvector bitwuzla/bitwuzla#103
The new TermManager interface that was added recently is now used. This solves the concurrency problems we had with older versions of Bitwuzla.
We included a SWIG script to auto-generate the JNI bindings whenever Bitwuzla is updated.

Open issues:

Due to phantom reference issues we had to disable some of the finalizers in the SWIG code. As a result old terms are not garbage collected, causing memory leaks.
I've seen a false positive in one of the CPAchecker benchmarks that seems to be caused by the fp casting workaround.

(This pull request is about moving the code from my fork to a new branch in the JavaSMT repository. It can then be merged with master from there.)

…o the C++ API.

…swig_cpp # Conflicts: # lib/native/source/libbitwuzla/compile.sh # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaOption.java

…lFunctionImpl as it seems unneeded.

…rom FloatingPointFormulaManagerTest.

…swig_cpp # Conflicts: # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaOption.java

…ws us to handle arbitrary size fp values. Improved native method mk_fp_value to handle scientific notation in input strings.

…finity'.

…d the affected tests and added a FIXME note to BitwuzlaFloatingPointManager.

…ovides a temporary fix to the phantom reference issue.

… to bitvector, which is not supported by the solver.

# Conflicts: # lib/ivy.xml # solvers_ivy_conf/ivy_bitwuzla.xml # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaArrayFormulaManager.java # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaBitvectorFormulaManager.java # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaBooleanFormulaManager.java # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaDeclaration.java # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormula.java # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaNativeApiTest.java # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaQuantifiedFormulaManager.java # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaUFManager.java # src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java # src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java # src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java

…ayFormulaManager.

…la does not support integer variables and will fail during parsing, even if integers are just mentioned in the signature of a function.

…twuzla will print variable declarations as define-const and not define-fun, so we have to check for both versions.

… with a solver that does not support int

…anguage level and avoid a warning.

…ipt. If this option is not specified, or set to false the SWIG wrapper will not be recreated.

…less trivial formula to parse. MathSAT would reduce the old formula to just "true", causing the failure.

…bitwuzlaJNI.

… moving

…0 (because the release is missing features for parse)

…ncy on libbitwuzla.so.0

daniel-raffler added 30 commits January 23, 2024 14:05

Bitwuzla: Added SWIG file to autogenerate JNI bindings and switched t…

93fd470

…o the C++ API.

Re-enabled dumpFormula in BitwuzlaFormulaManager.

68c9b64

Merge remote-tracking branch 'origin/add_bitwuzla' into add_bitwuzla_…

b3e6ea3

…swig_cpp # Conflicts: # lib/native/source/libbitwuzla/compile.sh # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaOption.java

Downgrade to local C++ build of Bitwuzla.

24a072a

Fixed includes in bitwuzla.i

573b6d2

Added bitwuzla_wrap.cpp to .gitignore

3671f10

Fixed a bug in BitwuzlaTheoremProver.getUnsatCore()

5f485ba

Improved error messages in BitwuzlaFormulaManager.parse()

44d4996

Fixed formating.

0a2431d

Fixed term substitution.

72772bb

Removed special case for BV_ZERO_EXTEND in BitwuzlaFormulaCreator.cal…

992cbe4

…lFunctionImpl as it seems unneeded.

Added termination hook.

bebae05

Removed duplicate %include from bitwuzla.i

bd3c009

Added default exception handler to the swig script.

33a328a

Make sure that rationals are supported in test rationalToFpMinusOne f…

b5d65f4

…rom FloatingPointFormulaManagerTest.

Fixed solver option description.

9fbbacd

Fixed handling of ProverOptions.Generate_MODELS

a3146e4

Merge remote-tracking branch 'origin/add_bitwuzla' into add_bitwuzla_…

8f0ab73

…swig_cpp # Conflicts: # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java # src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaOption.java

Fixed the last merge.

67043df

Bitwuzla: Added support for floating point values in the model.

7945be0

Bitwuzla: Re-enabled floating point tests.

aac0ffb

Bitwuzla: Rewrote Term.to_fp() to return a string as value. This allo…

126109c

…ws us to handle arbitrary size fp values. Improved native method mk_fp_value to handle scientific notation in input strings.

Bitwuzla: Fixed handling of negative zero in the JNI bindings.

e848771

Bitwuzla: Fixed bug in Term.to_fp() that affected the handling of 'In…

e7c09f6

…finity'.

Bitwuzla: Clear mpf in mk_fp_value.

0eac793

Bitwuzla does not seem to support casting float to bitvector. Disable…

de2258e

…d the affected tests and added a FIXME note to BitwuzlaFloatingPointManager.

Clean up bitwuzla_wrap.h in the build script.

9d3508b

Added patch to disable finalizers in the swig generated code. This pr…

93cc3c0

…ovides a temporary fix to the phantom reference issue.

Fix value type for bitvectors.

624a4f0

Disabled one more test for Bitwuzla as it requires casting form float…

334ba39

… to bitvector, which is not supported by the solver.

daniel-raffler added 7 commits April 9, 2024 11:31

Bitwuzla: Restored changes that were lost in the merge.

4bf6a71

Bitwuzla: Fixed the build script and updated the git version.

53cf8c9

Bitwuzla: Added new method for constant array creation to BitwuzlaArr…

9acfed2

…ayFormulaManager.

Bitwuzla: Restored changed to FormulaClassifierTest from 3372315

b0feace

Bitwuzla: Add requireInteger() checks to tests that need them. Bitwuz…

4066a3e

…la does not support integer variables and will fail during parsing, even if integers are just mentioned in the signature of a function.

Bitwuzla: Restored checkVariableIsDeclared in SolverFormulaIOTest. Bi…

8a50a25

…twuzla will print variable declarations as define-const and not define-fun, so we have to check for both versions.

daniel-raffler requested a review from baierd April 9, 2024 11:55

daniel-raffler and others added 19 commits April 9, 2024 14:05

Bitwuzla: Cleaned up some unnecessary changes.

49f26aa

Bitwuzla: Fixed format.

c3d65dd

Bitwuzla: Fixed some checkstyle issues.

c9ea122

Switch to current Bitwuzla dev version

49c6bc6

Format

54e90b9

Add support for SMTLIB2 comments to parse() for Bitwuzla

c32a817

Fix Java version when building bitwuzla script based jar

1516d6e

Disable tests that translate int formulas to SMTLIB2 and try to parse…

5d1d85a

… with a solver that does not support int

Improve ressource handling of Bitwuzla model

5023509

Bitwuzla: Use -release=11 when building the jar to also specify the l…

3ae7860

…anguage level and avoid a warning.

Bitwuzla: Add an option -Dbitwuzla.rebuildWrapper=on to the build scr…

566363d

…ipt. If this option is not specified, or set to false the SWIG wrapper will not be recreated.

Bitwuzla: Added auto-generated wrapper files to the repository.

10c62f8

Bitwuzla: Fixed test parseDeclareRedundantBv for MathSAT5 by using a …

961a4ef

…less trivial formula to parse. MathSAT would reduce the old formula to just "true", causing the failure.

Bitwuzla: Fixed the build script.

0df9aca

Bitwuzla: Removed unnecessary dependency on libgmp while building lib…

c1a256e

…bitwuzlaJNI.

Change Bitwuzla build script so that the JNI lib is patchelfed before…

6449569

… moving

Switch to correctly compiled version of Bitwuzla 0.4.0 commit 954bcfb…

1d86ad2

…0 (because the release is missing features for parse)

Bitwuzla: Re-enabled test bvOutOfRange as it works with Bitwuzla now.

71a6808

Bitwuzla: Run patchelf twice on libbitwuzlaJNI to resolve the depende…

52e09ae

…ncy on libbitwuzla.so.0

kfriedberger changed the title ~~Adding missing features to the Bitwuzla bindigs~~ Adding missing features to the Bitwuzla bindings Apr 10, 2024

baierd merged commit 52e09ae into sosy-lab:bitwuzla_updates Apr 11, 2024

baierd mentioned this pull request Apr 11, 2024

Add the SMT solver Bitwuzla to JavaSMT #370

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Adding missing features to the Bitwuzla bindings#369

Adding missing features to the Bitwuzla bindings#369
baierd merged 111 commits into
sosy-lab:bitwuzla_updatesfrom
daniel-raffler:add_bitwuzla_swig

daniel-raffler commented Apr 9, 2024

Uh oh!

Reviewers

Assignees

Labels

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

daniel-raffler commented Apr 9, 2024

Uh oh!

Reviewers

Assignees

Labels

Milestone

Development

Uh oh!

2 participants