diff --git a/build/build-publish-solvers.xml b/build/build-publish-solvers.xml
index 3f686a6622..c0b4de147f 100644
--- a/build/build-publish-solvers.xml
+++ b/build/build-publish-solvers.xml
@@ -147,6 +147,104 @@
svn ci repository/${ivy.organisation}/${ivy.module} -m"publish version ${cvc4.version} of CVC4 Solver"
to make the new version publicly available.
+
+
+
+
+ Please specify the path to Boolector with the flag -Dboolector.path=/path/to/boolector.
+ The path has to point to the root Boolector folder, i.e.,
+ a checkout of the official git repositoy from 'https://github.com/boolector/boolector'.
+ Note that shell substitutions do not work and a full absolute path has to be specified.
+
+
+ Please specify a custom revision with the flag -Dboolector.customRev=XXX.
+ The custom revision has to be unique amongst the already known version
+ numbers from the ivy repository. The script will append the git revision.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ You now want to run
+ svn add repository/${ivy.organisation}/${ivy.module}/*-${boolector.version}*
+ svn ci repository/${ivy.organisation}/${ivy.module} -m"publish version ${boolector.version} of Boolector Solver"
+ to make the new version publicly available.
+
+
diff --git a/lib/ivy.xml b/lib/ivy.xml
index 6c2d348c17..df8656322c 100644
--- a/lib/ivy.xml
+++ b/lib/ivy.xml
@@ -25,9 +25,10 @@
+
-
+
@@ -137,6 +138,7 @@
+
diff --git a/lib/native/source/libboolector/Boolector Build Documentation.txt b/lib/native/source/libboolector/Boolector Build Documentation.txt
new file mode 100644
index 0000000000..1ed00cdcd5
--- /dev/null
+++ b/lib/native/source/libboolector/Boolector Build Documentation.txt
@@ -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 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.
+
diff --git a/lib/native/source/libboolector/include_interface_and_jni.patch b/lib/native/source/libboolector/include_interface_and_jni.patch
new file mode 100644
index 0000000000..f5081bd8ab
--- /dev/null
+++ b/lib/native/source/libboolector/include_interface_and_jni.patch
@@ -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})
diff --git a/lib/native/source/libboolector/interface_wrap.c b/lib/native/source/libboolector/interface_wrap.c
new file mode 100644
index 0000000000..a72b87b134
--- /dev/null
+++ b/lib/native/source/libboolector/interface_wrap.c
@@ -0,0 +1,3570 @@
+/* ----------------------------------------------------------------------------
+ * This file was automatically generated by SWIG (http://www.swig.org).
+ * Version 4.0.0
+ *
+ * This file is not intended to be easily readable and contains a number of
+ * coding conventions designed to improve portability and efficiency. Do not make
+ * changes to this file unless you know what you are doing--modify the SWIG
+ * interface file instead.
+ * ----------------------------------------------------------------------------- */
+
+
+#ifndef SWIGJAVA
+#define SWIGJAVA
+#endif
+
+
+/* -----------------------------------------------------------------------------
+ * This section contains generic SWIG labels for method/variable
+ * declarations/attributes, and other compiler dependent labels.
+ * ----------------------------------------------------------------------------- */
+
+/* template workaround for compilers that cannot correctly implement the C++ standard */
+#ifndef SWIGTEMPLATEDISAMBIGUATOR
+# if defined(__SUNPRO_CC) && (__SUNPRO_CC <= 0x560)
+# define SWIGTEMPLATEDISAMBIGUATOR template
+# elif defined(__HP_aCC)
+/* Needed even with `aCC -AA' when `aCC -V' reports HP ANSI C++ B3910B A.03.55 */
+/* If we find a maximum version that requires this, the test would be __HP_aCC <= 35500 for A.03.55 */
+# define SWIGTEMPLATEDISAMBIGUATOR template
+# else
+# define SWIGTEMPLATEDISAMBIGUATOR
+# endif
+#endif
+
+/* inline attribute */
+#ifndef SWIGINLINE
+# if defined(__cplusplus) || (defined(__GNUC__) && !defined(__STRICT_ANSI__))
+# define SWIGINLINE inline
+# else
+# define SWIGINLINE
+# endif
+#endif
+
+/* attribute recognised by some compilers to avoid 'unused' warnings */
+#ifndef SWIGUNUSED
+# if defined(__GNUC__)
+# if !(defined(__cplusplus)) || (__GNUC__ > 3 || (__GNUC__ == 3 && __GNUC_MINOR__ >= 4))
+# define SWIGUNUSED __attribute__ ((__unused__))
+# define SWIGUNUSED __attribute__ ((__unused__))
+# else
+# define SWIGUNUSED
+# endif
+# elif defined(__ICC)
+# define SWIGUNUSED __attribute__ ((__unused__))
+# else
+# define SWIGUNUSED
+# endif
+#endif
+
+#ifndef SWIG_MSC_UNSUPPRESS_4505
+# if defined(_MSC_VER)
+# pragma warning(disable : 4505) /* unreferenced local function has been removed */
+# endif
+#endif
+
+#ifndef SWIGUNUSEDPARM
+# ifdef __cplusplus
+# define SWIGUNUSEDPARM(p)
+# else
+# define SWIGUNUSEDPARM(p) p SWIGUNUSED
+# endif
+#endif
+
+/* internal SWIG method */
+#ifndef SWIGINTERN
+# define SWIGINTERN static SWIGUNUSED
+#endif
+
+/* internal inline SWIG method */
+#ifndef SWIGINTERNINLINE
+# define SWIGINTERNINLINE SWIGINTERN SWIGINLINE
+#endif
+
+/* exporting methods */
+#if defined(__GNUC__)
+# if (__GNUC__ >= 4) || (__GNUC__ == 3 && __GNUC_MINOR__ >= 4)
+# ifndef GCC_HASCLASSVISIBILITY
+# define GCC_HASCLASSVISIBILITY
+# endif
+# endif
+#endif
+
+#ifndef SWIGEXPORT
+# if defined(_WIN32) || defined(__WIN32__) || defined(__CYGWIN__)
+# if defined(STATIC_LINKED)
+# define SWIGEXPORT
+# else
+# define SWIGEXPORT __declspec(dllexport)
+# endif
+# else
+# if defined(__GNUC__) && defined(GCC_HASCLASSVISIBILITY)
+# define SWIGEXPORT __attribute__ ((visibility("default")))
+# else
+# define SWIGEXPORT
+# endif
+# endif
+#endif
+
+/* calling conventions for Windows */
+#ifndef SWIGSTDCALL
+# if defined(_WIN32) || defined(__WIN32__) || defined(__CYGWIN__)
+# define SWIGSTDCALL __stdcall
+# else
+# define SWIGSTDCALL
+# endif
+#endif
+
+/* Deal with Microsoft's attempt at deprecating C standard runtime functions */
+#if !defined(SWIG_NO_CRT_SECURE_NO_DEPRECATE) && defined(_MSC_VER) && !defined(_CRT_SECURE_NO_DEPRECATE)
+# define _CRT_SECURE_NO_DEPRECATE
+#endif
+
+/* Deal with Microsoft's attempt at deprecating methods in the standard C++ library */
+#if !defined(SWIG_NO_SCL_SECURE_NO_DEPRECATE) && defined(_MSC_VER) && !defined(_SCL_SECURE_NO_DEPRECATE)
+# define _SCL_SECURE_NO_DEPRECATE
+#endif
+
+/* Deal with Apple's deprecated 'AssertMacros.h' from Carbon-framework */
+#if defined(__APPLE__) && !defined(__ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES)
+# define __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES 0
+#endif
+
+/* Intel's compiler complains if a variable which was never initialised is
+ * cast to void, which is a common idiom which we use to indicate that we
+ * are aware a variable isn't used. So we just silence that warning.
+ * See: https://github.com/swig/swig/issues/192 for more discussion.
+ */
+#ifdef __INTEL_COMPILER
+# pragma warning disable 592
+#endif
+
+
+/* Fix for jlong on some versions of gcc on Windows */
+#if defined(__GNUC__) && !defined(__INTEL_COMPILER)
+ typedef long long __int64;
+#endif
+
+/* Fix for jlong on 64-bit x86 Solaris */
+#if defined(__x86_64)
+# ifdef _LP64
+# undef _LP64
+# endif
+#endif
+
+#include
+#include
+#include
+
+
+/* Support for throwing Java exceptions */
+typedef enum {
+ SWIG_JavaOutOfMemoryError = 1,
+ SWIG_JavaIOException,
+ SWIG_JavaRuntimeException,
+ SWIG_JavaIndexOutOfBoundsException,
+ SWIG_JavaArithmeticException,
+ SWIG_JavaIllegalArgumentException,
+ SWIG_JavaNullPointerException,
+ SWIG_JavaDirectorPureVirtual,
+ SWIG_JavaUnknownError
+} SWIG_JavaExceptionCodes;
+
+typedef struct {
+ SWIG_JavaExceptionCodes code;
+ const char *java_exception;
+} SWIG_JavaExceptions_t;
+
+
+static void SWIGUNUSED SWIG_JavaThrowException(JNIEnv *jenv, SWIG_JavaExceptionCodes code, const char *msg) {
+ jclass excep;
+ static const SWIG_JavaExceptions_t java_exceptions[] = {
+ { SWIG_JavaOutOfMemoryError, "java/lang/OutOfMemoryError" },
+ { SWIG_JavaIOException, "java/io/IOException" },
+ { SWIG_JavaRuntimeException, "java/lang/RuntimeException" },
+ { SWIG_JavaIndexOutOfBoundsException, "java/lang/IndexOutOfBoundsException" },
+ { SWIG_JavaArithmeticException, "java/lang/ArithmeticException" },
+ { SWIG_JavaIllegalArgumentException, "java/lang/IllegalArgumentException" },
+ { SWIG_JavaNullPointerException, "java/lang/NullPointerException" },
+ { SWIG_JavaDirectorPureVirtual, "java/lang/RuntimeException" },
+ { SWIG_JavaUnknownError, "java/lang/UnknownError" },
+ { (SWIG_JavaExceptionCodes)0, "java/lang/UnknownError" }
+ };
+ const SWIG_JavaExceptions_t *except_ptr = java_exceptions;
+
+ while (except_ptr->code != code && except_ptr->code)
+ except_ptr++;
+
+ (*jenv)->ExceptionClear(jenv);
+ excep = (*jenv)->FindClass(jenv, except_ptr->java_exception);
+ if (excep)
+ (*jenv)->ThrowNew(jenv, excep, msg);
+}
+
+
+/* Contract support */
+
+#define SWIG_contract_assert(nullreturn, expr, msg) if (!(expr)) {SWIG_JavaThrowException(jenv, SWIG_JavaIllegalArgumentException, msg); return nullreturn; } else
+
+
+#include "boolector.h"
+#include "btortypes.h"
+
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_BOOLECTOR_1PARSE_1ERROR_1get(JNIEnv *jenv, jclass jcls) {
+ jint jresult = 0 ;
+ int result;
+
+ (void)jenv;
+ (void)jcls;
+ result = (int)(1);
+ jresult = (jint)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_BOOLECTOR_1PARSE_1UNKNOWN_1get(JNIEnv *jenv, jclass jcls) {
+ jint jresult = 0 ;
+ int result;
+
+ (void)jenv;
+ (void)jcls;
+ result = (int)(2);
+ jresult = (jint)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1new(JNIEnv *jenv, jclass jcls) {
+ jlong jresult = 0 ;
+ Btor *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ result = (Btor *)boolector_new();
+ *(Btor **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1clone(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ Btor *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ result = (Btor *)boolector_clone(arg1);
+ *(Btor **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1delete(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ Btor *arg1 = (Btor *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ boolector_delete(arg1);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1set_1term(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ Btor *arg1 = (Btor *) 0 ;
+ int32_t (*arg2)(void *) = (int32_t (*)(void *)) 0 ;
+ void *arg3 = (void *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(int32_t (**)(void *))&jarg2;
+ arg3 = *(void **)&jarg3;
+ boolector_set_term(arg1,arg2,arg3);
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1terminate(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ Btor *arg1 = (Btor *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ return boolector_terminate(arg1);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1set_1abort(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ void (*arg1)(char const *) = (void (*)(char const *)) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(void (**)(char const *))&jarg1;
+ boolector_set_abort(arg1);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1set_1msg_1prefix(JNIEnv *jenv, jclass jcls, jlong jarg1, jstring jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ char *arg2 = (char *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = 0;
+ if (jarg2) {
+ arg2 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg2, 0);
+ if (!arg2) return ;
+ }
+ boolector_set_msg_prefix(arg1,(char const *)arg2);
+ if (arg2) (*jenv)->ReleaseStringUTFChars(jenv, jarg2, (const char *)arg2);
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1get_1refs(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ Btor *arg1 = (Btor *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ return boolector_get_refs(arg1);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1reset_1time(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ Btor *arg1 = (Btor *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ boolector_reset_time(arg1);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1reset_1stats(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ Btor *arg1 = (Btor *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ boolector_reset_stats(arg1);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1print_1stats(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ Btor *arg1 = (Btor *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ boolector_print_stats(arg1);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1set_1trapi(JNIEnv *jenv, jclass jcls, jlong jarg1, jstring jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ char *arg2 = (char *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ if (jarg2) {
+ arg2 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg2, 0);
+ if (!arg2) perror("ERROR: couldn't set api trace because given path was wrong.");
+ }
+ FILE *f = 0;
+ f = fopen(arg2, "w");
+ if(f==NULL) {
+ perror("ERROR: couldn't set api trace because it couldnt open trace file.");
+ }
+ boolector_set_trapi(arg1,f);
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1get_1trapi(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ FILE *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ result = (FILE *)boolector_get_trapi(arg1);
+ *(FILE **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1push(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ uint32_t arg2 ;
+ uint32_t *argp2 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ argp2 = (uint32_t *)&jarg2;
+ if (!argp2) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null uint32_t");
+ return ;
+ }
+ arg2 = *argp2;
+ boolector_push(arg1,arg2);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1pop(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ uint32_t arg2 ;
+ uint32_t *argp2 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ argp2 = (uint32_t *)&jarg2;
+ if (!argp2) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null uint32_t");
+ return ;
+ }
+ arg2 = *argp2;
+ boolector_pop(arg1,arg2);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1assert(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ boolector_assert(arg1,arg2);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1assume(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ boolector_assume(arg1,arg2);
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1failed(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (bool)boolector_failed(arg1,arg2);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1get_1failed_1assumptions(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode **result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ result = (BoolectorNode **)boolector_get_failed_assumptions(arg1);
+ *(BoolectorNode ***)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1fixate_1assumptions(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ Btor *arg1 = (Btor *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ boolector_fixate_assumptions(arg1);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1reset_1assumptions(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ Btor *arg1 = (Btor *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ boolector_reset_assumptions(arg1);
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1sat(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ Btor *arg1 = (Btor *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ return boolector_sat(arg1);
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1limited_1sat(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ Btor *arg1 = (Btor *) 0 ;
+ int32_t arg2 ;
+ int32_t arg3 ;
+ int32_t *argp2 ;
+ int32_t *argp3 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ argp2 = (int32_t *)&jarg2;
+ if (!argp2) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null int32_t");
+ return 0;
+ }
+ arg2 = *argp2;
+ argp3 = (int32_t *)&jarg3;
+ if (!argp3) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null int32_t");
+ return 0;
+ }
+ arg3 = *argp3;
+ return boolector_limited_sat(arg1,arg2,arg3);
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1simplify(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ Btor *arg1 = (Btor *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ return boolector_simplify(arg1);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1set_1sat_1solver(JNIEnv *jenv, jclass jcls, jlong jarg1, jstring jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ char *arg2 = (char *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = 0;
+ if (jarg2) {
+ arg2 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg2, 0);
+ if (!arg2) return ;
+ }
+ boolector_set_sat_solver(arg1,(char const *)arg2);
+ if (arg2) (*jenv)->ReleaseStringUTFChars(jenv, jarg2, (const char *)arg2);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1set_1opt(JNIEnv *jenv, jclass jcls, jlong jarg1, jint jarg2, jlong jarg3) {
+ Btor *arg1 = (Btor *) 0 ;
+ BtorOption arg2 ;
+ uint32_t arg3 ;
+ uint32_t *argp3 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = (BtorOption)jarg2;
+ argp3 = (uint32_t *)&jarg3;
+ if (!argp3) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null uint32_t");
+ return ;
+ }
+ arg3 = *argp3;
+ boolector_set_opt(arg1,arg2,arg3);
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1get_1opt(JNIEnv *jenv, jclass jcls, jlong jarg1, jint jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ BtorOption arg2 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = (BtorOption)jarg2;
+ return boolector_get_opt(arg1,arg2);
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1get_1opt_1min(JNIEnv *jenv, jclass jcls, jlong jarg1, jint jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ BtorOption arg2 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = (BtorOption)jarg2;
+ return boolector_get_opt_min(arg1,arg2);
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1get_1opt_1max(JNIEnv *jenv, jclass jcls, jlong jarg1, jint jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ BtorOption arg2 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = (BtorOption)jarg2;
+ return boolector_get_opt_max(arg1,arg2);
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1get_1opt_1dflt(JNIEnv *jenv, jclass jcls, jlong jarg1, jint jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ BtorOption arg2 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = (BtorOption)jarg2;
+ return boolector_get_opt_dflt(arg1,arg2);
+}
+
+
+SWIGEXPORT jstring JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1get_1opt_1lng(JNIEnv *jenv, jclass jcls, jlong jarg1, jint jarg2) {
+ jstring jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BtorOption arg2 ;
+ char *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = (BtorOption)jarg2;
+ result = (char *)boolector_get_opt_lng(arg1,arg2);
+ if (result) jresult = (*jenv)->NewStringUTF(jenv, (const char *)result);
+ return jresult;
+}
+
+
+SWIGEXPORT jstring JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1get_1opt_1shrt(JNIEnv *jenv, jclass jcls, jlong jarg1, jint jarg2) {
+ jstring jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BtorOption arg2 ;
+ char *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = (BtorOption)jarg2;
+ result = (char *)boolector_get_opt_shrt(arg1,arg2);
+ if (result) jresult = (*jenv)->NewStringUTF(jenv, (const char *)result);
+ return jresult;
+}
+
+
+SWIGEXPORT jstring JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1get_1opt_1desc(JNIEnv *jenv, jclass jcls, jlong jarg1, jint jarg2) {
+ jstring jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BtorOption arg2 ;
+ char *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = (BtorOption)jarg2;
+ result = (char *)boolector_get_opt_desc(arg1,arg2);
+ if (result) jresult = (*jenv)->NewStringUTF(jenv, (const char *)result);
+ return jresult;
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1has_1opt(JNIEnv *jenv, jclass jcls, jlong jarg1, jint jarg2) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BtorOption arg2 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = (BtorOption)jarg2;
+ result = (bool)boolector_has_opt(arg1,arg2);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1first_1opt(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ jint jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BtorOption result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ result = (BtorOption)boolector_first_opt(arg1);
+ jresult = (jint)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1next_1opt(JNIEnv *jenv, jclass jcls, jlong jarg1, jint jarg2) {
+ jint jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BtorOption arg2 ;
+ BtorOption result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = (BtorOption)jarg2;
+ result = (BtorOption)boolector_next_opt(arg1,arg2);
+ jresult = (jint)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1copy(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (BoolectorNode *)boolector_copy(arg1,arg2);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1release(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ boolector_release(arg1,arg2);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1release_1all(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ Btor *arg1 = (Btor *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ boolector_release_all(arg1);
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1true(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ result = (BoolectorNode *)boolector_true(arg1);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1false(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ result = (BoolectorNode *)boolector_false(arg1);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1implies(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_implies(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1iff(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_iff(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1eq(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_eq(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1ne(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_ne(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1is_1bv_1const_1zero(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (bool)boolector_is_bv_const_zero(arg1,arg2);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1is_1bv_1const_1one(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (bool)boolector_is_bv_const_one(arg1,arg2);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1is_1bv_1const_1ones(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (bool)boolector_is_bv_const_ones(arg1,arg2);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1is_1bv_1const_1max_1signed(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (bool)boolector_is_bv_const_max_signed(arg1,arg2);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1is_1bv_1const_1min_1signed(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (bool)boolector_is_bv_const_min_signed(arg1,arg2);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1const(JNIEnv *jenv, jclass jcls, jlong jarg1, jstring jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ char *arg2 = (char *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = 0;
+ if (jarg2) {
+ arg2 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg2, 0);
+ if (!arg2) return 0;
+ }
+ result = (BoolectorNode *)boolector_const(arg1,(char const *)arg2);
+ *(BoolectorNode **)&jresult = result;
+ if (arg2) (*jenv)->ReleaseStringUTFChars(jenv, jarg2, (const char *)arg2);
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1constd(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jstring jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorSort arg2 = (BoolectorSort) 0 ;
+ char *arg3 = (char *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorSort *)&jarg2;
+ arg3 = 0;
+ if (jarg3) {
+ arg3 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg3, 0);
+ if (!arg3) return 0;
+ }
+ result = (BoolectorNode *)boolector_constd(arg1,arg2,(char const *)arg3);
+ *(BoolectorNode **)&jresult = result;
+ if (arg3) (*jenv)->ReleaseStringUTFChars(jenv, jarg3, (const char *)arg3);
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1consth(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jstring jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorSort arg2 = (BoolectorSort) 0 ;
+ char *arg3 = (char *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorSort *)&jarg2;
+ arg3 = 0;
+ if (jarg3) {
+ arg3 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg3, 0);
+ if (!arg3) return 0;
+ }
+ result = (BoolectorNode *)boolector_consth(arg1,arg2,(char const *)arg3);
+ *(BoolectorNode **)&jresult = result;
+ if (arg3) (*jenv)->ReleaseStringUTFChars(jenv, jarg3, (const char *)arg3);
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1zero(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorSort arg2 = (BoolectorSort) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorSort *)&jarg2;
+ result = (BoolectorNode *)boolector_zero(arg1,arg2);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1ones(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorSort arg2 = (BoolectorSort) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorSort *)&jarg2;
+ result = (BoolectorNode *)boolector_ones(arg1,arg2);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1one(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorSort arg2 = (BoolectorSort) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorSort *)&jarg2;
+ result = (BoolectorNode *)boolector_one(arg1,arg2);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1min_1signed(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorSort arg2 = (BoolectorSort) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorSort *)&jarg2;
+ result = (BoolectorNode *)boolector_min_signed(arg1,arg2);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1max_1signed(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorSort arg2 = (BoolectorSort) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorSort *)&jarg2;
+ result = (BoolectorNode *)boolector_max_signed(arg1,arg2);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1unsigned_1int(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ uint32_t arg2 ;
+ BoolectorSort arg3 = (BoolectorSort) 0 ;
+ uint32_t *argp2 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ argp2 = (uint32_t *)&jarg2;
+ if (!argp2) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null uint32_t");
+ return 0;
+ }
+ arg2 = *argp2;
+ arg3 = *(BoolectorSort *)&jarg3;
+ result = (BoolectorNode *)boolector_unsigned_int(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1int(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ int32_t arg2 ;
+ BoolectorSort arg3 = (BoolectorSort) 0 ;
+ int32_t *argp2 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ argp2 = (int32_t *)&jarg2;
+ if (!argp2) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null int32_t");
+ return 0;
+ }
+ arg2 = *argp2;
+ arg3 = *(BoolectorSort *)&jarg3;
+ result = (BoolectorNode *)boolector_int(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1var(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jstring jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorSort arg2 = (BoolectorSort) 0 ;
+ char *arg3 = (char *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorSort *)&jarg2;
+ arg3 = 0;
+ if (jarg3) {
+ arg3 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg3, 0);
+ if (!arg3) return 0;
+ }
+ result = (BoolectorNode *)boolector_var(arg1,arg2,(char const *)arg3);
+ *(BoolectorNode **)&jresult = result;
+ if (arg3) (*jenv)->ReleaseStringUTFChars(jenv, jarg3, (const char *)arg3);
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1array(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jstring jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorSort arg2 = (BoolectorSort) 0 ;
+ char *arg3 = (char *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorSort *)&jarg2;
+ arg3 = 0;
+ if (jarg3) {
+ arg3 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg3, 0);
+ if (!arg3) return 0;
+ }
+ result = (BoolectorNode *)boolector_array(arg1,arg2,(char const *)arg3);
+ *(BoolectorNode **)&jresult = result;
+ if (arg3) (*jenv)->ReleaseStringUTFChars(jenv, jarg3, (const char *)arg3);
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1uf(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jstring jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorSort arg2 = (BoolectorSort) 0 ;
+ char *arg3 = (char *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorSort *)&jarg2;
+ arg3 = 0;
+ if (jarg3) {
+ arg3 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg3, 0);
+ if (!arg3) return 0;
+ }
+ result = (BoolectorNode *)boolector_uf(arg1,arg2,(char const *)arg3);
+ *(BoolectorNode **)&jresult = result;
+ if (arg3) (*jenv)->ReleaseStringUTFChars(jenv, jarg3, (const char *)arg3);
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1not(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (BoolectorNode *)boolector_not(arg1,arg2);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1neg(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (BoolectorNode *)boolector_neg(arg1,arg2);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1redor(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (BoolectorNode *)boolector_redor(arg1,arg2);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1redxor(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (BoolectorNode *)boolector_redxor(arg1,arg2);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1redand(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (BoolectorNode *)boolector_redand(arg1,arg2);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1slice(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3, jlong jarg4) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ uint32_t arg3 ;
+ uint32_t arg4 ;
+ uint32_t *argp3 ;
+ uint32_t *argp4 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ argp3 = (uint32_t *)&jarg3;
+ if (!argp3) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null uint32_t");
+ return 0;
+ }
+ arg3 = *argp3;
+ argp4 = (uint32_t *)&jarg4;
+ if (!argp4) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null uint32_t");
+ return 0;
+ }
+ arg4 = *argp4;
+ result = (BoolectorNode *)boolector_slice(arg1,arg2,arg3,arg4);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1uext(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ uint32_t arg3 ;
+ uint32_t *argp3 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ argp3 = (uint32_t *)&jarg3;
+ if (!argp3) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null uint32_t");
+ return 0;
+ }
+ arg3 = *argp3;
+ result = (BoolectorNode *)boolector_uext(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1sext(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ uint32_t arg3 ;
+ uint32_t *argp3 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ argp3 = (uint32_t *)&jarg3;
+ if (!argp3) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null uint32_t");
+ return 0;
+ }
+ arg3 = *argp3;
+ result = (BoolectorNode *)boolector_sext(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1xor(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_xor(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1xnor(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_xnor(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1and(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_and(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1nand(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_nand(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1or(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_or(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1nor(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_nor(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1add(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_add(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1uaddo(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_uaddo(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1saddo(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_saddo(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1mul(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_mul(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1umulo(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_umulo(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1smulo(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_smulo(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1ult(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_ult(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1slt(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_slt(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1ulte(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_ulte(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1slte(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_slte(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1ugt(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_ugt(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1sgt(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_sgt(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1ugte(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_ugte(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1sgte(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_sgte(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1sll(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_sll(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1srl(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_srl(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1sra(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_sra(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1rol(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_rol(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1ror(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_ror(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1sub(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_sub(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1usubo(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_usubo(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1ssubo(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_ssubo(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1udiv(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_udiv(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1sdiv(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_sdiv(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1sdivo(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_sdivo(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1urem(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_urem(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1srem(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_srem(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1smod(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_smod(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1concat(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_concat(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1repeat(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ uint32_t arg3 ;
+ uint32_t *argp3 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ argp3 = (uint32_t *)&jarg3;
+ if (!argp3) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null uint32_t");
+ return 0;
+ }
+ arg3 = *argp3;
+ result = (BoolectorNode *)boolector_repeat(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1read(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (BoolectorNode *)boolector_read(arg1,arg2,arg3);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1write(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3, jlong jarg4) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg4 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ arg4 = *(BoolectorNode **)&jarg4;
+ result = (BoolectorNode *)boolector_write(arg1,arg2,arg3,arg4);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1cond(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3, jlong jarg4) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg4 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ arg4 = *(BoolectorNode **)&jarg4;
+ result = (BoolectorNode *)boolector_cond(arg1,arg2,arg3,arg4);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1param(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jstring jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorSort arg2 = (BoolectorSort) 0 ;
+ char *arg3 = (char *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorSort *)&jarg2;
+ arg3 = 0;
+ if (jarg3) {
+ arg3 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg3, 0);
+ if (!arg3) return 0;
+ }
+ result = (BoolectorNode *)boolector_param(arg1,arg2,(char const *)arg3);
+ *(BoolectorNode **)&jresult = result;
+ if (arg3) (*jenv)->ReleaseStringUTFChars(jenv, jarg3, (const char *)arg3);
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1fun(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3, jlong jarg4) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode **arg2 = (BoolectorNode **) 0 ;
+ uint32_t arg3 ;
+ BoolectorNode *arg4 = (BoolectorNode *) 0 ;
+ uint32_t *argp3 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode ***)&jarg2;
+ argp3 = (uint32_t *)&jarg3;
+ if (!argp3) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null uint32_t");
+ return 0;
+ }
+ arg3 = *argp3;
+ arg4 = *(BoolectorNode **)&jarg4;
+ result = (BoolectorNode *)boolector_fun(arg1,arg2,arg3,arg4);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1apply(JNIEnv *jenv, jclass jcls, jlong jarg1, jlongArray jarg2, jlong jarg3, jlong jarg4) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ jlong *array = (*jenv)->GetLongArrayElements(jenv, jarg2, 0);
+ uint32_t arg3 ;
+ BoolectorNode *arg4 = (BoolectorNode *) 0 ;
+ uint32_t *argp3 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ argp3 = (uint32_t *)&jarg3;
+ if (!argp3) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null uint32_t");
+ return 0;
+ }
+ arg3 = *argp3;
+ arg4 = *(BoolectorNode **)&jarg4;
+ result = (BoolectorNode *)boolector_apply(arg1,(BoolectorNode**)array,arg3,arg4);
+ *(BoolectorNode **)&jresult = result;
+ (*jenv)->ReleaseLongArrayElements(jenv, jarg2, array, 0);
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1inc(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (BoolectorNode *)boolector_inc(arg1,arg2);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1dec(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (BoolectorNode *)boolector_dec(arg1,arg2);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1forall(JNIEnv *jenv, jclass jcls, jlong jarg1, jlongArray jarg2, jint jarg3, jlong jarg4) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ uint32_t arg3 = jarg3;
+ BoolectorNode *arg4 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+
+ BoolectorNode **array = 0;
+ array = (BoolectorNode**)(*jenv)->GetLongArrayElements(jenv, jarg2, 0);
+ arg4 = *(BoolectorNode **)&jarg4;
+ result = (BoolectorNode *)boolector_forall(arg1, array,arg3,arg4);
+ *(BoolectorNode **)&jresult = result;
+ (*jenv)->ReleaseLongArrayElements(jenv, jarg2, (jlong*)array, 0);
+
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1exists(JNIEnv *jenv, jclass jcls, jlong jarg1, jlongArray jarg2, jint jarg3, jlong jarg4) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ uint32_t arg3 = jarg3;
+ BoolectorNode *arg4 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+
+ jlong *array = (*jenv)->GetLongArrayElements(jenv, jarg2, 0);
+ arg4 = *(BoolectorNode **)&jarg4;
+ result = (BoolectorNode *)boolector_exists(arg1,(BoolectorNode**)array,arg3,arg4);
+ *(BoolectorNode **)&jresult = result;
+ (*jenv)->ReleaseLongArrayElements(jenv, jarg2, array, 0);
+
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1get_1btor(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ jlong jresult = 0 ;
+ BoolectorNode *arg1 = (BoolectorNode *) 0 ;
+ Btor *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(BoolectorNode **)&jarg1;
+ result = (Btor *)boolector_get_btor(arg1);
+ *(Btor **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1get_1node_1id(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ int32_t result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ return boolector_get_node_id(arg1,arg2);
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1get_1sort(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorSort result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (BoolectorSort)boolector_get_sort(arg1,(struct BoolectorNode const *)arg2);
+ *(BoolectorSort *)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1fun_1get_1domain_1sort(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorSort result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (BoolectorSort)boolector_fun_get_domain_sort(arg1,(struct BoolectorNode const *)arg2);
+ *(BoolectorSort *)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1fun_1get_1codomain_1sort(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorSort result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (BoolectorSort)boolector_fun_get_codomain_sort(arg1,(struct BoolectorNode const *)arg2);
+ *(BoolectorSort *)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1match_1node_1by_1id(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ int32_t arg2 ;
+ int32_t *argp2 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ argp2 = (int32_t *)&jarg2;
+ if (!argp2) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null int32_t");
+ return 0;
+ }
+ arg2 = *argp2;
+ result = (BoolectorNode *)boolector_match_node_by_id(arg1,arg2);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1match_1node_1by_1symbol(JNIEnv *jenv, jclass jcls, jlong jarg1, jstring jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ char *arg2 = (char *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = 0;
+ if (jarg2) {
+ arg2 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg2, 0);
+ if (!arg2) return 0;
+ }
+ result = (BoolectorNode *)boolector_match_node_by_symbol(arg1,(char const *)arg2);
+ *(BoolectorNode **)&jresult = result;
+ if (arg2) (*jenv)->ReleaseStringUTFChars(jenv, jarg2, (const char *)arg2);
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1match_1node(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (BoolectorNode *)boolector_match_node(arg1,arg2);
+ *(BoolectorNode **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jstring JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1get_1symbol(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jstring jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ char *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (char *)boolector_get_symbol(arg1,arg2);
+ if (result) jresult = (*jenv)->NewStringUTF(jenv, (const char *)result);
+ return jresult;
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1set_1symbol(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jstring jarg3) {
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ char *arg3 = (char *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = 0;
+ if (jarg3) {
+ arg3 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg3, 0);
+ if (!arg3) return ;
+ }
+ boolector_set_symbol(arg1,arg2,(char const *)arg3);
+ if (arg3) (*jenv)->ReleaseStringUTFChars(jenv, jarg3, (const char *)arg3);
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1get_1width(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ return boolector_get_width(arg1,arg2);
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1get_1index_1width(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ return boolector_get_index_width(arg1,arg2);
+}
+
+
+SWIGEXPORT jstring JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1get_1bits(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jstring jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ char *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (char *)boolector_get_bits(arg1,arg2);
+ if (result) jresult = (*jenv)->NewStringUTF(jenv, (const char *)result);
+ return jresult;
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1free_1bits(JNIEnv *jenv, jclass jcls, jlong jarg1, jstring jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ char *arg2 = (char *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = 0;
+ if (jarg2) {
+ arg2 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg2, 0);
+ if (!arg2) return ;
+ }
+ boolector_free_bits(arg1,(char const *)arg2);
+ if (arg2) (*jenv)->ReleaseStringUTFChars(jenv, jarg2, (const char *)arg2);
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1get_1fun_1arity(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ uint32_t result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ return boolector_get_fun_arity(arg1,arg2);
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1is_1const(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (bool)boolector_is_const(arg1,arg2);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1is_1var(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (bool)boolector_is_var(arg1,arg2);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1is_1array(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (bool)boolector_is_array(arg1,arg2);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1is_1array_1var(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (bool)boolector_is_array_var(arg1,arg2);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1is_1param(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (bool)boolector_is_param(arg1,arg2);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1is_1bound_1param(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (bool)boolector_is_bound_param(arg1,arg2);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1is_1uf(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (bool)boolector_is_uf(arg1,arg2);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1is_1fun(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (bool)boolector_is_fun(arg1,arg2);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1fun_1sort_1check(JNIEnv *jenv, jclass jcls, jlong jarg1, jlongArray jarg2, jlong jarg3, jlong jarg4) {
+ Btor *arg1 = (Btor *) 0 ;
+ uint32_t arg3 ;
+ BoolectorNode *arg4 = (BoolectorNode *) 0 ;
+ uint32_t *argp3 ;
+ jint result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ jlong *array = (*jenv)->GetLongArrayElements(jenv, jarg2, 0);
+ argp3 = (uint32_t *)&jarg3;
+ if (!argp3) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null uint32_t");
+ return 0;
+ }
+ arg3 = *argp3;
+ arg4 = *(BoolectorNode **)&jarg4;
+ result = boolector_fun_sort_check(arg1,(BoolectorNode**)array,arg3,arg4);
+ (*jenv)->ReleaseLongArrayElements(jenv, jarg2, array, 0);
+ return result;
+}
+
+
+SWIGEXPORT jstring JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1bv_1assignment(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jstring jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ char *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ result = (char *)boolector_bv_assignment(arg1,arg2);
+ if (result) jresult = (*jenv)->NewStringUTF(jenv, (const char *)result);
+ return jresult;
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1free_1bv_1assignment(JNIEnv *jenv, jclass jcls, jlong jarg1, jstring jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ char *arg2 = (char *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = 0;
+ if (jarg2) {
+ arg2 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg2, 0);
+ if (!arg2) return ;
+ }
+ boolector_free_bv_assignment(arg1,(char const *)arg2);
+ if (arg2) (*jenv)->ReleaseStringUTFChars(jenv, jarg2, (const char *)arg2);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1array_1assignment(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3, jlong jarg4, jlong jarg5) {
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ char ***arg3 = (char ***) 0 ;
+ char ***arg4 = (char ***) 0 ;
+ uint32_t *arg5 = (uint32_t *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(char ****)&jarg3;
+ arg4 = *(char ****)&jarg4;
+ arg5 = (uint32_t *)&jarg5;
+ boolector_array_assignment(arg1,arg2,arg3,arg4,arg5);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1free_1array_1assignment(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3, jlong jarg4) {
+ Btor *arg1 = (Btor *) 0 ;
+ char **arg2 = (char **) 0 ;
+ char **arg3 = (char **) 0 ;
+ uint32_t arg4 ;
+ uint32_t *argp4 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(char ***)&jarg2;
+ arg3 = *(char ***)&jarg3;
+ argp4 = (uint32_t *)&jarg4;
+ if (!argp4) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null uint32_t");
+ return ;
+ }
+ arg4 = *argp4;
+ boolector_free_array_assignment(arg1,arg2,arg3,arg4);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1uf_1assignment(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3, jlong jarg4, jlong jarg5) {
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ char ***arg3 = (char ***) 0 ;
+ char ***arg4 = (char ***) 0 ;
+ uint32_t *arg5 = (uint32_t *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(char ****)&jarg3;
+ arg4 = *(char ****)&jarg4;
+ arg5 = *(uint32_t **)&jarg5;
+ boolector_uf_assignment(arg1,arg2,arg3,arg4,arg5);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1free_1uf_1assignment(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3, jlong jarg4) {
+ Btor *arg1 = (Btor *) 0 ;
+ char **arg2 = (char **) 0 ;
+ char **arg3 = (char **) 0 ;
+ uint32_t arg4 ;
+ uint32_t *argp4 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(char ***)&jarg2;
+ arg3 = *(char ***)&jarg3;
+ argp4 = (uint32_t *)&jarg4;
+ if (!argp4) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null uint32_t");
+ return ;
+ }
+ arg4 = *argp4;
+ boolector_free_uf_assignment(arg1,arg2,arg3,arg4);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1print_1model(JNIEnv *jenv, jclass jcls, jlong jarg1, jstring jarg2, jlong jarg3) {
+ Btor *arg1 = (Btor *) 0 ;
+ char *arg2 = (char *) 0 ;
+ FILE *arg3 = (FILE *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = 0;
+ if (jarg2) {
+ arg2 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg2, 0);
+ if (!arg2) return ;
+ }
+ arg3 = *(FILE **)&jarg3;
+ boolector_print_model(arg1,arg2,arg3);
+ if (arg2) (*jenv)->ReleaseStringUTFChars(jenv, jarg2, (const char *)arg2);
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1bool_1sort(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorSort result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ result = (BoolectorSort)boolector_bool_sort(arg1);
+ *(BoolectorSort *)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1bitvec_1sort(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ uint32_t arg2 ;
+ uint32_t *argp2 ;
+ BoolectorSort result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ argp2 = (uint32_t *)&jarg2;
+ if (!argp2) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null uint32_t");
+ return 0;
+ }
+ arg2 = *argp2;
+ result = (BoolectorSort)boolector_bitvec_sort(arg1,arg2);
+ *(BoolectorSort *)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1fun_1sort(JNIEnv *jenv, jclass jcls, jlong jarg1, jlongArray jarg2, jlong jarg3, jlong jarg4) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+
+ uint32_t arg3 ;
+ BoolectorSort arg4 = (BoolectorSort) 0 ;
+ uint32_t *argp3 ;
+ BoolectorSort result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ jlong *array = (*jenv)->GetLongArrayElements(jenv, jarg2, 0);
+ argp3 = (uint32_t *)&jarg3;
+ if (!argp3) {
+ SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "Attempt to dereference null uint32_t");
+ return 0;
+ }
+ arg3 = *argp3;
+ arg4 = *(BoolectorSort *)&jarg4;
+ result = (BoolectorSort)boolector_fun_sort(arg1,(BoolectorSort*)array,arg3,arg4);
+ *(BoolectorSort *)&jresult = result;
+ (*jenv)->ReleaseLongArrayElements(jenv, jarg2, array, 0);
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1array_1sort(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorSort arg2 = (BoolectorSort) 0 ;
+ BoolectorSort arg3 = (BoolectorSort) 0 ;
+ BoolectorSort result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorSort *)&jarg2;
+ arg3 = *(BoolectorSort *)&jarg3;
+ result = (BoolectorSort)boolector_array_sort(arg1,arg2,arg3);
+ *(BoolectorSort *)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1copy_1sort(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jlong jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorSort arg2 = (BoolectorSort) 0 ;
+ BoolectorSort result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorSort *)&jarg2;
+ result = (BoolectorSort)boolector_copy_sort(arg1,arg2);
+ *(BoolectorSort *)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1release_1sort(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorSort arg2 = (BoolectorSort) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorSort *)&jarg2;
+ boolector_release_sort(arg1,arg2);
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1is_1equal_1sort(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ result = (bool)boolector_is_equal_sort(arg1,arg2,arg3);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1is_1array_1sort(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorSort arg2 = (BoolectorSort) 0 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorSort *)&jarg2;
+ result = (bool)boolector_is_array_sort(arg1,arg2);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1is_1bitvec_1sort(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorSort arg2 = (BoolectorSort) 0 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorSort *)&jarg2;
+ result = (bool)boolector_is_bitvec_sort(arg1,arg2);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jboolean JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1is_1fun_1sort(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jboolean jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorSort arg2 = (BoolectorSort) 0 ;
+ bool result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorSort *)&jarg2;
+ result = (bool)boolector_is_fun_sort(arg1,arg2);
+ jresult = (jboolean)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1parse(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jstring jarg3, jlong jarg4, jlong jarg5, jlong jarg6) {
+ Btor *arg1 = (Btor *) 0 ;
+ FILE *arg2 = (FILE *) 0 ;
+ char *arg3 = (char *) 0 ;
+ FILE *arg4 = (FILE *) 0 ;
+ char **arg5 = (char **) 0 ;
+ int32_t *arg6 = (int32_t *) 0 ;
+ jint result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(FILE **)&jarg2;
+ arg3 = 0;
+ if (jarg3) {
+ arg3 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg3, 0);
+ if (!arg3) return 0;
+ }
+ arg4 = *(FILE **)&jarg4;
+ arg5 = *(char ***)&jarg5;
+ arg6 = *(int32_t **)&jarg6;
+ result = boolector_parse(arg1,arg2,(char const *)arg3,arg4,arg5,arg6);
+ if (arg3) (*jenv)->ReleaseStringUTFChars(jenv, jarg3, (const char *)arg3);
+ return result;
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1parse_1btor(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jstring jarg3, jlong jarg4, jlong jarg5, jlong jarg6) {
+ Btor *arg1 = (Btor *) 0 ;
+ FILE *arg2 = (FILE *) 0 ;
+ char *arg3 = (char *) 0 ;
+ FILE *arg4 = (FILE *) 0 ;
+ char **arg5 = (char **) 0 ;
+ int32_t *arg6 = (int32_t *) 0 ;
+ jint result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(FILE **)&jarg2;
+ arg3 = 0;
+ if (jarg3) {
+ arg3 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg3, 0);
+ if (!arg3) return 0;
+ }
+ arg4 = *(FILE **)&jarg4;
+ arg5 = *(char ***)&jarg5;
+ arg6 = *(int32_t **)&jarg6;
+ result = boolector_parse_btor(arg1,arg2,(char const *)arg3,arg4,arg5,arg6);
+ if (arg3) (*jenv)->ReleaseStringUTFChars(jenv, jarg3, (const char *)arg3);
+ return result;
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1parse_1btor2(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jstring jarg3, jlong jarg4, jlong jarg5, jlong jarg6) {
+ Btor *arg1 = (Btor *) 0 ;
+ FILE *arg2 = (FILE *) 0 ;
+ char *arg3 = (char *) 0 ;
+ FILE *arg4 = (FILE *) 0 ;
+ char **arg5 = (char **) 0 ;
+ int32_t *arg6 = (int32_t *) 0 ;
+ jint result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(FILE **)&jarg2;
+ arg3 = 0;
+ if (jarg3) {
+ arg3 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg3, 0);
+ if (!arg3) return 0;
+ }
+ arg4 = *(FILE **)&jarg4;
+ arg5 = *(char ***)&jarg5;
+ arg6 = *(int32_t **)&jarg6;
+ result = boolector_parse_btor2(arg1,arg2,(char const *)arg3,arg4,arg5,arg6);
+ if (arg3) (*jenv)->ReleaseStringUTFChars(jenv, jarg3, (const char *)arg3);
+ return result;
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1parse_1smt1(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jstring jarg3, jlong jarg4, jlong jarg5, jlong jarg6) {
+ Btor *arg1 = (Btor *) 0 ;
+ FILE *arg2 = (FILE *) 0 ;
+ char *arg3 = (char *) 0 ;
+ FILE *arg4 = (FILE *) 0 ;
+ char **arg5 = (char **) 0 ;
+ int32_t *arg6 = (int32_t *) 0 ;
+ jint result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(FILE **)&jarg2;
+ arg3 = 0;
+ if (jarg3) {
+ arg3 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg3, 0);
+ if (!arg3) return 0;
+ }
+ arg4 = *(FILE **)&jarg4;
+ arg5 = *(char ***)&jarg5;
+ arg6 = *(int32_t **)&jarg6;
+ result = boolector_parse_smt1(arg1,arg2,(char const *)arg3,arg4,arg5,arg6);
+ if (arg3) (*jenv)->ReleaseStringUTFChars(jenv, jarg3, (const char *)arg3);
+ return result;
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1parse_1smt2(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jstring jarg3, jlong jarg4, jlong jarg5, jlong jarg6) {
+ Btor *arg1 = (Btor *) 0 ;
+ FILE *arg2 = (FILE *) 0 ;
+ char *arg3 = (char *) 0 ;
+ FILE *arg4 = (FILE *) 0 ;
+ char **arg5 = (char **) 0 ;
+ int32_t *arg6 = (int32_t *) 0 ;
+ jint result;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(FILE **)&jarg2;
+ arg3 = 0;
+ if (jarg3) {
+ arg3 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg3, 0);
+ if (!arg3) return 0;
+ }
+ arg4 = *(FILE **)&jarg4;
+ arg5 = *(char ***)&jarg5;
+ arg6 = *(int32_t **)&jarg6;
+ result = boolector_parse_smt2(arg1,arg2,(char const *)arg3,arg4,arg5,arg6);
+ if (arg3) (*jenv)->ReleaseStringUTFChars(jenv, jarg3, (const char *)arg3);
+ return result;
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1dump_1btor_1node(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ Btor *arg1 = (Btor *) 0 ;
+ FILE *arg2 = (FILE *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(FILE **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ boolector_dump_btor_node(arg1,arg2,arg3);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1dump_1btor(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ FILE *arg2 = (FILE *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(FILE **)&jarg2;
+ boolector_dump_btor(arg1,arg2);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1dump_1smt2_1node(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
+ Btor *arg1 = (Btor *) 0 ;
+ FILE *arg2 = (FILE *) 0 ;
+ BoolectorNode *arg3 = (BoolectorNode *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(FILE **)&jarg2;
+ arg3 = *(BoolectorNode **)&jarg3;
+ boolector_dump_smt2_node(arg1,arg2,arg3);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1dump_1smt2(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ FILE *arg2 = (FILE *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(FILE **)&jarg2;
+ boolector_dump_smt2(arg1,arg2);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1dump_1aiger_1ascii(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jboolean jarg3) {
+ Btor *arg1 = (Btor *) 0 ;
+ FILE *arg2 = (FILE *) 0 ;
+ bool arg3 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(FILE **)&jarg2;
+ arg3 = jarg3 ? true : false;
+ boolector_dump_aiger_ascii(arg1,arg2,arg3);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1dump_1aiger_1binary(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jboolean jarg3) {
+ Btor *arg1 = (Btor *) 0 ;
+ FILE *arg2 = (FILE *) 0 ;
+ bool arg3 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(FILE **)&jarg2;
+ arg3 = jarg3 ? true : false;
+ boolector_dump_aiger_binary(arg1,arg2,arg3);
+}
+
+
+SWIGEXPORT jstring JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1copyright(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ jstring jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ char *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ result = (char *)boolector_copyright(arg1);
+ if (result) jresult = (*jenv)->NewStringUTF(jenv, (const char *)result);
+ return jresult;
+}
+
+
+SWIGEXPORT jstring JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1version(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ jstring jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ char *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ result = (char *)boolector_version(arg1);
+ if (result) jresult = (*jenv)->NewStringUTF(jenv, (const char *)result);
+ return jresult;
+}
+
+
+SWIGEXPORT jstring JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1git_1id(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ jstring jresult = 0 ;
+ Btor *arg1 = (Btor *) 0 ;
+ char *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ result = (char *)boolector_git_id(arg1);
+ if (result) jresult = (*jenv)->NewStringUTF(jenv, (const char *)result);
+ return jresult;
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_BTOR_1RESULT_1SAT_1get(JNIEnv *jenv, jclass jcls) {
+ jint jresult = 0 ;
+ enum BtorSolverResult result;
+
+ (void)jenv;
+ (void)jcls;
+ result = (enum BtorSolverResult)BTOR_RESULT_SAT;
+ jresult = (jint)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_BTOR_1RESULT_1UNSAT_1get(JNIEnv *jenv, jclass jcls) {
+ jint jresult = 0 ;
+ enum BtorSolverResult result;
+
+ (void)jenv;
+ (void)jcls;
+ result = (enum BtorSolverResult)BTOR_RESULT_UNSAT;
+ jresult = (jint)result;
+ return jresult;
+}
+
+
+SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_BTOR_1RESULT_1UNKNOWN_1get(JNIEnv *jenv, jclass jcls) {
+ jint jresult = 0 ;
+ enum BtorSolverResult result;
+
+ (void)jenv;
+ (void)jcls;
+ result = (enum BtorSolverResult)BTOR_RESULT_UNKNOWN;
+ jresult = (jint)result;
+ return jresult;
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_BtorAbortCallback_1abort_1fun_1set(JNIEnv *jenv, jclass jcls, jlong jarg1, jobject jarg1_, jlong jarg2) {
+ struct BtorAbortCallback *arg1 = (struct BtorAbortCallback *) 0 ;
+ void (*arg2)(char const *) = (void (*)(char const *)) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ (void)jarg1_;
+ arg1 = *(struct BtorAbortCallback **)&jarg1;
+ arg2 = *(void (**)(char const *))&jarg2;
+ if (arg1) (arg1)->abort_fun = arg2;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_BtorAbortCallback_1abort_1fun_1get(JNIEnv *jenv, jclass jcls, jlong jarg1, jobject jarg1_) {
+ jlong jresult = 0 ;
+ struct BtorAbortCallback *arg1 = (struct BtorAbortCallback *) 0 ;
+ void (*result)(char const *) = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ (void)jarg1_;
+ arg1 = *(struct BtorAbortCallback **)&jarg1;
+ result = (void (*)(char const *)) ((arg1)->abort_fun);
+ *(void (**)(char const *))&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_BtorAbortCallback_1cb_1fun_1set(JNIEnv *jenv, jclass jcls, jlong jarg1, jobject jarg1_, jlong jarg2) {
+ struct BtorAbortCallback *arg1 = (struct BtorAbortCallback *) 0 ;
+ void *arg2 = (void *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ (void)jarg1_;
+ arg1 = *(struct BtorAbortCallback **)&jarg1;
+ arg2 = *(void **)&jarg2;
+ if (arg1) (arg1)->cb_fun = arg2;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_BtorAbortCallback_1cb_1fun_1get(JNIEnv *jenv, jclass jcls, jlong jarg1, jobject jarg1_) {
+ jlong jresult = 0 ;
+ struct BtorAbortCallback *arg1 = (struct BtorAbortCallback *) 0 ;
+ void *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ (void)jarg1_;
+ arg1 = *(struct BtorAbortCallback **)&jarg1;
+ result = (void *) ((arg1)->cb_fun);
+ *(void **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_new_1BtorAbortCallback(JNIEnv *jenv, jclass jcls) {
+ jlong jresult = 0 ;
+ struct BtorAbortCallback *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ result = (struct BtorAbortCallback *)calloc(1, sizeof(struct BtorAbortCallback));
+ *(struct BtorAbortCallback **)&jresult = result;
+ return jresult;
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_delete_1BtorAbortCallback(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ struct BtorAbortCallback *arg1 = (struct BtorAbortCallback *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(struct BtorAbortCallback **)&jarg1;
+ free((char *) arg1);
+}
+
+
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_btor_1abort_1callback_1set(JNIEnv *jenv, jclass jcls, jlong jarg1, jobject jarg1_) {
+ BtorAbortCallback *arg1 = (BtorAbortCallback *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ (void)jarg1_;
+ arg1 = *(BtorAbortCallback **)&jarg1;
+ btor_abort_callback = *arg1;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_btor_1abort_1callback_1get(JNIEnv *jenv, jclass jcls) {
+ jlong jresult = 0 ;
+ BtorAbortCallback *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ result = (BtorAbortCallback *)&btor_abort_callback;
+ *(BtorAbortCallback **)&jresult = result;
+ return jresult;
+}
+
+//helpmethods
+
+ //dumps complete model into new file and reads it to give it back
+SWIGEXPORT jstring JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1help_1dump_1smt2(JNIEnv *jenv, jclass jcls, jlong jarg1) {
+ jstring jresult = 0;
+ Btor *arg1 = (Btor *) 0 ;
+ char *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+
+ char * buffer = 0;
+ long length;
+ FILE *f = 0;
+ f = fopen("temp", "w+");
+ if(f==NULL) {
+ perror("ERROR");
+ }
+
+ //fclose (f);
+
+ //write
+ boolector_dump_smt2(arg1, f);
+
+ //read
+ if (f)
+ {
+ fseek (f, 0, SEEK_END);
+ length = ftell (f);
+ fseek (f, 0, SEEK_SET);
+ buffer = malloc (length);
+ if (buffer)
+ {
+ fread (buffer, 1, length, f);
+ }
+ fclose (f);
+ }
+
+ if (buffer)
+ {
+ result = buffer;
+ }
+
+
+ if (result) jresult = (*jenv)->NewStringUTF(jenv, (const char *)result);
+ return jresult;
+}
+
+ //helper method for parsing string into btor
+ SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1help_1parse(JNIEnv *jenv, jclass jcls, jlong jarg1, jstring jarg2) {
+ int32_t result = 0;
+ Btor *arg1 = (Btor *) 0 ;
+ jint jresult = 0 ;
+ int32_t *status = (int32_t *) 0 ;
+ char **errormsg = (char **) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+ char *arg2 = (char *) 0 ;
+ if (jarg2) {
+ arg2 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg2, 0);
+ if (!arg2) return 0;
+ }
+
+ FILE *f = 0;
+ f = fopen("temp", "w+");
+ if(f==NULL) {
+ perror("ERROR_INPUTFILE");
+ }
+ fputs(arg2, f);
+ fclose (f);
+
+ FILE *fout = 0;
+ fout = fopen("tempout", "w+");
+ if(fout==NULL) {
+ perror("ERROR_OUTPUTFILE");
+ }
+ fclose (fout);
+
+ //"read" (parse)
+ result = boolector_parse(arg1, f, "temp", fout, errormsg, status);
+ jresult = (jint)result;
+
+ return jresult;
+}
+
+ //dumps NODE into new file and reads it to give it back
+SWIGEXPORT jstring JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1help_1dump_1node_1smt2(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ jstring jresult = 0;
+ Btor *arg1 = (Btor *) 0 ;
+ char *result = 0 ;
+
+ (void)jenv;
+ (void)jcls;
+ arg1 = *(Btor **)&jarg1;
+
+ char * buffer = 0;
+ long length;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ arg2 = *(BoolectorNode **)&jarg2;
+
+ FILE *f = 0;
+ f = fopen("temp", "w+");
+ if(f==NULL) {
+ perror("ERROR: COULDNT DUMP NODE BECAUSE IT COULDNT CREATE A DUMP FILE");
+ }
+
+ //fclose (f);
+
+ //write
+ boolector_dump_smt2_node(arg1, f, arg2);
+
+ //read
+ if (f)
+ {
+ fseek (f, 0, SEEK_END);
+ length = ftell (f);
+ fseek (f, 0, SEEK_SET);
+ buffer = malloc (length);
+ if (buffer)
+ {
+ fread (buffer, 1, length, f);
+ }
+ fclose (f);
+ }
+
+ if (buffer)
+ {
+ result = buffer;
+ }
+
+
+ if (result) jresult = (*jenv)->NewStringUTF(jenv, (const char *)result);
+ return jresult;
+}
+
+
+ //reads uf assignment and gives back array with 3 slots, first is size of the other 2 entrys, second and third are arrays, second is uf argument assignment strings, third is uf value assignments
+SWIGEXPORT void JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1uf_1assignment_1helper(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ char ***arg3 = (char ***) 0 ;
+ char ***arg4 = (char ***) 0 ;
+ uint32_t *arg5 = (uint32_t *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+
+ int i = 0;
+ int j = 0;
+
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+
+ boolector_uf_assignment(arg1,arg2,arg3,arg4,arg5);
+
+ if(arg3 == 0 || arg4 == 0 || arg5 == 0) return ((void*)0) ;
+
+ jsize arrayLength = *arg5;
+ int arrayLengthInt = *arg5;
+ char **workArray = *arg3;
+
+ jclass classString = (*jenv)->FindClass(jenv, "java/lang/String");
+ jclass classArray = (*jenv)->FindClass(jenv, "[Ljava/lang/Object;");
+
+ jobjectArray outerJNIArray = (jobjectArray)(*jenv)->NewObjectArray(jenv, 2, classArray, NULL);
+
+ for(i=0;i<2;i++) {
+ jobjectArray innerJNIArray = (jobjectArray)(*jenv)->NewObjectArray(jenv, arrayLength, classString, (*jenv)->NewStringUTF(jenv, ""));
+
+ for(j=0;jSetObjectArrayElement(jenv, innerJNIArray, j, (*jenv)->NewStringUTF(jenv, workArray[j]));
+ }
+ //switch to second Array
+ workArray = *arg4;
+ (*jenv)->SetObjectArrayElement(jenv, outerJNIArray, i, innerJNIArray);
+ (*jenv)->DeleteLocalRef(jenv, innerJNIArray);
+ }
+ (*jenv)->DeleteLocalRef(jenv, classString);
+ (*jenv)->DeleteLocalRef(jenv, classArray);
+
+ return outerJNIArray;
+}
+
+//helper method for arrays similiar to the uf one
+SWIGEXPORT jobjectArray JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1array_1assignment_1helper(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2) {
+ Btor *arg1 = (Btor *) 0 ;
+ BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+ char ***arg3 = (char ***) 0 ;
+ char ***arg4 = (char ***) 0 ;
+ uint32_t *arg5 = (uint32_t *) 0 ;
+
+ (void)jenv;
+ (void)jcls;
+
+ int i = 0;
+ int j = 0;
+
+ arg1 = *(Btor **)&jarg1;
+ arg2 = *(BoolectorNode **)&jarg2;
+
+ boolector_array_assignment(arg1,arg2,arg3,arg4,arg5);
+
+ if(arg3 == 0 || arg4 == 0 || arg5 == 0) return ((void*)0) ;
+
+ jsize arrayLength = *arg5;
+ int arrayLengthInt = *arg5;
+ char **workArray = *arg3;
+
+ jclass classString = (*jenv)->FindClass(jenv, "java/lang/String");
+ jclass classArray = (*jenv)->FindClass(jenv, "[Ljava/lang/Object;");
+
+ jobjectArray outerJNIArray = (jobjectArray)(*jenv)->NewObjectArray(jenv, 2, classArray, NULL);
+
+ for(i=0;i<2;i++) {
+ jobjectArray innerJNIArray = (jobjectArray)(*jenv)->NewObjectArray(jenv, arrayLength, classString, (*jenv)->NewStringUTF(jenv, ""));
+
+ for(j=0;jSetObjectArrayElement(jenv, innerJNIArray, j, (*jenv)->NewStringUTF(jenv, workArray[j]));
+ }
+ //switch to second Array
+ workArray = *arg4;
+ (*jenv)->SetObjectArrayElement(jenv, outerJNIArray, i, innerJNIArray);
+ (*jenv)->DeleteLocalRef(jenv, innerJNIArray);
+ }
+ (*jenv)->DeleteLocalRef(jenv, classString);
+ (*jenv)->DeleteLocalRef(jenv, classArray);
+
+ return outerJNIArray;
+}
+
+#ifdef __cplusplus
+}
+#endif
+
diff --git a/lib/native/x86_64-linux/libboolector.so b/lib/native/x86_64-linux/libboolector.so
new file mode 120000
index 0000000000..c20b21c0a9
--- /dev/null
+++ b/lib/native/x86_64-linux/libboolector.so
@@ -0,0 +1 @@
+../../java/runtime/libboolector.so
\ No newline at end of file
diff --git a/lib/native/x86_64-linux/libminisat.so b/lib/native/x86_64-linux/libminisat.so
new file mode 120000
index 0000000000..0aa60a0706
--- /dev/null
+++ b/lib/native/x86_64-linux/libminisat.so
@@ -0,0 +1 @@
+../../java/runtime/libminisat.so
\ No newline at end of file
diff --git a/lib/native/x86_64-linux/libpicosat.so b/lib/native/x86_64-linux/libpicosat.so
new file mode 120000
index 0000000000..15e9176866
--- /dev/null
+++ b/lib/native/x86_64-linux/libpicosat.so
@@ -0,0 +1 @@
+../../java/runtime/libpicosat.so
\ No newline at end of file
diff --git a/solvers_ivy_conf/ivy_boolector.xml b/solvers_ivy_conf/ivy_boolector.xml
new file mode 100644
index 0000000000..d3648b87c9
--- /dev/null
+++ b/solvers_ivy_conf/ivy_boolector.xml
@@ -0,0 +1,26 @@
+
+
+
+
+
+ Boolector solver and JavaSMT JNI wrapper.
+ Boolector is provided under the MIT License.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/src/org/sosy_lab/java_smt/SolverContextFactory.java b/src/org/sosy_lab/java_smt/SolverContextFactory.java
index f699ba452c..572b77552a 100644
--- a/src/org/sosy_lab/java_smt/SolverContextFactory.java
+++ b/src/org/sosy_lab/java_smt/SolverContextFactory.java
@@ -51,6 +51,7 @@
import org.sosy_lab.java_smt.api.SolverContext;
import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic;
import org.sosy_lab.java_smt.logging.LoggingSolverContext;
+import org.sosy_lab.java_smt.solvers.boolector.BoolectorSolverContext;
import org.sosy_lab.java_smt.solvers.cvc4.CVC4SolverContext;
import org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5SolverContext;
import org.sosy_lab.java_smt.solvers.princess.PrincessSolverContext;
@@ -70,6 +71,7 @@ public enum Solvers {
SMTINTERPOL,
Z3,
PRINCESS,
+ BOOLECTOR,
CVC4
}
@@ -225,6 +227,9 @@ private SolverContext generateContext0(Solvers solverToCreate)
return PrincessSolverContext.create(
config, shutdownNotifier, logfile, (int) randomSeed, nonLinearArithmetic);
+ case BOOLECTOR:
+ return BoolectorSolverContext.create(config, shutdownNotifier, logfile, (int) randomSeed);
+
default:
throw new AssertionError("no solver selected");
}
diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java
new file mode 100644
index 0000000000..f564bc5072
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java
@@ -0,0 +1,166 @@
+/*
+ * JavaSMT is an API wrapper for a collection of SMT solvers.
+ * This file is part of JavaSMT.
+ *
+ * Copyright (C) 2007-2019 Dirk Beyer
+ * All rights reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.sosy_lab.java_smt.solvers.boolector;
+
+import com.google.common.base.Preconditions;
+import java.util.ArrayDeque;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Deque;
+import java.util.List;
+import java.util.Optional;
+import java.util.Set;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.common.ShutdownNotifier;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Model;
+import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
+import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat;
+
+abstract class BoolectorAbstractProver extends AbstractProverWithAllSat {
+ // BoolectorAbstractProver extends AbstractProverWithAllSat
+ // AF = assertedFormulas; E = ?
+
+ private final long btor;
+ private final BoolectorFormulaManager manager;
+ private final BoolectorFormulaCreator creator;
+ protected final Deque> assertedFormulas = new ArrayDeque<>();
+ protected boolean wasLastSatCheckSat = false; // and stack is not changed
+
+ // Used/Built by TheoremProver
+ protected BoolectorAbstractProver(
+ BoolectorFormulaManager manager,
+ BoolectorFormulaCreator creator,
+ long btor,
+ ShutdownNotifier pShutdownNotifier,
+ Set pOptions) {
+ super(pOptions, manager.getBooleanFormulaManager(), pShutdownNotifier);
+ this.manager = manager;
+ this.creator = creator;
+ this.btor = btor;
+ }
+
+ @Override
+ public void close() {
+ if (!closed) {
+ // Problem: Cloning results in not beeing able to access var with old name (string)
+ // NOT Cloning results in murdering btor that is still beeing used
+ // closing of assertions only by using boolector_release
+ // BtorJNI.boolector_delete(btor);
+ BtorJNI.boolector_pop(manager.getEnvironment(), assertedFormulas.size());
+ assertedFormulas.clear();
+ closed = true;
+ }
+ }
+
+ /*
+ * Boolector should throw its own exceptions that tell you what went wrong!
+ */
+ @Override
+ public boolean isUnsat() throws SolverException {
+ Preconditions.checkState(!closed);
+ wasLastSatCheckSat = false;
+ final int result = BtorJNI.boolector_sat(btor);
+ if (result == BtorJNI.BTOR_RESULT_SAT_get()) {
+ wasLastSatCheckSat = true;
+ return false;
+ } else if (result == BtorJNI.BTOR_RESULT_UNSAT_get()) {
+ return true;
+ } else if (result == BtorJNI.BTOR_RESULT_UNKNOWN_get()) {
+ throw new SolverException(
+ "Boolector encountered a problem or ran out of stack or heap memory, "
+ + "try increasing their sizes.");
+ } else {
+ throw new SolverException("Boolector sat call returned " + result);
+ }
+ }
+
+ @Override
+ public void pop() {
+ assertedFormulas.pop();
+ BtorJNI.boolector_pop(manager.getEnvironment(), 1);
+ }
+
+ @Override
+ public void push() {
+ assertedFormulas.push(new ArrayList<>());
+ BtorJNI.boolector_push(manager.getEnvironment(), 1);
+ }
+
+ @Override
+ public boolean isUnsatWithAssumptions(Collection pAssumptions)
+ throws SolverException, InterruptedException {
+ Preconditions.checkState(!closed);
+ for (BooleanFormula assumption : pAssumptions) {
+ BtorJNI.boolector_assume(btor, BoolectorFormulaManager.getBtorTerm(assumption));
+ }
+ return isUnsat();
+ }
+
+ @Override
+ public Model getModel() throws SolverException {
+ Preconditions.checkState(!closed);
+ Preconditions.checkState(wasLastSatCheckSat, NO_MODEL_HELP);
+ checkGenerateModels();
+ return getModelWithoutChecks();
+ }
+
+ @Override
+ public List getUnsatCore() {
+ throw new UnsupportedOperationException("Unsat core is not supported by Boolector.");
+ }
+
+ @Override
+ public Optional> unsatCoreOverAssumptions(
+ Collection pAssumptions) throws SolverException, InterruptedException {
+ throw new UnsupportedOperationException(
+ "Unsat core with assumptions is not supported by Boolector.");
+ }
+
+ @Override
+ protected Model getModelWithoutChecks() {
+ return new BoolectorModel(btor, creator, this, getAssertedTerms());
+ }
+
+ @Override
+ @Nullable
+ public T addConstraint(BooleanFormula constraint) {
+ BtorJNI.boolector_assert(
+ manager.getEnvironment(), BoolectorFormulaManager.getBtorTerm(constraint));
+ assertedFormulas.peek().add(BoolectorFormulaManager.getBtorTerm(constraint));
+ return null;
+ }
+
+ protected Collection getAssertedTerms() {
+ List result = new ArrayList<>();
+ assertedFormulas.forEach(result::addAll);
+ return result;
+ }
+
+ /**
+ * Simply returns true if the prover is closed. False otherwise.
+ *
+ * @return bool return value.
+ */
+ protected boolean isClosed() {
+ return closed;
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorArrayFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorArrayFormulaManager.java
new file mode 100644
index 0000000000..b5713f8bcb
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorArrayFormulaManager.java
@@ -0,0 +1,79 @@
+/*
+ * JavaSMT is an API wrapper for a collection of SMT solvers.
+ * This file is part of JavaSMT.
+ *
+ * Copyright (C) 2007-2019 Dirk Beyer
+ * All rights reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.sosy_lab.java_smt.solvers.boolector;
+
+import com.google.common.collect.Table;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.FormulaType;
+import org.sosy_lab.java_smt.api.FormulaType.BitvectorType;
+import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager;
+
+public class BoolectorArrayFormulaManager
+ extends AbstractArrayFormulaManager {
+
+ private final long btor;
+ private final Table nameFormulaCache;
+
+ BoolectorArrayFormulaManager(BoolectorFormulaCreator pCreator) {
+ super(pCreator);
+ this.btor = pCreator.getEnv();
+ this.nameFormulaCache = pCreator.getCache();
+ }
+
+ // pIndex should be a bitVector
+ @Override
+ protected Long select(Long pArray, Long pIndex) {
+ return BtorJNI.boolector_read(btor, pArray, pIndex);
+ }
+
+ // pIndex and pValue should be bitVectors
+ @Override
+ protected Long store(Long pArray, Long pIndex, Long pValue) {
+ return BtorJNI.boolector_write(btor, pArray, pIndex, pValue);
+ }
+
+ @Override
+ protected Long internalMakeArray(
+ String name, FormulaType pIndexType, FormulaType pElementType) {
+ if (!pIndexType.isBitvectorType() || !pElementType.isBitvectorType()) {
+ throw new IllegalArgumentException("Boolector supports bitvector arrays only.");
+ }
+ BitvectorType indexType = (BitvectorType) pIndexType;
+ BitvectorType elementType = (BitvectorType) pElementType;
+ final long indexSort = BtorJNI.boolector_bitvec_sort(btor, indexType.getSize());
+ final long elementSort = BtorJNI.boolector_bitvec_sort(btor, elementType.getSize());
+ final long arraySort = BtorJNI.boolector_array_sort(btor, indexSort, elementSort);
+ Long maybeFormula = nameFormulaCache.get(name, arraySort);
+ if (maybeFormula != null) {
+ return maybeFormula;
+ }
+ if (nameFormulaCache.containsRow(name)) {
+ throw new IllegalArgumentException("Symbol already used: " + name);
+ }
+ final long array = BtorJNI.boolector_array(btor, arraySort, name);
+ nameFormulaCache.put(name, arraySort, array);
+ return array;
+ }
+
+ @Override
+ protected Long equivalence(Long pArray1, Long pArray2) {
+ return BtorJNI.boolector_eq(btor, pArray1, pArray2);
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBitvectorFormulaManager.java
new file mode 100644
index 0000000000..9c5f242e9f
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBitvectorFormulaManager.java
@@ -0,0 +1,218 @@
+/*
+ * JavaSMT is an API wrapper for a collection of SMT solvers.
+ * This file is part of JavaSMT.
+ *
+ * Copyright (C) 2007-2019 Dirk Beyer
+ * All rights reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.sosy_lab.java_smt.solvers.boolector;
+
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_add;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_and;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_concat;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_eq;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_mul;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_neg;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_not;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_or;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_sdiv;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_sext;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_sgt;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_sgte;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_sll;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_slt;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_slte;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_smod;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_sra;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_srl;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_sub;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_udiv;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_uext;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_ugt;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_ugte;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_ult;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_ulte;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_urem;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_xor;
+
+import java.math.BigInteger;
+import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager;
+
+class BoolectorBitvectorFormulaManager
+ extends AbstractBitvectorFormulaManager {
+
+ private final long btor;
+
+ BoolectorBitvectorFormulaManager(BoolectorFormulaCreator creator) {
+ super(creator);
+ this.btor = creator.getEnv();
+ }
+
+ @Override
+ public Long makeBitvectorImpl(int pLength, BigInteger pI) {
+ pI = transformValueToRange(pLength, pI);
+ long sort = BtorJNI.boolector_bitvec_sort(btor, pLength);
+ return BtorJNI.boolector_constd(btor, sort, pI.toString());
+ }
+
+ @Override
+ protected Long makeBitvectorImpl(int length, Long value) {
+ // The value is a pointer to an expression. Do not use the plain numberal value.
+ throw new UnsupportedOperationException("Boolector does not support INT theory");
+ }
+
+ @Override
+ public Long toIntegerFormulaImpl(Long pI, boolean pSigned) {
+ throw new UnsupportedOperationException("BV to INT conversion is not supported.");
+ }
+
+ @Override
+ public Long negate(Long bitVec) {
+ return boolector_neg(btor, bitVec);
+ }
+
+ @Override
+ public Long add(Long bitVec1, Long bitVec2) {
+ return boolector_add(btor, bitVec1, bitVec2);
+ }
+
+ @Override
+ public Long subtract(Long bitVec1, Long bitVec2) {
+ return boolector_sub(btor, bitVec1, bitVec2);
+ }
+
+ @Override
+ public Long divide(Long bitVec1, Long bitVec2, boolean signed) {
+ if (signed) {
+ return boolector_sdiv(btor, bitVec1, bitVec2);
+ } else {
+ return boolector_udiv(btor, bitVec1, bitVec2);
+ }
+ }
+
+ @Override
+ public Long modulo(Long bitVec1, Long bitVec2, boolean signed) {
+ if (signed) {
+ return boolector_smod(btor, bitVec1, bitVec2);
+ } else {
+ return boolector_urem(btor, bitVec1, bitVec2);
+ }
+ }
+
+ @Override
+ public Long multiply(Long bitVec1, Long bitVec2) {
+ return boolector_mul(btor, bitVec1, bitVec2);
+ }
+
+ @Override
+ public Long equal(Long bitVec1, Long bitVec2) {
+ return boolector_eq(btor, bitVec1, bitVec2);
+ }
+
+ @Override
+ public Long greaterThan(Long bitVec1, Long bitVec2, boolean signed) {
+ if (signed) {
+ return boolector_sgt(btor, bitVec1, bitVec2);
+ } else {
+ return boolector_ugt(btor, bitVec1, bitVec2);
+ }
+ }
+
+ @Override
+ public Long greaterOrEquals(Long bitVec1, Long bitVec2, boolean signed) {
+ if (signed) {
+ return boolector_sgte(btor, bitVec1, bitVec2);
+ } else {
+ return boolector_ugte(btor, bitVec1, bitVec2);
+ }
+ }
+
+ @Override
+ public Long lessThan(Long bitVec1, Long bitVec2, boolean signed) {
+ if (signed) {
+ return boolector_slt(btor, bitVec1, bitVec2);
+ } else {
+ return boolector_ult(btor, bitVec1, bitVec2);
+ }
+ }
+
+ @Override
+ public Long lessOrEquals(Long bitVec1, Long bitVec2, boolean signed) {
+ if (signed) {
+ return boolector_slte(btor, bitVec1, bitVec2);
+ } else {
+ return boolector_ulte(btor, bitVec1, bitVec2);
+ }
+ }
+
+ @Override
+ public Long not(Long bitVec) {
+ return boolector_not(btor, bitVec);
+ }
+
+ @Override
+ public Long and(Long bitVec1, Long bitVec2) {
+ return boolector_and(btor, bitVec1, bitVec2);
+ }
+
+ @Override
+ public Long or(Long bitVec1, Long bitVec2) {
+ return boolector_or(btor, bitVec1, bitVec2);
+ }
+
+ @Override
+ public Long xor(Long bitVec1, Long bitVec2) {
+ return boolector_xor(btor, bitVec1, bitVec2);
+ }
+
+ @Override
+ public Long makeVariableImpl(int pLength, String pVar) {
+ long sort = BtorJNI.boolector_bitvec_sort(btor, pLength);
+ return getFormulaCreator().makeVariable(sort, pVar);
+ }
+
+ @Override
+ public Long shiftRight(Long bitVec, Long toShift, boolean signed) {
+ if (signed) {
+ return boolector_sra(btor, bitVec, toShift);
+ } else {
+ return boolector_srl(btor, bitVec, toShift);
+ }
+ }
+
+ @Override
+ public Long shiftLeft(Long bitVec, Long toShift) {
+ return boolector_sll(btor, bitVec, toShift);
+ }
+
+ @Override
+ public Long concat(Long bitVec, Long bitVecAppend) {
+ return boolector_concat(btor, bitVec, bitVecAppend);
+ }
+
+ @Override
+ public Long extract(Long pNode, int pMsb, int pLsb, boolean pSigned) {
+ return BtorJNI.boolector_slice(btor, pNode, pMsb, pLsb);
+ }
+
+ @Override
+ public Long extend(Long bitVec, int extensionBits, boolean signed) {
+ if (signed) {
+ return boolector_sext(btor, bitVec, extensionBits);
+ } else {
+ return boolector_uext(btor, bitVec, extensionBits);
+ }
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBooleanFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBooleanFormulaManager.java
new file mode 100644
index 0000000000..2813846b7c
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBooleanFormulaManager.java
@@ -0,0 +1,112 @@
+/*
+ * JavaSMT is an API wrapper for a collection of SMT solvers.
+ * This file is part of JavaSMT.
+ *
+ * Copyright (C) 2007-2019 Dirk Beyer
+ * All rights reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.sosy_lab.java_smt.solvers.boolector;
+
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_and;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_cond;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_false;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_iff;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_not;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_or;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_true;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_xor;
+
+import com.google.common.primitives.Longs;
+import org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager;
+
+public class BoolectorBooleanFormulaManager
+ extends AbstractBooleanFormulaManager {
+
+ private final long btor;
+
+ BoolectorBooleanFormulaManager(BoolectorFormulaCreator pCreator) {
+ super(pCreator);
+ this.btor = pCreator.getEnv();
+ }
+
+ @Override
+ public Long makeVariableImpl(String varName) {
+ long boolType = getFormulaCreator().getBoolType();
+ return getFormulaCreator().makeVariable(boolType, varName);
+ }
+
+ @Override
+ public Long makeBooleanImpl(boolean pValue) {
+ if (pValue) {
+ return boolector_true(btor);
+ } else {
+ return boolector_false(btor);
+ }
+ }
+
+ @Override
+ public Long not(Long pParam1) {
+ return boolector_not(btor, pParam1);
+ }
+
+ @Override
+ public Long and(Long pParam1, Long pParam2) {
+ return boolector_and(btor, pParam1, pParam2);
+ }
+
+ @Override
+ public Long or(Long pParam1, Long pParam2) {
+ return boolector_or(btor, pParam1, pParam2);
+ }
+
+ @Override
+ public Long xor(Long pParam1, Long pParam2) {
+ return boolector_xor(btor, pParam1, pParam2);
+ }
+
+ @Override
+ public Long equivalence(Long pBits1, Long pBits2) {
+ return boolector_iff(btor, pBits1, pBits2);
+ }
+
+ @Override
+ public boolean isTrue(Long pBits) {
+ return isConstant(pBits, 1);
+ }
+
+ @Override
+ public boolean isFalse(Long pBits) {
+ return isConstant(pBits, 0);
+ }
+
+ private boolean isConstant(final long pBits, final int constant) {
+ if (BtorJNI.boolector_get_width(btor, pBits) == 1) {
+ String assignment;
+ if (BtorJNI.boolector_is_const(btor, pBits)) {
+ assignment = BtorJNI.boolector_get_bits(btor, pBits);
+ Long maybeLong = Longs.tryParse(assignment);
+ if (maybeLong != null && maybeLong == constant) {
+ return true;
+ }
+ }
+ }
+ return false;
+ }
+
+ @Override
+ public Long ifThenElse(Long pCond, Long pF1, Long pF2) {
+ return boolector_cond(btor, pCond, pF1, pF2);
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormula.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormula.java
new file mode 100644
index 0000000000..96480be7cb
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormula.java
@@ -0,0 +1,98 @@
+/*
+ * JavaSMT is an API wrapper for a collection of SMT solvers.
+ * This file is part of JavaSMT.
+ *
+ * Copyright (C) 2007-2019 Dirk Beyer
+ * All rights reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.sosy_lab.java_smt.solvers.boolector;
+
+import com.google.errorprone.annotations.Immutable;
+import org.sosy_lab.java_smt.api.ArrayFormula;
+import org.sosy_lab.java_smt.api.BitvectorFormula;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.FormulaType;
+
+@Immutable
+abstract class BoolectorFormula implements Formula {
+
+ private final long btorTerm;
+ private final long btor; // We need the boolector instance to calculate the hash
+
+ BoolectorFormula(long term, long btor) {
+ this.btorTerm = term;
+ this.btor = btor;
+ }
+
+ final long getTerm() {
+ return btorTerm;
+ }
+
+ @Override
+ public final boolean equals(Object o) {
+ if (o == this) {
+ return true;
+ }
+ if (!(o instanceof BoolectorFormula)) {
+ return false;
+ }
+ BoolectorFormula other = (BoolectorFormula) o;
+ return btor == other.btor && btorTerm == other.btorTerm;
+ }
+
+ @Override
+ public final int hashCode() {
+ // Boolector uses structural hashing on its nodes (formulas)
+ return BtorJNI.boolector_get_node_id(btor, btorTerm);
+ }
+
+ @Immutable
+ static final class BoolectorBitvectorFormula extends BoolectorFormula
+ implements BitvectorFormula {
+ BoolectorBitvectorFormula(long pTerm, long btor) {
+ super(pTerm, btor);
+ }
+ }
+
+ @Immutable
+ static final class BoolectorBooleanFormula extends BoolectorFormula implements BooleanFormula {
+ BoolectorBooleanFormula(long pTerm, long btor) {
+ super(pTerm, btor);
+ }
+ }
+
+ static final class BoolectorArrayFormula
+ extends BoolectorFormula implements ArrayFormula {
+
+ private final FormulaType indexType;
+ private final FormulaType elementType;
+
+ BoolectorArrayFormula(
+ long pTerm, FormulaType pIndexType, FormulaType pElementType, long btor) {
+ super(pTerm, btor);
+ indexType = pIndexType;
+ elementType = pElementType;
+ }
+
+ public FormulaType getIndexType() {
+ return indexType;
+ }
+
+ public FormulaType getElementType() {
+ return elementType;
+ }
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaCreator.java
new file mode 100644
index 0000000000..ce2af33cf6
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaCreator.java
@@ -0,0 +1,377 @@
+/*
+ * JavaSMT is an API wrapper for a collection of SMT solvers.
+ * This file is part of JavaSMT.
+ *
+ * Copyright (C) 2007-2019 Dirk Beyer
+ * All rights reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.sosy_lab.java_smt.solvers.boolector;
+
+import static com.google.common.base.Preconditions.checkArgument;
+
+import com.google.common.base.Preconditions;
+import com.google.common.collect.HashBasedTable;
+import com.google.common.collect.ImmutableList;
+import com.google.common.collect.Table;
+import com.google.common.primitives.Longs;
+import java.math.BigInteger;
+import java.util.List;
+import org.sosy_lab.java_smt.api.ArrayFormula;
+import org.sosy_lab.java_smt.api.BitvectorFormula;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.FormulaType;
+import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType;
+import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
+import org.sosy_lab.java_smt.api.FunctionDeclarationKind;
+import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
+import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
+import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl;
+import org.sosy_lab.java_smt.solvers.boolector.BoolectorFormula.BoolectorArrayFormula;
+import org.sosy_lab.java_smt.solvers.boolector.BoolectorFormula.BoolectorBitvectorFormula;
+import org.sosy_lab.java_smt.solvers.boolector.BoolectorFormula.BoolectorBooleanFormula;
+
+public class BoolectorFormulaCreator extends FormulaCreator {
+
+ // Boolector can give back 'x' for a arbitrary value that we change to this
+ private static final char ARBITRARY_VALUE = '1';
+
+ /** Maps a name and a variable or function type to a concrete formula node. */
+ private final Table nameFormulaCache = HashBasedTable.create();
+
+ BoolectorFormulaCreator(Long btor) {
+ super(btor, BtorJNI.boolector_bool_sort(btor), null, null);
+ }
+
+ @SuppressWarnings("unchecked")
+ @Override
+ public FormulaType getFormulaType(T pFormula) {
+ if (pFormula instanceof BitvectorFormula) {
+ long sort = BtorJNI.boolector_get_sort(getEnv(), extractInfo(pFormula));
+ checkArgument(
+ BtorJNI.boolector_is_bitvec_sort(getEnv(), sort),
+ "BitvectorFormula with type missmatch: " + pFormula);
+ return (FormulaType)
+ FormulaType.getBitvectorTypeWithSize(
+ BtorJNI.boolector_get_width(getEnv(), extractInfo(pFormula)));
+ } else if (pFormula instanceof ArrayFormula, ?>) {
+ FormulaType arrayIndexType = getArrayFormulaIndexType((ArrayFormula) pFormula);
+ FormulaType arrayElementType = getArrayFormulaElementType((ArrayFormula) pFormula);
+ return (FormulaType) FormulaType.getArrayType(arrayIndexType, arrayElementType);
+ }
+ return super.getFormulaType(pFormula);
+ }
+
+ @Override
+ public Long extractInfo(Formula pT) {
+ return BoolectorFormulaManager.getBtorTerm(pT);
+ }
+
+ @Override
+ public FormulaType> getFormulaType(Long pFormula) {
+ long sort = BtorJNI.boolector_get_sort(getEnv(), pFormula);
+ if (BtorJNI.boolector_is_bitvec_sort(getEnv(), sort)) {
+ if (sort == 1) {
+ return FormulaType.BooleanType;
+ } else {
+ return FormulaType.getBitvectorTypeWithSize(
+ BtorJNI.boolector_get_width(getEnv(), pFormula));
+ }
+ } else if (BtorJNI.boolector_is_array_sort(getEnv(), sort)) {
+ int indexWidth = BtorJNI.boolector_get_index_width(getEnv(), pFormula);
+ int elementWidth = BtorJNI.boolector_get_width(getEnv(), pFormula);
+ return FormulaType.getArrayType(
+ FormulaType.getBitvectorTypeWithSize(indexWidth),
+ FormulaType.getBitvectorTypeWithSize(elementWidth));
+ }
+ throw new IllegalArgumentException("Unknown formula type for " + pFormula);
+ }
+
+ @SuppressWarnings("unchecked")
+ @Override
+ public T encapsulate(FormulaType pType, Long pTerm) {
+ assert pType.equals(getFormulaType(pTerm))
+ : String.format(
+ "Trying to encapsulate formula of type %s as %s", getFormulaType(pTerm), pType);
+ if (pType.isBooleanType()) {
+ return (T) new BoolectorBooleanFormula(pTerm, getEnv());
+ } else if (pType.isArrayType()) {
+ ArrayFormulaType, ?> arrFt = (ArrayFormulaType, ?>) pType;
+ return (T)
+ new BoolectorArrayFormula<>(
+ pTerm, arrFt.getIndexType(), arrFt.getElementType(), getEnv());
+ } else if (pType.isBitvectorType()) {
+ return (T) new BoolectorBitvectorFormula(pTerm, getEnv());
+ }
+ throw new IllegalArgumentException(
+ "Cannot create formulas of type " + pType + " in Boolector.");
+ }
+
+ @Override
+ public BooleanFormula encapsulateBoolean(Long pTerm) {
+ assert getFormulaType(pTerm).isBooleanType()
+ : "Unexpected formula type for Boolean formula: " + getFormulaType(pTerm);
+ return new BoolectorBooleanFormula(pTerm, getEnv());
+ }
+
+ @Override
+ public BitvectorFormula encapsulateBitvector(Long pTerm) {
+ assert getFormulaType(pTerm).isBitvectorType()
+ : "Unexpected formula type for BV formula: " + getFormulaType(pTerm);
+ return new BoolectorBitvectorFormula(pTerm, getEnv());
+ }
+
+ @Override
+ protected ArrayFormula encapsulateArray(
+ Long pTerm, FormulaType pIndexType, FormulaType pElementType) {
+ assert getFormulaType(pTerm).isArrayType()
+ : "Unexpected formula type for array formula: " + getFormulaType(pTerm);
+ return new BoolectorArrayFormula<>(pTerm, pIndexType, pElementType, getEnv());
+ }
+
+ @Override
+ public Long getBitvectorType(int pBitwidth) {
+ return BtorJNI.boolector_bitvec_sort(getEnv(), pBitwidth);
+ }
+
+ @Override
+ public Long getFloatingPointType(FloatingPointType pType) {
+ throw new UnsupportedOperationException(
+ "Boolector does not support floating point operations.");
+ }
+
+ @Override
+ public Long getArrayType(Long pIndexType, Long pElementType) {
+ return BtorJNI.boolector_array_sort(getEnv(), pIndexType, pElementType);
+ }
+
+ // Checks if there is a variable with the exact same name and type and gives that back, or a new
+ // one, potentially with a new internal name (see cache).
+ @Override
+ public Long makeVariable(Long type, String varName) {
+ Long maybeFormula = nameFormulaCache.get(varName, type);
+ if (maybeFormula != null) {
+ return maybeFormula;
+ }
+ if (nameFormulaCache.containsRow(varName)) {
+ throw new IllegalArgumentException("Symbol already used: " + varName);
+ }
+ long newVar = BtorJNI.boolector_var(getEnv(), type, varName);
+ nameFormulaCache.put(varName, type, newVar);
+ return newVar;
+ }
+
+ // This method is a massive problem... you CANT get the value formulas(nodes) because they are
+ // only build and used internally in boolector. (See visit1 for help)
+ @Override
+ public R visit(FormulaVisitor visitor, Formula formula, Long f) {
+ throw new UnsupportedOperationException(
+ "We wait till the Boolector devs give us methods to do this.");
+ }
+
+ // Hopefully a helpful template for when visitor gets implemented
+ // Btor only has bitvec arrays and ufs with bitvecs and arrays of bitvecs
+ // (and quantifier with bitvecs only)
+ @SuppressWarnings("unused")
+ private R visit1(FormulaVisitor visitor, Formula formula, Long f) {
+ if (BtorJNI.boolector_is_const(getEnv(), f)) {
+ // Handles all constants (bitvec, bool)
+ String bits = BtorJNI.boolector_get_bits(getEnv(), f);
+ return visitor.visitConstant(formula, convertValue(f, parseBitvector(bits)));
+ } else if (BtorJNI.boolector_is_param(getEnv(), f)) {
+ // Quantifier have their own variables called param.
+ // They can only be bound once! (use them as bitvec)
+ int deBruijnIdx = 0; // TODO: Ask Developers for this because this is WRONG!
+ return visitor.visitBoundVariable(formula, deBruijnIdx);
+ } else if (false) {
+ // Quantifier
+ // there is currently no way to find out if the formula is a quantifier
+ // do we need them separately?
+ /*
+ * return visitor .visitQuantifier( (BoolectorBooleanFormula) formula, quantifier,
+ * boundVariables, new BoolectorBooleanFormula(body, getEnv()));
+ */
+ } else if (BtorJNI.boolector_is_var(getEnv(), f)) {
+ // bitvec var (size 1 is bool!)
+ return visitor.visitFreeVariable(formula, getName(f));
+ } else {
+ ImmutableList.Builder args = ImmutableList.builder();
+
+ ImmutableList.Builder> argTypes = ImmutableList.builder();
+
+ return visitor.visitFunction(
+ formula,
+ args.build(),
+ FunctionDeclarationImpl.of(
+ getName(f), getDeclarationKind(f), argTypes.build(), getFormulaType(f), f));
+ } // TODO: fix declaration in visitFunction
+ return null;
+ }
+
+ // TODO: returns kind of formula (add, uf etc....) once methods are provided
+ private FunctionDeclarationKind getDeclarationKind(@SuppressWarnings("unused") long f) {
+ return null;
+ }
+
+ @Override
+ public Long callFunctionImpl(Long pDeclaration, List pArgs) {
+ Preconditions.checkArgument(
+ !pArgs.isEmpty(), "Boolector does not support UFs without arguments.");
+ return BtorJNI.boolector_apply(getEnv(), Longs.toArray(pArgs), pArgs.size(), pDeclaration);
+ }
+
+ @Override
+ public Long declareUFImpl(String name, Long pReturnType, List pArgTypes) {
+ Preconditions.checkArgument(
+ !pArgTypes.isEmpty(), "Boolector does not support UFs without arguments.");
+
+ long[] funSorts = Longs.toArray(pArgTypes);
+ long sort = BtorJNI.boolector_fun_sort(getEnv(), funSorts, funSorts.length, pReturnType);
+ Long maybeFormula = nameFormulaCache.get(name, sort);
+ if (maybeFormula != null) {
+ return maybeFormula;
+ }
+ if (nameFormulaCache.containsRow(name)) {
+ throw new IllegalArgumentException("Symbol already used: " + name);
+ }
+ long uf = BtorJNI.boolector_uf(getEnv(), sort, name);
+ nameFormulaCache.put(name, sort, uf);
+ return uf;
+ }
+
+ @Override
+ public Object convertValue(Long key, Long term) {
+ String value = null;
+ if (BtorJNI.boolector_is_array(getEnv(), term)) {
+ value = BtorJNI.boolector_bv_assignment(getEnv(), term);
+ } else if (BtorJNI.boolector_is_const(getEnv(), term)) {
+ value = BtorJNI.boolector_get_bits(getEnv(), term);
+ } else if (BtorJNI.boolector_is_bitvec_sort(
+ getEnv(), BtorJNI.boolector_get_sort(getEnv(), term))) {
+ value = BtorJNI.boolector_bv_assignment(getEnv(), term);
+ } else {
+ throw new AssertionError("unknown sort and term");
+ // value = BtorJNI.boolector_bv_assignment(getEnv(), term);
+ }
+ // To get the correct type, we check the width of the term (== 1 means bool).
+ int width = BtorJNI.boolector_get_width(getEnv(), term);
+ if (width == 1) {
+ Long longValue = parseBigInt(value).longValue();
+ if (longValue == 1) {
+ return true;
+ } else if (longValue == 0) {
+ return false;
+ } else {
+ throw new IllegalArgumentException("Unexpected type with value: " + value);
+ }
+ }
+ return parseBigInt(value);
+ }
+
+ /**
+ * Boolector puts out Strings containing 1,0 or x that have to be parsed. If you want different
+ * values for x, change it in the constant! (BOOLECTOR_VARIABLE_ARBITRARI_REPLACEMENT)
+ *
+ * @param assignment String with the assignment of Boolector var.
+ * @return BigInteger in decimal.
+ */
+ private BigInteger parseBigInt(String assignment) {
+ try {
+ BigInteger bigInt = new BigInteger(assignment, 2);
+ return bigInt;
+ } catch (NumberFormatException e) {
+ char[] charArray = assignment.toCharArray();
+ for (int i = 0; i < charArray.length; i++) {
+ if (charArray[i] == 'x') {
+ charArray[i] = ARBITRARY_VALUE;
+ } else if (charArray[i] != '0' && charArray[i] != '1') {
+ throw new IllegalArgumentException(
+ "Boolector gave back an assignment that is not parseable.");
+ }
+ }
+ assignment = String.valueOf(charArray);
+ }
+ return new BigInteger(assignment, 2);
+ }
+
+ /**
+ * Transforms String bitvec into Long.
+ *
+ * @param bitVec return value of Boolector
+ * @return gives back the long version of the bitvector
+ */
+ private Long parseBitvector(String bitVec) {
+ try {
+ BigInteger bigInt = new BigInteger(bitVec, 2);
+ return bigInt.longValue();
+ } catch (NumberFormatException e) {
+ char[] charArray = bitVec.toCharArray();
+ for (int i = 0; i < charArray.length; i++) {
+ if (charArray[i] == 'x') {
+ charArray[i] = '1';
+ } else if (charArray[i] != '0' && charArray[i] != '1') {
+ throw new IllegalArgumentException(
+ "Boolector gave back an assignment that is not parseable.");
+ }
+ }
+ bitVec = String.valueOf(charArray);
+ }
+ BigInteger bigInt = new BigInteger(bitVec, 2);
+ return bigInt.longValue();
+ }
+
+ String getName(long pKey) {
+ return BtorJNI.boolector_get_symbol(getEnv(), pKey);
+ }
+
+ @Override
+ public Object convertValue(Long pF) {
+ throw new UnsupportedOperationException("Please use the other method.");
+ }
+
+ @Override
+ protected Long getBooleanVarDeclarationImpl(Long pTFormulaInfo) {
+ // declaration of constant or fun
+ if (BtorJNI.boolector_is_const(getEnv(), pTFormulaInfo)) {
+ return parseBitvector(BtorJNI.boolector_get_bits(getEnv(), pTFormulaInfo));
+ } else if (BtorJNI.boolector_is_var(getEnv(), pTFormulaInfo)) {
+ return parseBitvector(BtorJNI.boolector_bv_assignment(getEnv(), pTFormulaInfo));
+ } else {
+ throw new IllegalArgumentException(
+ "Debug only! getBooleanVarDeclarationImpl in BtorFormulaCreator");
+ }
+ }
+
+ /**
+ * Returns current variables cache.
+ *
+ * @return variables cache.
+ */
+ protected Table getCache() {
+ return nameFormulaCache;
+ }
+
+ @Override
+ protected FormulaType getArrayFormulaElementType(
+ ArrayFormula pArray) {
+ return ((BoolectorArrayFormula) pArray).getElementType();
+ }
+
+ @Override
+ protected FormulaType getArrayFormulaIndexType(
+ ArrayFormula pArray) {
+ return ((BoolectorArrayFormula) pArray).getIndexType();
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java
new file mode 100644
index 0000000000..bd8d38065a
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java
@@ -0,0 +1,76 @@
+/*
+ * JavaSMT is an API wrapper for a collection of SMT solvers.
+ * This file is part of JavaSMT.
+ *
+ * Copyright (C) 2007-2019 Dirk Beyer
+ * All rights reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.sosy_lab.java_smt.solvers.boolector;
+
+import java.io.IOException;
+import org.sosy_lab.common.Appender;
+import org.sosy_lab.common.Appenders;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager;
+
+final class BoolectorFormulaManager extends AbstractFormulaManager {
+
+ protected BoolectorFormulaManager(
+ BoolectorFormulaCreator pFormulaCreator,
+ BoolectorUFManager pFunctionManager,
+ BoolectorBooleanFormulaManager pBooleanManager,
+ BoolectorBitvectorFormulaManager pBitvectorManager,
+ BoolectorQuantifiedFormulaManager pQuantifierManager,
+ BoolectorArrayFormulaManager pArrayManager) {
+ super(
+ pFormulaCreator,
+ pFunctionManager,
+ pBooleanManager,
+ null,
+ null,
+ pBitvectorManager,
+ null,
+ pQuantifierManager,
+ pArrayManager,
+ null);
+ }
+
+ @Override
+ public BooleanFormula parse(String pS) throws IllegalArgumentException {
+ throw new UnsupportedOperationException("Boolector can not parse single formulas.");
+ }
+
+ @Override
+ public Appender dumpFormula(Long pT) {
+ return new Appenders.AbstractAppender() {
+ @Override
+ public void appendTo(Appendable out) throws IOException {
+ String dump = BtorJNI.boolector_help_dump_node_smt2(getEnvironment(), pT);
+ int length = dump.length();
+ int i = 1;
+ while (dump.charAt(length - i) != ')' && i < length) {
+ dump = dump.substring(0, length - i);
+ i++;
+ }
+ out.append(dump);
+ }
+ };
+ }
+
+ protected static long getBtorTerm(Formula pT) {
+ return ((BoolectorFormula) pT).getTerm();
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorModel.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorModel.java
new file mode 100644
index 0000000000..45cc06c56c
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorModel.java
@@ -0,0 +1,147 @@
+/*
+ * JavaSMT is an API wrapper for a collection of SMT solvers.
+ * This file is part of JavaSMT.
+ *
+ * Copyright (C) 2007-2019 Dirk Beyer
+ * All rights reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.sosy_lab.java_smt.solvers.boolector;
+
+import com.google.common.base.Preconditions;
+import com.google.common.collect.ImmutableList;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.List;
+import java.util.Map.Entry;
+import org.sosy_lab.java_smt.basicimpl.AbstractModel.CachingAbstractModel;
+
+class BoolectorModel extends CachingAbstractModel {
+
+ private final long btor;
+ private final BoolectorAbstractProver> prover;
+ private final BoolectorFormulaCreator bfCreator;
+ private boolean closed = false;
+
+ private final ImmutableList assertedTerms;
+
+ BoolectorModel(
+ long btor,
+ BoolectorFormulaCreator creator,
+ BoolectorAbstractProver> pProver,
+ Collection assertedTerms) {
+ super(creator);
+ this.bfCreator = creator;
+ this.btor = btor;
+ this.prover = pProver;
+ this.assertedTerms = ImmutableList.copyOf(assertedTerms);
+ }
+
+ @Override
+ public void close() {
+ if (!closed) {
+ // Technically boolector has no model
+ // but you could release all bindings.
+ closed = true;
+ }
+ }
+
+ @Override
+ protected ImmutableList toList() {
+ Preconditions.checkState(!closed);
+ Preconditions.checkState(!prover.isClosed(), "cannot use model after prover is closed");
+ // We wait till the Boolector devs give us methods to do this properly.
+ // See toList1 for help building this method! (delete toList1 later)
+ ImmutableList.Builder assignments = ImmutableList.builder();
+ return assignments.build();
+ }
+
+ @SuppressWarnings("unused")
+ private ImmutableList toList1() {
+ Preconditions.checkState(!closed);
+ Preconditions.checkState(!prover.isClosed(), "cannot use model after prover is closed");
+ ImmutableList.Builder assignments = ImmutableList.builder();
+ for (Long formula : assertedTerms) {
+ for (Entry entry : creator.extractVariablesAndUFs(formula, true).entrySet()) {
+ String name = entry.getKey();
+ Long var = entry.getValue();
+ if (BtorJNI.boolector_is_array(btor, var)) {
+ assignments.add(getArrayAssignment(formula));
+ } else if (BtorJNI.boolector_is_uf(btor, var)) {
+ assignments.add(getUFAssignment(formula));
+ } else {
+ assignments.add(getConstAssignment(formula));
+ }
+ }
+ }
+ return assignments.build();
+ }
+
+ private ValueAssignment getConstAssignment(long key) {
+ // Boolector does not give back a value "node" (formula), just an assignment string.
+ // We have to wait for the new methods and revisit this method!
+ List