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:    isIntegerValue
 463  * Signature: (J)Z
 464  */
 465 JNIEXPORT jboolean JNICALL
 466 Java_io_github_cvc5_api_Term_isIntegerValue(JNIEnv* env, jobject, jlong pointer)
 467 {
 468   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 469   Term* current = reinterpret_cast<Term*>(pointer);
 470   return static_cast<jboolean>(current->isIntegerValue());
 471   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 472 }
 473
 474 /*
 475  * Class:     io_github_cvc5_api_Term
 476  * Method:    getIntegerValue
 477  * Signature: (J)Ljava/lang/String;
 478  */
 479 JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_getIntegerValue(
 480     JNIEnv* env, jobject, jlong pointer)
 481 {
 482   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 483   Term* current = reinterpret_cast<Term*>(pointer);
 484   std::string value = current->getIntegerValue();
 485   jstring ret = env->NewStringUTF(value.c_str());
 486   return ret;
 487   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 488 }
 489
 490 /*
 491  * Class:     io_github_cvc5_api_Term
 492  * Method:    isStringValue
 493  * Signature: (J)Z
 494  */
 495 JNIEXPORT jboolean JNICALL
 496 Java_io_github_cvc5_api_Term_isStringValue(JNIEnv* env, jobject, jlong pointer)
 497 {
 498   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 499   Term* current = reinterpret_cast<Term*>(pointer);
 500   return static_cast<jboolean>(current->isStringValue());
 501   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 502 }
 503
 504 /*
 505  * Class:     io_github_cvc5_api_Term
 506  * Method:    getStringValue
 507  * Signature: (J)Ljava/lang/String;
 508  */
 509 JNIEXPORT jstring JNICALL
 510 Java_io_github_cvc5_api_Term_getStringValue(JNIEnv* env, jobject, jlong pointer)
 511 {
 512   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 513   Term* current = reinterpret_cast<Term*>(pointer);
 514   std::wstring termString = current->getStringValue();
 515
 516   size_t length = termString.length();
 517   jchar* unicode = new jchar[length];
 518   const wchar_t* s = termString.c_str();
 519   for (size_t i = 0; i < length; i++)
 520   {
 521     unicode[i] = s[i];
 522   }
 523   jstring ret = env->NewString(unicode, length);
 524   delete[] unicode;
 525   return ret;
 526   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 527 }
 528
 529 /*
 530  * Class:     io_github_cvc5_api_Term
 531  * Method:    isRealValue
 532  * Signature: (J)Z
 533  */
 534 JNIEXPORT jboolean JNICALL
 535 Java_io_github_cvc5_api_Term_isRealValue(JNIEnv* env, jobject, jlong pointer)
 536 {
 537   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 538   Term* current = reinterpret_cast<Term*>(pointer);
 539   return static_cast<jboolean>(current->isRealValue());
 540   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 541 }
 542
 543 /*
 544  * Class:     io_github_cvc5_api_Term
 545  * Method:    getRealValue
 546  * Signature: (J)Ljava/lang/String;
 547  */
 548 JNIEXPORT jstring JNICALL
 549 Java_io_github_cvc5_api_Term_getRealValue(JNIEnv* env, jobject, jlong pointer)
 550 {
 551   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 552   Term* current = reinterpret_cast<Term*>(pointer);
 553   std::string realValue = current->getRealValue();
 554   return env->NewStringUTF(realValue.c_str());
 555   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 556 }
 557
 558 /*
 559  * Class:     io_github_cvc5_api_Term
 560  * Method:    isBooleanValue
 561  * Signature: (J)Z
 562  */
 563 JNIEXPORT jboolean JNICALL
 564 Java_io_github_cvc5_api_Term_isBooleanValue(JNIEnv* env, jobject, jlong pointer)
 565 {
 566   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 567   Term* current = reinterpret_cast<Term*>(pointer);
 568   return static_cast<jboolean>(current->isBooleanValue());
 569   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 570 }
 571
 572 /*
 573  * Class:     io_github_cvc5_api_Term
 574  * Method:    getBooleanValue
 575  * Signature: (J)Z
 576  */
 577 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_getBooleanValue(
 578     JNIEnv* env, jobject, jlong pointer)
 579 {
 580   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 581   Term* current = reinterpret_cast<Term*>(pointer);
 582   return static_cast<jboolean>(current->getBooleanValue());
 583   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 584 }
 585
 586 /*
 587  * Class:     io_github_cvc5_api_Term
 588  * Method:    isBitVectorValue
 589  * Signature: (J)Z
 590  */
 591 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isBitVectorValue(
 592     JNIEnv* env, jobject, jlong pointer)
 593 {
 594   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 595   Term* current = reinterpret_cast<Term*>(pointer);
 596   return static_cast<jboolean>(current->isBitVectorValue());
 597   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 598 }
 599
 600 /*
 601  * Class:     io_github_cvc5_api_Term
 602  * Method:    getBitVectorValue
 603  * Signature: (JI)Ljava/lang/String;
 604  */
 605 JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_getBitVectorValue(
 606     JNIEnv* env, jobject, jlong pointer, jint base)
 607 {
 608   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 609   Term* current = reinterpret_cast<Term*>(pointer);
 610   std::string ret =
 611       current->getBitVectorValue(static_cast<std::uint32_t>(base));
 612   return env->NewStringUTF(ret.c_str());
 613   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 614 }
 615
 616 /*
 617  * Class:     io_github_cvc5_api_Term
 618  * Method:    isAbstractValue
 619  * Signature: (J)Z
 620  */
 621 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isAbstractValue(
 622     JNIEnv* env, jobject, jlong pointer)
 623 {
 624   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 625   Term* current = reinterpret_cast<Term*>(pointer);
 626   return static_cast<jboolean>(current->isAbstractValue());
 627   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 628 }
 629
 630 /*
 631  * Class:     io_github_cvc5_api_Term
 632  * Method:    getAbstractValue
 633  * Signature: (J)Ljava/lang/String;
 634  */
 635 JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_getAbstractValue(
 636     JNIEnv* env, jobject, jlong pointer)
 637 {
 638   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 639   Term* current = reinterpret_cast<Term*>(pointer);
 640   std::string ret = current->getAbstractValue();
 641   return env->NewStringUTF(ret.c_str());
 642   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 643 }
 644
 645 /*
 646  * Class:     io_github_cvc5_api_Term
 647  * Method:    isTupleValue
 648  * Signature: (J)Z
 649  */
 650 JNIEXPORT jboolean JNICALL
 651 Java_io_github_cvc5_api_Term_isTupleValue(JNIEnv* env, jobject, jlong pointer)
 652 {
 653   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 654   Term* current = reinterpret_cast<Term*>(pointer);
 655   return static_cast<jboolean>(current->isTupleValue());
 656   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 657 }
 658
 659 /*
 660  * Class:     io_github_cvc5_api_Term
 661  * Method:    getTupleValue
 662  * Signature: (J)[J
 663  */
 664 JNIEXPORT jlongArray JNICALL
 665 Java_io_github_cvc5_api_Term_getTupleValue(JNIEnv* env, jobject, jlong pointer)
 666 {
 667   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 668   Term* current = reinterpret_cast<Term*>(pointer);
 669   std::vector<Term> terms = current->getTupleValue();
 670   jlongArray ret = getPointersFromObjects<Term>(env, terms);
 671   return ret;
 672   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 673 }
 674
 675 /*
 676  * Class:     io_github_cvc5_api_Term
 677  * Method:    isFloatingPointPosZero
 678  * Signature: (J)Z
 679  */
 680 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isFloatingPointPosZero(
 681     JNIEnv* env, jobject, jlong pointer)
 682 {
 683   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 684   Term* current = reinterpret_cast<Term*>(pointer);
 685   return static_cast<jboolean>(current->isFloatingPointPosZero());
 686   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 687 }
 688
 689 /*
 690  * Class:     io_github_cvc5_api_Term
 691  * Method:    isFloatingPointNegZero
 692  * Signature: (J)Z
 693  */
 694 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isFloatingPointNegZero(
 695     JNIEnv* env, jobject, jlong pointer)
 696 {
 697   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 698   Term* current = reinterpret_cast<Term*>(pointer);
 699   return static_cast<jboolean>(current->isFloatingPointNegZero());
 700   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 701 }
 702
 703 /*
 704  * Class:     io_github_cvc5_api_Term
 705  * Method:    isFloatingPointPosInf
 706  * Signature: (J)Z
 707  */
 708 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isFloatingPointPosInf(
 709     JNIEnv* env, jobject, jlong pointer)
 710 {
 711   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 712   Term* current = reinterpret_cast<Term*>(pointer);
 713   return static_cast<jboolean>(current->isFloatingPointPosInf());
 714   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 715 }
 716
 717 /*
 718  * Class:     io_github_cvc5_api_Term
 719  * Method:    isFloatingPointNegInf
 720  * Signature: (J)Z
 721  */
 722 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isFloatingPointNegInf(
 723     JNIEnv* env, jobject, jlong pointer)
 724 {
 725   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 726   Term* current = reinterpret_cast<Term*>(pointer);
 727   return static_cast<jboolean>(current->isFloatingPointNegInf());
 728   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 729 }
 730
 731 /*
 732  * Class:     io_github_cvc5_api_Term
 733  * Method:    isFloatingPointNaN
 734  * Signature: (J)Z
 735  */
 736 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isFloatingPointNaN(
 737     JNIEnv* env, jobject, jlong pointer)
 738 {
 739   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 740   Term* current = reinterpret_cast<Term*>(pointer);
 741   return static_cast<jboolean>(current->isFloatingPointNaN());
 742   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 743 }
 744
 745 /*
 746  * Class:     io_github_cvc5_api_Term
 747  * Method:    isFloatingPointValue
 748  * Signature: (J)Z
 749  */
 750 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isFloatingPointValue(
 751     JNIEnv* env, jobject, jlong pointer)
 752 {
 753   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 754   Term* current = reinterpret_cast<Term*>(pointer);
 755   return static_cast<jboolean>(current->isFloatingPointValue());
 756   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 757 }
 758
 759 /*
 760  * Class:     io_github_cvc5_api_Term
 761  * Method:    getFloatingPointValue
 762  * Signature: (J)Lio/github/cvc5/api/Triplet;
 763  */
 764 JNIEXPORT jobject JNICALL Java_io_github_cvc5_api_Term_getFloatingPointValue(
 765     JNIEnv* env, jobject thisObject, jlong pointer)
 766 {
 767   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 768   Term* current = reinterpret_cast<Term*>(pointer);
 769   auto [exponent, significand, term] = current->getFloatingPointValue();
 770   Term* termPointer = new Term(term);
 771
 772   // Long longObject = new Long(pointer)
 773   jclass longClass = env->FindClass("Ljava/lang/Long;");
 774   jmethodID longConstructor = env->GetMethodID(longClass, "<init>", "(J)V");
 775   jobject e = env->NewObject(longClass, longConstructor, exponent);
 776   jobject s = env->NewObject(longClass, longConstructor, significand);
 777   jobject t = env->NewObject(longClass, longConstructor, termPointer);
 778
 779   // Triplet triplet = new Triplet<Long, Long, Long>(e, s, t);
 780   jclass tripletClass = env->FindClass("Lio/github/cvc5/api/Triplet;");
 781   jmethodID tripletConstructor = env->GetMethodID(
 782       tripletClass,
 783       "<init>",
 784       "(Ljava/lang/Object;Ljava/lang/Object;Ljava/lang/Object;)V");
 785   jobject triplet = env->NewObject(tripletClass, tripletConstructor, e, s, t);
 786
 787   return triplet;
 788   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 789 }
 790
 791 /*
 792  * Class:     io_github_cvc5_api_Term
 793  * Method:    isSetValue
 794  * Signature: (J)Z
 795  */
 796 JNIEXPORT jboolean JNICALL
 797 Java_io_github_cvc5_api_Term_isSetValue(JNIEnv* env, jobject, jlong pointer)
 798 {
 799   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 800   Term* current = reinterpret_cast<Term*>(pointer);
 801   return static_cast<jboolean>(current->isSetValue());
 802   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 803 }
 804
 805 /*
 806  * Class:     io_github_cvc5_api_Term
 807  * Method:    getSetValue
 808  * Signature: (J)[J
 809  */
 810 JNIEXPORT jlongArray JNICALL
 811 Java_io_github_cvc5_api_Term_getSetValue(JNIEnv* env, jobject, jlong pointer)
 812 {
 813   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 814   Term* current = reinterpret_cast<Term*>(pointer);
 815   std::set<Term> terms = current->getSetValue();
 816   std::vector<jlong> pointers(terms.size());
 817   int i = 0;
 818   for (const Term& t : terms)
 819   {
 820     pointers[i] = reinterpret_cast<jlong>(new Term(t));
 821     i++;
 822   }
 823   jlongArray ret = env->NewLongArray(pointers.size());
 824   env->SetLongArrayRegion(ret, 0, pointers.size(), pointers.data());
 825   return ret;
 826   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 827 }
 828
 829 /*
 830  * Class:     io_github_cvc5_api_Term
 831  * Method:    isSequenceValue
 832  * Signature: (J)Z
 833  */
 834 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isSequenceValue(
 835     JNIEnv* env, jobject, jlong pointer)
 836 {
 837   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 838   Term* current = reinterpret_cast<Term*>(pointer);
 839   return static_cast<jboolean>(current->isSequenceValue());
 840   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 841 }
 842
 843 /*
 844  * Class:     io_github_cvc5_api_Term
 845  * Method:    getSequenceValue
 846  * Signature: (J)[J
 847  */
 848 JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Term_getSequenceValue(
 849     JNIEnv* env, jobject, jlong pointer)
 850 {
 851   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 852   Term* current = reinterpret_cast<Term*>(pointer);
 853   std::vector<Term> terms = current->getSequenceValue();
 854   jlongArray ret = getPointersFromObjects<Term>(env, terms);
 855   return ret;
 856   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 857 }
 858
 859 /*
 860  * Class:     io_github_cvc5_api_Term
 861  * Method:    isUninterpretedValue
 862  * Signature: (J)Z
 863  */
 864 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isUninterpretedValue(
 865     JNIEnv* env, jobject, jlong pointer)
 866 {
 867   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 868   Term* current = reinterpret_cast<Term*>(pointer);
 869   return static_cast<jboolean>(current->isUninterpretedValue());
 870   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 871 }
 872
 873 /*
 874  * Class:     io_github_cvc5_api_Term
 875  * Method:    getUninterpretedValue
 876  * Signature: (J)Lio/github/cvc5/api/Pair;
 877  */
 878 JNIEXPORT jobject JNICALL Java_io_github_cvc5_api_Term_getUninterpretedValue(
 879     JNIEnv* env, jobject, jlong pointer)
 880 {
 881   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 882   Term* current = reinterpret_cast<Term*>(pointer);
 883   std::pair<Sort, std::int32_t> value = current->getUninterpretedValue();
 884
 885   Sort* sort = new Sort(value.first);
 886   jlong sortPointer = reinterpret_cast<jlong>(sort);
 887
 888   // Long longObject = new Long(pointer)
 889   jclass longClass = env->FindClass("Ljava/lang/Long;");
 890   jmethodID longConstructor = env->GetMethodID(longClass, "<init>", "(J)V");
 891   jobject longObject = env->NewObject(longClass, longConstructor, sortPointer);
 892
 893   // Integer integerObject = new Integer(pair.second)
 894   jclass integerClass = env->FindClass("Ljava/lang/Integer;");
 895   jmethodID integerConstructor =
 896       env->GetMethodID(integerClass, "<init>", "(I)V");
 897   jobject integerObject = env->NewObject(
 898       integerClass, integerConstructor, static_cast<jint>(value.second));
 899
 900   // Pair<String, Long> pair = new Pair<String, Long>(jName, longObject)
 901   jclass pairClass = env->FindClass("Lio/github/cvc5/api/Pair;");
 902   jmethodID pairConstructor = env->GetMethodID(
 903       pairClass, "<init>", "(Ljava/lang/Object;Ljava/lang/Object;)V");
 904   jobject pair =
 905       env->NewObject(pairClass, pairConstructor, longObject, integerObject);
 906
 907   return pair;
 908   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 909 }
 910
 911 /*
 912  * Class:     io_github_cvc5_api_Term
 913  * Method:    iterator
 914  * Signature: (J)J
 915  */
 916 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Term_iterator(JNIEnv* env,
 917                                                               jobject,
 918                                                               jlong pointer)
 919 {
 920   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 921   Term* current = reinterpret_cast<Term*>(pointer);
 922   Term::const_iterator* retPointer = new Term::const_iterator(current->begin());
 923   return reinterpret_cast<jlong>(retPointer);
 924   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 925 }