-
Notifications
You must be signed in to change notification settings - Fork 46
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #174 from sosy-lab/boolector_integration
Integration of the SMT Solver Boolector into JavaSMT
- Loading branch information
Showing
55 changed files
with
7,170 additions
and
183 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
85 changes: 85 additions & 0 deletions
85
lib/native/source/libboolector/Boolector Build Documentation.txt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,85 @@ | ||
| ################################################################# | ||
|
|
||
| INFO 2019-11-11: | ||
| This file might be outdated, please use 'ant publish-boolector' | ||
| for building Boolector and publishing into Ivy. | ||
| The ant steps are based on this documentation. | ||
|
|
||
| ################################################################# | ||
|
|
||
|
|
||
| NOTICE: This is a bare minimum guide that worked for me. I do not take responsibility in any damage or frustration you may encounter using this! | ||
|
|
||
| In the following the steps to update or change boolector and its JNI are outlined: | ||
|
|
||
| There are 2 files, both located in boolector/src/, that need (potential) editing to compile Boolector with JNI: | ||
|
|
||
| -interface_wrap.c (containing the JNI interface) | ||
| -CMakeLists.c (the cmakefile) | ||
|
|
||
|
|
||
| MakeFile: | ||
| CMakeLists.c needs to include ALL JNI .c files you want in its set(libboolector_src_files ...) list at the beginning. (interface_wrap.c should be there!) | ||
| Additionally it needs to find the JNI libs and set the path for linking. | ||
| Example: | ||
|
|
||
| find_package(JNI) | ||
| if(JNI_FOUND) | ||
| message (STATUS "JNI_INCLUDE_DIRS=${JNI_INCLUDE_DIRS}") | ||
| message (STATUS "JNI_LIBRARIES=${JNI_LIBRARIES}") | ||
| target_include_directories(boolector PRIVATE ${JNI_INCLUDE_DIRS}) | ||
| target_link_libraries(boolector ${JNI_LIBRARIES}) | ||
| endif() | ||
|
|
||
| (should be set and ready to go in the provided version of the cmakefile but here is a copy that should be working if copied in directly before the linking of the SAT solvers) | ||
|
|
||
| JNI (interface_wrap.c): | ||
| To change or update methods just edit this file! (DON'T CHANGE BOOLECTOR NATIVE CODE!) | ||
| The interface is set up with all C API methods (taken from the interfaces via SWIG, see SWIG part at the end of this) of Boolector. | ||
| Important: every pointer in Boolector is returned to Java via a Jlong. Just use this as a pointer once given back, but cast it properly! | ||
| Be careful, method names need the package in them, see JNI for more details! | ||
| There are multiple helper methods at the very end of the file, do not change them unless you know what you are doing! | ||
| Since Boolector sometimes writes to given objects, we need those to get the information back to Java. (Explanation via comments in the code) | ||
| In case you add new methods, remember to add them to the Java code as well. (Should be BtorJNI.java in the Boolector package) | ||
|
|
||
|
|
||
| To compile you need to follow these steps EVERY time since Boolector does not save your preferences: | ||
|
|
||
| 1. (Optional) Download new Boolector/Update Boolector and edit/create JNI interface and cmakefile | ||
| 2. Open terminal and switch to the boolector folder (java-smt3-boolector/lib/native/native boolector/boolector) | ||
| 3. Set up your build (See https://github.com/Boolector/boolector for more information. Important: do not try to include MiniSAT in a shared lib, it won't compile!(October 2019) But check for updates on this!) | ||
| Example: | ||
| ./contrib/setup-cadical.sh | ||
| ./contrib/setup-lingeling.sh | ||
| ./contrib/setup-picosat.sh | ||
| ./contrib/setup-btor2tools.sh | ||
|
|
||
| 4. Build Boolector shared lib (you can add more options if you wish): | ||
| ./configure.sh -fno-strict-aliasing -fpic --shared && cd build && make | ||
|
|
||
| 5. Your shared lib can be found in boolector/build/lib | ||
| 6. Copy it to java-smt3-boolector/lib/native/x86_64-linux/ and override the old lib | ||
| 7. Update your JNI Java files | ||
|
|
||
|
|
||
| If you choose to use SWIG (Java/C): | ||
| (Careful, you need to check your methods later anyway, SWIG tends to make mistakes. Example: it gives pointers back instead of the object, or a Jlong instead of an Jint etc.) | ||
| Download: http://www.swig.org/download.html && Install Guide: https://github.com/swig/swig/wiki/Getting-Started | ||
|
|
||
| Create an interface file (example: exampleinterface.i) | ||
| Lets say you want the C header file "stuff.h" with the function "int fact(int n)" in Java, enter it in the interface file as seen below. (Names are important, even filenames!) | ||
| /* File: exampleInterface.i */ | ||
| %module test | ||
| %{ | ||
| #include "stuff.h" | ||
| %} | ||
| int fact(int n); | ||
|
|
||
| If you want all methods of the header in your interface, just replace the methods and enter %include "stuff.h" where the methods used to be. | ||
| After finishing the interface file, execute SWIG with it and the header(s) you want (all in the same folder). | ||
| See documentation of SWIG for more details. (This will propably do: %swig -java exampleinterface.i ) | ||
| Swig has loads of options and customizations, read the doku! (Example: -package <name> will specify the java package, as it is important for method names) | ||
| Dokumentation, Java Command Line 26.2.2 : http://www.swig.org/Doc4.0/SWIGDocumentation.pdf | ||
| After executing SWIG correctly, there should be some .c and some .java files. | ||
| The .c part has to be bound to the native C code as described above, Java in Java. | ||
|
|
27 changes: 27 additions & 0 deletions
27
lib/native/source/libboolector/include_interface_and_jni.patch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,27 @@ | ||
| diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt | ||
| index e2781eb..b838d8e 100644 | ||
| --- a/src/CMakeLists.txt | ||
| +++ b/src/CMakeLists.txt | ||
| @@ -1,6 +1,7 @@ | ||
| set(libboolector_src_files | ||
| aigprop.c | ||
| boolector.c | ||
| + interface_wrap.c | ||
| boolectormc.c | ||
| btorabort.c | ||
| btoraig.c | ||
| @@ -96,6 +97,14 @@ target_include_directories(boolector | ||
| target_include_directories(boolector PRIVATE ${Btor2Tools_INCLUDE_DIR}) | ||
| target_link_libraries(boolector ${Btor2Tools_LIBRARIES}) | ||
|
|
||
| +find_package(JNI) | ||
| +if(JNI_FOUND) | ||
| + message (STATUS "JNI_INCLUDE_DIRS=${JNI_INCLUDE_DIRS}") | ||
| + message (STATUS "JNI_LIBRARIES=${JNI_LIBRARIES}") | ||
| + target_include_directories(boolector PRIVATE ${JNI_INCLUDE_DIRS}) | ||
| + target_link_libraries(boolector ${JNI_LIBRARIES}) | ||
| +endif() | ||
| + | ||
| if(GMP_FOUND) | ||
| target_include_directories(boolector PRIVATE ${GMP_INCLUDE_DIR}) | ||
| target_link_libraries(boolector ${GMP_LIBRARIES}) |
Oops, something went wrong.