From 93fd47047bd59595035c62fae6a1f5a689e5a75d Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 23 Jan 2024 14:05:50 +0100 Subject: [PATCH 001/158] Bitwuzla: Added SWIG file to autogenerate JNI bindings and switched to the C++ API. --- .idea/JavaSMT.iml | 9 + build/build-publish-solvers.xml | 166 +- lib/native/source/libbitwuzla/bitwuzla.i | 454 + lib/native/source/libbitwuzla/bitwuzla_wrap.c | 8324 ----------------- lib/native/source/libbitwuzla/compile.sh | 73 - solvers_ivy_conf/ivy_bitwuzla.xml | 24 +- .../bitwuzla/BitwuzlaArrayFormulaManager.java | 28 +- .../BitwuzlaBitvectorFormulaManager.java | 146 +- .../BitwuzlaBooleanFormulaManager.java | 64 +- .../solvers/bitwuzla/BitwuzlaDeclaration.java | 30 +- .../BitwuzlaFloatingPointManager.java | 217 +- .../solvers/bitwuzla/BitwuzlaFormula.java | 26 +- .../bitwuzla/BitwuzlaFormulaCreator.java | 499 +- .../bitwuzla/BitwuzlaFormulaManager.java | 57 +- .../solvers/bitwuzla/BitwuzlaJNI.java | 758 -- .../solvers/bitwuzla/BitwuzlaKind.java | 314 - .../solvers/bitwuzla/BitwuzlaModel.java | 126 +- .../bitwuzla/BitwuzlaNativeApiTest.java | 1041 +-- .../solvers/bitwuzla/BitwuzlaOption.java | 168 - .../solvers/bitwuzla/BitwuzlaOptionInfo.java | 86 - .../BitwuzlaQuantifiedFormulaManager.java | 44 +- .../solvers/bitwuzla/BitwuzlaResult.java | 73 - .../bitwuzla/BitwuzlaSolverContext.java | 146 +- .../bitwuzla/BitwuzlaTheoremProver.java | 122 +- .../solvers/bitwuzla/BitwuzlaUFManager.java | 6 +- .../solvers/bitwuzla/NumericValue.java | 2 + 26 files changed, 1685 insertions(+), 11318 deletions(-) create mode 100644 lib/native/source/libbitwuzla/bitwuzla.i delete mode 100644 lib/native/source/libbitwuzla/bitwuzla_wrap.c delete mode 100755 lib/native/source/libbitwuzla/compile.sh delete mode 100644 src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaJNI.java delete mode 100644 src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaKind.java delete mode 100644 src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaOption.java delete mode 100644 src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaOptionInfo.java delete mode 100644 src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaResult.java diff --git a/.idea/JavaSMT.iml b/.idea/JavaSMT.iml index c9ee959dbd..6923bc643d 100644 --- a/.idea/JavaSMT.iml +++ b/.idea/JavaSMT.iml @@ -322,6 +322,15 @@ SPDX-License-Identifier: Apache-2.0 + + + + + + + + +