diff options
Diffstat (limited to 'src/api/java/jni')
-rw-r--r-- | src/api/java/jni/api_utilities.cpp (renamed from src/api/java/jni/cvc5JavaApi.cpp) | 2 | ||||
-rw-r--r-- | src/api/java/jni/api_utilities.h (renamed from src/api/java/jni/cvc5JavaApi.h) | 42 | ||||
-rw-r--r-- | src/api/java/jni/datatype.cpp (renamed from src/api/java/jni/cvc5_Datatype.cpp) | 110 | ||||
-rw-r--r-- | src/api/java/jni/datatype_constructor.cpp (renamed from src/api/java/jni/cvc5_DatatypeConstructor.cpp) | 84 | ||||
-rw-r--r-- | src/api/java/jni/datatype_constructor_decl.cpp (renamed from src/api/java/jni/cvc5_DatatypeConstructorDecl.cpp) | 37 | ||||
-rw-r--r-- | src/api/java/jni/datatype_decl.cpp (renamed from src/api/java/jni/cvc5_DatatypeDecl.cpp) | 55 | ||||
-rw-r--r-- | src/api/java/jni/datatype_selector.cpp (renamed from src/api/java/jni/cvc5_DatatypeSelector.cpp) | 53 | ||||
-rw-r--r-- | src/api/java/jni/grammar.cpp (renamed from src/api/java/jni/cvc5_Grammar.cpp) | 68 | ||||
-rw-r--r-- | src/api/java/jni/op.cpp (renamed from src/api/java/jni/cvc5_Op.cpp) | 75 | ||||
-rw-r--r-- | src/api/java/jni/option_Info.cpp (renamed from src/api/java/jni/cvc5_OptionInfo.cpp) | 122 | ||||
-rw-r--r-- | src/api/java/jni/option_info.cpp | 345 | ||||
-rw-r--r-- | src/api/java/jni/result.cpp (renamed from src/api/java/jni/cvc5_Result.cpp) | 89 | ||||
-rw-r--r-- | src/api/java/jni/solver.cpp (renamed from src/api/java/jni/cvc5_Solver.cpp) | 1203 | ||||
-rw-r--r-- | src/api/java/jni/sort.cpp (renamed from src/api/java/jni/cvc5_Sort.cpp) | 489 | ||||
-rw-r--r-- | src/api/java/jni/stat.cpp (renamed from src/api/java/jni/cvc5_Stat.cpp) | 99 | ||||
-rw-r--r-- | src/api/java/jni/statistics.cpp (renamed from src/api/java/jni/cvc5_Statistics.cpp) | 69 | ||||
-rw-r--r-- | src/api/java/jni/term.cpp (renamed from src/api/java/jni/cvc5_Term.cpp) | 410 |
17 files changed, 1777 insertions, 1575 deletions
diff --git a/src/api/java/jni/cvc5JavaApi.cpp b/src/api/java/jni/api_utilities.cpp index 378fa0948..8827b506c 100644 --- a/src/api/java/jni/cvc5JavaApi.cpp +++ b/src/api/java/jni/api_utilities.cpp @@ -13,7 +13,7 @@ * The cvc5 Java API. */ -#include "cvc5JavaApi.h" +#include "api_utilities.h" #include <string> #include <vector> diff --git a/src/api/java/jni/cvc5JavaApi.h b/src/api/java/jni/api_utilities.h index 73f2fb396..08c315e20 100644 --- a/src/api/java/jni/cvc5JavaApi.h +++ b/src/api/java/jni/api_utilities.h @@ -13,8 +13,8 @@ * The cvc5 Java API. */ -#ifndef CVC5__JAVA_API_H -#define CVC5__JAVA_API_H +#ifndef CVC5__API_UTILITIES_H +#define CVC5__API_UTILITIES_H #include <jni.h> @@ -24,23 +24,25 @@ #define CVC5_JAVA_API_TRY_CATCH_BEGIN \ try \ { -#define CVC5_JAVA_API_TRY_CATCH_END(env) \ - } \ - catch (const CVC5ApiOptionException& e) \ - { \ - jclass exceptionClass = env->FindClass("cvc5/CVC5ApiOptionException"); \ - env->ThrowNew(exceptionClass, e.what()); \ - } \ - catch (const CVC5ApiRecoverableException& e) \ - { \ - jclass exceptionClass = \ - env->FindClass("cvc5/CVC5ApiRecoverableException"); \ - env->ThrowNew(exceptionClass, e.what()); \ - } \ - catch (const CVC5ApiException& e) \ - { \ - jclass exceptionClass = env->FindClass("cvc5/CVC5ApiException"); \ - env->ThrowNew(exceptionClass, e.what()); \ +#define CVC5_JAVA_API_TRY_CATCH_END(env) \ + } \ + catch (const CVC5ApiOptionException& e) \ + { \ + jclass exceptionClass = \ + env->FindClass("io/github/cvc5/api/CVC5ApiOptionException"); \ + env->ThrowNew(exceptionClass, e.what()); \ + } \ + catch (const CVC5ApiRecoverableException& e) \ + { \ + jclass exceptionClass = \ + env->FindClass("io/github/cvc5/api/CVC5ApiRecoverableException"); \ + env->ThrowNew(exceptionClass, e.what()); \ + } \ + catch (const CVC5ApiException& e) \ + { \ + jclass exceptionClass = \ + env->FindClass("io/github/cvc5/api/CVC5ApiException"); \ + env->ThrowNew(exceptionClass, e.what()); \ } #define CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, returnValue) \ CVC5_JAVA_API_TRY_CATCH_END(env) \ @@ -137,4 +139,4 @@ jobject getDoubleObject(JNIEnv* env, double value); */ jobject getBooleanObject(JNIEnv* env, bool value); -#endif // CVC5__JAVA_API_H
\ No newline at end of file +#endif // CVC5__API_UTILITIES_H diff --git a/src/api/java/jni/cvc5_Datatype.cpp b/src/api/java/jni/datatype.cpp index eb834da59..5efff9f2c 100644 --- a/src/api/java/jni/cvc5_Datatype.cpp +++ b/src/api/java/jni/datatype.cpp @@ -13,34 +13,30 @@ * The cvc5 Java API. */ -#include "cvc5_Datatype.h" - #include "api/cpp/cvc5.h" -#include "cvc5JavaApi.h" +#include "api_utilities.h" +#include "io_github_cvc5_api_Datatype.h" using namespace cvc5::api; /* - * Class: cvc5_Datatype + * Class: io_github_cvc5_api_Datatype * Method: deletePointer * Signature: (J)V */ -JNIEXPORT void JNICALL Java_cvc5_Datatype_deletePointer(JNIEnv* env, - jclass, - jlong pointer) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Datatype_deletePointer( + JNIEnv* env, jclass, jlong pointer) { delete ((Datatype*)pointer); } /* - * Class: cvc5_Datatype + * Class: io_github_cvc5_api_Datatype * Method: getConstructor * Signature: (JI)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Datatype_getConstructor__JI(JNIEnv* env, - jobject, - jlong pointer, - jint idx) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Datatype_getConstructor__JI( + JNIEnv* env, jobject, jlong pointer, jint idx) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Datatype* current = (Datatype*)pointer; @@ -51,11 +47,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Datatype_getConstructor__JI(JNIEnv* env, } /* - * Class: cvc5_Datatype + * Class: io_github_cvc5_api_Datatype * Method: getConstructor * Signature: (JLjava/lang/String;)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Datatype_getConstructor__JLjava_lang_String_2( +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Datatype_getConstructor__JLjava_lang_String_2( JNIEnv* env, jobject, jlong pointer, jstring jName) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -70,14 +67,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Datatype_getConstructor__JLjava_lang_String_2( } /* - * Class: cvc5_Datatype + * Class: io_github_cvc5_api_Datatype * Method: getConstructorTerm * Signature: (JLjava/lang/String;)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Datatype_getConstructorTerm(JNIEnv* env, - jobject, - jlong pointer, - jstring jName) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Datatype_getConstructorTerm( + JNIEnv* env, jobject, jlong pointer, jstring jName) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Datatype* current = (Datatype*)pointer; @@ -90,13 +85,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Datatype_getConstructorTerm(JNIEnv* env, } /* - * Class: cvc5_Datatype + * Class: io_github_cvc5_api_Datatype * Method: getName * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Datatype_getName(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL +Java_io_github_cvc5_api_Datatype_getName(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Datatype* current = (Datatype*)pointer; @@ -105,13 +99,12 @@ JNIEXPORT jstring JNICALL Java_cvc5_Datatype_getName(JNIEnv* env, } /* - * Class: cvc5_Datatype + * Class: io_github_cvc5_api_Datatype * Method: getNumConstructors * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Datatype_getNumConstructors(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Datatype_getNumConstructors( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Datatype* current = (Datatype*)pointer; @@ -120,13 +113,12 @@ JNIEXPORT jint JNICALL Java_cvc5_Datatype_getNumConstructors(JNIEnv* env, } /* - * Class: cvc5_Datatype + * Class: io_github_cvc5_api_Datatype * Method: isParametric * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isParametric(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Datatype_isParametric( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Datatype* current = (Datatype*)pointer; @@ -135,13 +127,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isParametric(JNIEnv* env, } /* - * Class: cvc5_Datatype + * Class: io_github_cvc5_api_Datatype * Method: isCodatatype * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isCodatatype(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Datatype_isCodatatype( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Datatype* current = (Datatype*)pointer; @@ -150,13 +141,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isCodatatype(JNIEnv* env, } /* - * Class: cvc5_Datatype + * Class: io_github_cvc5_api_Datatype * Method: isTuple * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isTuple(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Datatype_isTuple(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Datatype* current = (Datatype*)pointer; @@ -165,13 +155,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isTuple(JNIEnv* env, } /* - * Class: cvc5_Datatype + * Class: io_github_cvc5_api_Datatype * Method: isRecord * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isRecord(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Datatype_isRecord(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Datatype* current = (Datatype*)pointer; @@ -180,13 +169,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isRecord(JNIEnv* env, } /* - * Class: cvc5_Datatype + * Class: io_github_cvc5_api_Datatype * Method: isFinite * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isFinite(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Datatype_isFinite(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Datatype* current = (Datatype*)pointer; @@ -195,13 +183,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isFinite(JNIEnv* env, } /* - * Class: cvc5_Datatype + * Class: io_github_cvc5_api_Datatype * Method: isWellFounded * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isWellFounded(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Datatype_isWellFounded( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Datatype* current = (Datatype*)pointer; @@ -210,13 +197,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isWellFounded(JNIEnv* env, } /* - * Class: cvc5_Datatype + * Class: io_github_cvc5_api_Datatype * Method: hasNestedRecursion * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_hasNestedRecursion(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Datatype_hasNestedRecursion( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Datatype* current = (Datatype*)pointer; @@ -225,13 +211,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_hasNestedRecursion(JNIEnv* env, } /* - * Class: cvc5_Datatype + * Class: io_github_cvc5_api_Datatype * Method: isNull * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isNull(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Datatype_isNull(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Datatype* current = (Datatype*)pointer; @@ -240,13 +225,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Datatype_isNull(JNIEnv* env, } /* - * Class: cvc5_Datatype + * Class: io_github_cvc5_api_Datatype * Method: toString * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Datatype_toString(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL +Java_io_github_cvc5_api_Datatype_toString(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Datatype* current = (Datatype*)pointer; diff --git a/src/api/java/jni/cvc5_DatatypeConstructor.cpp b/src/api/java/jni/datatype_constructor.cpp index 63aed366d..853766c3c 100644 --- a/src/api/java/jni/cvc5_DatatypeConstructor.cpp +++ b/src/api/java/jni/datatype_constructor.cpp @@ -13,32 +13,32 @@ * The cvc5 Java API. */ -#include "cvc5_DatatypeConstructor.h" - #include "api/cpp/cvc5.h" -#include "cvc5JavaApi.h" +#include "api_utilities.h" +#include "io_github_cvc5_api_DatatypeConstructor.h" using namespace cvc5::api; /* - * Class: cvc5_DatatypeConstructor + * Class: io_github_cvc5_api_DatatypeConstructor * Method: deletePointer * Signature: (J)V */ JNIEXPORT void JNICALL -Java_cvc5_DatatypeConstructor_deletePointer(JNIEnv*, jclass, jlong pointer) +Java_io_github_cvc5_api_DatatypeConstructor_deletePointer(JNIEnv*, + jclass, + jlong pointer) { delete ((DatatypeConstructor*)pointer); } /* - * Class: cvc5_DatatypeConstructor + * Class: io_github_cvc5_api_DatatypeConstructor * Method: getName * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_DatatypeConstructor_getName(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_DatatypeConstructor_getName( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeConstructor* current = (DatatypeConstructor*)pointer; @@ -47,12 +47,14 @@ JNIEXPORT jstring JNICALL Java_cvc5_DatatypeConstructor_getName(JNIEnv* env, } /* - * Class: cvc5_DatatypeConstructor + * Class: io_github_cvc5_api_DatatypeConstructor * Method: getConstructorTerm * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_DatatypeConstructor_getConstructorTerm( - JNIEnv* env, jobject, jlong pointer) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_DatatypeConstructor_getConstructorTerm(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeConstructor* current = (DatatypeConstructor*)pointer; @@ -62,12 +64,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_DatatypeConstructor_getConstructorTerm( } /* - * Class: cvc5_DatatypeConstructor + * Class: io_github_cvc5_api_DatatypeConstructor * Method: getSpecializedConstructorTerm * Signature: (JJ)J */ JNIEXPORT jlong JNICALL -Java_cvc5_DatatypeConstructor_getSpecializedConstructorTerm( +Java_io_github_cvc5_api_DatatypeConstructor_getSpecializedConstructorTerm( JNIEnv* env, jobject, jlong pointer, jlong retSortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -79,12 +81,14 @@ Java_cvc5_DatatypeConstructor_getSpecializedConstructorTerm( } /* - * Class: cvc5_DatatypeConstructor + * Class: io_github_cvc5_api_DatatypeConstructor * Method: getTesterTerm * Signature: (J)J */ JNIEXPORT jlong JNICALL -Java_cvc5_DatatypeConstructor_getTesterTerm(JNIEnv* env, jobject, jlong pointer) +Java_io_github_cvc5_api_DatatypeConstructor_getTesterTerm(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeConstructor* current = (DatatypeConstructor*)pointer; @@ -94,12 +98,14 @@ Java_cvc5_DatatypeConstructor_getTesterTerm(JNIEnv* env, jobject, jlong pointer) } /* - * Class: cvc5_DatatypeConstructor + * Class: io_github_cvc5_api_DatatypeConstructor * Method: getNumSelectors * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_DatatypeConstructor_getNumSelectors( - JNIEnv* env, jobject, jlong pointer) +JNIEXPORT jint JNICALL +Java_io_github_cvc5_api_DatatypeConstructor_getNumSelectors(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeConstructor* current = (DatatypeConstructor*)pointer; @@ -108,12 +114,15 @@ JNIEXPORT jint JNICALL Java_cvc5_DatatypeConstructor_getNumSelectors( } /* - * Class: cvc5_DatatypeConstructor + * Class: io_github_cvc5_api_DatatypeConstructor * Method: getSelector * Signature: (JI)J */ -JNIEXPORT jlong JNICALL Java_cvc5_DatatypeConstructor_getSelector__JI( - JNIEnv* env, jobject, jlong pointer, jint index) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_DatatypeConstructor_getSelector__JI(JNIEnv* env, + jobject, + jlong pointer, + jint index) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeConstructor* current = (DatatypeConstructor*)pointer; @@ -124,15 +133,13 @@ JNIEXPORT jlong JNICALL Java_cvc5_DatatypeConstructor_getSelector__JI( } /* - * Class: cvc5_DatatypeConstructor + * Class: io_github_cvc5_api_DatatypeConstructor * Method: getSelector * Signature: (JLjava/lang/String;)J */ JNIEXPORT jlong JNICALL -Java_cvc5_DatatypeConstructor_getSelector__JLjava_lang_String_2(JNIEnv* env, - jobject, - jlong pointer, - jstring jName) +Java_io_github_cvc5_api_DatatypeConstructor_getSelector__JLjava_lang_String_2( + JNIEnv* env, jobject, jlong pointer, jstring jName) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeConstructor* current = (DatatypeConstructor*)pointer; @@ -146,12 +153,15 @@ Java_cvc5_DatatypeConstructor_getSelector__JLjava_lang_String_2(JNIEnv* env, } /* - * Class: cvc5_DatatypeConstructor + * Class: io_github_cvc5_api_DatatypeConstructor * Method: getSelectorTerm * Signature: (JLjava/lang/String;)J */ -JNIEXPORT jlong JNICALL Java_cvc5_DatatypeConstructor_getSelectorTerm( - JNIEnv* env, jobject, jlong pointer, jstring jName) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_DatatypeConstructor_getSelectorTerm(JNIEnv* env, + jobject, + jlong pointer, + jstring jName) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeConstructor* current = (DatatypeConstructor*)pointer; @@ -164,13 +174,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_DatatypeConstructor_getSelectorTerm( } /* - * Class: cvc5_DatatypeConstructor + * Class: io_github_cvc5_api_DatatypeConstructor * Method: isNull * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_DatatypeConstructor_isNull(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_DatatypeConstructor_isNull( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeConstructor* current = (DatatypeConstructor*)pointer; @@ -179,13 +188,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_DatatypeConstructor_isNull(JNIEnv* env, } /* - * Class: cvc5_DatatypeConstructor + * Class: io_github_cvc5_api_DatatypeConstructor * Method: toString * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_DatatypeConstructor_toString(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_DatatypeConstructor_toString( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeConstructor* current = (DatatypeConstructor*)pointer; diff --git a/src/api/java/jni/cvc5_DatatypeConstructorDecl.cpp b/src/api/java/jni/datatype_constructor_decl.cpp index ce3c69585..b13b75e45 100644 --- a/src/api/java/jni/cvc5_DatatypeConstructorDecl.cpp +++ b/src/api/java/jni/datatype_constructor_decl.cpp @@ -13,30 +13,32 @@ * The cvc5 Java API. */ -#include "cvc5_DatatypeConstructorDecl.h" - #include "api/cpp/cvc5.h" -#include "cvc5JavaApi.h" +#include "api_utilities.h" +#include "io_github_cvc5_api_DatatypeConstructorDecl.h" using namespace cvc5::api; /* - * Class: cvc5_DatatypeConstructorDecl + * Class: io_github_cvc5_api_DatatypeConstructorDecl * Method: deletePointer * Signature: (J)V */ JNIEXPORT void JNICALL -Java_cvc5_DatatypeConstructorDecl_deletePointer(JNIEnv*, jclass, jlong pointer) +Java_io_github_cvc5_api_DatatypeConstructorDecl_deletePointer(JNIEnv*, + jclass, + jlong pointer) { delete ((DatatypeConstructorDecl*)pointer); } /* - * Class: cvc5_DatatypeConstructorDecl + * Class: io_github_cvc5_api_DatatypeConstructorDecl * Method: addSelector * Signature: (JLjava/lang/String;J)V */ -JNIEXPORT void JNICALL Java_cvc5_DatatypeConstructorDecl_addSelector( +JNIEXPORT void JNICALL +Java_io_github_cvc5_api_DatatypeConstructorDecl_addSelector( JNIEnv* env, jobject, jlong pointer, jstring jName, jlong sortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -50,12 +52,15 @@ JNIEXPORT void JNICALL Java_cvc5_DatatypeConstructorDecl_addSelector( } /* - * Class: cvc5_DatatypeConstructorDecl + * Class: io_github_cvc5_api_DatatypeConstructorDecl * Method: addSelectorSelf * Signature: (JLjava/lang/String;)V */ -JNIEXPORT void JNICALL Java_cvc5_DatatypeConstructorDecl_addSelectorSelf( - JNIEnv* env, jobject, jlong pointer, jstring jName) +JNIEXPORT void JNICALL +Java_io_github_cvc5_api_DatatypeConstructorDecl_addSelectorSelf(JNIEnv* env, + jobject, + jlong pointer, + jstring jName) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeConstructorDecl* current = (DatatypeConstructorDecl*)pointer; @@ -67,12 +72,14 @@ JNIEXPORT void JNICALL Java_cvc5_DatatypeConstructorDecl_addSelectorSelf( } /* - * Class: cvc5_DatatypeConstructorDecl + * Class: io_github_cvc5_api_DatatypeConstructorDecl * Method: isNull * Signature: (J)Z */ JNIEXPORT jboolean JNICALL -Java_cvc5_DatatypeConstructorDecl_isNull(JNIEnv* env, jobject, jlong pointer) +Java_io_github_cvc5_api_DatatypeConstructorDecl_isNull(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeConstructorDecl* current = (DatatypeConstructorDecl*)pointer; @@ -81,12 +88,14 @@ Java_cvc5_DatatypeConstructorDecl_isNull(JNIEnv* env, jobject, jlong pointer) } /* - * Class: cvc5_DatatypeConstructorDecl + * Class: io_github_cvc5_api_DatatypeConstructorDecl * Method: toString * Signature: (J)Ljava/lang/String; */ JNIEXPORT jstring JNICALL -Java_cvc5_DatatypeConstructorDecl_toString(JNIEnv* env, jobject, jlong pointer) +Java_io_github_cvc5_api_DatatypeConstructorDecl_toString(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeConstructorDecl* current = (DatatypeConstructorDecl*)pointer; diff --git a/src/api/java/jni/cvc5_DatatypeDecl.cpp b/src/api/java/jni/datatype_decl.cpp index b68c37842..845afac9d 100644 --- a/src/api/java/jni/cvc5_DatatypeDecl.cpp +++ b/src/api/java/jni/datatype_decl.cpp @@ -13,34 +13,30 @@ * The cvc5 Java API. */ -#include "cvc5_DatatypeDecl.h" - #include "api/cpp/cvc5.h" -#include "cvc5JavaApi.h" +#include "api_utilities.h" +#include "io_github_cvc5_api_DatatypeDecl.h" using namespace cvc5::api; /* - * Class: cvc5_DatatypeDecl + * Class: io_github_cvc5_api_DatatypeDecl * Method: deletePointer * Signature: (J)V */ -JNIEXPORT void JNICALL Java_cvc5_DatatypeDecl_deletePointer(JNIEnv*, - jclass, - jlong pointer) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_DatatypeDecl_deletePointer( + JNIEnv*, jclass, jlong pointer) { delete ((DatatypeDecl*)pointer); } /* - * Class: cvc5_DatatypeDecl + * Class: io_github_cvc5_api_DatatypeDecl * Method: addConstructor * Signature: (JJ)V */ -JNIEXPORT void JNICALL Java_cvc5_DatatypeDecl_addConstructor(JNIEnv* env, - jobject, - jlong pointer, - jlong declPointer) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_DatatypeDecl_addConstructor( + JNIEnv* env, jobject, jlong pointer, jlong declPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeDecl* current = (DatatypeDecl*)pointer; @@ -50,13 +46,12 @@ JNIEXPORT void JNICALL Java_cvc5_DatatypeDecl_addConstructor(JNIEnv* env, } /* - * Class: cvc5_DatatypeDecl + * Class: io_github_cvc5_api_DatatypeDecl * Method: getNumConstructors * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_DatatypeDecl_getNumConstructors(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL Java_io_github_cvc5_api_DatatypeDecl_getNumConstructors( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeDecl* current = (DatatypeDecl*)pointer; @@ -65,13 +60,12 @@ JNIEXPORT jint JNICALL Java_cvc5_DatatypeDecl_getNumConstructors(JNIEnv* env, } /* - * Class: cvc5_DatatypeDecl + * Class: io_github_cvc5_api_DatatypeDecl * Method: isParametric * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_DatatypeDecl_isParametric(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_DatatypeDecl_isParametric( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeDecl* current = (DatatypeDecl*)pointer; @@ -80,13 +74,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_DatatypeDecl_isParametric(JNIEnv* env, } /* - * Class: cvc5_DatatypeDecl + * Class: io_github_cvc5_api_DatatypeDecl * Method: isNull * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_DatatypeDecl_isNull(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_DatatypeDecl_isNull(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeDecl* current = (DatatypeDecl*)pointer; @@ -95,13 +88,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_DatatypeDecl_isNull(JNIEnv* env, } /* - * Class: cvc5_DatatypeDecl + * Class: io_github_cvc5_api_DatatypeDecl * Method: toString * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_DatatypeDecl_toString(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_DatatypeDecl_toString( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeDecl* current = (DatatypeDecl*)pointer; @@ -110,13 +102,12 @@ JNIEXPORT jstring JNICALL Java_cvc5_DatatypeDecl_toString(JNIEnv* env, } /* - * Class: cvc5_DatatypeDecl + * Class: io_github_cvc5_api_DatatypeDecl * Method: getName * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_DatatypeDecl_getName(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_DatatypeDecl_getName( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeDecl* current = (DatatypeDecl*)pointer; diff --git a/src/api/java/jni/cvc5_DatatypeSelector.cpp b/src/api/java/jni/datatype_selector.cpp index fee0b33a4..964eb24f5 100644 --- a/src/api/java/jni/cvc5_DatatypeSelector.cpp +++ b/src/api/java/jni/datatype_selector.cpp @@ -13,33 +13,30 @@ * The cvc5 Java API. */ -#include "cvc5_DatatypeSelector.h" - #include "api/cpp/cvc5.h" -#include "cvc5JavaApi.h" +#include "api_utilities.h" +#include "io_github_cvc5_api_DatatypeSelector.h" using namespace cvc5::api; /* - * Class: cvc5_DatatypeSelector + * Class: io_github_cvc5_api_DatatypeSelector * Method: deletePointer * Signature: (J)V */ -JNIEXPORT void JNICALL Java_cvc5_DatatypeSelector_deletePointer(JNIEnv*, - jclass, - jlong pointer) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_DatatypeSelector_deletePointer( + JNIEnv*, jclass, jlong pointer) { delete ((DatatypeSelector*)pointer); } /* - * Class: cvc5_DatatypeSelector + * Class: io_github_cvc5_api_DatatypeSelector * Method: getName * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_DatatypeSelector_getName(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_DatatypeSelector_getName( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeSelector* current = (DatatypeSelector*)pointer; @@ -48,12 +45,14 @@ JNIEXPORT jstring JNICALL Java_cvc5_DatatypeSelector_getName(JNIEnv* env, } /* - * Class: cvc5_DatatypeSelector + * Class: io_github_cvc5_api_DatatypeSelector * Method: getSelectorTerm * Signature: (J)J */ JNIEXPORT jlong JNICALL -Java_cvc5_DatatypeSelector_getSelectorTerm(JNIEnv* env, jobject, jlong pointer) +Java_io_github_cvc5_api_DatatypeSelector_getSelectorTerm(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeSelector* current = (DatatypeSelector*)pointer; @@ -63,13 +62,12 @@ Java_cvc5_DatatypeSelector_getSelectorTerm(JNIEnv* env, jobject, jlong pointer) } /* - * Class: cvc5_DatatypeSelector + * Class: io_github_cvc5_api_DatatypeSelector * Method: getUpdaterTerm * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_DatatypeSelector_getUpdaterTerm(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_DatatypeSelector_getUpdaterTerm( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeSelector* current = (DatatypeSelector*)pointer; @@ -79,13 +77,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_DatatypeSelector_getUpdaterTerm(JNIEnv* env, } /* - * Class: cvc5_DatatypeSelector + * Class: io_github_cvc5_api_DatatypeSelector * Method: getRangeSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_DatatypeSelector_getRangeSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_DatatypeSelector_getRangeSort( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeSelector* current = (DatatypeSelector*)pointer; @@ -95,13 +92,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_DatatypeSelector_getRangeSort(JNIEnv* env, } /* - * Class: cvc5_DatatypeSelector + * Class: io_github_cvc5_api_DatatypeSelector * Method: isNull * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_DatatypeSelector_isNull(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_DatatypeSelector_isNull( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeSelector* current = (DatatypeSelector*)pointer; @@ -110,13 +106,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_DatatypeSelector_isNull(JNIEnv* env, } /* - * Class: cvc5_DatatypeSelector + * Class: io_github_cvc5_api_DatatypeSelector * Method: toString * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_DatatypeSelector_toString(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_DatatypeSelector_toString( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeSelector* current = (DatatypeSelector*)pointer; diff --git a/src/api/java/jni/cvc5_Grammar.cpp b/src/api/java/jni/grammar.cpp index 1ca9ea701..4bafd54d6 100644 --- a/src/api/java/jni/cvc5_Grammar.cpp +++ b/src/api/java/jni/grammar.cpp @@ -13,21 +13,19 @@ * The cvc5 Java API. */ -#include "cvc5_Grammar.h" - #include "api/cpp/cvc5.h" -#include "cvc5JavaApi.h" +#include "api_utilities.h" +#include "io_github_cvc5_api_Grammar.h" using namespace cvc5::api; /* - * Class: cvc5_Grammar + * Class: io_github_cvc5_api_Grammar * Method: copyGrammar * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Grammar_copyGrammar(JNIEnv* env, - jclass, - jlong pointer) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Grammar_copyGrammar(JNIEnv* env, jclass, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Grammar* current = reinterpret_cast<Grammar*>(pointer); @@ -37,27 +35,27 @@ JNIEXPORT jlong JNICALL Java_cvc5_Grammar_copyGrammar(JNIEnv* env, } /* - * Class: cvc5_Grammar + * Class: io_github_cvc5_api_Grammar * Method: deletePointer * Signature: (J)V */ -JNIEXPORT void JNICALL Java_cvc5_Grammar_deletePointer(JNIEnv*, - jclass, - jlong pointer) +JNIEXPORT void JNICALL +Java_io_github_cvc5_api_Grammar_deletePointer(JNIEnv*, jclass, jlong pointer) { delete reinterpret_cast<Grammar*>(pointer); } /* - * Class: cvc5_Grammar + * Class: io_github_cvc5_api_Grammar * Method: addRule * Signature: (JJJ)V */ -JNIEXPORT void JNICALL Java_cvc5_Grammar_addRule(JNIEnv* env, - jobject, - jlong pointer, - jlong ntSymbolPointer, - jlong rulePointer) +JNIEXPORT void JNICALL +Java_io_github_cvc5_api_Grammar_addRule(JNIEnv* env, + jobject, + jlong pointer, + jlong ntSymbolPointer, + jlong rulePointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Grammar* current = reinterpret_cast<Grammar*>(pointer); @@ -68,15 +66,16 @@ JNIEXPORT void JNICALL Java_cvc5_Grammar_addRule(JNIEnv* env, } /* - * Class: cvc5_Grammar + * Class: io_github_cvc5_api_Grammar * Method: addRules * Signature: (JJ[J)V */ -JNIEXPORT void JNICALL Java_cvc5_Grammar_addRules(JNIEnv* env, - jobject, - jlong pointer, - jlong ntSymbolPointer, - jlongArray rulePointers) +JNIEXPORT void JNICALL +Java_io_github_cvc5_api_Grammar_addRules(JNIEnv* env, + jobject, + jlong pointer, + jlong ntSymbolPointer, + jlongArray rulePointers) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Grammar* current = reinterpret_cast<Grammar*>(pointer); @@ -87,14 +86,12 @@ JNIEXPORT void JNICALL Java_cvc5_Grammar_addRules(JNIEnv* env, } /* - * Class: cvc5_Grammar + * Class: io_github_cvc5_api_Grammar * Method: addAnyConstant * Signature: (JJ)V */ -JNIEXPORT void JNICALL Java_cvc5_Grammar_addAnyConstant(JNIEnv* env, - jobject, - jlong pointer, - jlong ntSymbolPointer) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Grammar_addAnyConstant( + JNIEnv* env, jobject, jlong pointer, jlong ntSymbolPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Grammar* current = reinterpret_cast<Grammar*>(pointer); @@ -104,14 +101,12 @@ JNIEXPORT void JNICALL Java_cvc5_Grammar_addAnyConstant(JNIEnv* env, } /* - * Class: cvc5_Grammar + * Class: io_github_cvc5_api_Grammar * Method: addAnyVariable * Signature: (JJ)V */ -JNIEXPORT void JNICALL Java_cvc5_Grammar_addAnyVariable(JNIEnv* env, - jobject, - jlong pointer, - jlong ntSymbolPointer) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Grammar_addAnyVariable( + JNIEnv* env, jobject, jlong pointer, jlong ntSymbolPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Grammar* current = reinterpret_cast<Grammar*>(pointer); @@ -121,13 +116,12 @@ JNIEXPORT void JNICALL Java_cvc5_Grammar_addAnyVariable(JNIEnv* env, } /* - * Class: cvc5_Grammar + * Class: io_github_cvc5_api_Grammar * Method: toString * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Grammar_toString(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL +Java_io_github_cvc5_api_Grammar_toString(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Grammar* current = reinterpret_cast<Grammar*>(pointer); diff --git a/src/api/java/jni/cvc5_Op.cpp b/src/api/java/jni/op.cpp index 5c2a00657..cb6a7a728 100644 --- a/src/api/java/jni/cvc5_Op.cpp +++ b/src/api/java/jni/op.cpp @@ -13,34 +13,33 @@ * The cvc5 Java API. */ -#include "cvc5_Op.h" - #include "api/cpp/cvc5.h" -#include "cvc5JavaApi.h" +#include "api_utilities.h" +#include "io_github_cvc5_api_Op.h" using namespace cvc5::api; /* - * Class: cvc5_Op + * Class: io_github_cvc5_api_Op * Method: deletePointer * Signature: (J)V */ -JNIEXPORT void JNICALL Java_cvc5_Op_deletePointer(JNIEnv*, - jclass, - jlong pointer) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Op_deletePointer(JNIEnv*, + jclass, + jlong pointer) { delete reinterpret_cast<Op*>(pointer); } /* - * Class: cvc5_Op + * Class: io_github_cvc5_api_Op * Method: equals * Signature: (JJ)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Op_equals(JNIEnv* env, - jobject, - jlong pointer1, - jlong pointer2) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Op_equals(JNIEnv* env, + jobject, + jlong pointer1, + jlong pointer2) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Op* op1 = reinterpret_cast<Op*>(pointer1); @@ -51,11 +50,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Op_equals(JNIEnv* env, } /* - * Class: cvc5_Op + * Class: io_github_cvc5_api_Op * Method: getKind * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Op_getKind(JNIEnv* env, jobject, jlong pointer) +JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Op_getKind(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Op* current = reinterpret_cast<Op*>(pointer); @@ -64,13 +65,13 @@ JNIEXPORT jint JNICALL Java_cvc5_Op_getKind(JNIEnv* env, jobject, jlong pointer) } /* - * Class: cvc5_Op + * Class: io_github_cvc5_api_Op * Method: isNull * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Op_isNull(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Op_isNull(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Op* current = reinterpret_cast<Op*>(pointer); @@ -79,13 +80,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Op_isNull(JNIEnv* env, } /* - * Class: cvc5_Op + * Class: io_github_cvc5_api_Op * Method: isIndexed * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Op_isIndexed(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Op_isIndexed(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Op* current = reinterpret_cast<Op*>(pointer); @@ -94,13 +95,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Op_isIndexed(JNIEnv* env, } /* - * Class: cvc5_Op + * Class: io_github_cvc5_api_Op * Method: getNumIndices * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Op_getNumIndices(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Op_getNumIndices(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Op* current = reinterpret_cast<Op*>(pointer); @@ -109,13 +110,12 @@ JNIEXPORT jint JNICALL Java_cvc5_Op_getNumIndices(JNIEnv* env, } /* - * Class: cvc5_Op + * Class: io_github_cvc5_api_Op * Method: getIntegerIndices * Signature: (J)[I */ -JNIEXPORT jintArray JNICALL Java_cvc5_Op_getIntegerIndices(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jintArray JNICALL Java_io_github_cvc5_api_Op_getIntegerIndices( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Op* current = reinterpret_cast<Op*>(pointer); @@ -148,13 +148,12 @@ JNIEXPORT jintArray JNICALL Java_cvc5_Op_getIntegerIndices(JNIEnv* env, } /* - * Class: cvc5_Op + * Class: io_github_cvc5_api_Op * Method: getStringIndices * Signature: (J)[Ljava/lang/String; */ -JNIEXPORT jobjectArray JNICALL Java_cvc5_Op_getStringIndices(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jobjectArray JNICALL +Java_io_github_cvc5_api_Op_getStringIndices(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Op* current = reinterpret_cast<Op*>(pointer); @@ -185,13 +184,13 @@ JNIEXPORT jobjectArray JNICALL Java_cvc5_Op_getStringIndices(JNIEnv* env, } /* - * Class: cvc5_Op + * Class: io_github_cvc5_api_Op * Method: toString * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Op_toString(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Op_toString(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Op* current = reinterpret_cast<Op*>(pointer); diff --git a/src/api/java/jni/cvc5_OptionInfo.cpp b/src/api/java/jni/option_Info.cpp index c4bcc2e04..4c6025357 100644 --- a/src/api/java/jni/cvc5_OptionInfo.cpp +++ b/src/api/java/jni/option_Info.cpp @@ -13,33 +13,30 @@ * The cvc5 Java API. */ -#include "cvc5_OptionInfo.h" - #include "api/cpp/cvc5.h" -#include "cvc5JavaApi.h" +#include "api_utilities.h" +#include "io_github_cvc5_api_OptionInfo.h" using namespace cvc5::api; /* - * Class: cvc5_OptionInfo + * Class: io_github_cvc5_api_OptionInfo * Method: deletePointer * Signature: (J)V */ -JNIEXPORT void JNICALL Java_cvc5_OptionInfo_deletePointer(JNIEnv*, - jclass, - jlong pointer) +JNIEXPORT void JNICALL +Java_io_github_cvc5_api_OptionInfo_deletePointer(JNIEnv*, jclass, jlong pointer) { delete reinterpret_cast<OptionInfo*>(pointer); } /* - * Class: cvc5_OptionInfo + * Class: io_github_cvc5_api_OptionInfo * Method: toString * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_OptionInfo_toString(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL +Java_io_github_cvc5_api_OptionInfo_toString(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer); @@ -50,13 +47,12 @@ JNIEXPORT jstring JNICALL Java_cvc5_OptionInfo_toString(JNIEnv* env, } /* - * Class: cvc5_OptionInfo + * Class: io_github_cvc5_api_OptionInfo * Method: getName * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_OptionInfo_getName(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL +Java_io_github_cvc5_api_OptionInfo_getName(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer); @@ -65,13 +61,12 @@ JNIEXPORT jstring JNICALL Java_cvc5_OptionInfo_getName(JNIEnv* env, } /* - * Class: cvc5_OptionInfo + * Class: io_github_cvc5_api_OptionInfo * Method: getAliases * Signature: (J)[Ljava/lang/String; */ -JNIEXPORT jobjectArray JNICALL Java_cvc5_OptionInfo_getAliases(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jobjectArray JNICALL Java_io_github_cvc5_api_OptionInfo_getAliases( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer); @@ -81,13 +76,12 @@ JNIEXPORT jobjectArray JNICALL Java_cvc5_OptionInfo_getAliases(JNIEnv* env, } /* - * Class: cvc5_OptionInfo + * Class: io_github_cvc5_api_OptionInfo * Method: getSetByUser * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_OptionInfo_getSetByUser(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_OptionInfo_getSetByUser( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer); @@ -151,13 +145,12 @@ jobject getNumberInfoFromInteger(JNIEnv* env, const OptionInfo::NumberInfo<uint64_t>& info); /* - * Class: cvc5_OptionInfo + * Class: io_github_cvc5_api_OptionInfo * Method: getBaseInfo - * Signature: (J)Lcvc5/BaseInfo; + * Signature: (J)Lio/github/cvc5/api/BaseInfo; */ -JNIEXPORT jobject JNICALL Java_cvc5_OptionInfo_getBaseInfo(JNIEnv* env, - jobject optionInfo, - jlong pointer) +JNIEXPORT jobject JNICALL Java_io_github_cvc5_api_OptionInfo_getBaseInfo( + JNIEnv* env, jobject optionInfo, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer); @@ -172,9 +165,10 @@ JNIEXPORT jobject JNICALL Java_cvc5_OptionInfo_getBaseInfo(JNIEnv* env, if (std::holds_alternative<OptionInfo::VoidInfo>(v)) { - jclass voidInfoClass = env->FindClass("cvc5/OptionInfo$VoidInfo"); - jmethodID methodId = - env->GetMethodID(voidInfoClass, "<init>", "(Lcvc5/OptionInfo;)V"); + jclass voidInfoClass = + env->FindClass("io/github/cvc5/api/OptionInfo$VoidInfo"); + jmethodID methodId = env->GetMethodID( + voidInfoClass, "<init>", "(Lio/github/cvc5/api/OptionInfo;)V"); jobject ret = env->NewObject(voidInfoClass, methodId, optionInfo); return ret; } @@ -182,11 +176,13 @@ JNIEXPORT jobject JNICALL Java_cvc5_OptionInfo_getBaseInfo(JNIEnv* env, if (std::holds_alternative<OptionInfo::ValueInfo<bool>>(v) || std::holds_alternative<OptionInfo::ValueInfo<std::string>>(v)) { - jclass valueInfoClass = env->FindClass("cvc5/OptionInfo$ValueInfo"); - jmethodID methodId = env->GetMethodID( - valueInfoClass, - "<init>", - "(Lcvc5/OptionInfo;Ljava/lang/Object;Ljava/lang/Object;)V"); + jclass valueInfoClass = + env->FindClass("io/github/cvc5/api/OptionInfo$ValueInfo"); + jmethodID methodId = + env->GetMethodID(valueInfoClass, + "<init>", + "(Lio/github/cvc5/api/OptionInfo;Ljava/lang/" + "Object;Ljava/lang/Object;)V"); if (std::holds_alternative<OptionInfo::ValueInfo<bool>>(v)) { @@ -213,12 +209,13 @@ JNIEXPORT jobject JNICALL Java_cvc5_OptionInfo_getBaseInfo(JNIEnv* env, || std::holds_alternative<OptionInfo::NumberInfo<uint64_t>>(v) || std::holds_alternative<OptionInfo::NumberInfo<double>>(v)) { - jclass numberInfoClass = env->FindClass("cvc5/OptionInfo$NumberInfo"); - jmethodID methodId = - env->GetMethodID(numberInfoClass, - "<init>", - "(Lcvc5/OptionInfo;Ljava/lang/Object;Ljava/lang/" - "Object;Ljava/lang/Object;Ljava/lang/Object;)V"); + jclass numberInfoClass = + env->FindClass("io/github/cvc5/api/OptionInfo$NumberInfo"); + jmethodID methodId = env->GetMethodID( + numberInfoClass, + "<init>", + "(Lio/github/cvc5/api/OptionInfo;Ljava/lang/Object;Ljava/lang/" + "Object;Ljava/lang/Object;Ljava/lang/Object;)V"); if (std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(v)) { @@ -262,12 +259,13 @@ JNIEXPORT jobject JNICALL Java_cvc5_OptionInfo_getBaseInfo(JNIEnv* env, if (std::holds_alternative<OptionInfo::ModeInfo>(v)) { - jclass modeInfoClass = env->FindClass("cvc5/OptionInfo$ModeInfo"); - jmethodID methodId = - env->GetMethodID(modeInfoClass, - "<init>", - "(Lcvc5/OptionInfo;Ljava/lang/String;Ljava/lang/" - "String;[Ljava/lang/String;)V"); + jclass modeInfoClass = + env->FindClass("io/github/cvc5/api/OptionInfo$ModeInfo"); + jmethodID methodId = env->GetMethodID( + modeInfoClass, + "<init>", + "(Lio/github/cvc5/api/OptionInfo;Ljava/lang/String;Ljava/lang/" + "String;[Ljava/lang/String;)V"); auto info = std::get<OptionInfo::ModeInfo>(v); jstring defaultValue = env->NewStringUTF(info.defaultValue.c_str()); @@ -287,13 +285,12 @@ JNIEXPORT jobject JNICALL Java_cvc5_OptionInfo_getBaseInfo(JNIEnv* env, } /* - * Class: cvc5_OptionInfo + * Class: io_github_cvc5_api_OptionInfo * Method: booleanValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_OptionInfo_booleanValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_OptionInfo_booleanValue( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer); @@ -302,13 +299,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_OptionInfo_booleanValue(JNIEnv* env, } /* - * Class: cvc5_OptionInfo + * Class: io_github_cvc5_api_OptionInfo * Method: stringValue * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_OptionInfo_stringValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_OptionInfo_stringValue( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer); @@ -318,13 +314,12 @@ JNIEXPORT jstring JNICALL Java_cvc5_OptionInfo_stringValue(JNIEnv* env, } /* - * Class: cvc5_OptionInfo + * Class: io_github_cvc5_api_OptionInfo * Method: intValue * Signature: (J)Ljava/math/BigInteger; */ -JNIEXPORT jobject JNICALL Java_cvc5_OptionInfo_intValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jobject JNICALL +Java_io_github_cvc5_api_OptionInfo_intValue(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer); @@ -335,13 +330,12 @@ JNIEXPORT jobject JNICALL Java_cvc5_OptionInfo_intValue(JNIEnv* env, } /* - * Class: cvc5_OptionInfo + * Class: io_github_cvc5_api_OptionInfo * Method: doubleValue * Signature: (J)D */ -JNIEXPORT jdouble JNICALL Java_cvc5_OptionInfo_doubleValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jdouble JNICALL Java_io_github_cvc5_api_OptionInfo_doubleValue( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer); diff --git a/src/api/java/jni/option_info.cpp b/src/api/java/jni/option_info.cpp new file mode 100644 index 000000000..031b1bae9 --- /dev/null +++ b/src/api/java/jni/option_info.cpp @@ -0,0 +1,345 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The cvc5 Java API. + */ + +#include "api/cpp/cvc5.h" +#include "api_utilities.h" +#include "io_github_cvc5_api_OptionInfo.h" + +using namespace cvc5::api; + +/* + * Class: io_github_cvc5_api_OptionInfo + * Method: deletePointer + * Signature: (J)V + */ +JNIEXPORT void JNICALL +Java_io_github_cvc5_api_OptionInfo_deletePointer(JNIEnv*, jclass, jlong pointer) +{ + delete reinterpret_cast<OptionInfo*>(pointer); +} + +/* + * Class: io_github_cvc5_api_OptionInfo + * Method: toString + * Signature: (J)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL +Java_io_github_cvc5_api_OptionInfo_toString(JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer); + std::stringstream ss; + ss << *current; + return env->NewStringUTF(ss.str().c_str()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: io_github_cvc5_api_OptionInfo + * Method: getName + * Signature: (J)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL +Java_io_github_cvc5_api_OptionInfo_getName(JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer); + return env->NewStringUTF(current->name.c_str()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: io_github_cvc5_api_OptionInfo + * Method: getAliases + * Signature: (J)[Ljava/lang/String; + */ +JNIEXPORT jobjectArray JNICALL Java_io_github_cvc5_api_OptionInfo_getAliases( + JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer); + jobjectArray ret = getStringArrayFromStringVector(env, current->aliases); + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: io_github_cvc5_api_OptionInfo + * Method: getSetByUser + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_OptionInfo_getSetByUser( + JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer); + return static_cast<jboolean>(current->setByUser); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false)); +} + +/** + * Convert OptionInfo::NumberInfo cpp object to OptionInfo.NumberInfo java + * object + * @tparam T cpp integer types int64_t, uint64_t, etc + * @param env jni environment + * @param optionInfo a java object for this OptionInfo + * @param numberInfoClass the java class for OptionInfo.NumberInfo + * @param methodId a constructor for OptionInfo.NumberInfo + * @param info the cpp OptionInfo::NumberInfo object + * @return a java object of class OptionInfo.NumberInfo<BigInteger> + */ +template <typename T> +jobject getNumberInfoFromInteger(JNIEnv* env, + const _jobject* optionInfo, + jclass numberInfoClass, + jmethodID methodId, + const OptionInfo::NumberInfo<T>& info) +{ + jobject defaultValue = getBigIntegerObject<T>(env, info.defaultValue); + jobject currentValue = getBigIntegerObject<T>(env, info.currentValue); + jobject minimum = nullptr; + if (info.minimum) + { + minimum = getBigIntegerObject<T>(env, *info.minimum); + } + jobject maximum = nullptr; + if (info.maximum) + { + maximum = getBigIntegerObject<T>(env, *info.maximum); + } + jobject ret = env->NewObject(numberInfoClass, + methodId, + optionInfo, + defaultValue, + currentValue, + minimum, + maximum); + + return ret; +} + +template <typename T> +jobject getNumberInfoFromInteger(JNIEnv* env, + const _jobject* optionInfo, + jclass numberInfoClass, + jmethodID methodId, + const OptionInfo::NumberInfo<int64_t>& info); + +template <typename T> +jobject getNumberInfoFromInteger(JNIEnv* env, + const _jobject* optionInfo, + jclass numberInfoClass, + jmethodID methodId, + const OptionInfo::NumberInfo<uint64_t>& info); + +/* + * Class: io_github_cvc5_api_OptionInfo + * Method: getBaseInfo + * Signature: (J)Lio/github/cvc5/api/OptionInfo/BaseInfo; + */ +JNIEXPORT jobject JNICALL Java_io_github_cvc5_api_OptionInfo_getBaseInfo( + JNIEnv* env, jobject optionInfo, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer); + std::variant<OptionInfo::VoidInfo, + OptionInfo::ValueInfo<bool>, + OptionInfo::ValueInfo<std::string>, + OptionInfo::NumberInfo<int64_t>, + OptionInfo::NumberInfo<uint64_t>, + OptionInfo::NumberInfo<double>, + OptionInfo::ModeInfo> + v = current->valueInfo; + + if (std::holds_alternative<OptionInfo::VoidInfo>(v)) + { + jclass voidInfoClass = + env->FindClass("io/github/cvc5/api/OptionInfo$VoidInfo"); + jmethodID methodId = env->GetMethodID( + voidInfoClass, "<init>", "(Lio/github/cvc5/api/OptionInfo;)V"); + jobject ret = env->NewObject(voidInfoClass, methodId, optionInfo); + return ret; + } + + if (std::holds_alternative<OptionInfo::ValueInfo<bool>>(v) + || std::holds_alternative<OptionInfo::ValueInfo<std::string>>(v)) + { + jclass valueInfoClass = + env->FindClass("io/github/cvc5/api/OptionInfo$ValueInfo"); + jmethodID methodId = + env->GetMethodID(valueInfoClass, + "<init>", + "(Lio/github/cvc5/api/OptionInfo;Ljava/lang/" + "Object;Ljava/lang/Object;)V"); + + if (std::holds_alternative<OptionInfo::ValueInfo<bool>>(v)) + { + auto info = std::get<OptionInfo::ValueInfo<bool>>(v); + jobject currentValue = getBooleanObject(env, info.currentValue); + jobject defaultValue = getBooleanObject(env, info.defaultValue); + jobject ret = env->NewObject( + valueInfoClass, methodId, optionInfo, defaultValue, currentValue); + return ret; + } + + if (std::holds_alternative<OptionInfo::ValueInfo<std::string>>(v)) + { + auto info = std::get<OptionInfo::ValueInfo<std::string>>(v); + jstring defaultValue = env->NewStringUTF(info.defaultValue.c_str()); + jstring currentValue = env->NewStringUTF(info.currentValue.c_str()); + jobject ret = env->NewObject( + valueInfoClass, methodId, optionInfo, defaultValue, currentValue); + return ret; + } + } + + if (std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(v) + || std::holds_alternative<OptionInfo::NumberInfo<uint64_t>>(v) + || std::holds_alternative<OptionInfo::NumberInfo<double>>(v)) + { + jclass numberInfoClass = + env->FindClass("io/github/cvc5/api/OptionInfo$NumberInfo"); + jmethodID methodId = env->GetMethodID( + numberInfoClass, + "<init>", + "(Lio/github/cvc5/api/OptionInfo;Ljava/lang/Object;Ljava/lang/" + "Object;Ljava/lang/Object;Ljava/lang/Object;)V"); + + if (std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(v)) + { + auto info = std::get<OptionInfo::NumberInfo<int64_t>>(v); + return getNumberInfoFromInteger( + env, optionInfo, numberInfoClass, methodId, info); + } + + if (std::holds_alternative<OptionInfo::NumberInfo<uint64_t>>(v)) + { + auto info = std::get<OptionInfo::NumberInfo<uint64_t>>(v); + return getNumberInfoFromInteger( + env, optionInfo, numberInfoClass, methodId, info); + } + + if (std::holds_alternative<OptionInfo::NumberInfo<double>>(v)) + { + auto info = std::get<OptionInfo::NumberInfo<double>>(v); + jobject defaultValue = getDoubleObject(env, info.defaultValue); + jobject currentValue = getDoubleObject(env, info.currentValue); + jobject minimum = nullptr; + if (info.minimum) + { + minimum = getDoubleObject(env, *info.minimum); + } + jobject maximum = nullptr; + if (info.maximum) + { + maximum = getDoubleObject(env, *info.maximum); + } + jobject ret = env->NewObject(numberInfoClass, + methodId, + optionInfo, + defaultValue, + currentValue, + minimum, + maximum); + return ret; + } + } + + if (std::holds_alternative<OptionInfo::ModeInfo>(v)) + { + jclass modeInfoClass = + env->FindClass("io/github/cvc5/api/OptionInfo$ModeInfo"); + jmethodID methodId = env->GetMethodID( + modeInfoClass, + "<init>", + "(Lio/github/cvc5/api/OptionInfo;Ljava/lang/String;Ljava/lang/" + "String;[Ljava/lang/String;)V"); + + auto info = std::get<OptionInfo::ModeInfo>(v); + jstring defaultValue = env->NewStringUTF(info.defaultValue.c_str()); + jstring currentValue = env->NewStringUTF(info.currentValue.c_str()); + jobject stringArray = getStringArrayFromStringVector(env, info.modes); + jobject ret = env->NewObject(modeInfoClass, + methodId, + optionInfo, + defaultValue, + currentValue, + stringArray); + return ret; + } + + return nullptr; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: io_github_cvc5_api_OptionInfo + * Method: booleanValue + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_OptionInfo_booleanValue( + JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer); + return static_cast<jboolean>(current->boolValue()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false)); +} + +/* + * Class: io_github_cvc5_api_OptionInfo + * Method: stringValue + * Signature: (J)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_OptionInfo_stringValue( + JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer); + std::string ret = current->stringValue(); + return env->NewStringUTF(ret.c_str()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: io_github_cvc5_api_OptionInfo + * Method: intValue + * Signature: (J)Ljava/math/BigInteger; + */ +JNIEXPORT jobject JNICALL +Java_io_github_cvc5_api_OptionInfo_intValue(JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer); + std::int64_t value = current->intValue(); + jobject ret = getBigIntegerObject<std::int64_t>(env, value); + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: io_github_cvc5_api_OptionInfo + * Method: doubleValue + * Signature: (J)D + */ +JNIEXPORT jdouble JNICALL Java_io_github_cvc5_api_OptionInfo_doubleValue( + JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer); + double ret = current->doubleValue(); + return static_cast<jdouble>(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jdouble>(0.0)); +} diff --git a/src/api/java/jni/cvc5_Result.cpp b/src/api/java/jni/result.cpp index 4bc5cec1b..34b3262ca 100644 --- a/src/api/java/jni/cvc5_Result.cpp +++ b/src/api/java/jni/result.cpp @@ -13,33 +13,31 @@ * The cvc5 Java API. */ -#include "cvc5_Result.h" - #include "api/cpp/cvc5.h" -#include "cvc5JavaApi.h" +#include "api_utilities.h" +#include "io_github_cvc5_api_Result.h" using namespace cvc5::api; /* - * Class: cvc5_Result + * Class: io_github_cvc5_api_Result * Method: deletePointer * Signature: (J)V */ -JNIEXPORT void JNICALL Java_cvc5_Result_deletePointer(JNIEnv*, - jclass, - jlong pointer) +JNIEXPORT void JNICALL +Java_io_github_cvc5_api_Result_deletePointer(JNIEnv*, jclass, jlong pointer) { delete ((Result*)pointer); } /* - * Class: cvc5_Result + * Class: io_github_cvc5_api_Result * Method: isNull * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Result_isNull(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Result_isNull(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Result* current = (Result*)pointer; @@ -48,13 +46,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Result_isNull(JNIEnv* env, } /* - * Class: cvc5_Result + * Class: io_github_cvc5_api_Result * Method: isSat * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Result_isSat(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Result_isSat(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Result* current = (Result*)pointer; @@ -63,13 +61,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Result_isSat(JNIEnv* env, } /* - * Class: cvc5_Result + * Class: io_github_cvc5_api_Result * Method: isUnsat * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Result_isUnsat(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Result_isUnsat(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Result* current = (Result*)pointer; @@ -78,13 +76,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Result_isUnsat(JNIEnv* env, } /* - * Class: cvc5_Result + * Class: io_github_cvc5_api_Result * Method: isSatUnknown * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Result_isSatUnknown(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Result_isSatUnknown(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Result* current = (Result*)pointer; @@ -93,13 +90,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Result_isSatUnknown(JNIEnv* env, } /* - * Class: cvc5_Result + * Class: io_github_cvc5_api_Result * Method: isEntailed * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Result_isEntailed(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Result_isEntailed(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Result* current = (Result*)pointer; @@ -108,13 +104,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Result_isEntailed(JNIEnv* env, } /* - * Class: cvc5_Result + * Class: io_github_cvc5_api_Result * Method: isNotEntailed * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Result_isNotEntailed(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Result_isNotEntailed( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Result* current = (Result*)pointer; @@ -123,13 +118,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Result_isNotEntailed(JNIEnv* env, } /* - * Class: cvc5_Result + * Class: io_github_cvc5_api_Result * Method: isEntailmentUnknown * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Result_isEntailmentUnknown(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Result_isEntailmentUnknown( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Result* current = (Result*)pointer; @@ -138,14 +132,14 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Result_isEntailmentUnknown(JNIEnv* env, } /* - * Class: cvc5_Result + * Class: io_github_cvc5_api_Result * Method: equals * Signature: (JJ)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Result_equals(JNIEnv* env, - jobject, - jlong pointer1, - jlong pointer2) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Result_equals(JNIEnv* env, + jobject, + jlong pointer1, + jlong pointer2) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Result* result1 = (Result*)pointer1; @@ -156,13 +150,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Result_equals(JNIEnv* env, } /* - * Class: cvc5_Result + * Class: io_github_cvc5_api_Result * Method: getUnknownExplanation * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Result_getUnknownExplanation(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Result_getUnknownExplanation( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Result* current = (Result*)pointer; @@ -171,13 +164,13 @@ JNIEXPORT jint JNICALL Java_cvc5_Result_getUnknownExplanation(JNIEnv* env, } /* - * Class: cvc5_Result + * Class: io_github_cvc5_api_Result * Method: toString * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Result_toString(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Result_toString(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Result* current = (Result*)pointer; diff --git a/src/api/java/jni/cvc5_Solver.cpp b/src/api/java/jni/solver.cpp index cdbb48db0..882a74794 100644 --- a/src/api/java/jni/cvc5_Solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -13,44 +13,42 @@ * The cvc5 Java API. */ -#include "cvc5_Solver.h" - #include "api/cpp/cvc5.h" -#include "cvc5JavaApi.h" +#include "api_utilities.h" +#include "io_github_cvc5_api_Solver.h" using namespace cvc5::api; /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: newSolver * Signature: ()J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_newSolver(JNIEnv*, jobject) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_newSolver(JNIEnv*, + jobject) { Solver* solver = new Solver(); return reinterpret_cast<jlong>(solver); } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: deletePointer * Signature: (J)V */ -JNIEXPORT void JNICALL Java_cvc5_Solver_deletePointer(JNIEnv*, - jclass, - jlong pointer) +JNIEXPORT void JNICALL +Java_io_github_cvc5_api_Solver_deletePointer(JNIEnv*, jclass, jlong pointer) { delete (reinterpret_cast<Solver*>(pointer)); } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getNullSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_getNullSort(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -60,13 +58,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullSort(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getBooleanSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getBooleanSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getBooleanSort( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -76,13 +73,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getBooleanSort(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getIntegerSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getIntegerSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getIntegerSort( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -92,13 +88,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getIntegerSort(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getRealSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getRealSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_getRealSort(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -108,13 +103,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getRealSort(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getRegExpSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getRegExpSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getRegExpSort( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -124,13 +118,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getRegExpSort(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getRoundingModeSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getRoundingModeSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getRoundingModeSort( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -140,13 +133,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getRoundingModeSort(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getStringSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getStringSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getStringSort( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -156,15 +148,16 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getStringSort(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkArraySort * Signature: (JJJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkArraySort(JNIEnv* env, - jobject, - jlong pointer, - jlong indexSortPointer, - jlong elementSortPointer) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkArraySort(JNIEnv* env, + jobject, + jlong pointer, + jlong indexSortPointer, + jlong elementSortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -176,14 +169,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkArraySort(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkBitVectorSort * Signature: (JI)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkBitVectorSort(JNIEnv* env, - jobject, - jlong pointer, - jint size) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkBitVectorSort( + JNIEnv* env, jobject, jlong pointer, jint size) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -193,11 +184,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkBitVectorSort(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkFloatingPointSort * Signature: (JII)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkFloatingPointSort( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkFloatingPointSort( JNIEnv* env, jobject, jlong pointer, jint exp, jint sig) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -209,11 +200,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkFloatingPointSort( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkDatatypeSort * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkDatatypeSort( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkDatatypeSort( JNIEnv* env, jobject, jlong pointer, jlong datatypeDeclPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -225,12 +216,15 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkDatatypeSort( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkDatatypeSorts * Signature: (J[J)[J */ -JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_mkDatatypeSorts__J_3J( - JNIEnv* env, jobject, jlong pointer, jlongArray jDecls) +JNIEXPORT jlongArray JNICALL +Java_io_github_cvc5_api_Solver_mkDatatypeSorts__J_3J(JNIEnv* env, + jobject, + jlong pointer, + jlongArray jDecls) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -251,16 +245,16 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_mkDatatypeSorts__J_3J( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkDatatypeSorts * Signature: (J[J[J)[J */ JNIEXPORT jlongArray JNICALL -Java_cvc5_Solver_mkDatatypeSorts__J_3J_3J(JNIEnv* env, - jobject, - jlong pointer, - jlongArray jDecls, - jlongArray jUnresolved) +Java_io_github_cvc5_api_Solver_mkDatatypeSorts__J_3J_3J(JNIEnv* env, + jobject, + jlong pointer, + jlongArray jDecls, + jlongArray jUnresolved) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -276,16 +270,16 @@ Java_cvc5_Solver_mkDatatypeSorts__J_3J_3J(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkFunctionSort * Signature: (JJJ)J */ JNIEXPORT jlong JNICALL -Java_cvc5_Solver_mkFunctionSort__JJJ(JNIEnv* env, - jobject, - jlong pointer, - jlong domainPointer, - jlong codomainPointer) +Java_io_github_cvc5_api_Solver_mkFunctionSort__JJJ(JNIEnv* env, + jobject, + jlong pointer, + jlong domainPointer, + jlong codomainPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -297,16 +291,16 @@ Java_cvc5_Solver_mkFunctionSort__JJJ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkFunctionSort * Signature: (J[JJ)J */ JNIEXPORT jlong JNICALL -Java_cvc5_Solver_mkFunctionSort__J_3JJ(JNIEnv* env, - jobject, - jlong pointer, - jlongArray sortPointers, - jlong codomainPointer) +Java_io_github_cvc5_api_Solver_mkFunctionSort__J_3JJ(JNIEnv* env, + jobject, + jlong pointer, + jlongArray sortPointers, + jlong codomainPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -318,14 +312,12 @@ Java_cvc5_Solver_mkFunctionSort__J_3JJ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkParamSort * Signature: (JLjava/lang/String;)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkParamSort(JNIEnv* env, - jobject, - jlong pointer, - jstring jSymbol) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkParamSort( + JNIEnv* env, jobject, jlong pointer, jstring jSymbol) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -338,11 +330,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkParamSort(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkPredicateSort * Signature: (J[J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkPredicateSort( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkPredicateSort( JNIEnv* env, jobject, jlong pointer, jlongArray sortPointers) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -354,20 +346,18 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkPredicateSort( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkRecordSort - * Signature: (J[Lcvc5/Pair;)J + * Signature: (J[Lio/github/cvc5/api/Pair;)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkRecordSort(JNIEnv* env, - jobject, - jlong pointer, - jobjectArray jFields) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRecordSort( + JNIEnv* env, jobject, jlong pointer, jobjectArray jFields) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); jsize size = env->GetArrayLength(jFields); - // Lcvc5/Pair; is signature of cvc5.Pair<String, Long> - jclass pairClass = env->FindClass("Lcvc5/Pair;"); + // Lio/github/cvc5/api/Pair; is signature of cvc5.Pair<String, Long> + jclass pairClass = env->FindClass("Lio/github/cvc5/api/Pair;"); jclass longClass = env->FindClass("Ljava/lang/Long;"); // Ljava/lang/Object; is the signature of cvc5.Pair.first field jfieldID firstFieldId = @@ -404,14 +394,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkRecordSort(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkSetSort * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSetSort(JNIEnv* env, - jobject, - jlong pointer, - jlong elemSortPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkSetSort( + JNIEnv* env, jobject, jlong pointer, jlong elemSortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -422,14 +410,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSetSort(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkBagSort * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkBagSort(JNIEnv* env, - jobject, - jlong pointer, - jlong elemSortPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkBagSort( + JNIEnv* env, jobject, jlong pointer, jlong elemSortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -440,14 +426,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkBagSort(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkSequenceSort * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSequenceSort(JNIEnv* env, - jobject, - jlong pointer, - jlong elemSortPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkSequenceSort( + JNIEnv* env, jobject, jlong pointer, jlong elemSortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -458,14 +442,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSequenceSort(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkUninterpretedSort * Signature: (JLjava/lang/String;)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkUninterpretedSort(JNIEnv* env, - jobject, - jlong pointer, - jstring jSymbol) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkUninterpretedSort( + JNIEnv* env, jobject, jlong pointer, jstring jSymbol) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -479,11 +461,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkUninterpretedSort(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkSortConstructorSort * Signature: (JLjava/lang/String;I)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSortConstructorSort( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkSortConstructorSort( JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jint arity) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -500,14 +482,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSortConstructorSort( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkTupleSort * Signature: (J[J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTupleSort(JNIEnv* env, - jobject, - jlong pointer, - jlongArray sortPointers) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkTupleSort( + JNIEnv* env, jobject, jlong pointer, jlongArray sortPointers) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -518,14 +498,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTupleSort(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkTerm * Signature: (JI)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JI(JNIEnv* env, - jobject, - jlong pointer, - jint kindValue) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkTerm__JI( + JNIEnv* env, jobject, jlong pointer, jint kindValue) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -536,11 +514,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JI(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkTerm * Signature: (JIJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JIJ( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkTerm__JIJ( JNIEnv* env, jobject, jlong pointer, jint kindValue, jlong childPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -553,16 +531,17 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JIJ( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkTerm * Signature: (JIJJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JIJJ(JNIEnv* env, - jobject, - jlong pointer, - jint kindValue, - jlong child1Pointer, - jlong child2Pointer) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkTerm__JIJJ(JNIEnv* env, + jobject, + jlong pointer, + jint kindValue, + jlong child1Pointer, + jlong child2Pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -575,17 +554,18 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JIJJ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkTerm * Signature: (JIJJJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JIJJJ(JNIEnv* env, - jobject, - jlong pointer, - jint kindValue, - jlong child1Pointer, - jlong child2Pointer, - jlong child3Pointer) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkTerm__JIJJJ(JNIEnv* env, + jobject, + jlong pointer, + jint kindValue, + jlong child1Pointer, + jlong child2Pointer, + jlong child3Pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -599,16 +579,16 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JIJJJ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkTerm * Signature: (JI[J)J */ JNIEXPORT jlong JNICALL -Java_cvc5_Solver_mkTerm__JI_3J(JNIEnv* env, - jobject, - jlong pointer, - jint kindValue, - jlongArray childrenPointers) +Java_io_github_cvc5_api_Solver_mkTerm__JI_3J(JNIEnv* env, + jobject, + jlong pointer, + jint kindValue, + jlongArray childrenPointers) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -621,14 +601,12 @@ Java_cvc5_Solver_mkTerm__JI_3J(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkTerm * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JJ(JNIEnv* env, - jobject, - jlong pointer, - jlong opPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkTerm__JJ( + JNIEnv* env, jobject, jlong pointer, jlong opPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -639,11 +617,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JJ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkTerm * Signature: (JJJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JJJ( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkTerm__JJJ( JNIEnv* env, jobject, jlong pointer, jlong opPointer, jlong childPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -656,16 +634,17 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JJJ( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkTerm * Signature: (JJJJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JJJJ(JNIEnv* env, - jobject, - jlong pointer, - jlong opPointer, - jlong child1Pointer, - jlong child2Pointer) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkTerm__JJJJ(JNIEnv* env, + jobject, + jlong pointer, + jlong opPointer, + jlong child1Pointer, + jlong child2Pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -678,17 +657,18 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JJJJ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkTerm * Signature: (JJJJJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JJJJJ(JNIEnv* env, - jobject, - jlong pointer, - jlong opPointer, - jlong child1Pointer, - jlong child2Pointer, - jlong child3Pointer) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkTerm__JJJJJ(JNIEnv* env, + jobject, + jlong pointer, + jlong opPointer, + jlong child1Pointer, + jlong child2Pointer, + jlong child3Pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -702,16 +682,16 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JJJJJ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkTerm * Signature: (JJ[J)J */ JNIEXPORT jlong JNICALL -Java_cvc5_Solver_mkTerm__JJ_3J(JNIEnv* env, - jobject, - jlong pointer, - jlong opPointer, - jlongArray childrenPointers) +Java_io_github_cvc5_api_Solver_mkTerm__JJ_3J(JNIEnv* env, + jobject, + jlong pointer, + jlong opPointer, + jlongArray childrenPointers) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -724,15 +704,16 @@ Java_cvc5_Solver_mkTerm__JJ_3J(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkTuple * Signature: (J[J[J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTuple(JNIEnv* env, - jobject, - jlong pointer, - jlongArray sortPointers, - jlongArray termPointers) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkTuple(JNIEnv* env, + jobject, + jlong pointer, + jlongArray sortPointers, + jlongArray termPointers) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -744,14 +725,14 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTuple(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkOp * Signature: (JI)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkOp__JI(JNIEnv* env, - jobject, - jlong pointer, - jint kindValue) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkOp__JI(JNIEnv* env, + jobject, + jlong pointer, + jint kindValue) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -762,11 +743,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkOp__JI(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkOp * Signature: (JILjava/lang/String;)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkOp__JILjava_lang_String_2( +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkOp__JILjava_lang_String_2( JNIEnv* env, jobject, jlong pointer, jint kindValue, jstring jArg) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -783,11 +765,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkOp__JILjava_lang_String_2( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkOp * Signature: (JII)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkOp__JII( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkOp__JII( JNIEnv* env, jobject, jlong pointer, jint kindValue, jint arg) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -799,11 +781,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkOp__JII( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkOp * Signature: (JIII)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkOp__JIII( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkOp__JIII( JNIEnv* env, jobject, jlong pointer, jint kindValue, jint arg1, jint arg2) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -815,11 +797,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkOp__JIII( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkOp * Signature: (JI[I)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkOp__JI_3I( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkOp__JI_3I( JNIEnv* env, jobject, jlong pointer, jint kindValue, jintArray jArgs) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -842,13 +824,13 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkOp__JI_3I( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkTrue * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTrue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkTrue(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -858,13 +840,13 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTrue(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkFalse * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkFalse(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkFalse(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -874,14 +856,14 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkFalse(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkBoolean * Signature: (JZ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkBoolean(JNIEnv* env, - jobject, - jlong pointer, - jboolean val) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkBoolean(JNIEnv* env, + jobject, + jlong pointer, + jboolean val) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -891,13 +873,13 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkBoolean(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkPi * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkPi(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkPi(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -907,12 +889,15 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkPi(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkInteger * Signature: (JLjava/lang/String;)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkInteger__JLjava_lang_String_2( - JNIEnv* env, jobject, jlong pointer, jstring jS) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkInteger__JLjava_lang_String_2(JNIEnv* env, + jobject, + jlong pointer, + jstring jS) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -925,14 +910,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkInteger__JLjava_lang_String_2( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkInteger * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkInteger__JJ(JNIEnv* env, - jobject, - jlong pointer, - jlong val) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkInteger__JJ( + JNIEnv* env, jobject, jlong pointer, jlong val) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -942,12 +925,15 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkInteger__JJ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkReal * Signature: (JLjava/lang/String;)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkReal__JLjava_lang_String_2( - JNIEnv* env, jobject, jlong pointer, jstring jS) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkReal__JLjava_lang_String_2(JNIEnv* env, + jobject, + jlong pointer, + jstring jS) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -960,14 +946,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkReal__JLjava_lang_String_2( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkRealValue * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkRealValue(JNIEnv* env, - jobject, - jlong pointer, - jlong val) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRealValue( + JNIEnv* env, jobject, jlong pointer, jlong val) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -977,11 +961,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkRealValue(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkReal * Signature: (JJJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkReal__JJJ( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkReal__JJJ( JNIEnv* env, jobject, jlong pointer, jlong num, jlong den) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -992,13 +976,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkReal__JJJ( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkRegexpEmpty * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkRegexpEmpty(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRegexpEmpty( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1008,13 +991,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkRegexpEmpty(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkRegexpSigma * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkRegexpSigma(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRegexpSigma( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1024,14 +1006,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkRegexpSigma(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkEmptySet * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkEmptySet(JNIEnv* env, - jobject, - jlong pointer, - jlong sortPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkEmptySet( + JNIEnv* env, jobject, jlong pointer, jlong sortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1042,14 +1022,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkEmptySet(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkEmptyBag * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkEmptyBag(JNIEnv* env, - jobject, - jlong pointer, - jlong sortPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkEmptyBag( + JNIEnv* env, jobject, jlong pointer, jlong sortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1060,13 +1038,13 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkEmptyBag(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkSepEmp - * Signature: (JJ)J + * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSepEmp(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkSepEmp(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1076,14 +1054,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSepEmp(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkSepNil * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSepNil(JNIEnv* env, - jobject, - jlong pointer, - jlong sortPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkSepNil( + JNIEnv* env, jobject, jlong pointer, jlong sortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1094,11 +1070,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSepNil(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkString * Signature: (JLjava/lang/String;Z)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkString__JLjava_lang_String_2Z( +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkString__JLjava_lang_String_2Z( JNIEnv* env, jobject, jlong pointer, jstring jS, jboolean useEscSequences) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -1112,14 +1089,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkString__JLjava_lang_String_2Z( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkEmptySequence * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkEmptySequence(JNIEnv* env, - jobject, - jlong pointer, - jlong sortPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkEmptySequence( + JNIEnv* env, jobject, jlong pointer, jlong sortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1130,14 +1105,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkEmptySequence(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkUniverseSet * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkUniverseSet(JNIEnv* env, - jobject, - jlong pointer, - jlong sortPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkUniverseSet( + JNIEnv* env, jobject, jlong pointer, jlong sortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1148,11 +1121,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkUniverseSet(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkBitVector * Signature: (JIJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkBitVector__JIJ( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkBitVector__JIJ( JNIEnv* env, jobject, jlong pointer, jint size, jlong val) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -1164,11 +1137,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkBitVector__JIJ( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkBitVector * Signature: (JILjava/lang/String;I)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkBitVector__JILjava_lang_String_2I( +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkBitVector__JILjava_lang_String_2I( JNIEnv* env, jobject, jlong pointer, jint size, jstring jS, jint base) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -1183,11 +1157,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkBitVector__JILjava_lang_String_2I( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkConstArray * Signature: (JJJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkConstArray( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkConstArray( JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jlong valPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -1200,11 +1174,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkConstArray( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkPosInf * Signature: (JII)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkPosInf( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkPosInf( JNIEnv* env, jobject, jlong pointer, jint exp, jint sig) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -1215,11 +1189,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkPosInf( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkNegInf * Signature: (JII)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkNegInf( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkNegInf( JNIEnv* env, jobject, jlong pointer, jint exp, jint sig) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -1230,12 +1204,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkNegInf( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkNaN * Signature: (JII)J */ -JNIEXPORT jlong JNICALL -Java_cvc5_Solver_mkNaN(JNIEnv* env, jobject, jlong pointer, jint exp, jint sig) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkNaN( + JNIEnv* env, jobject, jlong pointer, jint exp, jint sig) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1245,11 +1219,11 @@ Java_cvc5_Solver_mkNaN(JNIEnv* env, jobject, jlong pointer, jint exp, jint sig) } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkPosZero * Signature: (JII)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkPosZero( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkPosZero( JNIEnv* env, jobject, jlong pointer, jint exp, jint sig) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -1260,11 +1234,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkPosZero( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkNegZero * Signature: (JII)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkNegZero( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkNegZero( JNIEnv* env, jobject, jlong pointer, jint exp, jint sig) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -1275,14 +1249,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkNegZero( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkRoundingMode * Signature: (JI)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkRoundingMode(JNIEnv* env, - jobject, - jlong pointer, - jint rm) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRoundingMode( + JNIEnv* env, jobject, jlong pointer, jint rm) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1292,11 +1264,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkRoundingMode(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkUninterpretedConst * Signature: (JJI)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkUninterpretedConst( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkUninterpretedConst( JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jint index) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -1309,11 +1281,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkUninterpretedConst( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkAbstractValue * Signature: (JLjava/lang/String;)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkAbstractValue__JLjava_lang_String_2( +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkAbstractValue__JLjava_lang_String_2( JNIEnv* env, jobject, jlong pointer, jstring jIndex) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -1327,14 +1300,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkAbstractValue__JLjava_lang_String_2( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkAbstractValue * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkAbstractValue__JJ(JNIEnv* env, - jobject, - jlong pointer, - jlong index) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkAbstractValue__JJ( + JNIEnv* env, jobject, jlong pointer, jlong index) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1344,11 +1315,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkAbstractValue__JJ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkFloatingPoint * Signature: (JIIJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkFloatingPoint( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkFloatingPoint( JNIEnv* env, jobject, jlong pointer, jint exp, jint sig, jlong valPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -1361,11 +1332,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkFloatingPoint( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkConst * Signature: (JJLjava/lang/String;)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkConst__JJLjava_lang_String_2( +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkConst__JJLjava_lang_String_2( JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jstring jSymbol) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -1380,14 +1352,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkConst__JJLjava_lang_String_2( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkConst * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkConst__JJ(JNIEnv* env, - jobject, - jlong pointer, - jlong sortPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkConst__JJ( + JNIEnv* env, jobject, jlong pointer, jlong sortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1398,11 +1368,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkConst__JJ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkVar * Signature: (JJLjava/lang/String;)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkVar( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkVar( JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jstring jSymbol) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -1418,12 +1388,15 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkVar( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkDatatypeConstructorDecl * Signature: (JLjava/lang/String;)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkDatatypeConstructorDecl( - JNIEnv* env, jobject, jlong pointer, jstring jName) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkDatatypeConstructorDecl(JNIEnv* env, + jobject, + jlong pointer, + jstring jName) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1438,11 +1411,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkDatatypeConstructorDecl( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkDatatypeDecl * Signature: (JLjava/lang/String;Z)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkDatatypeDecl__JLjava_lang_String_2Z( +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkDatatypeDecl__JLjava_lang_String_2Z( JNIEnv* env, jobject, jlong pointer, jstring jName, jboolean isCoDatatype) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -1457,17 +1431,18 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkDatatypeDecl__JLjava_lang_String_2Z( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkDatatypeDecl * Signature: (JLjava/lang/String;JZ)J */ JNIEXPORT jlong JNICALL -Java_cvc5_Solver_mkDatatypeDecl__JLjava_lang_String_2JZ(JNIEnv* env, - jobject, - jlong pointer, - jstring jName, - jlong paramPointer, - jboolean isCoDatatype) +Java_io_github_cvc5_api_Solver_mkDatatypeDecl__JLjava_lang_String_2JZ( + JNIEnv* env, + jobject, + jlong pointer, + jstring jName, + jlong paramPointer, + jboolean isCoDatatype) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1482,17 +1457,18 @@ Java_cvc5_Solver_mkDatatypeDecl__JLjava_lang_String_2JZ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkDatatypeDecl * Signature: (JLjava/lang/String;[JZ)J */ JNIEXPORT jlong JNICALL -Java_cvc5_Solver_mkDatatypeDecl__JLjava_lang_String_2_3JZ(JNIEnv* env, - jobject, - jlong pointer, - jstring jName, - jlongArray jParams, - jboolean isCoDatatype) +Java_io_github_cvc5_api_Solver_mkDatatypeDecl__JLjava_lang_String_2_3JZ( + JNIEnv* env, + jobject, + jlong pointer, + jstring jName, + jlongArray jParams, + jboolean isCoDatatype) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1507,14 +1483,12 @@ Java_cvc5_Solver_mkDatatypeDecl__JLjava_lang_String_2_3JZ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: simplify * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_simplify(JNIEnv* env, - jobject, - jlong pointer, - jlong termPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_simplify( + JNIEnv* env, jobject, jlong pointer, jlong termPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1525,14 +1499,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_simplify(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: assertFormula * Signature: (JJ)V */ -JNIEXPORT void JNICALL Java_cvc5_Solver_assertFormula(JNIEnv* env, - jobject, - jlong pointer, - jlong termPointer) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_assertFormula( + JNIEnv* env, jobject, jlong pointer, jlong termPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1542,13 +1514,13 @@ JNIEXPORT void JNICALL Java_cvc5_Solver_assertFormula(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: checkSat * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_checkSat(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkSat(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1558,11 +1530,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_checkSat(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: checkSatAssuming * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_checkSatAssuming__JJ( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkSatAssuming__JJ( JNIEnv* env, jobject, jlong pointer, jlong assumptionPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -1574,11 +1546,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_checkSatAssuming__JJ( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: checkSatAssuming * Signature: (J[J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_checkSatAssuming__J_3J( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkSatAssuming__J_3J( JNIEnv* env, jobject, jlong pointer, jlongArray jAssumptions) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -1591,14 +1563,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_checkSatAssuming__J_3J( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: checkEntailed * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_checkEntailed__JJ(JNIEnv* env, - jobject, - jlong pointer, - jlong termPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkEntailed__JJ( + JNIEnv* env, jobject, jlong pointer, jlong termPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1609,14 +1579,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_checkEntailed__JJ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: checkEntailed * Signature: (J[J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_checkEntailed__J_3J(JNIEnv* env, - jobject, - jlong pointer, - jlongArray jTerms) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkEntailed__J_3J( + JNIEnv* env, jobject, jlong pointer, jlongArray jTerms) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1627,11 +1595,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_checkEntailed__J_3J(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: declareDatatype * Signature: (JLjava/lang/String;[J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_declareDatatype( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_declareDatatype( JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jlongArray jCtors) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -1647,16 +1615,17 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_declareDatatype( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: declareFun * Signature: (JLjava/lang/String;[JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_declareFun(JNIEnv* env, - jobject, - jlong pointer, - jstring jSymbol, - jlongArray jSorts, - jlong sortPointer) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_declareFun(JNIEnv* env, + jobject, + jlong pointer, + jstring jSymbol, + jlongArray jSorts, + jlong sortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1671,11 +1640,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_declareFun(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: declareSort * Signature: (JLjava/lang/String;I)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_declareSort( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_declareSort( JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jint arity) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -1688,19 +1657,20 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_declareSort( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: defineFun * Signature: (JLjava/lang/String;[JJJZ)J */ JNIEXPORT jlong JNICALL -Java_cvc5_Solver_defineFun__JLjava_lang_String_2_3JJJZ(JNIEnv* env, - jobject, - jlong pointer, - jstring jSymbol, - jlongArray jVars, - jlong sortPointer, - jlong termPointer, - jboolean global) +Java_io_github_cvc5_api_Solver_defineFun__JLjava_lang_String_2_3JJJZ( + JNIEnv* env, + jobject, + jlong pointer, + jstring jSymbol, + jlongArray jVars, + jlong sortPointer, + jlong termPointer, + jboolean global) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1717,17 +1687,18 @@ Java_cvc5_Solver_defineFun__JLjava_lang_String_2_3JJJZ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: defineFun * Signature: (JJ[JJZ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_defineFun__JJ_3JJZ(JNIEnv* env, - jobject, - jlong pointer, - jlong funPointer, - jlongArray jVars, - jlong termPointer, - jboolean global) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_defineFun__JJ_3JJZ(JNIEnv* env, + jobject, + jlong pointer, + jlong funPointer, + jlongArray jVars, + jlong termPointer, + jboolean global) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1741,19 +1712,20 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_defineFun__JJ_3JJZ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: defineFunRec * Signature: (JLjava/lang/String;[JJJZ)J */ JNIEXPORT jlong JNICALL -Java_cvc5_Solver_defineFunRec__JLjava_lang_String_2_3JJJZ(JNIEnv* env, - jobject, - jlong pointer, - jstring jSymbol, - jlongArray jVars, - jlong sortPointer, - jlong termPointer, - jboolean global) +Java_io_github_cvc5_api_Solver_defineFunRec__JLjava_lang_String_2_3JJJZ( + JNIEnv* env, + jobject, + jlong pointer, + jstring jSymbol, + jlongArray jVars, + jlong sortPointer, + jlong termPointer, + jboolean global) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1770,18 +1742,18 @@ Java_cvc5_Solver_defineFunRec__JLjava_lang_String_2_3JJJZ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: defineFunRec * Signature: (JJ[JJZ)J */ JNIEXPORT jlong JNICALL -Java_cvc5_Solver_defineFunRec__JJ_3JJZ(JNIEnv* env, - jobject, - jlong pointer, - jlong funPointer, - jlongArray jVars, - jlong termPointer, - jboolean global) +Java_io_github_cvc5_api_Solver_defineFunRec__JJ_3JJZ(JNIEnv* env, + jobject, + jlong pointer, + jlong funPointer, + jlongArray jVars, + jlong termPointer, + jboolean global) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1795,17 +1767,18 @@ Java_cvc5_Solver_defineFunRec__JJ_3JJZ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: defineFunsRec * Signature: (J[J[[J[JZ)V */ -JNIEXPORT void JNICALL Java_cvc5_Solver_defineFunsRec(JNIEnv* env, - jobject, - jlong pointer, - jlongArray jFuns, - jobjectArray jVars, - jlongArray jTerms, - jboolean global) +JNIEXPORT void JNICALL +Java_io_github_cvc5_api_Solver_defineFunsRec(JNIEnv* env, + jobject, + jlong pointer, + jlongArray jFuns, + jobjectArray jVars, + jlongArray jTerms, + jboolean global) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1831,13 +1804,12 @@ JNIEXPORT void JNICALL Java_cvc5_Solver_defineFunsRec(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getAssertions * Signature: (J)[J */ -JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getAssertions(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Solver_getAssertions( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1848,14 +1820,14 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getAssertions(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getInfo * Signature: (JLjava/lang/String;)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Solver_getInfo(JNIEnv* env, - jobject, - jlong pointer, - jstring jFlag) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Solver_getInfo(JNIEnv* env, + jobject, + jlong pointer, + jstring jFlag) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1867,14 +1839,12 @@ JNIEXPORT jstring JNICALL Java_cvc5_Solver_getInfo(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getOption * Signature: (JLjava/lang/String;)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Solver_getOption(JNIEnv* env, - jobject, - jlong pointer, - jstring jOption) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Solver_getOption( + JNIEnv* env, jobject, jlong pointer, jstring jOption) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1886,13 +1856,12 @@ JNIEXPORT jstring JNICALL Java_cvc5_Solver_getOption(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getOptionNames * Signature: (J)[Ljava/lang/String; */ -JNIEXPORT jobjectArray JNICALL Java_cvc5_Solver_getOptionNames(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jobjectArray JNICALL Java_io_github_cvc5_api_Solver_getOptionNames( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1903,14 +1872,12 @@ JNIEXPORT jobjectArray JNICALL Java_cvc5_Solver_getOptionNames(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getOptionInfo * Signature: (JLjava/lang/String;)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getOptionInfo(JNIEnv* env, - jobject, - jlong pointer, - jstring jOption) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getOptionInfo( + JNIEnv* env, jobject, jlong pointer, jstring jOption) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1921,13 +1888,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getOptionInfo(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getDriverOptions * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getDriverOptions(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getDriverOptions( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1937,13 +1903,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getDriverOptions(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getUnsatAssumptions * Signature: (J)[J */ -JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getUnsatAssumptions(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Solver_getUnsatAssumptions( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1954,13 +1919,12 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getUnsatAssumptions(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getUnsatCore * Signature: (J)[J */ -JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getUnsatCore(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlongArray JNICALL +Java_io_github_cvc5_api_Solver_getUnsatCore(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -1971,13 +1935,12 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getUnsatCore(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getDifficulty * Signature: (J)Ljava/util/Map; */ -JNIEXPORT jobject JNICALL Java_cvc5_Solver_getDifficulty(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jobject JNICALL Java_io_github_cvc5_api_Solver_getDifficulty( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2011,13 +1974,13 @@ JNIEXPORT jobject JNICALL Java_cvc5_Solver_getDifficulty(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getProof * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Solver_getProof(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Solver_getProof(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2027,14 +1990,12 @@ JNIEXPORT jstring JNICALL Java_cvc5_Solver_getProof(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getValue * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getValue__JJ(JNIEnv* env, - jobject, - jlong pointer, - jlong termPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getValue__JJ( + JNIEnv* env, jobject, jlong pointer, jlong termPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2045,11 +2006,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getValue__JJ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getValue * Signature: (J[J)[J */ -JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getValue__J_3J( +JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Solver_getValue__J_3J( JNIEnv* env, jobject, jlong pointer, jlongArray termPointers) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -2062,12 +2023,15 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getValue__J_3J( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getModelDomainElements * Signature: (JJ)[J */ -JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getModelDomainElements( - JNIEnv* env, jobject, jlong pointer, jlong sortPointer) +JNIEXPORT jlongArray JNICALL +Java_io_github_cvc5_api_Solver_getModelDomainElements(JNIEnv* env, + jobject, + jlong pointer, + jlong sortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2079,14 +2043,12 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getModelDomainElements( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: isModelCoreSymbol * Signature: (JJ)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Solver_isModelCoreSymbol(JNIEnv* env, - jobject, - jlong pointer, - jlong termPointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_isModelCoreSymbol( + JNIEnv* env, jobject, jlong pointer, jlong termPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2096,15 +2058,16 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Solver_isModelCoreSymbol(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getModel * Signature: (J[J[J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Solver_getModel(JNIEnv* env, - jobject, - jlong pointer, - jlongArray sortPointers, - jlongArray varPointers) +JNIEXPORT jstring JNICALL +Java_io_github_cvc5_api_Solver_getModel(JNIEnv* env, + jobject, + jlong pointer, + jlongArray sortPointers, + jlongArray varPointers) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2116,11 +2079,11 @@ JNIEXPORT jstring JNICALL Java_cvc5_Solver_getModel(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getQuantifierElimination * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getQuantifierElimination( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getQuantifierElimination( JNIEnv* env, jobject, jlong pointer, jlong qPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -2132,12 +2095,15 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getQuantifierElimination( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getQuantifierEliminationDisjunct * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getQuantifierEliminationDisjunct( - JNIEnv* env, jobject, jlong pointer, jlong qPointer) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_getQuantifierEliminationDisjunct(JNIEnv* env, + jobject, + jlong pointer, + jlong qPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2148,16 +2114,16 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getQuantifierEliminationDisjunct( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: declareSeparationHeap * Signature: (JJJ)V */ JNIEXPORT void JNICALL -Java_cvc5_Solver_declareSeparationHeap(JNIEnv* env, - jobject, - jlong pointer, - jlong locSortPointer, - jlong dataSortPointer) +Java_io_github_cvc5_api_Solver_declareSeparationHeap(JNIEnv* env, + jobject, + jlong pointer, + jlong locSortPointer, + jlong dataSortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2168,13 +2134,12 @@ Java_cvc5_Solver_declareSeparationHeap(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getSeparationHeap * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getSeparationHeap(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getSeparationHeap( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2184,13 +2149,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getSeparationHeap(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getSeparationNilTerm * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getSeparationNilTerm(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getSeparationNilTerm( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2200,14 +2164,14 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getSeparationNilTerm(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: pop * Signature: (JI)V */ -JNIEXPORT void JNICALL Java_cvc5_Solver_pop(JNIEnv* env, - jobject, - jlong pointer, - jint nscopes) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_pop(JNIEnv* env, + jobject, + jlong pointer, + jint nscopes) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2216,11 +2180,11 @@ JNIEXPORT void JNICALL Java_cvc5_Solver_pop(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getInterpolant * Signature: (JJJ)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Solver_getInterpolant__JJJ( +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_getInterpolant__JJJ( JNIEnv* env, jobject, jlong pointer, jlong conjPointer, jlong outputPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -2232,17 +2196,17 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Solver_getInterpolant__JJJ( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getInterpolant * Signature: (JJJJ)Z */ JNIEXPORT jboolean JNICALL -Java_cvc5_Solver_getInterpolant__JJJJ(JNIEnv* env, - jobject, - jlong pointer, - jlong conjPointer, - jlong grammarPointer, - jlong outputPointer) +Java_io_github_cvc5_api_Solver_getInterpolant__JJJJ(JNIEnv* env, + jobject, + jlong pointer, + jlong conjPointer, + jlong grammarPointer, + jlong outputPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2254,11 +2218,11 @@ Java_cvc5_Solver_getInterpolant__JJJJ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getAbduct * Signature: (JJJ)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Solver_getAbduct__JJJ( +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_getAbduct__JJJ( JNIEnv* env, jobject, jlong pointer, jlong conjPointer, jlong outputPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -2270,17 +2234,17 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Solver_getAbduct__JJJ( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getAbduct * Signature: (JJJJ)Z */ JNIEXPORT jboolean JNICALL -Java_cvc5_Solver_getAbduct__JJJJ(JNIEnv* env, - jobject, - jlong pointer, - jlong conjPointer, - jlong grammarPointer, - jlong outputPointer) +Java_io_github_cvc5_api_Solver_getAbduct__JJJJ(JNIEnv* env, + jobject, + jlong pointer, + jlong conjPointer, + jlong grammarPointer, + jlong outputPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2292,13 +2256,13 @@ Java_cvc5_Solver_getAbduct__JJJJ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: blockModel * Signature: (J)V */ -JNIEXPORT void JNICALL Java_cvc5_Solver_blockModel(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_blockModel(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2307,14 +2271,12 @@ JNIEXPORT void JNICALL Java_cvc5_Solver_blockModel(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: blockModelValues * Signature: (J[J)V */ -JNIEXPORT void JNICALL Java_cvc5_Solver_blockModelValues(JNIEnv* env, - jobject, - jlong pointer, - jlongArray jTerms) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_blockModelValues( + JNIEnv* env, jobject, jlong pointer, jlongArray jTerms) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2324,14 +2286,14 @@ JNIEXPORT void JNICALL Java_cvc5_Solver_blockModelValues(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: push * Signature: (JI)V */ -JNIEXPORT void JNICALL Java_cvc5_Solver_push(JNIEnv* env, - jobject, - jlong pointer, - jint nscopes) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_push(JNIEnv* env, + jobject, + jlong pointer, + jint nscopes) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2340,13 +2302,12 @@ JNIEXPORT void JNICALL Java_cvc5_Solver_push(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: resetAssertions * Signature: (J)V */ -JNIEXPORT void JNICALL Java_cvc5_Solver_resetAssertions(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_resetAssertions( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2355,11 +2316,11 @@ JNIEXPORT void JNICALL Java_cvc5_Solver_resetAssertions(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: setInfo * Signature: (JLjava/lang/String;Ljava/lang/String;)V */ -JNIEXPORT void JNICALL Java_cvc5_Solver_setInfo( +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_setInfo( JNIEnv* env, jobject, jlong pointer, jstring jKeyword, jstring jValue) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -2375,14 +2336,14 @@ JNIEXPORT void JNICALL Java_cvc5_Solver_setInfo( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: setLogic * Signature: (JLjava/lang/String;)V */ -JNIEXPORT void JNICALL Java_cvc5_Solver_setLogic(JNIEnv* env, - jobject, - jlong pointer, - jstring jLogic) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_setLogic(JNIEnv* env, + jobject, + jlong pointer, + jstring jLogic) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -2394,11 +2355,11 @@ JNIEXPORT void JNICALL Java_cvc5_Solver_setLogic(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: setOption * Signature: (JLjava/lang/String;Ljava/lang/String;)V */ -JNIEXPORT void JNICALL Java_cvc5_Solver_setOption( +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_setOption( JNIEnv* env, jobject, jlong pointer, jstring jOption, jstring jValue) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -2414,11 +2375,11 @@ JNIEXPORT void JNICALL Java_cvc5_Solver_setOption( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: ensureTermSort * Signature: (JJJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_ensureTermSort( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_ensureTermSort( JNIEnv* env, jobject, jlong pointer, jlong termPointer, jlong sortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -2431,11 +2392,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_ensureTermSort( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkSygusVar * Signature: (JJLjava/lang/String;)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSygusVar( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkSygusVar( JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jstring jSymbol) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -2450,15 +2411,16 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSygusVar( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: mkSygusGrammar * Signature: (J[J[J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSygusGrammar(JNIEnv* env, - jobject, - jlong pointer, - jlongArray jBoundVars, - jlongArray jNtSymbols) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkSygusGrammar(JNIEnv* env, + jobject, + jlong pointer, + jlongArray jBoundVars, + jlongArray jNtSymbols) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2471,17 +2433,18 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSygusGrammar(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: synthFun * Signature: (JLjava/lang/String;[JJ)J */ JNIEXPORT jlong JNICALL -Java_cvc5_Solver_synthFun__JLjava_lang_String_2_3JJ(JNIEnv* env, - jobject, - jlong pointer, - jstring jSymbol, - jlongArray jVars, - jlong sortPointer) +Java_io_github_cvc5_api_Solver_synthFun__JLjava_lang_String_2_3JJ( + JNIEnv* env, + jobject, + jlong pointer, + jstring jSymbol, + jlongArray jVars, + jlong sortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2496,18 +2459,19 @@ Java_cvc5_Solver_synthFun__JLjava_lang_String_2_3JJ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: synthFun * Signature: (JLjava/lang/String;[JJJ)J */ JNIEXPORT jlong JNICALL -Java_cvc5_Solver_synthFun__JLjava_lang_String_2_3JJJ(JNIEnv* env, - jobject, - jlong pointer, - jstring jSymbol, - jlongArray jVars, - jlong sortPointer, - jlong grammarPointer) +Java_io_github_cvc5_api_Solver_synthFun__JLjava_lang_String_2_3JJJ( + JNIEnv* env, + jobject, + jlong pointer, + jstring jSymbol, + jlongArray jVars, + jlong sortPointer, + jlong grammarPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2524,11 +2488,12 @@ Java_cvc5_Solver_synthFun__JLjava_lang_String_2_3JJJ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: synthInv * Signature: (JLjava/lang/String;[J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_synthInv__JLjava_lang_String_2_3J( +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_synthInv__JLjava_lang_String_2_3J( JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jlongArray jVars) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -2543,17 +2508,18 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_synthInv__JLjava_lang_String_2_3J( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: synthInv * Signature: (JLjava/lang/String;[JJ)J */ JNIEXPORT jlong JNICALL -Java_cvc5_Solver_synthInv__JLjava_lang_String_2_3JJ(JNIEnv* env, - jobject, - jlong pointer, - jstring jSymbol, - jlongArray jVars, - jlong grammarPointer) +Java_io_github_cvc5_api_Solver_synthInv__JLjava_lang_String_2_3JJ( + JNIEnv* env, + jobject, + jlong pointer, + jstring jSymbol, + jlongArray jVars, + jlong grammarPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2568,14 +2534,12 @@ Java_cvc5_Solver_synthInv__JLjava_lang_String_2_3JJ(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: addSygusConstraint * Signature: (JJ)V */ -JNIEXPORT void JNICALL Java_cvc5_Solver_addSygusConstraint(JNIEnv* env, - jobject, - jlong pointer, - jlong termPointer) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_addSygusConstraint( + JNIEnv* env, jobject, jlong pointer, jlong termPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2585,14 +2549,12 @@ JNIEXPORT void JNICALL Java_cvc5_Solver_addSygusConstraint(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: addSygusAssume * Signature: (JJ)V */ -JNIEXPORT void JNICALL Java_cvc5_Solver_addSygusAssume(JNIEnv* env, - jobject, - jlong pointer, - jlong termPointer) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_addSygusAssume( + JNIEnv* env, jobject, jlong pointer, jlong termPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2602,18 +2564,18 @@ JNIEXPORT void JNICALL Java_cvc5_Solver_addSygusAssume(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: addSygusInvConstraint * Signature: (JJJJJ)V */ JNIEXPORT void JNICALL -Java_cvc5_Solver_addSygusInvConstraint(JNIEnv* env, - jobject, - jlong pointer, - jlong invPointer, - jlong prePointer, - jlong transPointer, - jlong postPointer) +Java_io_github_cvc5_api_Solver_addSygusInvConstraint(JNIEnv* env, + jobject, + jlong pointer, + jlong invPointer, + jlong prePointer, + jlong transPointer, + jlong postPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2626,13 +2588,13 @@ Java_cvc5_Solver_addSygusInvConstraint(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: checkSynth * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_checkSynth(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkSynth(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2642,14 +2604,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_checkSynth(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getSynthSolution * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getSynthSolution(JNIEnv* env, - jobject, - jlong pointer, - jlong termPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getSynthSolution( + JNIEnv* env, jobject, jlong pointer, jlong termPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2660,11 +2620,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getSynthSolution(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getSynthSolutions * Signature: (J[J)[J */ -JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getSynthSolutions( +JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Solver_getSynthSolutions( JNIEnv* env, jobject, jlong pointer, jlongArray jTerms) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -2677,13 +2637,12 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getSynthSolutions( } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getStatistics * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getStatistics(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getStatistics( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast<Solver*>(pointer); @@ -2693,13 +2652,13 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getStatistics(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getNullTerm * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullTerm(JNIEnv* env, - jobject, - jlong) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getNullTerm(JNIEnv* env, + jobject, + jlong) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* ret = new Term(); @@ -2708,13 +2667,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullTerm(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getNullResult * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullResult(JNIEnv* env, - jobject, - jlong) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_getNullResult(JNIEnv* env, jobject, jlong) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Result* ret = new Result(); @@ -2723,11 +2681,13 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullResult(JNIEnv* env, } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getNullOp * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullOp(JNIEnv* env, jobject, jlong) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getNullOp(JNIEnv* env, + jobject, + jlong) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Op* ret = new Op(); @@ -2736,16 +2696,15 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullOp(JNIEnv* env, jobject, jlong) } /* - * Class: cvc5_Solver + * Class: io_github_cvc5_api_Solver * Method: getNullDatatypeDecl * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullDatatypeDecl(JNIEnv* env, - jobject, - jlong) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_getNullDatatypeDecl(JNIEnv* env, jobject, jlong) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeDecl* ret = new DatatypeDecl(); return reinterpret_cast<jlong>(ret); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); -} +}
\ No newline at end of file diff --git a/src/api/java/jni/cvc5_Sort.cpp b/src/api/java/jni/sort.cpp index 36ba81249..fed1f3a41 100644 --- a/src/api/java/jni/cvc5_Sort.cpp +++ b/src/api/java/jni/sort.cpp @@ -13,34 +13,33 @@ * The cvc5 Java API. */ -#include "cvc5_Sort.h" - #include "api/cpp/cvc5.h" -#include "cvc5JavaApi.h" +#include "api_utilities.h" +#include "io_github_cvc5_api_Sort.h" using namespace cvc5::api; /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: deletePointer * Signature: (J)V */ -JNIEXPORT void JNICALL Java_cvc5_Sort_deletePointer(JNIEnv*, - jclass, - jlong pointer) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Sort_deletePointer(JNIEnv*, + jclass, + jlong pointer) { delete reinterpret_cast<Sort*>(pointer); } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: equals * Signature: (JJ)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_equals(JNIEnv* env, - jobject, - jlong pointer1, - jlong pointer2) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_equals(JNIEnv* env, + jobject, + jlong pointer1, + jlong pointer2) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort sort1 = *(reinterpret_cast<Sort*>(pointer1)); @@ -50,14 +49,14 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_equals(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: compareTo * Signature: (JJ)I */ -JNIEXPORT jint JNICALL Java_cvc5_Sort_compareTo(JNIEnv* env, - jobject, - jlong pointer1, - jlong pointer2) +JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Sort_compareTo(JNIEnv* env, + jobject, + jlong pointer1, + jlong pointer2) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* sort1 = reinterpret_cast<Sort*>(pointer1); @@ -75,13 +74,13 @@ JNIEXPORT jint JNICALL Java_cvc5_Sort_compareTo(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isNull * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isNull(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isNull(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -90,13 +89,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isNull(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isBoolean * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isBoolean(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isBoolean(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -105,13 +104,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isBoolean(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isInteger * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isInteger(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isInteger(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -120,13 +119,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isInteger(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isReal * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isReal(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isReal(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -135,13 +134,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isReal(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isString * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isString(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isString(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -150,13 +149,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isString(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isRegExp * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isRegExp(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isRegExp(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -165,13 +164,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isRegExp(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isRoundingMode * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isRoundingMode(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Sort_isRoundingMode(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -180,13 +178,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isRoundingMode(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isBitVector * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isBitVector(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Sort_isBitVector(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -195,13 +192,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isBitVector(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isFloatingPoint * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isFloatingPoint(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isFloatingPoint( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -210,13 +206,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isFloatingPoint(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isDatatype * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isDatatype(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Sort_isDatatype(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -225,13 +220,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isDatatype(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isParametricDatatype * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isParametricDatatype(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isParametricDatatype( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -240,13 +234,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isParametricDatatype(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isConstructor * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isConstructor(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Sort_isConstructor(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -255,13 +248,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isConstructor(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isSelector * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isSelector(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Sort_isSelector(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -270,13 +262,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isSelector(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isTester * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isTester(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isTester(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -285,13 +277,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isTester(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isUpdater * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isUpdater(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isUpdater(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -300,13 +292,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isUpdater(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isFunction * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isFunction(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Sort_isFunction(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -315,13 +306,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isFunction(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isPredicate * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isPredicate(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Sort_isPredicate(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -330,13 +320,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isPredicate(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isTuple * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isTuple(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isTuple(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -345,13 +335,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isTuple(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isRecord * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isRecord(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isRecord(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -360,13 +350,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isRecord(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isArray * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isArray(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isArray(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -375,13 +365,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isArray(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isSet * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isSet(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isSet(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -390,13 +380,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isSet(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isBag * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isBag(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isBag(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -405,13 +395,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isBag(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isSequence * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isSequence(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Sort_isSequence(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -420,13 +409,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isSequence(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isUninterpretedSort * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isUninterpretedSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isUninterpretedSort( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -435,13 +423,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isUninterpretedSort(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isSortConstructor * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isSortConstructor(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isSortConstructor( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -450,13 +437,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isSortConstructor(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isFirstClass * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isFirstClass(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Sort_isFirstClass(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -465,13 +451,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isFirstClass(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isFunctionLike * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isFunctionLike(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Sort_isFunctionLike(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -480,14 +465,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isFunctionLike(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isSubsortOf * Signature: (JJ)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isSubsortOf(JNIEnv* env, - jobject, - jlong pointer, - jlong sortPointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isSubsortOf( + JNIEnv* env, jobject, jlong pointer, jlong sortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -497,14 +480,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isSubsortOf(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isComparableTo * Signature: (JJ)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isComparableTo(JNIEnv* env, - jobject, - jlong pointer, - jlong sortPointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isComparableTo( + JNIEnv* env, jobject, jlong pointer, jlong sortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -514,13 +495,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isComparableTo(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getDatatype * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Sort_getDatatype(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Sort_getDatatype(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -530,14 +511,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Sort_getDatatype(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: instantiate * Signature: (J[J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Sort_instantiate(JNIEnv* env, - jobject, - jlong pointer, - jlongArray paramsPointers) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Sort_instantiate( + JNIEnv* env, jobject, jlong pointer, jlongArray paramsPointers) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -563,15 +542,16 @@ JNIEXPORT jlong JNICALL Java_cvc5_Sort_instantiate(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: substitute * Signature: (JJJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Sort_substitute__JJJ(JNIEnv* env, - jobject, - jlong pointer, - jlong sortPointer, - jlong replacementPointer) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Sort_substitute__JJJ(JNIEnv* env, + jobject, + jlong pointer, + jlong sortPointer, + jlong replacementPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -583,16 +563,16 @@ JNIEXPORT jlong JNICALL Java_cvc5_Sort_substitute__JJJ(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: substitute * Signature: (J[J[J)J */ JNIEXPORT jlong JNICALL -Java_cvc5_Sort_substitute__J_3J_3J(JNIEnv* env, - jobject, - jlong pointer, - jlongArray sortPointers, - jlongArray replacementPointers) +Java_io_github_cvc5_api_Sort_substitute__J_3J_3J(JNIEnv* env, + jobject, + jlong pointer, + jlongArray sortPointers, + jlongArray replacementPointers) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -631,13 +611,13 @@ Java_cvc5_Sort_substitute__J_3J_3J(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: toString * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Sort_toString(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Sort_toString(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -646,13 +626,12 @@ JNIEXPORT jstring JNICALL Java_cvc5_Sort_toString(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getConstructorArity * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Sort_getConstructorArity(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Sort_getConstructorArity( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -661,12 +640,14 @@ JNIEXPORT jint JNICALL Java_cvc5_Sort_getConstructorArity(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getConstructorDomainSorts * Signature: (J)[J */ JNIEXPORT jlongArray JNICALL -Java_cvc5_Sort_getConstructorDomainSorts(JNIEnv* env, jobject, jlong pointer) +Java_io_github_cvc5_api_Sort_getConstructorDomainSorts(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -683,13 +664,12 @@ Java_cvc5_Sort_getConstructorDomainSorts(JNIEnv* env, jobject, jlong pointer) } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getConstructorCodomainSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Sort_getConstructorCodomainSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Sort_getConstructorCodomainSort( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -699,13 +679,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Sort_getConstructorCodomainSort(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getSelectorDomainSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Sort_getSelectorDomainSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Sort_getSelectorDomainSort( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -715,13 +694,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Sort_getSelectorDomainSort(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getSelectorCodomainSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Sort_getSelectorCodomainSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Sort_getSelectorCodomainSort( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -731,13 +709,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Sort_getSelectorCodomainSort(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getTesterDomainSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Sort_getTesterDomainSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Sort_getTesterDomainSort( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -747,13 +724,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Sort_getTesterDomainSort(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getTesterCodomainSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Sort_getTesterCodomainSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Sort_getTesterCodomainSort( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -763,13 +739,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Sort_getTesterCodomainSort(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getFunctionArity * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Sort_getFunctionArity(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Sort_getFunctionArity( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -778,12 +753,14 @@ JNIEXPORT jint JNICALL Java_cvc5_Sort_getFunctionArity(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getFunctionDomainSorts * Signature: (J)[J */ JNIEXPORT jlongArray JNICALL -Java_cvc5_Sort_getFunctionDomainSorts(JNIEnv* env, jobject, jlong pointer) +Java_io_github_cvc5_api_Sort_getFunctionDomainSorts(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -800,13 +777,12 @@ Java_cvc5_Sort_getFunctionDomainSorts(JNIEnv* env, jobject, jlong pointer) } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getFunctionCodomainSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Sort_getFunctionCodomainSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Sort_getFunctionCodomainSort( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -816,13 +792,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Sort_getFunctionCodomainSort(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getArrayIndexSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Sort_getArrayIndexSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Sort_getArrayIndexSort( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -832,13 +807,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Sort_getArrayIndexSort(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getArrayElementSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Sort_getArrayElementSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Sort_getArrayElementSort( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -848,13 +822,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Sort_getArrayElementSort(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getSetElementSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Sort_getSetElementSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Sort_getSetElementSort( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -864,13 +837,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Sort_getSetElementSort(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getBagElementSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Sort_getBagElementSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Sort_getBagElementSort( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -880,13 +852,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Sort_getBagElementSort(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getSequenceElementSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Sort_getSequenceElementSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Sort_getSequenceElementSort( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -896,13 +867,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Sort_getSequenceElementSort(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getUninterpretedSortName * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Sort_getUninterpretedSortName(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Sort_getUninterpretedSortName( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -911,12 +881,14 @@ JNIEXPORT jstring JNICALL Java_cvc5_Sort_getUninterpretedSortName(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: isUninterpretedSortParameterized * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isUninterpretedSortParameterized( - JNIEnv* env, jobject, jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Sort_isUninterpretedSortParameterized(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -925,12 +897,14 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Sort_isUninterpretedSortParameterized( } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getUninterpretedSortParamSorts * Signature: (J)[J */ -JNIEXPORT jlongArray JNICALL Java_cvc5_Sort_getUninterpretedSortParamSorts( - JNIEnv* env, jobject, jlong pointer) +JNIEXPORT jlongArray JNICALL +Java_io_github_cvc5_api_Sort_getUninterpretedSortParamSorts(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -947,13 +921,12 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Sort_getUninterpretedSortParamSorts( } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getSortConstructorName * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Sort_getSortConstructorName(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Sort_getSortConstructorName( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -962,13 +935,12 @@ JNIEXPORT jstring JNICALL Java_cvc5_Sort_getSortConstructorName(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getSortConstructorArity * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Sort_getSortConstructorArity(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Sort_getSortConstructorArity( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -977,13 +949,12 @@ JNIEXPORT jint JNICALL Java_cvc5_Sort_getSortConstructorArity(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getBitVectorSize * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Sort_getBitVectorSize(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Sort_getBitVectorSize( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -992,12 +963,14 @@ JNIEXPORT jint JNICALL Java_cvc5_Sort_getBitVectorSize(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getFloatingPointExponentSize * Signature: (J)I */ JNIEXPORT jint JNICALL -Java_cvc5_Sort_getFloatingPointExponentSize(JNIEnv* env, jobject, jlong pointer) +Java_io_github_cvc5_api_Sort_getFloatingPointExponentSize(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -1006,12 +979,14 @@ Java_cvc5_Sort_getFloatingPointExponentSize(JNIEnv* env, jobject, jlong pointer) } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getFloatingPointSignificandSize * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Sort_getFloatingPointSignificandSize( - JNIEnv* env, jobject, jlong pointer) +JNIEXPORT jint JNICALL +Java_io_github_cvc5_api_Sort_getFloatingPointSignificandSize(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -1020,13 +995,12 @@ JNIEXPORT jint JNICALL Java_cvc5_Sort_getFloatingPointSignificandSize( } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getDatatypeParamSorts * Signature: (J)[J */ -JNIEXPORT jlongArray JNICALL Java_cvc5_Sort_getDatatypeParamSorts(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Sort_getDatatypeParamSorts( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -1043,13 +1017,12 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Sort_getDatatypeParamSorts(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getDatatypeArity * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Sort_getDatatypeArity(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Sort_getDatatypeArity( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -1058,13 +1031,12 @@ JNIEXPORT jint JNICALL Java_cvc5_Sort_getDatatypeArity(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getTupleLength * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Sort_getTupleLength(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL +Java_io_github_cvc5_api_Sort_getTupleLength(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); @@ -1073,13 +1045,12 @@ JNIEXPORT jint JNICALL Java_cvc5_Sort_getTupleLength(JNIEnv* env, } /* - * Class: cvc5_Sort + * Class: io_github_cvc5_api_Sort * Method: getTupleSorts * Signature: (J)[J */ -JNIEXPORT jlongArray JNICALL Java_cvc5_Sort_getTupleSorts(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlongArray JNICALL +Java_io_github_cvc5_api_Sort_getTupleSorts(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast<Sort*>(pointer); diff --git a/src/api/java/jni/cvc5_Stat.cpp b/src/api/java/jni/stat.cpp index 9345729cb..5db362ce2 100644 --- a/src/api/java/jni/cvc5_Stat.cpp +++ b/src/api/java/jni/stat.cpp @@ -13,33 +13,32 @@ * The cvc5 Java API. */ -#include "cvc5_Stat.h" - #include "api/cpp/cvc5.h" -#include "cvc5JavaApi.h" +#include "api_utilities.h" +#include "io_github_cvc5_api_Stat.h" using namespace cvc5::api; /* - * Class: cvc5_Stat + * Class: io_github_cvc5_api_Stat * Method: deletePointer * Signature: (J)V */ -JNIEXPORT void JNICALL Java_cvc5_Stat_deletePointer(JNIEnv*, - jclass, - jlong pointer) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Stat_deletePointer(JNIEnv*, + jclass, + jlong pointer) { delete reinterpret_cast<Stat*>(pointer); } /* - * Class: cvc5_Stat + * Class: io_github_cvc5_api_Stat * Method: toString * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Stat_toString(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Stat_toString(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -51,13 +50,13 @@ JNIEXPORT jstring JNICALL Java_cvc5_Stat_toString(JNIEnv* env, } /* - * Class: cvc5_Stat + * Class: io_github_cvc5_api_Stat * Method: isExpert * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Stat_isExpert(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Stat_isExpert(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Stat* current = reinterpret_cast<Stat*>(pointer); @@ -66,13 +65,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Stat_isExpert(JNIEnv* env, } /* - * Class: cvc5_Stat + * Class: io_github_cvc5_api_Stat * Method: isDefault * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Stat_isDefault(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Stat_isDefault(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Stat* current = reinterpret_cast<Stat*>(pointer); @@ -81,13 +80,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Stat_isDefault(JNIEnv* env, } /* - * Class: cvc5_Stat + * Class: io_github_cvc5_api_Stat * Method: isInt * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Stat_isInt(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Stat_isInt(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Stat* current = reinterpret_cast<Stat*>(pointer); @@ -96,13 +95,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Stat_isInt(JNIEnv* env, } /* - * Class: cvc5_Stat + * Class: io_github_cvc5_api_Stat * Method: getInt * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Stat_getInt(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Stat_getInt(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Stat* current = reinterpret_cast<Stat*>(pointer); @@ -111,13 +110,13 @@ JNIEXPORT jlong JNICALL Java_cvc5_Stat_getInt(JNIEnv* env, } /* - * Class: cvc5_Stat + * Class: io_github_cvc5_api_Stat * Method: isDouble * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Stat_isDouble(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Stat_isDouble(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Stat* current = reinterpret_cast<Stat*>(pointer); @@ -126,13 +125,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Stat_isDouble(JNIEnv* env, } /* - * Class: cvc5_Stat + * Class: io_github_cvc5_api_Stat * Method: getDouble * Signature: (J)D */ -JNIEXPORT jdouble JNICALL Java_cvc5_Stat_getDouble(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jdouble JNICALL Java_io_github_cvc5_api_Stat_getDouble(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Stat* current = reinterpret_cast<Stat*>(pointer); @@ -141,13 +140,13 @@ JNIEXPORT jdouble JNICALL Java_cvc5_Stat_getDouble(JNIEnv* env, } /* - * Class: cvc5_Stat + * Class: io_github_cvc5_api_Stat * Method: isString * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Stat_isString(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Stat_isString(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Stat* current = reinterpret_cast<Stat*>(pointer); @@ -156,13 +155,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Stat_isString(JNIEnv* env, } /* - * Class: cvc5_Stat + * Class: io_github_cvc5_api_Stat * Method: getString * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Stat_getString(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Stat_getString(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Stat* current = reinterpret_cast<Stat*>(pointer); @@ -171,13 +170,12 @@ JNIEXPORT jstring JNICALL Java_cvc5_Stat_getString(JNIEnv* env, } /* - * Class: cvc5_Stat + * Class: io_github_cvc5_api_Stat * Method: isHistogram * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Stat_isHistogram(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Stat_isHistogram(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Stat* current = reinterpret_cast<Stat*>(pointer); @@ -186,13 +184,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Stat_isHistogram(JNIEnv* env, } /* - * Class: cvc5_Stat + * Class: io_github_cvc5_api_Stat * Method: getHistogram * Signature: (J)Ljava/util/Map; */ -JNIEXPORT jobject JNICALL Java_cvc5_Stat_getHistogram(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jobject JNICALL +Java_io_github_cvc5_api_Stat_getHistogram(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Stat* current = reinterpret_cast<Stat*>(pointer); diff --git a/src/api/java/jni/cvc5_Statistics.cpp b/src/api/java/jni/statistics.cpp index 8db2e156a..827c3184a 100644 --- a/src/api/java/jni/cvc5_Statistics.cpp +++ b/src/api/java/jni/statistics.cpp @@ -13,34 +13,32 @@ * The cvc5 Java API. */ -#include "cvc5_Statistics.h" +#include <sstream> #include "api/cpp/cvc5.h" -#include "cvc5JavaApi.h" -#include <sstream> +#include "api_utilities.h" +#include "io_github_cvc5_api_Statistics.h" using namespace cvc5::api; /* - * Class: cvc5_Statistics + * Class: io_github_cvc5_api_Statistics * Method: deletePointer * Signature: (J)V */ -JNIEXPORT void JNICALL Java_cvc5_Statistics_deletePointer(JNIEnv*, - jclass, - jlong pointer) +JNIEXPORT void JNICALL +Java_io_github_cvc5_api_Statistics_deletePointer(JNIEnv*, jclass, jlong pointer) { delete reinterpret_cast<Statistics*>(pointer); } /* - * Class: cvc5_Statistics + * Class: io_github_cvc5_api_Statistics * Method: toString * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Statistics_toString(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL +Java_io_github_cvc5_api_Statistics_toString(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -52,14 +50,14 @@ JNIEXPORT jstring JNICALL Java_cvc5_Statistics_toString(JNIEnv* env, } /* - * Class: cvc5_Statistics + * Class: io_github_cvc5_api_Statistics * Method: get * Signature: (JLjava/lang/String;)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Statistics_get(JNIEnv* env, - jobject, - jlong pointer, - jstring jName) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Statistics_get(JNIEnv* env, + jobject, + jlong pointer, + jstring jName) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Statistics* current = reinterpret_cast<Statistics*>(pointer); @@ -72,13 +70,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Statistics_get(JNIEnv* env, } /* - * Class: cvc5_Statistics + * Class: io_github_cvc5_api_Statistics * Method: getIterator * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Statistics_getIterator(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Statistics_getIterator( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Statistics* current = reinterpret_cast<Statistics*>(pointer); @@ -89,14 +86,12 @@ JNIEXPORT jlong JNICALL Java_cvc5_Statistics_getIterator(JNIEnv* env, } /* - * Class: cvc5_Statistics + * Class: io_github_cvc5_api_Statistics * Method: hasNext * Signature: (JJ)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Statistics_hasNext(JNIEnv* env, - jobject, - jlong pointer, - jlong iteratorPointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Statistics_hasNext( + JNIEnv* env, jobject, jlong pointer, jlong iteratorPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Statistics* current = reinterpret_cast<Statistics*>(pointer); @@ -107,14 +102,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Statistics_hasNext(JNIEnv* env, } /* - * Class: cvc5_Statistics + * Class: io_github_cvc5_api_Statistics * Method: getNext - * Signature: (JJ)Lcvc5/Pair; + * Signature: (JJ)Lio/github/cvc5/api/Pair; */ -JNIEXPORT jobject JNICALL Java_cvc5_Statistics_getNext(JNIEnv* env, - jobject, - jlong, - jlong iteratorPointer) +JNIEXPORT jobject JNICALL Java_io_github_cvc5_api_Statistics_getNext( + JNIEnv* env, jobject, jlong, jlong iteratorPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Statistics::iterator it = @@ -130,7 +123,7 @@ JNIEXPORT jobject JNICALL Java_cvc5_Statistics_getNext(JNIEnv* env, jobject longObject = env->NewObject(longClass, longConstructor, statPointer); // Pair<String, Long> pair = new Pair<String, Long>(jName, longObject) - jclass pairClass = env->FindClass("Lcvc5/Pair;"); + jclass pairClass = env->FindClass("Lio/github/cvc5/api/Pair;"); jmethodID pairConstructor = env->GetMethodID( pairClass, "<init>", "(Ljava/lang/Object;Ljava/lang/Object;)V"); jobject pair = env->NewObject(pairClass, pairConstructor, jName, longObject); @@ -141,14 +134,12 @@ JNIEXPORT jobject JNICALL Java_cvc5_Statistics_getNext(JNIEnv* env, } /* - * Class: cvc5_Statistics + * Class: io_github_cvc5_api_Statistics * Method: increment * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Statistics_increment(JNIEnv* env, - jobject, - jlong pointer, - jlong iteratorPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Statistics_increment( + JNIEnv* env, jobject, jlong pointer, jlong iteratorPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Statistics* current = reinterpret_cast<Statistics*>(pointer); @@ -169,11 +160,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Statistics_increment(JNIEnv* env, } /* - * Class: cvc5_Statistics + * Class: io_github_cvc5_api_Statistics * Method: deleteIteratorPointer * Signature: (J)V */ -JNIEXPORT void JNICALL Java_cvc5_Statistics_deleteIteratorPointer( +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Statistics_deleteIteratorPointer( JNIEnv*, jobject, jlong iteratorPointer) { delete reinterpret_cast<Statistics::iterator*>(iteratorPointer); diff --git a/src/api/java/jni/cvc5_Term.cpp b/src/api/java/jni/term.cpp index 325a9c744..5c8300e17 100644 --- a/src/api/java/jni/cvc5_Term.cpp +++ b/src/api/java/jni/term.cpp @@ -13,34 +13,33 @@ * The cvc5 Java API. */ -#include "cvc5_Term.h" - #include "api/cpp/cvc5.h" -#include "cvc5JavaApi.h" +#include "api_utilities.h" +#include "io_github_cvc5_api_Term.h" using namespace cvc5::api; /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: deletePointer * Signature: (J)V */ -JNIEXPORT void JNICALL Java_cvc5_Term_deletePointer(JNIEnv* env, - jclass, - jlong pointer) +JNIEXPORT void JNICALL Java_io_github_cvc5_api_Term_deletePointer(JNIEnv* env, + jclass, + jlong pointer) { delete reinterpret_cast<Term*>(pointer); } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: equals * Signature: (JJ)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_equals(JNIEnv* env, - jobject, - jlong pointer1, - jlong pointer2) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_equals(JNIEnv* env, + jobject, + jlong pointer1, + jlong pointer2) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* term1 = reinterpret_cast<Term*>(pointer1); @@ -51,14 +50,14 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_equals(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: compareTo * Signature: (JJ)I */ -JNIEXPORT jint JNICALL Java_cvc5_Term_compareTo(JNIEnv* env, - jobject, - jlong pointer1, - jlong pointer2) +JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Term_compareTo(JNIEnv* env, + jobject, + jlong pointer1, + jlong pointer2) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* term1 = reinterpret_cast<Term*>(pointer1); @@ -76,13 +75,12 @@ JNIEXPORT jint JNICALL Java_cvc5_Term_compareTo(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: getNumChildren * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Term_getNumChildren(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL +Java_io_github_cvc5_api_Term_getNumChildren(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -91,14 +89,14 @@ JNIEXPORT jint JNICALL Java_cvc5_Term_getNumChildren(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: getChild * Signature: (JI)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Term_getChild(JNIEnv* env, - jobject, - jlong pointer, - jint index) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_getChild(JNIEnv* env, + jobject, + jlong pointer, + jint index) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -108,13 +106,13 @@ JNIEXPORT jlong JNICALL Java_cvc5_Term_getChild(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: getId * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Term_getId(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_getId(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -123,13 +121,13 @@ JNIEXPORT jlong JNICALL Java_cvc5_Term_getId(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: getKind * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Term_getKind(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Term_getKind(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -138,13 +136,13 @@ JNIEXPORT jint JNICALL Java_cvc5_Term_getKind(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: getSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Term_getSort(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_getSort(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -154,15 +152,16 @@ JNIEXPORT jlong JNICALL Java_cvc5_Term_getSort(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: substitute * Signature: (JJJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Term_substitute__JJJ(JNIEnv* env, - jobject, - jlong pointer, - jlong termPointer, - jlong replacementPointer) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Term_substitute__JJJ(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer, + jlong replacementPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -174,16 +173,16 @@ JNIEXPORT jlong JNICALL Java_cvc5_Term_substitute__JJJ(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: substitute * Signature: (J[J[J)J */ JNIEXPORT jlong JNICALL -Java_cvc5_Term_substitute__J_3J_3J(JNIEnv* env, - jobject, - jlong pointer, - jlongArray termPointers, - jlongArray replacementPointers) +Java_io_github_cvc5_api_Term_substitute__J_3J_3J(JNIEnv* env, + jobject, + jlong pointer, + jlongArray termPointers, + jlongArray replacementPointers) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -216,13 +215,13 @@ Java_cvc5_Term_substitute__J_3J_3J(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: hasOp * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_hasOp(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_hasOp(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -231,13 +230,13 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_hasOp(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: getOp * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Term_getOp(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_getOp(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -247,13 +246,13 @@ JNIEXPORT jlong JNICALL Java_cvc5_Term_getOp(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: isNull * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isNull(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isNull(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -262,13 +261,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isNull(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: isConstArray * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isConstArray(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Term_isConstArray(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -277,13 +275,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isConstArray(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: getConstArrayBase * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Term_getConstArrayBase(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_getConstArrayBase( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -293,13 +290,13 @@ JNIEXPORT jlong JNICALL Java_cvc5_Term_getConstArrayBase(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: notTerm * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Term_notTerm(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_notTerm(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -309,14 +306,14 @@ JNIEXPORT jlong JNICALL Java_cvc5_Term_notTerm(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: andTerm * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Term_andTerm(JNIEnv* env, - jobject, - jlong pointer, - jlong termPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_andTerm(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -327,14 +324,14 @@ JNIEXPORT jlong JNICALL Java_cvc5_Term_andTerm(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: orTerm * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Term_orTerm(JNIEnv* env, - jobject, - jlong pointer, - jlong termPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_orTerm(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -345,14 +342,14 @@ JNIEXPORT jlong JNICALL Java_cvc5_Term_orTerm(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: xorTerm * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Term_xorTerm(JNIEnv* env, - jobject, - jlong pointer, - jlong termPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_xorTerm(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -363,14 +360,14 @@ JNIEXPORT jlong JNICALL Java_cvc5_Term_xorTerm(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: eqTerm * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Term_eqTerm(JNIEnv* env, - jobject, - jlong pointer, - jlong termPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_eqTerm(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -381,14 +378,14 @@ JNIEXPORT jlong JNICALL Java_cvc5_Term_eqTerm(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: impTerm * Signature: (JJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Term_impTerm(JNIEnv* env, - jobject, - jlong pointer, - jlong termPointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_impTerm(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -399,11 +396,11 @@ JNIEXPORT jlong JNICALL Java_cvc5_Term_impTerm(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: iteTerm * Signature: (JJJ)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Term_iteTerm( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_iteTerm( JNIEnv* env, jobject, jlong pointer, jlong thenPointer, jlong elsePointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -416,13 +413,13 @@ JNIEXPORT jlong JNICALL Java_cvc5_Term_iteTerm( } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: toString * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Term_toString(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_toString(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -431,13 +428,12 @@ JNIEXPORT jstring JNICALL Java_cvc5_Term_toString(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: isIntegerValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isIntegerValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Term_isIntegerValue(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -446,13 +442,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isIntegerValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: getIntegerValue * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Term_getIntegerValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_getIntegerValue( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -463,13 +458,12 @@ JNIEXPORT jstring JNICALL Java_cvc5_Term_getIntegerValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: isStringValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isStringValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Term_isStringValue(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -478,13 +472,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isStringValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: getStringValue * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Term_getStringValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL +Java_io_github_cvc5_api_Term_getStringValue(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -504,13 +497,12 @@ JNIEXPORT jstring JNICALL Java_cvc5_Term_getStringValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: isRealValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isRealValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Term_isRealValue(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -519,13 +511,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isRealValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: getRealValue * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Term_getRealValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL +Java_io_github_cvc5_api_Term_getRealValue(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -535,13 +526,12 @@ JNIEXPORT jstring JNICALL Java_cvc5_Term_getRealValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: isBooleanValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isBooleanValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Term_isBooleanValue(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -550,13 +540,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isBooleanValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: getBooleanValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_getBooleanValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_getBooleanValue( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -565,13 +554,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_getBooleanValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: isBitVectorValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isBitVectorValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isBitVectorValue( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -580,14 +568,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isBitVectorValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: getBitVectorValue * Signature: (JI)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Term_getBitVectorValue(JNIEnv* env, - jobject, - jlong pointer, - jint base) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_getBitVectorValue( + JNIEnv* env, jobject, jlong pointer, jint base) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -598,13 +584,12 @@ JNIEXPORT jstring JNICALL Java_cvc5_Term_getBitVectorValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: isAbstractValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isAbstractValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isAbstractValue( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -613,13 +598,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isAbstractValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: getAbstractValue * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_cvc5_Term_getAbstractValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_getAbstractValue( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -629,13 +613,12 @@ JNIEXPORT jstring JNICALL Java_cvc5_Term_getAbstractValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: isTupleValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isTupleValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Term_isTupleValue(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -644,13 +627,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isTupleValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: getTupleValue * Signature: (J)[J */ -JNIEXPORT jlongArray JNICALL Java_cvc5_Term_getTupleValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlongArray JNICALL +Java_io_github_cvc5_api_Term_getTupleValue(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -661,13 +643,12 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Term_getTupleValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: isFloatingPointPosZero * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointPosZero(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isFloatingPointPosZero( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -676,13 +657,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointPosZero(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: isFloatingPointNegZero * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointNegZero(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isFloatingPointNegZero( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -691,13 +671,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointNegZero(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: isFloatingPointPosInf * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointPosInf(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isFloatingPointPosInf( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -706,13 +685,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointPosInf(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: isFloatingPointNegInf * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointNegInf(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isFloatingPointNegInf( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -721,13 +699,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointNegInf(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: isFloatingPointNaN * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointNaN(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isFloatingPointNaN( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -736,13 +713,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointNaN(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: isFloatingPointValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isFloatingPointValue( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -751,11 +727,11 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isFloatingPointValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: getFloatingPointValue - * Signature: (J)Lcvc5/Triplet; + * Signature: (J)Lio/github/cvc5/api/Triplet; */ -JNIEXPORT jobject JNICALL Java_cvc5_Term_getFloatingPointValue( +JNIEXPORT jobject JNICALL Java_io_github_cvc5_api_Term_getFloatingPointValue( JNIEnv* env, jobject thisObject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -771,7 +747,7 @@ JNIEXPORT jobject JNICALL Java_cvc5_Term_getFloatingPointValue( jobject t = env->NewObject(longClass, longConstructor, termPointer); // Triplet triplet = new Triplet<Long, Long, Long>(e, s, t); - jclass tripletClass = env->FindClass("Lcvc5/Triplet;"); + jclass tripletClass = env->FindClass("Lio/github/cvc5/api/Triplet;"); jmethodID tripletConstructor = env->GetMethodID( tripletClass, "<init>", @@ -783,13 +759,12 @@ JNIEXPORT jobject JNICALL Java_cvc5_Term_getFloatingPointValue( } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: isSetValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isSetValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Term_isSetValue(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -798,13 +773,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isSetValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: getSetValue * Signature: (J)[J */ -JNIEXPORT jlongArray JNICALL Java_cvc5_Term_getSetValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlongArray JNICALL +Java_io_github_cvc5_api_Term_getSetValue(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -823,13 +797,12 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Term_getSetValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: isSequenceValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isSequenceValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isSequenceValue( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -838,13 +811,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isSequenceValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: getSequenceValue * Signature: (J)[J */ -JNIEXPORT jlongArray JNICALL Java_cvc5_Term_getSequenceValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Term_getSequenceValue( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -855,13 +827,12 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Term_getSequenceValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: isUninterpretedValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isUninterpretedValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isUninterpretedValue( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -870,13 +841,12 @@ JNIEXPORT jboolean JNICALL Java_cvc5_Term_isUninterpretedValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: getUninterpretedValue - * Signature: (J)Lcvc5/Pair; + * Signature: (J)Lio/github/cvc5/api/Pair; */ -JNIEXPORT jobject JNICALL Java_cvc5_Term_getUninterpretedValue(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jobject JNICALL Java_io_github_cvc5_api_Term_getUninterpretedValue( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); @@ -898,7 +868,7 @@ JNIEXPORT jobject JNICALL Java_cvc5_Term_getUninterpretedValue(JNIEnv* env, integerClass, integerConstructor, static_cast<jint>(value.second)); // Pair<String, Long> pair = new Pair<String, Long>(jName, longObject) - jclass pairClass = env->FindClass("Lcvc5/Pair;"); + jclass pairClass = env->FindClass("Lio/github/cvc5/api/Pair;"); jmethodID pairConstructor = env->GetMethodID( pairClass, "<init>", "(Ljava/lang/Object;Ljava/lang/Object;)V"); jobject pair = @@ -909,13 +879,13 @@ JNIEXPORT jobject JNICALL Java_cvc5_Term_getUninterpretedValue(JNIEnv* env, } /* - * Class: cvc5_Term + * Class: io_github_cvc5_api_Term * Method: iterator * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_cvc5_Term_iterator(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_iterator(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast<Term*>(pointer); |