src/api/java/jni/term.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Mudathir Mohamed
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * The cvc5 Java API.
  14  */
  15
  16 #include "api/cpp/cvc5.h"
  17 #include "api_utilities.h"
  18 #include "io_github_cvc5_api_Term.h"
  19
  20 using namespace cvc5::api;
  21
  22 /*
  23  * Class:     io_github_cvc5_api_Term
  24  * Method:    deletePointer
  25  * Signature: (J)V
  26  */
  27 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Term_deletePointer(JNIEnv* env,
  28                                                                   jobject,
  29                                                                   jlong pointer)
  30 {
  31   delete reinterpret_cast<Term*>(pointer);
  32 }
  33
  34 /*
  35  * Class:     io_github_cvc5_api_Term
  36  * Method:    equals
  37  * Signature: (JJ)Z
  38  */
  39 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_equals(JNIEnv* env,
  40                                                                jobject,
  41                                                                jlong pointer1,
  42                                                                jlong pointer2)
  43 {
  44   CVC5_JAVA_API_TRY_CATCH_BEGIN;
  45   Term* term1 = reinterpret_cast<Term*>(pointer1);
  46   Term* term2 = reinterpret_cast<Term*>(pointer2);
  47   // We compare the actual terms, not their pointers.
  48   return static_cast<jboolean>(*term1 == *term2);
  49   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
  50 }
  51
  52 /*
  53  * Class:     io_github_cvc5_api_Term
  54  * Method:    compareTo
  55  * Signature: (JJ)I
  56  */
  57 JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Term_compareTo(JNIEnv* env,
  58                                                               jobject,
  59                                                               jlong pointer1,
  60                                                               jlong pointer2)
  61 {
  62   CVC5_JAVA_API_TRY_CATCH_BEGIN;
  63   Term* term1 = reinterpret_cast<Term*>(pointer1);
  64   Term* term2 = reinterpret_cast<Term*>(pointer2);
  65   if (*term1 < *term2)
  66   {
  67     return static_cast<jint>(-1);
  68   }
  69   if (*term1 == *term2)
  70   {
  71     return 0;
  72   }
  73   return static_cast<jint>(1);
  74   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
  75 }
  76
  77 /*
  78  * Class:     io_github_cvc5_api_Term
  79  * Method:    getNumChildren
  80  * Signature: (J)I
  81  */
  82 JNIEXPORT jint JNICALL
  83 Java_io_github_cvc5_api_Term_getNumChildren(JNIEnv* env, jobject, jlong pointer)
  84 {
  85   CVC5_JAVA_API_TRY_CATCH_BEGIN;
  86   Term* current = reinterpret_cast<Term*>(pointer);
  87   return static_cast<jint>(current->getNumChildren());
  88   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
  89 }
  90
  91 /*
  92  * Class:     io_github_cvc5_api_Term
  93  * Method:    getChild
  94  * Signature: (JI)J
  95  */
  96 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_getChild(JNIEnv* env,
  97                                                               jobject,
  98                                                               jlong pointer,
  99                                                               jint index)
 100 {
 101   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 102   Term* current = reinterpret_cast<Term*>(pointer);
 103   Term* ret = new Term((*current)[static_cast<size_t>(index)]);
 104   return reinterpret_cast<jlong>(ret);
 105   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 106 }
 107
 108 /*
 109  * Class:     io_github_cvc5_api_Term
 110  * Method:    getId
 111  * Signature: (J)J
 112  */
 113 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_getId(JNIEnv* env,
 114                                                            jobject,
 115                                                            jlong pointer)
 116 {
 117   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 118   Term* current = reinterpret_cast<Term*>(pointer);
 119   return static_cast<jlong>(current->getId());
 120   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 121 }
 122
 123 /*
 124  * Class:     io_github_cvc5_api_Term
 125  * Method:    getKind
 126  * Signature: (J)I
 127  */
 128 JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Term_getKind(JNIEnv* env,
 129                                                             jobject,
 130                                                             jlong pointer)
 131 {
 132   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 133   Term* current = reinterpret_cast<Term*>(pointer);
 134   return static_cast<jint>(current->getKind());
 135   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 136 }
 137
 138 /*
 139  * Class:     io_github_cvc5_api_Term
 140  * Method:    getSort
 141  * Signature: (J)J
 142  */
 143 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_getSort(JNIEnv* env,
 144                                                              jobject,
 145                                                              jlong pointer)
 146 {
 147   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 148   Term* current = reinterpret_cast<Term*>(pointer);
 149   Sort* ret = new Sort(current->getSort());
 150   return reinterpret_cast<jlong>(ret);
 151   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 152 }
 153
 154 /*
 155  * Class:     io_github_cvc5_api_Term
 156  * Method:    substitute
 157  * Signature: (JJJ)J
 158  */
 159 JNIEXPORT jlong JNICALL
 160 Java_io_github_cvc5_api_Term_substitute__JJJ(JNIEnv* env,
 161                                              jobject,
 162                                              jlong pointer,
 163                                              jlong termPointer,
 164                                              jlong replacementPointer)
 165 {
 166   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 167   Term* current = reinterpret_cast<Term*>(pointer);
 168   Term* term = reinterpret_cast<Term*>(termPointer);
 169   Term* replacement = reinterpret_cast<Term*>(replacementPointer);
 170   Term* ret = new Term(current->substitute(*term, *replacement));
 171   return reinterpret_cast<jlong>(ret);
 172   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 173 }
 174
 175 /*
 176  * Class:     io_github_cvc5_api_Term
 177  * Method:    substitute
 178  * Signature: (J[J[J)J
 179  */
 180 JNIEXPORT jlong JNICALL
 181 Java_io_github_cvc5_api_Term_substitute__J_3J_3J(JNIEnv* env,
 182                                                  jobject,
 183                                                  jlong pointer,
 184                                                  jlongArray termPointers,
 185                                                  jlongArray replacementPointers)
 186 {
 187   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 188   Term* current = reinterpret_cast<Term*>(pointer);
 189   jsize termsSize = env->GetArrayLength(termPointers);
 190   jsize replacementsSize = env->GetArrayLength(replacementPointers);
 191   jlong* termElements = env->GetLongArrayElements(termPointers, nullptr);
 192   jlong* replacementElements =
 193       env->GetLongArrayElements(replacementPointers, nullptr);
 194
 195   std::vector<Term> terms(termsSize);
 196   std::vector<Term> replacements(replacementsSize);
 197
 198   for (jsize i = 0; i < termsSize; i++)
 199   {
 200     Term* term = (Term*)termElements[i];
 201     terms[i] = *term;
 202   }
 203   env->ReleaseLongArrayElements(termPointers, termElements, 0);
 204
 205   for (jsize i = 0; i < replacementsSize; i++)
 206   {
 207     Term* term = (Term*)replacementElements[i];
 208     replacements[i] = *term;
 209   }
 210   env->ReleaseLongArrayElements(replacementPointers, replacementElements, 0);
 211
 212   Term* ret = new Term(current->substitute(terms, replacements));
 213   return reinterpret_cast<jlong>(ret);
 214   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 215 }
 216
 217 /*
 218  * Class:     io_github_cvc5_api_Term
 219  * Method:    hasOp
 220  * Signature: (J)Z
 221  */
 222 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_hasOp(JNIEnv* env,
 223                                                               jobject,
 224                                                               jlong pointer)
 225 {
 226   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 227   Term* current = reinterpret_cast<Term*>(pointer);
 228   return static_cast<jboolean>(current->hasOp());
 229   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 230 }
 231
 232 /*
 233  * Class:     io_github_cvc5_api_Term
 234  * Method:    getOp
 235  * Signature: (J)J
 236  */
 237 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_getOp(JNIEnv* env,
 238                                                            jobject,
 239                                                            jlong pointer)
 240 {
 241   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 242   Term* current = reinterpret_cast<Term*>(pointer);
 243   Op* ret = new Op(current->getOp());
 244   return reinterpret_cast<jlong>(ret);
 245   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 246 }
 247
 248 /*
 249  * Class:     io_github_cvc5_api_Term
 250  * Method:    hasSymbol
 251  * Signature: (J)Z
 252  */
 253 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_hasSymbol(JNIEnv* env,
 254                                                                   jobject,
 255                                                                   jlong pointer)
 256 {
 257   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 258   Term* current = reinterpret_cast<Term*>(pointer);
 259   return static_cast<jboolean>(current->hasSymbol());
 260   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 261 }
 262
 263 /*
 264  * Class:     io_github_cvc5_api_Term
 265  * Method:    getSymbol
 266  * Signature: (J)Ljava/lang/String;
 267  */
 268 JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_getSymbol(JNIEnv* env,
 269                                                                  jobject,
 270                                                                  jlong pointer)
 271 {
 272   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 273   Term* current = reinterpret_cast<Term*>(pointer);
 274   return env->NewStringUTF(current->getSymbol().c_str());
 275   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 276 }
 277
 278 /*
 279  * Class:     io_github_cvc5_api_Term
 280  * Method:    isNull
 281  * Signature: (J)Z
 282  */
 283 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isNull(JNIEnv* env,
 284                                                                jobject,
 285                                                                jlong pointer)
 286 {
 287   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 288   Term* current = reinterpret_cast<Term*>(pointer);
 289   return static_cast<jboolean>(current->isNull());
 290   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 291 }
 292
 293 /*
 294  * Class:     io_github_cvc5_api_Term
 295  * Method:    isConstArray
 296  * Signature: (J)Z
 297  */
 298 JNIEXPORT jboolean JNICALL
 299 Java_io_github_cvc5_api_Term_isConstArray(JNIEnv* env, jobject, jlong pointer)
 300 {
 301   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 302   Term* current = reinterpret_cast<Term*>(pointer);
 303   return static_cast<jboolean>(current->isConstArray());
 304   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 305 }
 306
 307 /*
 308  * Class:     io_github_cvc5_api_Term
 309  * Method:    getConstArrayBase
 310  * Signature: (J)J
 311  */
 312 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_getConstArrayBase(
 313     JNIEnv* env, jobject, jlong pointer)
 314 {
 315   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 316   Term* current = reinterpret_cast<Term*>(pointer);
 317   Term* ret = new Term(current->getConstArrayBase());
 318   return reinterpret_cast<jlong>(ret);
 319   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 320 }
 321
 322 /*
 323  * Class:     io_github_cvc5_api_Term
 324  * Method:    notTerm
 325  * Signature: (J)J
 326  */
 327 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_notTerm(JNIEnv* env,
 328                                                              jobject,
 329                                                              jlong pointer)
 330 {
 331   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 332   Term* current = reinterpret_cast<Term*>(pointer);
 333   Term* ret = new Term(current->notTerm());
 334   return reinterpret_cast<jlong>(ret);
 335   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 336 }
 337
 338 /*
 339  * Class:     io_github_cvc5_api_Term
 340  * Method:    andTerm
 341  * Signature: (JJ)J
 342  */
 343 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_andTerm(JNIEnv* env,
 344                                                              jobject,
 345                                                              jlong pointer,
 346                                                              jlong termPointer)
 347 {
 348   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 349   Term* current = reinterpret_cast<Term*>(pointer);
 350   Term* term = reinterpret_cast<Term*>(termPointer);
 351   Term* ret = new Term(current->andTerm(*term));
 352   return reinterpret_cast<jlong>(ret);
 353   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 354 }
 355
 356 /*
 357  * Class:     io_github_cvc5_api_Term
 358  * Method:    orTerm
 359  * Signature: (JJ)J
 360  */
 361 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_orTerm(JNIEnv* env,
 362                                                             jobject,
 363                                                             jlong pointer,
 364                                                             jlong termPointer)
 365 {
 366   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 367   Term* current = reinterpret_cast<Term*>(pointer);
 368   Term* term = reinterpret_cast<Term*>(termPointer);
 369   Term* ret = new Term(current->orTerm(*term));
 370   return reinterpret_cast<jlong>(ret);
 371   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 372 }
 373
 374 /*
 375  * Class:     io_github_cvc5_api_Term
 376  * Method:    xorTerm
 377  * Signature: (JJ)J
 378  */
 379 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_xorTerm(JNIEnv* env,
 380                                                              jobject,
 381                                                              jlong pointer,
 382                                                              jlong termPointer)
 383 {
 384   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 385   Term* current = reinterpret_cast<Term*>(pointer);
 386   Term* term = reinterpret_cast<Term*>(termPointer);
 387   Term* ret = new Term(current->xorTerm(*term));
 388   return reinterpret_cast<jlong>(ret);
 389   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 390 }
 391
 392 /*
 393  * Class:     io_github_cvc5_api_Term
 394  * Method:    eqTerm
 395  * Signature: (JJ)J
 396  */
 397 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_eqTerm(JNIEnv* env,
 398                                                             jobject,
 399                                                             jlong pointer,
 400                                                             jlong termPointer)
 401 {
 402   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 403   Term* current = reinterpret_cast<Term*>(pointer);
 404   Term* term = reinterpret_cast<Term*>(termPointer);
 405   Term* ret = new Term(current->eqTerm(*term));
 406   return reinterpret_cast<jlong>(ret);
 407   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 408 }
 409
 410 /*
 411  * Class:     io_github_cvc5_api_Term
 412  * Method:    impTerm
 413  * Signature: (JJ)J
 414  */
 415 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_impTerm(JNIEnv* env,
 416                                                              jobject,
 417                                                              jlong pointer,
 418                                                              jlong termPointer)
 419 {
 420   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 421   Term* current = reinterpret_cast<Term*>(pointer);
 422   Term* term = reinterpret_cast<Term*>(termPointer);
 423   Term* ret = new Term(current->impTerm(*term));
 424   return reinterpret_cast<jlong>(ret);
 425   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 426 }
 427
 428 /*
 429  * Class:     io_github_cvc5_api_Term
 430  * Method:    iteTerm
 431  * Signature: (JJJ)J
 432  */
 433 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_iteTerm(
 434     JNIEnv* env, jobject, jlong pointer, jlong thenPointer, jlong elsePointer)
 435 {
 436   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 437   Term* current = reinterpret_cast<Term*>(pointer);
 438   Term* thenTerm = reinterpret_cast<Term*>(thenPointer);
 439   Term* elseTerm = reinterpret_cast<Term*>(elsePointer);
 440   Term* ret = new Term(current->iteTerm(*thenTerm, *elseTerm));
 441   return reinterpret_cast<jlong>(ret);
 442   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 443 }
 444
 445 /*
 446  * Class:     io_github_cvc5_api_Term
 447  * Method:    toString
 448  * Signature: (J)Ljava/lang/String;
 449  */
 450 JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_toString(JNIEnv* env,
 451                                                                 jobject,
 452                                                                 jlong pointer)
 453 {
 454   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 455   Term* current = reinterpret_cast<Term*>(pointer);
 456   return env->NewStringUTF(current->toString().c_str());
 457   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 458 }
 459
 460 /*
 461  * Class:     io_github_cvc5_api_Term
 462  * Method:    getRealOrIntegerValueSign
 463  * Signature: (J)Z
 464  */
 465 JNIEXPORT jint JNICALL
 466 Java_io_github_cvc5_api_Term_getRealOrIntegerValueSign(JNIEnv* env,
 467                                                        jobject,
 468                                                        jlong pointer)
 469 {
 470   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 471   Term* current = reinterpret_cast<Term*>(pointer);
 472   return static_cast<jint>(current->getRealOrIntegerValueSign());
 473   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jint>(0));
 474 }
 475
 476 /*
 477  * Class:     io_github_cvc5_api_Term
 478  * Method:    isIntegerValue
 479  * Signature: (J)Z
 480  */
 481 JNIEXPORT jboolean JNICALL
 482 Java_io_github_cvc5_api_Term_isIntegerValue(JNIEnv* env, jobject, jlong pointer)
 483 {
 484   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 485   Term* current = reinterpret_cast<Term*>(pointer);
 486   return static_cast<jboolean>(current->isIntegerValue());
 487   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 488 }
 489
 490 /*
 491  * Class:     io_github_cvc5_api_Term
 492  * Method:    getIntegerValue
 493  * Signature: (J)Ljava/lang/String;
 494  */
 495 JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_getIntegerValue(
 496     JNIEnv* env, jobject, jlong pointer)
 497 {
 498   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 499   Term* current = reinterpret_cast<Term*>(pointer);
 500   std::string value = current->getIntegerValue();
 501   jstring ret = env->NewStringUTF(value.c_str());
 502   return ret;
 503   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 504 }
 505
 506 /*
 507  * Class:     io_github_cvc5_api_Term
 508  * Method:    isStringValue
 509  * Signature: (J)Z
 510  */
 511 JNIEXPORT jboolean JNICALL
 512 Java_io_github_cvc5_api_Term_isStringValue(JNIEnv* env, jobject, jlong pointer)
 513 {
 514   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 515   Term* current = reinterpret_cast<Term*>(pointer);
 516   return static_cast<jboolean>(current->isStringValue());
 517   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 518 }
 519
 520 /*
 521  * Class:     io_github_cvc5_api_Term
 522  * Method:    getStringValue
 523  * Signature: (J)Ljava/lang/String;
 524  */
 525 JNIEXPORT jstring JNICALL
 526 Java_io_github_cvc5_api_Term_getStringValue(JNIEnv* env, jobject, jlong pointer)
 527 {
 528   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 529   Term* current = reinterpret_cast<Term*>(pointer);
 530   std::wstring termString = current->getStringValue();
 531
 532   size_t length = termString.length();
 533   jchar* unicode = new jchar[length];
 534   const wchar_t* s = termString.c_str();
 535   for (size_t i = 0; i < length; i++)
 536   {
 537     unicode[i] = s[i];
 538   }
 539   jstring ret = env->NewString(unicode, length);
 540   delete[] unicode;
 541   return ret;
 542   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 543 }
 544
 545 /*
 546  * Class:     io_github_cvc5_api_Term
 547  * Method:    isRealValue
 548  * Signature: (J)Z
 549  */
 550 JNIEXPORT jboolean JNICALL
 551 Java_io_github_cvc5_api_Term_isRealValue(JNIEnv* env, jobject, jlong pointer)
 552 {
 553   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 554   Term* current = reinterpret_cast<Term*>(pointer);
 555   return static_cast<jboolean>(current->isRealValue());
 556   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 557 }
 558
 559 /*
 560  * Class:     io_github_cvc5_api_Term
 561  * Method:    getRealValue
 562  * Signature: (J)Ljava/lang/String;
 563  */
 564 JNIEXPORT jstring JNICALL
 565 Java_io_github_cvc5_api_Term_getRealValue(JNIEnv* env, jobject, jlong pointer)
 566 {
 567   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 568   Term* current = reinterpret_cast<Term*>(pointer);
 569   std::string realValue = current->getRealValue();
 570   return env->NewStringUTF(realValue.c_str());
 571   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 572 }
 573
 574 /*
 575  * Class:     io_github_cvc5_api_Term
 576  * Method:    isBooleanValue
 577  * Signature: (J)Z
 578  */
 579 JNIEXPORT jboolean JNICALL
 580 Java_io_github_cvc5_api_Term_isBooleanValue(JNIEnv* env, jobject, jlong pointer)
 581 {
 582   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 583   Term* current = reinterpret_cast<Term*>(pointer);
 584   return static_cast<jboolean>(current->isBooleanValue());
 585   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 586 }
 587
 588 /*
 589  * Class:     io_github_cvc5_api_Term
 590  * Method:    getBooleanValue
 591  * Signature: (J)Z
 592  */
 593 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_getBooleanValue(
 594     JNIEnv* env, jobject, jlong pointer)
 595 {
 596   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 597   Term* current = reinterpret_cast<Term*>(pointer);
 598   return static_cast<jboolean>(current->getBooleanValue());
 599   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 600 }
 601
 602 /*
 603  * Class:     io_github_cvc5_api_Term
 604  * Method:    isBitVectorValue
 605  * Signature: (J)Z
 606  */
 607 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isBitVectorValue(
 608     JNIEnv* env, jobject, jlong pointer)
 609 {
 610   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 611   Term* current = reinterpret_cast<Term*>(pointer);
 612   return static_cast<jboolean>(current->isBitVectorValue());
 613   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 614 }
 615
 616 /*
 617  * Class:     io_github_cvc5_api_Term
 618  * Method:    getBitVectorValue
 619  * Signature: (JI)Ljava/lang/String;
 620  */
 621 JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_getBitVectorValue(
 622     JNIEnv* env, jobject, jlong pointer, jint base)
 623 {
 624   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 625   Term* current = reinterpret_cast<Term*>(pointer);
 626   std::string ret =
 627       current->getBitVectorValue(static_cast<std::uint32_t>(base));
 628   return env->NewStringUTF(ret.c_str());
 629   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 630 }
 631
 632 /*
 633  * Class:     io_github_cvc5_api_Term
 634  * Method:    isAbstractValue
 635  * Signature: (J)Z
 636  */
 637 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isAbstractValue(
 638     JNIEnv* env, jobject, jlong pointer)
 639 {
 640   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 641   Term* current = reinterpret_cast<Term*>(pointer);
 642   return static_cast<jboolean>(current->isAbstractValue());
 643   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 644 }
 645
 646 /*
 647  * Class:     io_github_cvc5_api_Term
 648  * Method:    getAbstractValue
 649  * Signature: (J)Ljava/lang/String;
 650  */
 651 JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_getAbstractValue(
 652     JNIEnv* env, jobject, jlong pointer)
 653 {
 654   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 655   Term* current = reinterpret_cast<Term*>(pointer);
 656   std::string ret = current->getAbstractValue();
 657   return env->NewStringUTF(ret.c_str());
 658   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 659 }
 660
 661 /*
 662  * Class:     io_github_cvc5_api_Term
 663  * Method:    isTupleValue
 664  * Signature: (J)Z
 665  */
 666 JNIEXPORT jboolean JNICALL
 667 Java_io_github_cvc5_api_Term_isTupleValue(JNIEnv* env, jobject, jlong pointer)
 668 {
 669   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 670   Term* current = reinterpret_cast<Term*>(pointer);
 671   return static_cast<jboolean>(current->isTupleValue());
 672   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 673 }
 674
 675 /*
 676  * Class:     io_github_cvc5_api_Term
 677  * Method:    getTupleValue
 678  * Signature: (J)[J
 679  */
 680 JNIEXPORT jlongArray JNICALL
 681 Java_io_github_cvc5_api_Term_getTupleValue(JNIEnv* env, jobject, jlong pointer)
 682 {
 683   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 684   Term* current = reinterpret_cast<Term*>(pointer);
 685   std::vector<Term> terms = current->getTupleValue();
 686   jlongArray ret = getPointersFromObjects<Term>(env, terms);
 687   return ret;
 688   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 689 }
 690
 691 /*
 692  * Class:     io_github_cvc5_api_Term
 693  * Method:    isFloatingPointPosZero
 694  * Signature: (J)Z
 695  */
 696 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isFloatingPointPosZero(
 697     JNIEnv* env, jobject, jlong pointer)
 698 {
 699   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 700   Term* current = reinterpret_cast<Term*>(pointer);
 701   return static_cast<jboolean>(current->isFloatingPointPosZero());
 702   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 703 }
 704
 705 /*
 706  * Class:     io_github_cvc5_api_Term
 707  * Method:    isFloatingPointNegZero
 708  * Signature: (J)Z
 709  */
 710 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isFloatingPointNegZero(
 711     JNIEnv* env, jobject, jlong pointer)
 712 {
 713   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 714   Term* current = reinterpret_cast<Term*>(pointer);
 715   return static_cast<jboolean>(current->isFloatingPointNegZero());
 716   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 717 }
 718
 719 /*
 720  * Class:     io_github_cvc5_api_Term
 721  * Method:    isFloatingPointPosInf
 722  * Signature: (J)Z
 723  */
 724 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isFloatingPointPosInf(
 725     JNIEnv* env, jobject, jlong pointer)
 726 {
 727   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 728   Term* current = reinterpret_cast<Term*>(pointer);
 729   return static_cast<jboolean>(current->isFloatingPointPosInf());
 730   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 731 }
 732
 733 /*
 734  * Class:     io_github_cvc5_api_Term
 735  * Method:    isFloatingPointNegInf
 736  * Signature: (J)Z
 737  */
 738 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isFloatingPointNegInf(
 739     JNIEnv* env, jobject, jlong pointer)
 740 {
 741   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 742   Term* current = reinterpret_cast<Term*>(pointer);
 743   return static_cast<jboolean>(current->isFloatingPointNegInf());
 744   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 745 }
 746
 747 /*
 748  * Class:     io_github_cvc5_api_Term
 749  * Method:    isFloatingPointNaN
 750  * Signature: (J)Z
 751  */
 752 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isFloatingPointNaN(
 753     JNIEnv* env, jobject, jlong pointer)
 754 {
 755   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 756   Term* current = reinterpret_cast<Term*>(pointer);
 757   return static_cast<jboolean>(current->isFloatingPointNaN());
 758   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 759 }
 760
 761 /*
 762  * Class:     io_github_cvc5_api_Term
 763  * Method:    isFloatingPointValue
 764  * Signature: (J)Z
 765  */
 766 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isFloatingPointValue(
 767     JNIEnv* env, jobject, jlong pointer)
 768 {
 769   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 770   Term* current = reinterpret_cast<Term*>(pointer);
 771   return static_cast<jboolean>(current->isFloatingPointValue());
 772   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 773 }
 774
 775 /*
 776  * Class:     io_github_cvc5_api_Term
 777  * Method:    getFloatingPointValue
 778  * Signature: (J)Lio/github/cvc5/api/Triplet;
 779  */
 780 JNIEXPORT jobject JNICALL Java_io_github_cvc5_api_Term_getFloatingPointValue(
 781     JNIEnv* env, jobject thisObject, jlong pointer)
 782 {
 783   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 784   Term* current = reinterpret_cast<Term*>(pointer);
 785   auto [exponent, significand, term] = current->getFloatingPointValue();
 786   Term* termPointer = new Term(term);
 787
 788   // Long longObject = new Long(pointer)
 789   jclass longClass = env->FindClass("Ljava/lang/Long;");
 790   jmethodID longConstructor = env->GetMethodID(longClass, "<init>", "(J)V");
 791   jobject e = env->NewObject(longClass, longConstructor, exponent);
 792   jobject s = env->NewObject(longClass, longConstructor, significand);
 793   jobject t = env->NewObject(longClass, longConstructor, termPointer);
 794
 795   // Triplet triplet = new Triplet<Long, Long, Long>(e, s, t);
 796   jclass tripletClass = env->FindClass("Lio/github/cvc5/api/Triplet;");
 797   jmethodID tripletConstructor = env->GetMethodID(
 798       tripletClass,
 799       "<init>",
 800       "(Ljava/lang/Object;Ljava/lang/Object;Ljava/lang/Object;)V");
 801   jobject triplet = env->NewObject(tripletClass, tripletConstructor, e, s, t);
 802
 803   return triplet;
 804   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 805 }
 806
 807 /*
 808  * Class:     io_github_cvc5_api_Term
 809  * Method:    isSetValue
 810  * Signature: (J)Z
 811  */
 812 JNIEXPORT jboolean JNICALL
 813 Java_io_github_cvc5_api_Term_isSetValue(JNIEnv* env, jobject, jlong pointer)
 814 {
 815   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 816   Term* current = reinterpret_cast<Term*>(pointer);
 817   return static_cast<jboolean>(current->isSetValue());
 818   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 819 }
 820
 821 /*
 822  * Class:     io_github_cvc5_api_Term
 823  * Method:    getSetValue
 824  * Signature: (J)[J
 825  */
 826 JNIEXPORT jlongArray JNICALL
 827 Java_io_github_cvc5_api_Term_getSetValue(JNIEnv* env, jobject, jlong pointer)
 828 {
 829   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 830   Term* current = reinterpret_cast<Term*>(pointer);
 831   std::set<Term> terms = current->getSetValue();
 832   std::vector<jlong> pointers(terms.size());
 833   int i = 0;
 834   for (const Term& t : terms)
 835   {
 836     pointers[i] = reinterpret_cast<jlong>(new Term(t));
 837     i++;
 838   }
 839   jlongArray ret = env->NewLongArray(pointers.size());
 840   env->SetLongArrayRegion(ret, 0, pointers.size(), pointers.data());
 841   return ret;
 842   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 843 }
 844
 845 /*
 846  * Class:     io_github_cvc5_api_Term
 847  * Method:    isSequenceValue
 848  * Signature: (J)Z
 849  */
 850 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isSequenceValue(
 851     JNIEnv* env, jobject, jlong pointer)
 852 {
 853   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 854   Term* current = reinterpret_cast<Term*>(pointer);
 855   return static_cast<jboolean>(current->isSequenceValue());
 856   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 857 }
 858
 859 /*
 860  * Class:     io_github_cvc5_api_Term
 861  * Method:    getSequenceValue
 862  * Signature: (J)[J
 863  */
 864 JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Term_getSequenceValue(
 865     JNIEnv* env, jobject, jlong pointer)
 866 {
 867   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 868   Term* current = reinterpret_cast<Term*>(pointer);
 869   std::vector<Term> terms = current->getSequenceValue();
 870   jlongArray ret = getPointersFromObjects<Term>(env, terms);
 871   return ret;
 872   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 873 }
 874
 875 /*
 876  * Class:     io_github_cvc5_api_Term
 877  * Method:    isUninterpretedValue
 878  * Signature: (J)Z
 879  */
 880 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isUninterpretedValue(
 881     JNIEnv* env, jobject, jlong pointer)
 882 {
 883   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 884   Term* current = reinterpret_cast<Term*>(pointer);
 885   return static_cast<jboolean>(current->isUninterpretedValue());
 886   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 887 }
 888
 889 /*
 890  * Class:     io_github_cvc5_api_Term
 891  * Method:    getUninterpretedValue
 892  * Signature: (J)Lio/github/cvc5/api/Pair;
 893  */
 894 JNIEXPORT jobject JNICALL Java_io_github_cvc5_api_Term_getUninterpretedValue(
 895     JNIEnv* env, jobject, jlong pointer)
 896 {
 897   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 898   Term* current = reinterpret_cast<Term*>(pointer);
 899   std::pair<Sort, std::int32_t> value = current->getUninterpretedValue();
 900
 901   Sort* sort = new Sort(value.first);
 902   jlong sortPointer = reinterpret_cast<jlong>(sort);
 903
 904   // Long longObject = new Long(pointer)
 905   jclass longClass = env->FindClass("Ljava/lang/Long;");
 906   jmethodID longConstructor = env->GetMethodID(longClass, "<init>", "(J)V");
 907   jobject longObject = env->NewObject(longClass, longConstructor, sortPointer);
 908
 909   // Integer integerObject = new Integer(pair.second)
 910   jclass integerClass = env->FindClass("Ljava/lang/Integer;");
 911   jmethodID integerConstructor =
 912       env->GetMethodID(integerClass, "<init>", "(I)V");
 913   jobject integerObject = env->NewObject(
 914       integerClass, integerConstructor, static_cast<jint>(value.second));
 915
 916   // Pair<String, Long> pair = new Pair<String, Long>(jName, longObject)
 917   jclass pairClass = env->FindClass("Lio/github/cvc5/api/Pair;");
 918   jmethodID pairConstructor = env->GetMethodID(
 919       pairClass, "<init>", "(Ljava/lang/Object;Ljava/lang/Object;)V");
 920   jobject pair =
 921       env->NewObject(pairClass, pairConstructor, longObject, integerObject);
 922
 923   return pair;
 924   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 925 }
 926
 927 /*
 928  * Class:     io_github_cvc5_api_Term
 929  * Method:    iterator
 930  * Signature: (J)J
 931  */
 932 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_iterator(JNIEnv* env,
 933                                                               jobject,
 934                                                               jlong pointer)
 935 {
 936   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 937   Term* current = reinterpret_cast<Term*>(pointer);
 938   Term::const_iterator* retPointer = new Term::const_iterator(current->begin());
 939   return reinterpret_cast<jlong>(retPointer);
 940   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 941 }