Support get-abduct-next (#7850)

[cvc5.git] / src / api / java / jni / term.cpp

diff --git a/src/api/java/jni/term.cpp b/src/api/java/jni/term.cpp
index 5c8300e17a429c611fd4b435cd2b2deaad99b397..1e8669873eb1938db1b75411df1acbee4cc2ccb3 100644 (file)
--- a/src/api/java/jni/term.cpp
+++ b/src/api/java/jni/term.cpp
@@ -25,7 +25,7 @@ using namespace cvc5::api;
  * Signature: (J)V
  */
 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Term_deletePointer(JNIEnv* env,
-                                                                  jclass,
+                                                                  jobject,
                                                                   jlong pointer)
 {
   delete reinterpret_cast<Term*>(pointer);
@@ -245,6 +245,36 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_getOp(JNIEnv* env,
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
+/*
+ * Class:     io_github_cvc5_api_Term
+ * Method:    hasSymbol
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_hasSymbol(JNIEnv* env,
+                                                                  jobject,
+                                                                  jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->hasSymbol());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     io_github_cvc5_api_Term
+ * Method:    getSymbol
+ * Signature: (J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_getSymbol(JNIEnv* env,
+                                                                 jobject,
+                                                                 jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return env->NewStringUTF(current->getSymbol().c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
 /*
  * Class:     io_github_cvc5_api_Term
  * Method:    isNull
@@ -427,6 +457,22 @@ JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_toString(JNIEnv* env,
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 }
 
+/*
+ * Class:     io_github_cvc5_api_Term
+ * Method:    getRealOrIntegerValueSign
+ * Signature: (J)Z
+ */
+JNIEXPORT jint JNICALL
+Java_io_github_cvc5_api_Term_getRealOrIntegerValueSign(JNIEnv* env,
+                                                       jobject,
+                                                       jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jint>(current->getRealOrIntegerValueSign());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jint>(0));
+}
+
 /*
  * Class:     io_github_cvc5_api_Term
  * Method:    isIntegerValue