src/api/java/jni/solver.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_Solver.h"
  19
  20 using namespace cvc5::api;
  21
  22 /*
  23  * Class:     io_github_cvc5_api_Solver
  24  * Method:    newSolver
  25  * Signature: ()J
  26  */
  27 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_newSolver(JNIEnv*,
  28                                                                  jobject)
  29 {
  30   Solver* solver = new Solver();
  31   return reinterpret_cast<jlong>(solver);
  32 }
  33
  34 /*
  35  * Class:     io_github_cvc5_api_Solver
  36  * Method:    deletePointer
  37  * Signature: (J)V
  38  */
  39 JNIEXPORT void JNICALL
  40 Java_io_github_cvc5_api_Solver_deletePointer(JNIEnv*, jclass, jlong pointer)
  41 {
  42   delete (reinterpret_cast<Solver*>(pointer));
  43 }
  44
  45 /*
  46  * Class:     io_github_cvc5_api_Solver
  47  * Method:    getNullSort
  48  * Signature: (J)J
  49  */
  50 JNIEXPORT jlong JNICALL
  51 Java_io_github_cvc5_api_Solver_getNullSort(JNIEnv* env, jobject, jlong pointer)
  52 {
  53   CVC5_JAVA_API_TRY_CATCH_BEGIN;
  54   Solver* solver = reinterpret_cast<Solver*>(pointer);
  55   Sort* sortPointer = new Sort(solver->getNullSort());
  56   return reinterpret_cast<jlong>(sortPointer);
  57   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
  58 }
  59
  60 /*
  61  * Class:     io_github_cvc5_api_Solver
  62  * Method:    getBooleanSort
  63  * Signature: (J)J
  64  */
  65 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getBooleanSort(
  66     JNIEnv* env, jobject, jlong pointer)
  67 {
  68   CVC5_JAVA_API_TRY_CATCH_BEGIN;
  69   Solver* solver = reinterpret_cast<Solver*>(pointer);
  70   Sort* sortPointer = new Sort(solver->getBooleanSort());
  71   return reinterpret_cast<jlong>(sortPointer);
  72   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
  73 }
  74
  75 /*
  76  * Class:     io_github_cvc5_api_Solver
  77  * Method:    getIntegerSort
  78  * Signature: (J)J
  79  */
  80 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getIntegerSort(
  81     JNIEnv* env, jobject, jlong pointer)
  82 {
  83   CVC5_JAVA_API_TRY_CATCH_BEGIN;
  84   Solver* solver = reinterpret_cast<Solver*>(pointer);
  85   Sort* sortPointer = new Sort(solver->getIntegerSort());
  86   return reinterpret_cast<jlong>(sortPointer);
  87   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
  88 }
  89
  90 /*
  91  * Class:     io_github_cvc5_api_Solver
  92  * Method:    getRealSort
  93  * Signature: (J)J
  94  */
  95 JNIEXPORT jlong JNICALL
  96 Java_io_github_cvc5_api_Solver_getRealSort(JNIEnv* env, jobject, jlong pointer)
  97 {
  98   CVC5_JAVA_API_TRY_CATCH_BEGIN;
  99   Solver* solver = reinterpret_cast<Solver*>(pointer);
 100   Sort* sortPointer = new Sort(solver->getRealSort());
 101   return reinterpret_cast<jlong>(sortPointer);
 102   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 103 }
 104
 105 /*
 106  * Class:     io_github_cvc5_api_Solver
 107  * Method:    getRegExpSort
 108  * Signature: (J)J
 109  */
 110 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getRegExpSort(
 111     JNIEnv* env, jobject, jlong pointer)
 112 {
 113   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 114   Solver* solver = reinterpret_cast<Solver*>(pointer);
 115   Sort* sortPointer = new Sort(solver->getRegExpSort());
 116   return reinterpret_cast<jlong>(sortPointer);
 117   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 118 }
 119
 120 /*
 121  * Class:     io_github_cvc5_api_Solver
 122  * Method:    getRoundingModeSort
 123  * Signature: (J)J
 124  */
 125 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getRoundingModeSort(
 126     JNIEnv* env, jobject, jlong pointer)
 127 {
 128   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 129   Solver* solver = reinterpret_cast<Solver*>(pointer);
 130   Sort* sortPointer = new Sort(solver->getRoundingModeSort());
 131   return reinterpret_cast<jlong>(sortPointer);
 132   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 133 }
 134
 135 /*
 136  * Class:     io_github_cvc5_api_Solver
 137  * Method:    getStringSort
 138  * Signature: (J)J
 139  */
 140 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getStringSort(
 141     JNIEnv* env, jobject, jlong pointer)
 142 {
 143   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 144   Solver* solver = reinterpret_cast<Solver*>(pointer);
 145   Sort* sortPointer = new Sort(solver->getStringSort());
 146   return reinterpret_cast<jlong>(sortPointer);
 147   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 148 }
 149
 150 /*
 151  * Class:     io_github_cvc5_api_Solver
 152  * Method:    mkArraySort
 153  * Signature: (JJJ)J
 154  */
 155 JNIEXPORT jlong JNICALL
 156 Java_io_github_cvc5_api_Solver_mkArraySort(JNIEnv* env,
 157                                            jobject,
 158                                            jlong pointer,
 159                                            jlong indexSortPointer,
 160                                            jlong elementSortPointer)
 161 {
 162   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 163   Solver* solver = reinterpret_cast<Solver*>(pointer);
 164   Sort* indexSort = reinterpret_cast<Sort*>(indexSortPointer);
 165   Sort* elementSort = reinterpret_cast<Sort*>(elementSortPointer);
 166   Sort* retPointer = new Sort(solver->mkArraySort(*indexSort, *elementSort));
 167   return reinterpret_cast<jlong>(retPointer);
 168   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 169 }
 170
 171 /*
 172  * Class:     io_github_cvc5_api_Solver
 173  * Method:    mkBitVectorSort
 174  * Signature: (JI)J
 175  */
 176 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkBitVectorSort(
 177     JNIEnv* env, jobject, jlong pointer, jint size)
 178 {
 179   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 180   Solver* solver = reinterpret_cast<Solver*>(pointer);
 181   Sort* sortPointer = new Sort(solver->mkBitVectorSort((uint32_t)size));
 182   return reinterpret_cast<jlong>(sortPointer);
 183   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 184 }
 185
 186 /*
 187  * Class:     io_github_cvc5_api_Solver
 188  * Method:    mkFloatingPointSort
 189  * Signature: (JII)J
 190  */
 191 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkFloatingPointSort(
 192     JNIEnv* env, jobject, jlong pointer, jint exp, jint sig)
 193 {
 194   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 195   Solver* solver = reinterpret_cast<Solver*>(pointer);
 196   Sort* sortPointer =
 197       new Sort(solver->mkFloatingPointSort((uint32_t)exp, (uint32_t)sig));
 198   return reinterpret_cast<jlong>(sortPointer);
 199   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 200 }
 201
 202 /*
 203  * Class:     io_github_cvc5_api_Solver
 204  * Method:    mkDatatypeSort
 205  * Signature: (JJ)J
 206  */
 207 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkDatatypeSort(
 208     JNIEnv* env, jobject, jlong pointer, jlong datatypeDeclPointer)
 209 {
 210   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 211   Solver* solver = reinterpret_cast<Solver*>(pointer);
 212   DatatypeDecl* decl = reinterpret_cast<DatatypeDecl*>(datatypeDeclPointer);
 213   Sort* retPointer = new Sort(solver->mkDatatypeSort(*decl));
 214   return reinterpret_cast<jlong>(retPointer);
 215   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 216 }
 217
 218 /*
 219  * Class:     io_github_cvc5_api_Solver
 220  * Method:    mkDatatypeSorts
 221  * Signature: (J[J)[J
 222  */
 223 JNIEXPORT jlongArray JNICALL
 224 Java_io_github_cvc5_api_Solver_mkDatatypeSorts__J_3J(JNIEnv* env,
 225                                                      jobject,
 226                                                      jlong pointer,
 227                                                      jlongArray jDecls)
 228 {
 229   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 230   Solver* solver = reinterpret_cast<Solver*>(pointer);
 231   std::vector<DatatypeDecl> decls =
 232       getObjectsFromPointers<DatatypeDecl>(env, jDecls);
 233   std::vector<Sort> sorts = solver->mkDatatypeSorts(decls);
 234   std::vector<jlong> sortPointers(sorts.size());
 235
 236   for (size_t i = 0; i < sorts.size(); i++)
 237   {
 238     sortPointers[i] = reinterpret_cast<jlong>(new Sort(sorts[i]));
 239   }
 240
 241   jlongArray ret = env->NewLongArray(sorts.size());
 242   env->SetLongArrayRegion(ret, 0, sorts.size(), sortPointers.data());
 243   return ret;
 244   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 245 }
 246
 247 /*
 248  * Class:     io_github_cvc5_api_Solver
 249  * Method:    mkDatatypeSorts
 250  * Signature: (J[J[J)[J
 251  */
 252 JNIEXPORT jlongArray JNICALL
 253 Java_io_github_cvc5_api_Solver_mkDatatypeSorts__J_3J_3J(JNIEnv* env,
 254                                                         jobject,
 255                                                         jlong pointer,
 256                                                         jlongArray jDecls,
 257                                                         jlongArray jUnresolved)
 258 {
 259   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 260   Solver* solver = reinterpret_cast<Solver*>(pointer);
 261   std::vector<DatatypeDecl> decls =
 262       getObjectsFromPointers<DatatypeDecl>(env, jDecls);
 263   std::vector<Sort> cUnresolved =
 264       getObjectsFromPointers<Sort>(env, jUnresolved);
 265   std::set<Sort> unresolved(cUnresolved.begin(), cUnresolved.end());
 266   std::vector<Sort> sorts = solver->mkDatatypeSorts(decls, unresolved);
 267   jlongArray ret = getPointersFromObjects<Sort>(env, sorts);
 268   return ret;
 269   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 270 }
 271
 272 /*
 273  * Class:     io_github_cvc5_api_Solver
 274  * Method:    mkFunctionSort
 275  * Signature: (JJJ)J
 276  */
 277 JNIEXPORT jlong JNICALL
 278 Java_io_github_cvc5_api_Solver_mkFunctionSort__JJJ(JNIEnv* env,
 279                                                    jobject,
 280                                                    jlong pointer,
 281                                                    jlong domainPointer,
 282                                                    jlong codomainPointer)
 283 {
 284   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 285   Solver* solver = reinterpret_cast<Solver*>(pointer);
 286   Sort* domain = reinterpret_cast<Sort*>(domainPointer);
 287   Sort* codomain = reinterpret_cast<Sort*>(codomainPointer);
 288   Sort* sortPointer = new Sort(solver->mkFunctionSort(*domain, *codomain));
 289   return reinterpret_cast<jlong>(sortPointer);
 290   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 291 }
 292
 293 /*
 294  * Class:     io_github_cvc5_api_Solver
 295  * Method:    mkFunctionSort
 296  * Signature: (J[JJ)J
 297  */
 298 JNIEXPORT jlong JNICALL
 299 Java_io_github_cvc5_api_Solver_mkFunctionSort__J_3JJ(JNIEnv* env,
 300                                                      jobject,
 301                                                      jlong pointer,
 302                                                      jlongArray sortPointers,
 303                                                      jlong codomainPointer)
 304 {
 305   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 306   Solver* solver = reinterpret_cast<Solver*>(pointer);
 307   Sort* codomain = reinterpret_cast<Sort*>(codomainPointer);
 308   std::vector<Sort> sorts = getObjectsFromPointers<Sort>(env, sortPointers);
 309   Sort* retPointer = new Sort(solver->mkFunctionSort(sorts, *codomain));
 310   return reinterpret_cast<jlong>(retPointer);
 311   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 312 }
 313
 314 /*
 315  * Class:     io_github_cvc5_api_Solver
 316  * Method:    mkParamSort
 317  * Signature: (JLjava/lang/String;)J
 318  */
 319 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkParamSort(
 320     JNIEnv* env, jobject, jlong pointer, jstring jSymbol)
 321 {
 322   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 323   Solver* solver = reinterpret_cast<Solver*>(pointer);
 324   const char* s = env->GetStringUTFChars(jSymbol, nullptr);
 325   std::string cSymbol(s);
 326   Sort* retPointer = new Sort(solver->mkParamSort(cSymbol));
 327   env->ReleaseStringUTFChars(jSymbol, s);
 328   return reinterpret_cast<jlong>(retPointer);
 329   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 330 }
 331
 332 /*
 333  * Class:     io_github_cvc5_api_Solver
 334  * Method:    mkPredicateSort
 335  * Signature: (J[J)J
 336  */
 337 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkPredicateSort(
 338     JNIEnv* env, jobject, jlong pointer, jlongArray sortPointers)
 339 {
 340   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 341   Solver* solver = reinterpret_cast<Solver*>(pointer);
 342   std::vector<Sort> sorts = getObjectsFromPointers<Sort>(env, sortPointers);
 343   Sort* retPointer = new Sort(solver->mkPredicateSort(sorts));
 344   return reinterpret_cast<jlong>(retPointer);
 345   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 346 }
 347
 348 /*
 349  * Class:     io_github_cvc5_api_Solver
 350  * Method:    mkRecordSort
 351  * Signature: (J[Lio/github/cvc5/api/Pair;)J
 352  */
 353 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRecordSort(
 354     JNIEnv* env, jobject, jlong pointer, jobjectArray jFields)
 355 {
 356   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 357   Solver* solver = reinterpret_cast<Solver*>(pointer);
 358   jsize size = env->GetArrayLength(jFields);
 359   // Lio/github/cvc5/api/Pair; is signature of cvc5.Pair<String, Long>
 360   jclass pairClass = env->FindClass("Lio/github/cvc5/api/Pair;");
 361   jclass longClass = env->FindClass("Ljava/lang/Long;");
 362   // Ljava/lang/Object; is the signature of cvc5.Pair.first field
 363   jfieldID firstFieldId =
 364       env->GetFieldID(pairClass, "first", "Ljava/lang/Object;");
 365   // Ljava/lang/Object; is the signature of cvc5.Pair.second field
 366   jfieldID secondFieldId =
 367       env->GetFieldID(pairClass, "second", "Ljava/lang/Object;");
 368   // we need to call method longValue to get long Long object
 369   jmethodID methodId = env->GetMethodID(longClass, "longValue", "()J");
 370
 371   std::vector<std::pair<std::string, Sort>> cFields;
 372   for (jsize i = 0; i < size; i++)
 373   {
 374     // get the pair at index i
 375     jobject object = env->GetObjectArrayElement(jFields, i);
 376
 377     // get the object at cvc5.Pair.first and convert it to char *
 378     jstring jFirst = (jstring)env->GetObjectField(object, firstFieldId);
 379     const char* cFirst = env->GetStringUTFChars(jFirst, nullptr);
 380
 381     // get the object at cvc5.Pair.second and convert it to Sort
 382     jobject jSecond = env->GetObjectField(object, secondFieldId);
 383     jlong sortPointer = env->CallLongMethod(jSecond, methodId);
 384     Sort* sort = reinterpret_cast<Sort*>(sortPointer);
 385
 386     // add the pair to to the list of fields
 387     cFields.push_back(std::make_pair(std::string(cFirst), *sort));
 388   }
 389   // get the record sort from the solver
 390   Sort* retPointer = new Sort(solver->mkRecordSort(cFields));
 391   // return a pointer to the sort
 392   return reinterpret_cast<jlong>(retPointer);
 393   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 394 }
 395
 396 /*
 397  * Class:     io_github_cvc5_api_Solver
 398  * Method:    mkSetSort
 399  * Signature: (JJ)J
 400  */
 401 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkSetSort(
 402     JNIEnv* env, jobject, jlong pointer, jlong elemSortPointer)
 403 {
 404   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 405   Solver* solver = reinterpret_cast<Solver*>(pointer);
 406   Sort* elemSort = reinterpret_cast<Sort*>(elemSortPointer);
 407   Sort* retPointer = new Sort(solver->mkSetSort(*elemSort));
 408   return reinterpret_cast<jlong>(retPointer);
 409   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 410 }
 411
 412 /*
 413  * Class:     io_github_cvc5_api_Solver
 414  * Method:    mkBagSort
 415  * Signature: (JJ)J
 416  */
 417 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkBagSort(
 418     JNIEnv* env, jobject, jlong pointer, jlong elemSortPointer)
 419 {
 420   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 421   Solver* solver = reinterpret_cast<Solver*>(pointer);
 422   Sort* elemSort = reinterpret_cast<Sort*>(elemSortPointer);
 423   Sort* retPointer = new Sort(solver->mkBagSort(*elemSort));
 424   return reinterpret_cast<jlong>(retPointer);
 425   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 426 }
 427
 428 /*
 429  * Class:     io_github_cvc5_api_Solver
 430  * Method:    mkSequenceSort
 431  * Signature: (JJ)J
 432  */
 433 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkSequenceSort(
 434     JNIEnv* env, jobject, jlong pointer, jlong elemSortPointer)
 435 {
 436   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 437   Solver* solver = reinterpret_cast<Solver*>(pointer);
 438   Sort* elemSort = reinterpret_cast<Sort*>(elemSortPointer);
 439   Sort* sortPointer = new Sort(solver->mkSequenceSort(*elemSort));
 440   return reinterpret_cast<jlong>(sortPointer);
 441   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 442 }
 443
 444 /*
 445  * Class:     io_github_cvc5_api_Solver
 446  * Method:    mkUninterpretedSort
 447  * Signature: (JLjava/lang/String;)J
 448  */
 449 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkUninterpretedSort(
 450     JNIEnv* env, jobject, jlong pointer, jstring jSymbol)
 451 {
 452   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 453
 454   Solver* solver = reinterpret_cast<Solver*>(pointer);
 455   const char* cSymbol = env->GetStringUTFChars(jSymbol, nullptr);
 456   Sort* sort = new Sort(solver->mkUninterpretedSort(std::string(cSymbol)));
 457   env->ReleaseStringUTFChars(jSymbol, cSymbol);
 458   return reinterpret_cast<jlong>(sort);
 459
 460   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 461 }
 462
 463 /*
 464  * Class:     io_github_cvc5_api_Solver
 465  * Method:    mkUnresolvedSort
 466  * Signature: (JLjava/lang/String;I)J
 467  */
 468 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkUnresolvedSort(
 469     JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jint arity)
 470 {
 471   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 472
 473   Solver* solver = reinterpret_cast<Solver*>(pointer);
 474   const char* s = env->GetStringUTFChars(jSymbol, nullptr);
 475   std::string cSymbol(s);
 476   Sort* retPointer = new Sort(solver->mkUnresolvedSort(cSymbol, (size_t)arity));
 477   env->ReleaseStringUTFChars(jSymbol, s);
 478   return reinterpret_cast<jlong>(retPointer);
 479
 480   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 481 }
 482
 483 /*
 484  * Class:     io_github_cvc5_api_Solver
 485  * Method:    mkSortConstructorSort
 486  * Signature: (JLjava/lang/String;I)J
 487  */
 488 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkSortConstructorSort(
 489     JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jint arity)
 490 {
 491   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 492
 493   Solver* solver = reinterpret_cast<Solver*>(pointer);
 494   const char* s = env->GetStringUTFChars(jSymbol, nullptr);
 495   std::string cSymbol(s);
 496   Sort* retPointer =
 497       new Sort(solver->mkSortConstructorSort(cSymbol, (size_t)arity));
 498   env->ReleaseStringUTFChars(jSymbol, s);
 499   return reinterpret_cast<jlong>(retPointer);
 500
 501   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 502 }
 503
 504 /*
 505  * Class:     io_github_cvc5_api_Solver
 506  * Method:    mkTupleSort
 507  * Signature: (J[J)J
 508  */
 509 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkTupleSort(
 510     JNIEnv* env, jobject, jlong pointer, jlongArray sortPointers)
 511 {
 512   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 513   Solver* solver = reinterpret_cast<Solver*>(pointer);
 514   std::vector<Sort> sorts = getObjectsFromPointers<Sort>(env, sortPointers);
 515   Sort* retPointer = new Sort(solver->mkTupleSort(sorts));
 516   return reinterpret_cast<jlong>(retPointer);
 517   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 518 }
 519
 520 /*
 521  * Class:     io_github_cvc5_api_Solver
 522  * Method:    mkTerm
 523  * Signature: (JI)J
 524  */
 525 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkTerm__JI(
 526     JNIEnv* env, jobject, jlong pointer, jint kindValue)
 527 {
 528   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 529   Solver* solver = reinterpret_cast<Solver*>(pointer);
 530   Kind kind = (Kind)kindValue;
 531   Term* retPointer = new Term(solver->mkTerm(kind));
 532   return reinterpret_cast<jlong>(retPointer);
 533   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 534 }
 535
 536 /*
 537  * Class:     io_github_cvc5_api_Solver
 538  * Method:    mkTerm
 539  * Signature: (JIJ)J
 540  */
 541 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkTerm__JIJ(
 542     JNIEnv* env, jobject, jlong pointer, jint kindValue, jlong childPointer)
 543 {
 544   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 545   Solver* solver = reinterpret_cast<Solver*>(pointer);
 546   Kind kind = (Kind)kindValue;
 547   Term* child = reinterpret_cast<Term*>(childPointer);
 548   Term* termPointer = new Term(solver->mkTerm(kind, *child));
 549   return reinterpret_cast<jlong>(termPointer);
 550   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 551 }
 552
 553 /*
 554  * Class:     io_github_cvc5_api_Solver
 555  * Method:    mkTerm
 556  * Signature: (JIJJ)J
 557  */
 558 JNIEXPORT jlong JNICALL
 559 Java_io_github_cvc5_api_Solver_mkTerm__JIJJ(JNIEnv* env,
 560                                             jobject,
 561                                             jlong pointer,
 562                                             jint kindValue,
 563                                             jlong child1Pointer,
 564                                             jlong child2Pointer)
 565 {
 566   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 567   Solver* solver = reinterpret_cast<Solver*>(pointer);
 568   Kind kind = (Kind)kindValue;
 569   Term* child1 = reinterpret_cast<Term*>(child1Pointer);
 570   Term* child2 = reinterpret_cast<Term*>(child2Pointer);
 571   Term* termPointer = new Term(solver->mkTerm(kind, *child1, *child2));
 572   return reinterpret_cast<jlong>(termPointer);
 573   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 574 }
 575
 576 /*
 577  * Class:     io_github_cvc5_api_Solver
 578  * Method:    mkTerm
 579  * Signature: (JIJJJ)J
 580  */
 581 JNIEXPORT jlong JNICALL
 582 Java_io_github_cvc5_api_Solver_mkTerm__JIJJJ(JNIEnv* env,
 583                                              jobject,
 584                                              jlong pointer,
 585                                              jint kindValue,
 586                                              jlong child1Pointer,
 587                                              jlong child2Pointer,
 588                                              jlong child3Pointer)
 589 {
 590   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 591   Solver* solver = reinterpret_cast<Solver*>(pointer);
 592   Kind kind = (Kind)kindValue;
 593   Term* child1 = reinterpret_cast<Term*>(child1Pointer);
 594   Term* child2 = reinterpret_cast<Term*>(child2Pointer);
 595   Term* child3 = reinterpret_cast<Term*>(child3Pointer);
 596   Term* retPointer = new Term(solver->mkTerm(kind, *child1, *child2, *child3));
 597   return reinterpret_cast<jlong>(retPointer);
 598   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 599 }
 600
 601 /*
 602  * Class:     io_github_cvc5_api_Solver
 603  * Method:    mkTerm
 604  * Signature: (JI[J)J
 605  */
 606 JNIEXPORT jlong JNICALL
 607 Java_io_github_cvc5_api_Solver_mkTerm__JI_3J(JNIEnv* env,
 608                                              jobject,
 609                                              jlong pointer,
 610                                              jint kindValue,
 611                                              jlongArray childrenPointers)
 612 {
 613   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 614   Solver* solver = reinterpret_cast<Solver*>(pointer);
 615   Kind kind = (Kind)kindValue;
 616   std::vector<Term> children =
 617       getObjectsFromPointers<Term>(env, childrenPointers);
 618   Term* retPointer = new Term(solver->mkTerm(kind, children));
 619   return reinterpret_cast<jlong>(retPointer);
 620   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 621 }
 622
 623 /*
 624  * Class:     io_github_cvc5_api_Solver
 625  * Method:    mkTerm
 626  * Signature: (JJ)J
 627  */
 628 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkTerm__JJ(
 629     JNIEnv* env, jobject, jlong pointer, jlong opPointer)
 630 {
 631   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 632   Solver* solver = reinterpret_cast<Solver*>(pointer);
 633   Op* op = reinterpret_cast<Op*>(opPointer);
 634   Term* retPointer = new Term(solver->mkTerm(*op));
 635   return reinterpret_cast<jlong>(retPointer);
 636   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 637 }
 638
 639 /*
 640  * Class:     io_github_cvc5_api_Solver
 641  * Method:    mkTerm
 642  * Signature: (JJJ)J
 643  */
 644 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkTerm__JJJ(
 645     JNIEnv* env, jobject, jlong pointer, jlong opPointer, jlong childPointer)
 646 {
 647   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 648   Solver* solver = reinterpret_cast<Solver*>(pointer);
 649   Op* op = reinterpret_cast<Op*>(opPointer);
 650   Term* child = reinterpret_cast<Term*>(childPointer);
 651   Term* retPointer = new Term(solver->mkTerm(*op, *child));
 652   return reinterpret_cast<jlong>(retPointer);
 653   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 654 }
 655
 656 /*
 657  * Class:     io_github_cvc5_api_Solver
 658  * Method:    mkTerm
 659  * Signature: (JJJJ)J
 660  */
 661 JNIEXPORT jlong JNICALL
 662 Java_io_github_cvc5_api_Solver_mkTerm__JJJJ(JNIEnv* env,
 663                                             jobject,
 664                                             jlong pointer,
 665                                             jlong opPointer,
 666                                             jlong child1Pointer,
 667                                             jlong child2Pointer)
 668 {
 669   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 670   Solver* solver = reinterpret_cast<Solver*>(pointer);
 671   Op* op = reinterpret_cast<Op*>(opPointer);
 672   Term* child1 = reinterpret_cast<Term*>(child1Pointer);
 673   Term* child2 = reinterpret_cast<Term*>(child2Pointer);
 674   Term* retPointer = new Term(solver->mkTerm(*op, *child1, *child2));
 675   return reinterpret_cast<jlong>(retPointer);
 676   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 677 }
 678
 679 /*
 680  * Class:     io_github_cvc5_api_Solver
 681  * Method:    mkTerm
 682  * Signature: (JJJJJ)J
 683  */
 684 JNIEXPORT jlong JNICALL
 685 Java_io_github_cvc5_api_Solver_mkTerm__JJJJJ(JNIEnv* env,
 686                                              jobject,
 687                                              jlong pointer,
 688                                              jlong opPointer,
 689                                              jlong child1Pointer,
 690                                              jlong child2Pointer,
 691                                              jlong child3Pointer)
 692 {
 693   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 694   Solver* solver = reinterpret_cast<Solver*>(pointer);
 695   Op* op = reinterpret_cast<Op*>(opPointer);
 696   Term* child1 = reinterpret_cast<Term*>(child1Pointer);
 697   Term* child2 = reinterpret_cast<Term*>(child2Pointer);
 698   Term* child3 = reinterpret_cast<Term*>(child3Pointer);
 699   Term* retPointer = new Term(solver->mkTerm(*op, *child1, *child2, *child3));
 700   return reinterpret_cast<jlong>(retPointer);
 701   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 702 }
 703
 704 /*
 705  * Class:     io_github_cvc5_api_Solver
 706  * Method:    mkTerm
 707  * Signature: (JJ[J)J
 708  */
 709 JNIEXPORT jlong JNICALL
 710 Java_io_github_cvc5_api_Solver_mkTerm__JJ_3J(JNIEnv* env,
 711                                              jobject,
 712                                              jlong pointer,
 713                                              jlong opPointer,
 714                                              jlongArray childrenPointers)
 715 {
 716   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 717   Solver* solver = reinterpret_cast<Solver*>(pointer);
 718   Op* op = reinterpret_cast<Op*>(opPointer);
 719   std::vector<Term> children =
 720       getObjectsFromPointers<Term>(env, childrenPointers);
 721   Term* retPointer = new Term(solver->mkTerm(*op, children));
 722   return reinterpret_cast<jlong>(retPointer);
 723   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 724 }
 725
 726 /*
 727  * Class:     io_github_cvc5_api_Solver
 728  * Method:    mkTuple
 729  * Signature: (J[J[J)J
 730  */
 731 JNIEXPORT jlong JNICALL
 732 Java_io_github_cvc5_api_Solver_mkTuple(JNIEnv* env,
 733                                        jobject,
 734                                        jlong pointer,
 735                                        jlongArray sortPointers,
 736                                        jlongArray termPointers)
 737 {
 738   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 739   Solver* solver = reinterpret_cast<Solver*>(pointer);
 740   std::vector<Sort> sorts = getObjectsFromPointers<Sort>(env, sortPointers);
 741   std::vector<Term> terms = getObjectsFromPointers<Term>(env, termPointers);
 742   Term* retPointer = new Term(solver->mkTuple(sorts, terms));
 743   return reinterpret_cast<jlong>(retPointer);
 744   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 745 }
 746
 747 /*
 748  * Class:     io_github_cvc5_api_Solver
 749  * Method:    mkOp
 750  * Signature: (JI)J
 751  */
 752 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkOp__JI(JNIEnv* env,
 753                                                                 jobject,
 754                                                                 jlong pointer,
 755                                                                 jint kindValue)
 756 {
 757   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 758   Solver* solver = reinterpret_cast<Solver*>(pointer);
 759   Kind kind = (Kind)kindValue;
 760   Op* retPointer = new Op(solver->mkOp(kind));
 761   return reinterpret_cast<jlong>(retPointer);
 762   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 763 }
 764
 765 /*
 766  * Class:     io_github_cvc5_api_Solver
 767  * Method:    mkOp
 768  * Signature: (JILjava/lang/String;)J
 769  */
 770 JNIEXPORT jlong JNICALL
 771 Java_io_github_cvc5_api_Solver_mkOp__JILjava_lang_String_2(
 772     JNIEnv* env, jobject, jlong pointer, jint kindValue, jstring jArg)
 773 {
 774   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 775   Solver* solver = reinterpret_cast<Solver*>(pointer);
 776   Kind kind = (Kind)kindValue;
 777   const char* s = env->GetStringUTFChars(jArg, nullptr);
 778   std::string cArg(s);
 779
 780   Op* retPointer = new Op(solver->mkOp(kind, cArg));
 781
 782   env->ReleaseStringUTFChars(jArg, s);
 783   return reinterpret_cast<jlong>(retPointer);
 784   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 785 }
 786
 787 /*
 788  * Class:     io_github_cvc5_api_Solver
 789  * Method:    mkOp
 790  * Signature: (JII)J
 791  */
 792 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkOp__JII(
 793     JNIEnv* env, jobject, jlong pointer, jint kindValue, jint arg)
 794 {
 795   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 796   Solver* solver = reinterpret_cast<Solver*>(pointer);
 797   Kind kind = (Kind)kindValue;
 798   Op* retPointer = new Op(solver->mkOp(kind, (uint32_t)arg));
 799   return reinterpret_cast<jlong>(retPointer);
 800   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 801 }
 802
 803 /*
 804  * Class:     io_github_cvc5_api_Solver
 805  * Method:    mkOp
 806  * Signature: (JIII)J
 807  */
 808 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkOp__JIII(
 809     JNIEnv* env, jobject, jlong pointer, jint kindValue, jint arg1, jint arg2)
 810 {
 811   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 812   Solver* solver = reinterpret_cast<Solver*>(pointer);
 813   Kind kind = (Kind)kindValue;
 814   Op* retPointer = new Op(solver->mkOp(kind, (uint32_t)arg1, (uint32_t)arg2));
 815   return reinterpret_cast<jlong>(retPointer);
 816   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 817 }
 818
 819 /*
 820  * Class:     io_github_cvc5_api_Solver
 821  * Method:    mkOp
 822  * Signature: (JI[I)J
 823  */
 824 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkOp__JI_3I(
 825     JNIEnv* env, jobject, jlong pointer, jint kindValue, jintArray jArgs)
 826 {
 827   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 828   Solver* solver = reinterpret_cast<Solver*>(pointer);
 829   Kind kind = (Kind)kindValue;
 830
 831   jsize size = env->GetArrayLength(jArgs);
 832   jint* argElements = env->GetIntArrayElements(jArgs, nullptr);
 833
 834   std::vector<uint32_t> cArgs(size);
 835   for (jsize i = 0; i < size; i++)
 836   {
 837     cArgs[i] = (uint32_t)argElements[i];
 838   }
 839   env->ReleaseIntArrayElements(jArgs, argElements, 0);
 840
 841   Op* retPointer = new Op(solver->mkOp(kind, cArgs));
 842   return reinterpret_cast<jlong>(retPointer);
 843   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 844 }
 845
 846 /*
 847  * Class:     io_github_cvc5_api_Solver
 848  * Method:    mkTrue
 849  * Signature: (J)J
 850  */
 851 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkTrue(JNIEnv* env,
 852                                                               jobject,
 853                                                               jlong pointer)
 854 {
 855   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 856   Solver* solver = reinterpret_cast<Solver*>(pointer);
 857   Term* termPointer = new Term(solver->mkTrue());
 858   return reinterpret_cast<jlong>(termPointer);
 859   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 860 }
 861
 862 /*
 863  * Class:     io_github_cvc5_api_Solver
 864  * Method:    mkFalse
 865  * Signature: (J)J
 866  */
 867 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkFalse(JNIEnv* env,
 868                                                                jobject,
 869                                                                jlong pointer)
 870 {
 871   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 872   Solver* solver = reinterpret_cast<Solver*>(pointer);
 873   Term* termPointer = new Term(solver->mkFalse());
 874   return reinterpret_cast<jlong>(termPointer);
 875   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 876 }
 877
 878 /*
 879  * Class:     io_github_cvc5_api_Solver
 880  * Method:    mkBoolean
 881  * Signature: (JZ)J
 882  */
 883 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkBoolean(JNIEnv* env,
 884                                                                  jobject,
 885                                                                  jlong pointer,
 886                                                                  jboolean val)
 887 {
 888   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 889   Solver* solver = reinterpret_cast<Solver*>(pointer);
 890   Term* retPointer = new Term(solver->mkBoolean((bool)val));
 891   return reinterpret_cast<jlong>(retPointer);
 892   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 893 }
 894
 895 /*
 896  * Class:     io_github_cvc5_api_Solver
 897  * Method:    mkPi
 898  * Signature: (J)J
 899  */
 900 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkPi(JNIEnv* env,
 901                                                             jobject,
 902                                                             jlong pointer)
 903 {
 904   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 905   Solver* solver = reinterpret_cast<Solver*>(pointer);
 906   Term* retPointer = new Term(solver->mkPi());
 907   return reinterpret_cast<jlong>(retPointer);
 908   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 909 }
 910
 911 /*
 912  * Class:     io_github_cvc5_api_Solver
 913  * Method:    mkInteger
 914  * Signature: (JLjava/lang/String;)J
 915  */
 916 JNIEXPORT jlong JNICALL
 917 Java_io_github_cvc5_api_Solver_mkInteger__JLjava_lang_String_2(JNIEnv* env,
 918                                                                jobject,
 919                                                                jlong pointer,
 920                                                                jstring jS)
 921 {
 922   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 923   Solver* solver = reinterpret_cast<Solver*>(pointer);
 924   const char* s = env->GetStringUTFChars(jS, nullptr);
 925   std::string cS(s);
 926   Term* retPointer = new Term(solver->mkInteger(cS));
 927   env->ReleaseStringUTFChars(jS, s);
 928   return reinterpret_cast<jlong>(retPointer);
 929   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 930 }
 931
 932 /*
 933  * Class:     io_github_cvc5_api_Solver
 934  * Method:    mkInteger
 935  * Signature: (JJ)J
 936  */
 937 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkInteger__JJ(
 938     JNIEnv* env, jobject, jlong pointer, jlong val)
 939 {
 940   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 941   Solver* solver = reinterpret_cast<Solver*>(pointer);
 942   Term* termPointer = new Term(solver->mkInteger((int64_t)val));
 943   return reinterpret_cast<jlong>(termPointer);
 944   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 945 }
 946
 947 /*
 948  * Class:     io_github_cvc5_api_Solver
 949  * Method:    mkReal
 950  * Signature: (JLjava/lang/String;)J
 951  */
 952 JNIEXPORT jlong JNICALL
 953 Java_io_github_cvc5_api_Solver_mkReal__JLjava_lang_String_2(JNIEnv* env,
 954                                                             jobject,
 955                                                             jlong pointer,
 956                                                             jstring jS)
 957 {
 958   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 959   Solver* solver = reinterpret_cast<Solver*>(pointer);
 960   const char* s = env->GetStringUTFChars(jS, nullptr);
 961   std::string cS(s);
 962   Term* retPointer = new Term(solver->mkReal(cS));
 963   env->ReleaseStringUTFChars(jS, s);
 964   return reinterpret_cast<jlong>(retPointer);
 965   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 966 }
 967
 968 /*
 969  * Class:     io_github_cvc5_api_Solver
 970  * Method:    mkRealValue
 971  * Signature: (JJ)J
 972  */
 973 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRealValue(
 974     JNIEnv* env, jobject, jlong pointer, jlong val)
 975 {
 976   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 977   Solver* solver = reinterpret_cast<Solver*>(pointer);
 978   Term* retPointer = new Term(solver->mkReal((int64_t)val));
 979   return reinterpret_cast<jlong>(retPointer);
 980   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 981 }
 982
 983 /*
 984  * Class:     io_github_cvc5_api_Solver
 985  * Method:    mkReal
 986  * Signature: (JJJ)J
 987  */
 988 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkReal__JJJ(
 989     JNIEnv* env, jobject, jlong pointer, jlong num, jlong den)
 990 {
 991   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 992   Solver* solver = reinterpret_cast<Solver*>(pointer);
 993   Term* retPointer = new Term(solver->mkReal((int64_t)num, (int64_t)den));
 994   return reinterpret_cast<jlong>(retPointer);
 995   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 996 }
 997
 998 /*
 999  * Class:     io_github_cvc5_api_Solver
1000  * Method:    mkRegexpNone
1001  * Signature: (J)J
1002  */
1003 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRegexpNone(
1004     JNIEnv* env, jobject, jlong pointer)
1005 {
1006   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1007   Solver* solver = reinterpret_cast<Solver*>(pointer);
1008   Term* retPointer = new Term(solver->mkRegexpNone());
1009   return reinterpret_cast<jlong>(retPointer);
1010   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1011 }
1012
1013 /*
1014  * Class:     io_github_cvc5_api_Solver
1015  * Method:    mkRegexpAll
1016  * Signature: (J)J
1017  */
1018 JNIEXPORT jlong JNICALL
1019 Java_io_github_cvc5_api_Solver_mkRegexpAll(JNIEnv* env, jobject, jlong pointer)
1020 {
1021   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1022   Solver* solver = reinterpret_cast<Solver*>(pointer);
1023   Term* retPointer = new Term(solver->mkRegexpAll());
1024   return reinterpret_cast<jlong>(retPointer);
1025   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1026 }
1027
1028 /*
1029  * Class:     io_github_cvc5_api_Solver
1030  * Method:    mkRegexpAllchar
1031  * Signature: (J)J
1032  */
1033 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRegexpAllchar(
1034     JNIEnv* env, jobject, jlong pointer)
1035 {
1036   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1037   Solver* solver = reinterpret_cast<Solver*>(pointer);
1038   Term* retPointer = new Term(solver->mkRegexpAllchar());
1039   return reinterpret_cast<jlong>(retPointer);
1040   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1041 }
1042
1043 /*
1044  * Class:     io_github_cvc5_api_Solver
1045  * Method:    mkEmptySet
1046  * Signature: (JJ)J
1047  */
1048 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkEmptySet(
1049     JNIEnv* env, jobject, jlong pointer, jlong sortPointer)
1050 {
1051   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1052   Solver* solver = reinterpret_cast<Solver*>(pointer);
1053   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
1054   Term* retPointer = new Term(solver->mkEmptySet(*sort));
1055   return reinterpret_cast<jlong>(retPointer);
1056   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1057 }
1058
1059 /*
1060  * Class:     io_github_cvc5_api_Solver
1061  * Method:    mkEmptyBag
1062  * Signature: (JJ)J
1063  */
1064 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkEmptyBag(
1065     JNIEnv* env, jobject, jlong pointer, jlong sortPointer)
1066 {
1067   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1068   Solver* solver = reinterpret_cast<Solver*>(pointer);
1069   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
1070   Term* retPointer = new Term(solver->mkEmptyBag(*sort));
1071   return reinterpret_cast<jlong>(retPointer);
1072   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1073 }
1074
1075 /*
1076  * Class:     io_github_cvc5_api_Solver
1077  * Method:    mkSepEmp
1078  * Signature: (J)J
1079  */
1080 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkSepEmp(JNIEnv* env,
1081                                                                 jobject,
1082                                                                 jlong pointer)
1083 {
1084   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1085   Solver* solver = reinterpret_cast<Solver*>(pointer);
1086   Term* retPointer = new Term(solver->mkSepEmp());
1087   return reinterpret_cast<jlong>(retPointer);
1088   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1089 }
1090
1091 /*
1092  * Class:     io_github_cvc5_api_Solver
1093  * Method:    mkSepNil
1094  * Signature: (JJ)J
1095  */
1096 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkSepNil(
1097     JNIEnv* env, jobject, jlong pointer, jlong sortPointer)
1098 {
1099   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1100   Solver* solver = reinterpret_cast<Solver*>(pointer);
1101   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
1102   Term* retPointer = new Term(solver->mkSepNil(*sort));
1103   return reinterpret_cast<jlong>(retPointer);
1104   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1105 }
1106
1107 /*
1108  * Class:     io_github_cvc5_api_Solver
1109  * Method:    mkString
1110  * Signature: (JLjava/lang/String;Z)J
1111  */
1112 JNIEXPORT jlong JNICALL
1113 Java_io_github_cvc5_api_Solver_mkString__JLjava_lang_String_2Z(
1114     JNIEnv* env, jobject, jlong pointer, jstring jS, jboolean useEscSequences)
1115 {
1116   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1117   Solver* solver = reinterpret_cast<Solver*>(pointer);
1118   const char* s = env->GetStringUTFChars(jS, nullptr);
1119   std::string cS(s);
1120   Term* retPointer = new Term(solver->mkString(cS, (bool)useEscSequences));
1121   env->ReleaseStringUTFChars(jS, s);
1122   return reinterpret_cast<jlong>(retPointer);
1123   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1124 }
1125
1126 /*
1127  * Class:     io_github_cvc5_api_Solver
1128  * Method:    mkEmptySequence
1129  * Signature: (JJ)J
1130  */
1131 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkEmptySequence(
1132     JNIEnv* env, jobject, jlong pointer, jlong sortPointer)
1133 {
1134   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1135   Solver* solver = reinterpret_cast<Solver*>(pointer);
1136   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
1137   Term* retPointer = new Term(solver->mkEmptySequence(*sort));
1138   return reinterpret_cast<jlong>(retPointer);
1139   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1140 }
1141
1142 /*
1143  * Class:     io_github_cvc5_api_Solver
1144  * Method:    mkUniverseSet
1145  * Signature: (JJ)J
1146  */
1147 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkUniverseSet(
1148     JNIEnv* env, jobject, jlong pointer, jlong sortPointer)
1149 {
1150   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1151   Solver* solver = reinterpret_cast<Solver*>(pointer);
1152   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
1153   Term* retPointer = new Term(solver->mkUniverseSet(*sort));
1154   return reinterpret_cast<jlong>(retPointer);
1155   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1156 }
1157
1158 /*
1159  * Class:     io_github_cvc5_api_Solver
1160  * Method:    mkBitVector
1161  * Signature: (JIJ)J
1162  */
1163 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkBitVector__JIJ(
1164     JNIEnv* env, jobject, jlong pointer, jint size, jlong val)
1165 {
1166   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1167   Solver* solver = reinterpret_cast<Solver*>(pointer);
1168   Term* retPointer =
1169       new Term(solver->mkBitVector((uint32_t)size, (uint64_t)val));
1170   return reinterpret_cast<jlong>(retPointer);
1171   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1172 }
1173
1174 /*
1175  * Class:     io_github_cvc5_api_Solver
1176  * Method:    mkBitVector
1177  * Signature: (JILjava/lang/String;I)J
1178  */
1179 JNIEXPORT jlong JNICALL
1180 Java_io_github_cvc5_api_Solver_mkBitVector__JILjava_lang_String_2I(
1181     JNIEnv* env, jobject, jlong pointer, jint size, jstring jS, jint base)
1182 {
1183   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1184   Solver* solver = reinterpret_cast<Solver*>(pointer);
1185   const char* s = env->GetStringUTFChars(jS, nullptr);
1186   std::string cS(s);
1187   Term* retPointer =
1188       new Term(solver->mkBitVector((uint32_t)size, cS, (uint32_t)base));
1189   env->ReleaseStringUTFChars(jS, s);
1190   return reinterpret_cast<jlong>(retPointer);
1191   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1192 }
1193
1194 /*
1195  * Class:     io_github_cvc5_api_Solver
1196  * Method:    mkConstArray
1197  * Signature: (JJJ)J
1198  */
1199 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkConstArray(
1200     JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jlong valPointer)
1201 {
1202   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1203   Solver* solver = reinterpret_cast<Solver*>(pointer);
1204   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
1205   Term* val = reinterpret_cast<Term*>(valPointer);
1206   Term* retPointer = new Term(solver->mkConstArray(*sort, *val));
1207   return reinterpret_cast<jlong>(retPointer);
1208   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1209 }
1210
1211 /*
1212  * Class:     io_github_cvc5_api_Solver
1213  * Method:    mkPosInf
1214  * Signature: (JII)J
1215  */
1216 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkPosInf(
1217     JNIEnv* env, jobject, jlong pointer, jint exp, jint sig)
1218 {
1219   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1220   Solver* solver = reinterpret_cast<Solver*>(pointer);
1221   Term* retPointer = new Term(solver->mkPosInf((uint32_t)exp, (uint32_t)sig));
1222   return reinterpret_cast<jlong>(retPointer);
1223   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1224 }
1225
1226 /*
1227  * Class:     io_github_cvc5_api_Solver
1228  * Method:    mkNegInf
1229  * Signature: (JII)J
1230  */
1231 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkNegInf(
1232     JNIEnv* env, jobject, jlong pointer, jint exp, jint sig)
1233 {
1234   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1235   Solver* solver = reinterpret_cast<Solver*>(pointer);
1236   Term* retPointer = new Term(solver->mkNegInf((uint32_t)exp, (uint32_t)sig));
1237   return reinterpret_cast<jlong>(retPointer);
1238   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1239 }
1240
1241 /*
1242  * Class:     io_github_cvc5_api_Solver
1243  * Method:    mkNaN
1244  * Signature: (JII)J
1245  */
1246 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkNaN(
1247     JNIEnv* env, jobject, jlong pointer, jint exp, jint sig)
1248 {
1249   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1250   Solver* solver = reinterpret_cast<Solver*>(pointer);
1251   Term* retPointer = new Term(solver->mkNaN((uint32_t)exp, (uint32_t)sig));
1252   return reinterpret_cast<jlong>(retPointer);
1253   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1254 }
1255
1256 /*
1257  * Class:     io_github_cvc5_api_Solver
1258  * Method:    mkPosZero
1259  * Signature: (JII)J
1260  */
1261 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkPosZero(
1262     JNIEnv* env, jobject, jlong pointer, jint exp, jint sig)
1263 {
1264   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1265   Solver* solver = reinterpret_cast<Solver*>(pointer);
1266   Term* retPointer = new Term(solver->mkPosZero((uint32_t)exp, (uint32_t)sig));
1267   return reinterpret_cast<jlong>(retPointer);
1268   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1269 }
1270
1271 /*
1272  * Class:     io_github_cvc5_api_Solver
1273  * Method:    mkNegZero
1274  * Signature: (JII)J
1275  */
1276 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkNegZero(
1277     JNIEnv* env, jobject, jlong pointer, jint exp, jint sig)
1278 {
1279   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1280   Solver* solver = reinterpret_cast<Solver*>(pointer);
1281   Term* retPointer = new Term(solver->mkNegZero((uint32_t)exp, (uint32_t)sig));
1282   return reinterpret_cast<jlong>(retPointer);
1283   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1284 }
1285
1286 /*
1287  * Class:     io_github_cvc5_api_Solver
1288  * Method:    mkRoundingMode
1289  * Signature: (JI)J
1290  */
1291 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRoundingMode(
1292     JNIEnv* env, jobject, jlong pointer, jint rm)
1293 {
1294   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1295   Solver* solver = reinterpret_cast<Solver*>(pointer);
1296   Term* retPointer = new Term(solver->mkRoundingMode((RoundingMode)rm));
1297   return reinterpret_cast<jlong>(retPointer);
1298   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1299 }
1300
1301 /*
1302  * Class:     io_github_cvc5_api_Solver
1303  * Method:    mkUninterpretedConst
1304  * Signature: (JJI)J
1305  */
1306 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkUninterpretedConst(
1307     JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jint index)
1308 {
1309   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1310   Solver* solver = reinterpret_cast<Solver*>(pointer);
1311   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
1312   Term* retPointer =
1313       new Term(solver->mkUninterpretedConst(*sort, (int32_t)index));
1314   return reinterpret_cast<jlong>(retPointer);
1315   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1316 }
1317
1318 /*
1319  * Class:     io_github_cvc5_api_Solver
1320  * Method:    mkAbstractValue
1321  * Signature: (JLjava/lang/String;)J
1322  */
1323 JNIEXPORT jlong JNICALL
1324 Java_io_github_cvc5_api_Solver_mkAbstractValue__JLjava_lang_String_2(
1325     JNIEnv* env, jobject, jlong pointer, jstring jIndex)
1326 {
1327   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1328   Solver* solver = reinterpret_cast<Solver*>(pointer);
1329   const char* s = env->GetStringUTFChars(jIndex, nullptr);
1330   std::string cIndex(s);
1331   Term* retPointer = new Term(solver->mkAbstractValue(cIndex));
1332   env->ReleaseStringUTFChars(jIndex, s);
1333   return reinterpret_cast<jlong>(retPointer);
1334   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1335 }
1336
1337 /*
1338  * Class:     io_github_cvc5_api_Solver
1339  * Method:    mkAbstractValue
1340  * Signature: (JJ)J
1341  */
1342 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkAbstractValue__JJ(
1343     JNIEnv* env, jobject, jlong pointer, jlong index)
1344 {
1345   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1346   Solver* solver = reinterpret_cast<Solver*>(pointer);
1347   Term* retPointer = new Term(solver->mkAbstractValue((uint64_t)index));
1348   return reinterpret_cast<jlong>(retPointer);
1349   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1350 }
1351
1352 /*
1353  * Class:     io_github_cvc5_api_Solver
1354  * Method:    mkFloatingPoint
1355  * Signature: (JIIJ)J
1356  */
1357 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkFloatingPoint(
1358     JNIEnv* env, jobject, jlong pointer, jint exp, jint sig, jlong valPointer)
1359 {
1360   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1361   Solver* solver = reinterpret_cast<Solver*>(pointer);
1362   Term* val = reinterpret_cast<Term*>(valPointer);
1363   Term* retPointer =
1364       new Term(solver->mkFloatingPoint((uint32_t)exp, (uint32_t)sig, *val));
1365   return reinterpret_cast<jlong>(retPointer);
1366   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1367 }
1368
1369 /*
1370  * Class:     io_github_cvc5_api_Solver
1371  * Method:    mkCardinalityConstraint
1372  * Signature: (JJI)J
1373  */
1374 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkCardinalityConstraint(
1375     JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jint upperBound)
1376 {
1377   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1378   Solver* solver = reinterpret_cast<Solver*>(pointer);
1379   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
1380   Term* retPointer =
1381       new Term(solver->mkCardinalityConstraint(*sort, (int32_t)upperBound));
1382   return reinterpret_cast<jlong>(retPointer);
1383   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1384 }
1385
1386 /*
1387  * Class:     io_github_cvc5_api_Solver
1388  * Method:    mkConst
1389  * Signature: (JJLjava/lang/String;)J
1390  */
1391 JNIEXPORT jlong JNICALL
1392 Java_io_github_cvc5_api_Solver_mkConst__JJLjava_lang_String_2(
1393     JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jstring jSymbol)
1394 {
1395   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1396   Solver* solver = reinterpret_cast<Solver*>(pointer);
1397   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
1398   const char* s = env->GetStringUTFChars(jSymbol, nullptr);
1399   std::string cSymbol(s);
1400   Term* retPointer = new Term(solver->mkConst(*sort, cSymbol));
1401   env->ReleaseStringUTFChars(jSymbol, s);
1402   return reinterpret_cast<jlong>(retPointer);
1403   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1404 }
1405
1406 /*
1407  * Class:     io_github_cvc5_api_Solver
1408  * Method:    mkConst
1409  * Signature: (JJ)J
1410  */
1411 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkConst__JJ(
1412     JNIEnv* env, jobject, jlong pointer, jlong sortPointer)
1413 {
1414   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1415   Solver* solver = reinterpret_cast<Solver*>(pointer);
1416   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
1417   Term* retPointer = new Term(solver->mkConst(*sort));
1418   return reinterpret_cast<jlong>(retPointer);
1419   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1420 }
1421
1422 /*
1423  * Class:     io_github_cvc5_api_Solver
1424  * Method:    mkVar
1425  * Signature: (JJLjava/lang/String;)J
1426  */
1427 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkVar(
1428     JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jstring jSymbol)
1429 {
1430   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1431
1432   Solver* solver = reinterpret_cast<Solver*>(pointer);
1433   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
1434   const char* s = env->GetStringUTFChars(jSymbol, nullptr);
1435   std::string cSymbol(s);
1436   Term* ret = new Term(solver->mkVar(*sort, cSymbol));
1437   env->ReleaseStringUTFChars(jSymbol, s);
1438   return reinterpret_cast<jlong>(ret);
1439   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1440 }
1441
1442 /*
1443  * Class:     io_github_cvc5_api_Solver
1444  * Method:    mkDatatypeConstructorDecl
1445  * Signature: (JLjava/lang/String;)J
1446  */
1447 JNIEXPORT jlong JNICALL
1448 Java_io_github_cvc5_api_Solver_mkDatatypeConstructorDecl(JNIEnv* env,
1449                                                          jobject,
1450                                                          jlong pointer,
1451                                                          jstring jName)
1452 {
1453   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1454   Solver* solver = reinterpret_cast<Solver*>(pointer);
1455   const char* s = env->GetStringUTFChars(jName, nullptr);
1456   std::string cName(s);
1457
1458   DatatypeConstructorDecl* retPointer =
1459       new DatatypeConstructorDecl(solver->mkDatatypeConstructorDecl(cName));
1460   env->ReleaseStringUTFChars(jName, s);
1461   return reinterpret_cast<jlong>(retPointer);
1462   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1463 }
1464
1465 /*
1466  * Class:     io_github_cvc5_api_Solver
1467  * Method:    mkDatatypeDecl
1468  * Signature: (JLjava/lang/String;Z)J
1469  */
1470 JNIEXPORT jlong JNICALL
1471 Java_io_github_cvc5_api_Solver_mkDatatypeDecl__JLjava_lang_String_2Z(
1472     JNIEnv* env, jobject, jlong pointer, jstring jName, jboolean isCoDatatype)
1473 {
1474   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1475   Solver* solver = reinterpret_cast<Solver*>(pointer);
1476   const char* s = env->GetStringUTFChars(jName, nullptr);
1477   std::string cName(s);
1478   DatatypeDecl* retPointer =
1479       new DatatypeDecl(solver->mkDatatypeDecl(cName, (bool)isCoDatatype));
1480   env->ReleaseStringUTFChars(jName, s);
1481   return reinterpret_cast<jlong>(retPointer);
1482   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1483 }
1484
1485 /*
1486  * Class:     io_github_cvc5_api_Solver
1487  * Method:    mkDatatypeDecl
1488  * Signature: (JLjava/lang/String;JZ)J
1489  */
1490 JNIEXPORT jlong JNICALL
1491 Java_io_github_cvc5_api_Solver_mkDatatypeDecl__JLjava_lang_String_2JZ(
1492     JNIEnv* env,
1493     jobject,
1494     jlong pointer,
1495     jstring jName,
1496     jlong paramPointer,
1497     jboolean isCoDatatype)
1498 {
1499   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1500   Solver* solver = reinterpret_cast<Solver*>(pointer);
1501   const char* s = env->GetStringUTFChars(jName, nullptr);
1502   std::string cName(s);
1503   Sort* param = reinterpret_cast<Sort*>(paramPointer);
1504   DatatypeDecl* retPointer = new DatatypeDecl(
1505       solver->mkDatatypeDecl(cName, *param, (bool)isCoDatatype));
1506   env->ReleaseStringUTFChars(jName, s);
1507   return reinterpret_cast<jlong>(retPointer);
1508   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1509 }
1510
1511 /*
1512  * Class:     io_github_cvc5_api_Solver
1513  * Method:    mkDatatypeDecl
1514  * Signature: (JLjava/lang/String;[JZ)J
1515  */
1516 JNIEXPORT jlong JNICALL
1517 Java_io_github_cvc5_api_Solver_mkDatatypeDecl__JLjava_lang_String_2_3JZ(
1518     JNIEnv* env,
1519     jobject,
1520     jlong pointer,
1521     jstring jName,
1522     jlongArray jParams,
1523     jboolean isCoDatatype)
1524 {
1525   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1526   Solver* solver = reinterpret_cast<Solver*>(pointer);
1527   const char* s = env->GetStringUTFChars(jName, nullptr);
1528   std::string cName(s);
1529   std::vector<Sort> params = getObjectsFromPointers<Sort>(env, jParams);
1530   DatatypeDecl* retPointer = new DatatypeDecl(
1531       solver->mkDatatypeDecl(cName, params, (bool)isCoDatatype));
1532   env->ReleaseStringUTFChars(jName, s);
1533   return reinterpret_cast<jlong>(retPointer);
1534   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1535 }
1536
1537 /*
1538  * Class:     io_github_cvc5_api_Solver
1539  * Method:    simplify
1540  * Signature: (JJ)J
1541  */
1542 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_simplify(
1543     JNIEnv* env, jobject, jlong pointer, jlong termPointer)
1544 {
1545   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1546   Solver* solver = reinterpret_cast<Solver*>(pointer);
1547   Term* term = reinterpret_cast<Term*>(termPointer);
1548   Term* retPointer = new Term(solver->simplify(*term));
1549   return reinterpret_cast<jlong>(retPointer);
1550   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1551 }
1552
1553 /*
1554  * Class:     io_github_cvc5_api_Solver
1555  * Method:    assertFormula
1556  * Signature: (JJ)V
1557  */
1558 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_assertFormula(
1559     JNIEnv* env, jobject, jlong pointer, jlong termPointer)
1560 {
1561   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1562   Solver* solver = reinterpret_cast<Solver*>(pointer);
1563   Term* term = reinterpret_cast<Term*>(termPointer);
1564   solver->assertFormula(*term);
1565   CVC5_JAVA_API_TRY_CATCH_END(env);
1566 }
1567
1568 /*
1569  * Class:     io_github_cvc5_api_Solver
1570  * Method:    checkSat
1571  * Signature: (J)J
1572  */
1573 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkSat(JNIEnv* env,
1574                                                                 jobject,
1575                                                                 jlong pointer)
1576 {
1577   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1578   Solver* solver = reinterpret_cast<Solver*>(pointer);
1579   Result* retPointer = new Result(solver->checkSat());
1580   return reinterpret_cast<jlong>(retPointer);
1581   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1582 }
1583
1584 /*
1585  * Class:     io_github_cvc5_api_Solver
1586  * Method:    checkSatAssuming
1587  * Signature: (JJ)J
1588  */
1589 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkSatAssuming__JJ(
1590     JNIEnv* env, jobject, jlong pointer, jlong assumptionPointer)
1591 {
1592   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1593   Solver* solver = reinterpret_cast<Solver*>(pointer);
1594   Term* assumption = reinterpret_cast<Term*>(assumptionPointer);
1595   Result* retPointer = new Result(solver->checkSatAssuming(*assumption));
1596   return reinterpret_cast<jlong>(retPointer);
1597   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1598 }
1599
1600 /*
1601  * Class:     io_github_cvc5_api_Solver
1602  * Method:    checkSatAssuming
1603  * Signature: (J[J)J
1604  */
1605 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkSatAssuming__J_3J(
1606     JNIEnv* env, jobject, jlong pointer, jlongArray jAssumptions)
1607 {
1608   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1609   Solver* solver = reinterpret_cast<Solver*>(pointer);
1610   std::vector<Term> assumptions =
1611       getObjectsFromPointers<Term>(env, jAssumptions);
1612   Result* retPointer = new Result(solver->checkSatAssuming(assumptions));
1613   return reinterpret_cast<jlong>(retPointer);
1614   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1615 }
1616
1617 /*
1618  * Class:     io_github_cvc5_api_Solver
1619  * Method:    checkEntailed
1620  * Signature: (JJ)J
1621  */
1622 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkEntailed__JJ(
1623     JNIEnv* env, jobject, jlong pointer, jlong termPointer)
1624 {
1625   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1626   Solver* solver = reinterpret_cast<Solver*>(pointer);
1627   Term* term = reinterpret_cast<Term*>(termPointer);
1628   Result* retPointer = new Result(solver->checkEntailed(*term));
1629   return reinterpret_cast<jlong>(retPointer);
1630   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1631 }
1632
1633 /*
1634  * Class:     io_github_cvc5_api_Solver
1635  * Method:    checkEntailed
1636  * Signature: (J[J)J
1637  */
1638 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkEntailed__J_3J(
1639     JNIEnv* env, jobject, jlong pointer, jlongArray jTerms)
1640 {
1641   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1642   Solver* solver = reinterpret_cast<Solver*>(pointer);
1643   std::vector<Term> terms = getObjectsFromPointers<Term>(env, jTerms);
1644   Result* retPointer = new Result(solver->checkEntailed(terms));
1645   return reinterpret_cast<jlong>(retPointer);
1646   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1647 }
1648
1649 /*
1650  * Class:     io_github_cvc5_api_Solver
1651  * Method:    declareDatatype
1652  * Signature: (JLjava/lang/String;[J)J
1653  */
1654 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_declareDatatype(
1655     JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jlongArray jCtors)
1656 {
1657   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1658   Solver* solver = reinterpret_cast<Solver*>(pointer);
1659   const char* s = env->GetStringUTFChars(jSymbol, nullptr);
1660   std::string cSymbol(s);
1661   std::vector<DatatypeConstructorDecl> ctors =
1662       getObjectsFromPointers<DatatypeConstructorDecl>(env, jCtors);
1663   Sort* retPointer = new Sort(solver->declareDatatype(cSymbol, ctors));
1664   env->ReleaseStringUTFChars(jSymbol, s);
1665   return reinterpret_cast<jlong>(retPointer);
1666   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1667 }
1668
1669 /*
1670  * Class:     io_github_cvc5_api_Solver
1671  * Method:    declareFun
1672  * Signature: (JLjava/lang/String;[JJ)J
1673  */
1674 JNIEXPORT jlong JNICALL
1675 Java_io_github_cvc5_api_Solver_declareFun(JNIEnv* env,
1676                                           jobject,
1677                                           jlong pointer,
1678                                           jstring jSymbol,
1679                                           jlongArray jSorts,
1680                                           jlong sortPointer)
1681 {
1682   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1683   Solver* solver = reinterpret_cast<Solver*>(pointer);
1684   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
1685   const char* s = env->GetStringUTFChars(jSymbol, nullptr);
1686   std::string cSymbol(s);
1687   std::vector<Sort> sorts = getObjectsFromPointers<Sort>(env, jSorts);
1688   Term* retPointer = new Term(solver->declareFun(cSymbol, sorts, *sort));
1689   env->ReleaseStringUTFChars(jSymbol, s);
1690   return reinterpret_cast<jlong>(retPointer);
1691   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1692 }
1693
1694 /*
1695  * Class:     io_github_cvc5_api_Solver
1696  * Method:    declareSort
1697  * Signature: (JLjava/lang/String;I)J
1698  */
1699 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_declareSort(
1700     JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jint arity)
1701 {
1702   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1703   Solver* solver = reinterpret_cast<Solver*>(pointer);
1704   const char* s = env->GetStringUTFChars(jSymbol, nullptr);
1705   std::string cSymbol(s);
1706   Sort* retPointer = new Sort(solver->declareSort(cSymbol, (uint32_t)arity));
1707   return reinterpret_cast<jlong>(retPointer);
1708   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1709 }
1710
1711 /*
1712  * Class:     io_github_cvc5_api_Solver
1713  * Method:    defineFun
1714  * Signature: (JLjava/lang/String;[JJJZ)J
1715  */
1716 JNIEXPORT jlong JNICALL
1717 Java_io_github_cvc5_api_Solver_defineFun(JNIEnv* env,
1718                                          jobject,
1719                                          jlong pointer,
1720                                          jstring jSymbol,
1721                                          jlongArray jVars,
1722                                          jlong sortPointer,
1723                                          jlong termPointer,
1724                                          jboolean global)
1725 {
1726   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1727   Solver* solver = reinterpret_cast<Solver*>(pointer);
1728   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
1729   Term* term = reinterpret_cast<Term*>(termPointer);
1730   const char* s = env->GetStringUTFChars(jSymbol, nullptr);
1731   std::string cSymbol(s);
1732   std::vector<Term> vars = getObjectsFromPointers<Term>(env, jVars);
1733   Term* retPointer =
1734       new Term(solver->defineFun(cSymbol, vars, *sort, *term, (bool)global));
1735   env->ReleaseStringUTFChars(jSymbol, s);
1736   return reinterpret_cast<jlong>(retPointer);
1737   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1738 }
1739
1740 /*
1741  * Class:     io_github_cvc5_api_Solver
1742  * Method:    defineFunRec
1743  * Signature: (JLjava/lang/String;[JJJZ)J
1744  */
1745 JNIEXPORT jlong JNICALL
1746 Java_io_github_cvc5_api_Solver_defineFunRec__JLjava_lang_String_2_3JJJZ(
1747     JNIEnv* env,
1748     jobject,
1749     jlong pointer,
1750     jstring jSymbol,
1751     jlongArray jVars,
1752     jlong sortPointer,
1753     jlong termPointer,
1754     jboolean global)
1755 {
1756   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1757   Solver* solver = reinterpret_cast<Solver*>(pointer);
1758   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
1759   Term* term = reinterpret_cast<Term*>(termPointer);
1760   const char* s = env->GetStringUTFChars(jSymbol, nullptr);
1761   std::string cSymbol(s);
1762   std::vector<Term> vars = getObjectsFromPointers<Term>(env, jVars);
1763   Term* retPointer =
1764       new Term(solver->defineFunRec(cSymbol, vars, *sort, *term, (bool)global));
1765   env->ReleaseStringUTFChars(jSymbol, s);
1766   return reinterpret_cast<jlong>(retPointer);
1767   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1768 }
1769
1770 /*
1771  * Class:     io_github_cvc5_api_Solver
1772  * Method:    defineFunRec
1773  * Signature: (JJ[JJZ)J
1774  */
1775 JNIEXPORT jlong JNICALL
1776 Java_io_github_cvc5_api_Solver_defineFunRec__JJ_3JJZ(JNIEnv* env,
1777                                                      jobject,
1778                                                      jlong pointer,
1779                                                      jlong funPointer,
1780                                                      jlongArray jVars,
1781                                                      jlong termPointer,
1782                                                      jboolean global)
1783 {
1784   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1785   Solver* solver = reinterpret_cast<Solver*>(pointer);
1786   Term* fun = reinterpret_cast<Term*>(funPointer);
1787   Term* term = reinterpret_cast<Term*>(termPointer);
1788   std::vector<Term> vars = getObjectsFromPointers<Term>(env, jVars);
1789   Term* retPointer =
1790       new Term(solver->defineFunRec(*fun, vars, *term, (bool)global));
1791   return reinterpret_cast<jlong>(retPointer);
1792   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1793 }
1794
1795 /*
1796  * Class:     io_github_cvc5_api_Solver
1797  * Method:    defineFunsRec
1798  * Signature: (J[J[[J[JZ)V
1799  */
1800 JNIEXPORT void JNICALL
1801 Java_io_github_cvc5_api_Solver_defineFunsRec(JNIEnv* env,
1802                                              jobject,
1803                                              jlong pointer,
1804                                              jlongArray jFuns,
1805                                              jobjectArray jVars,
1806                                              jlongArray jTerms,
1807                                              jboolean global)
1808 {
1809   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1810   Solver* solver = reinterpret_cast<Solver*>(pointer);
1811   std::vector<Term> funs = getObjectsFromPointers<Term>(env, jFuns);
1812   std::vector<Term> terms = getObjectsFromPointers<Term>(env, jTerms);
1813   std::vector<std::vector<Term>> varsMatrix;
1814   jsize rows = env->GetArrayLength(jVars);
1815   for (jint i = 0; i < rows; i++)
1816   {
1817     std::vector<Term> vars;
1818     jlongArray row = (jlongArray)env->GetObjectArrayElement(jVars, i);
1819     jsize columns = env->GetArrayLength(row);
1820     jlong* columnElements = env->GetLongArrayElements(row, nullptr);
1821     for (jint j = 0; j < columns; j++)
1822     {
1823       Term* var = reinterpret_cast<Term*>((jlongArray)columnElements[j]);
1824       vars.push_back(*var);
1825     }
1826     varsMatrix.push_back(vars);
1827   }
1828   solver->defineFunsRec(funs, varsMatrix, terms, (bool)global);
1829   CVC5_JAVA_API_TRY_CATCH_END(env);
1830 }
1831
1832 /*
1833  * Class:     io_github_cvc5_api_Solver
1834  * Method:    getAssertions
1835  * Signature: (J)[J
1836  */
1837 JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Solver_getAssertions(
1838     JNIEnv* env, jobject, jlong pointer)
1839 {
1840   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1841   Solver* solver = reinterpret_cast<Solver*>(pointer);
1842   std::vector<Term> assertions = solver->getAssertions();
1843   jlongArray ret = getPointersFromObjects<Term>(env, assertions);
1844   return ret;
1845   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
1846 }
1847
1848 /*
1849  * Class:     io_github_cvc5_api_Solver
1850  * Method:    getInfo
1851  * Signature: (JLjava/lang/String;)Ljava/lang/String;
1852  */
1853 JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Solver_getInfo(JNIEnv* env,
1854                                                                  jobject,
1855                                                                  jlong pointer,
1856                                                                  jstring jFlag)
1857 {
1858   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1859   Solver* solver = reinterpret_cast<Solver*>(pointer);
1860   const char* s = env->GetStringUTFChars(jFlag, nullptr);
1861   std::string cFlag(s);
1862   env->ReleaseStringUTFChars(jFlag, s);
1863   return env->NewStringUTF(solver->getInfo(cFlag).c_str());
1864   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1865 }
1866
1867 /*
1868  * Class:     io_github_cvc5_api_Solver
1869  * Method:    getOption
1870  * Signature: (JLjava/lang/String;)Ljava/lang/String;
1871  */
1872 JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Solver_getOption(
1873     JNIEnv* env, jobject, jlong pointer, jstring jOption)
1874 {
1875   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1876   Solver* solver = reinterpret_cast<Solver*>(pointer);
1877   const char* s = env->GetStringUTFChars(jOption, nullptr);
1878   std::string cOption(s);
1879   env->ReleaseStringUTFChars(jOption, s);
1880   return env->NewStringUTF(solver->getOption(cOption).c_str());
1881   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1882 }
1883
1884 /*
1885  * Class:     io_github_cvc5_api_Solver
1886  * Method:    getOptionNames
1887  * Signature: (J)[Ljava/lang/String;
1888  */
1889 JNIEXPORT jobjectArray JNICALL Java_io_github_cvc5_api_Solver_getOptionNames(
1890     JNIEnv* env, jobject, jlong pointer)
1891 {
1892   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1893   Solver* solver = reinterpret_cast<Solver*>(pointer);
1894   std::vector<std::string> options = solver->getOptionNames();
1895   jobjectArray ret = getStringArrayFromStringVector(env, options);
1896   return ret;
1897   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
1898 }
1899
1900 /*
1901  * Class:     io_github_cvc5_api_Solver
1902  * Method:    getOptionInfo
1903  * Signature: (JLjava/lang/String;)J
1904  */
1905 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getOptionInfo(
1906     JNIEnv* env, jobject, jlong pointer, jstring jOption)
1907 {
1908   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1909   Solver* solver = reinterpret_cast<Solver*>(pointer);
1910   std::string cOption(env->GetStringUTFChars(jOption, nullptr));
1911   OptionInfo* ret = new OptionInfo(solver->getOptionInfo(cOption));
1912   return reinterpret_cast<jlong>(ret);
1913   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1914 }
1915
1916 /*
1917  * Class:     io_github_cvc5_api_Solver
1918  * Method:    getDriverOptions
1919  * Signature: (J)J
1920  */
1921 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getDriverOptions(
1922     JNIEnv* env, jobject, jlong pointer)
1923 {
1924   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1925   Solver* solver = reinterpret_cast<Solver*>(pointer);
1926   DriverOptions* ret = new DriverOptions(solver->getDriverOptions());
1927   return reinterpret_cast<jlong>(ret);
1928   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
1929 }
1930
1931 /*
1932  * Class:     io_github_cvc5_api_Solver
1933  * Method:    getUnsatAssumptions
1934  * Signature: (J)[J
1935  */
1936 JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Solver_getUnsatAssumptions(
1937     JNIEnv* env, jobject, jlong pointer)
1938 {
1939   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1940   Solver* solver = reinterpret_cast<Solver*>(pointer);
1941   std::vector<Term> core = solver->getUnsatAssumptions();
1942   jlongArray ret = getPointersFromObjects<Term>(env, core);
1943   return ret;
1944   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
1945 }
1946
1947 /*
1948  * Class:     io_github_cvc5_api_Solver
1949  * Method:    getUnsatCore
1950  * Signature: (J)[J
1951  */
1952 JNIEXPORT jlongArray JNICALL
1953 Java_io_github_cvc5_api_Solver_getUnsatCore(JNIEnv* env, jobject, jlong pointer)
1954 {
1955   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1956   Solver* solver = reinterpret_cast<Solver*>(pointer);
1957   std::vector<Term> core = solver->getUnsatCore();
1958   jlongArray ret = getPointersFromObjects<Term>(env, core);
1959   return ret;
1960   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
1961 }
1962
1963 /*
1964  * Class:     io_github_cvc5_api_Solver
1965  * Method:    getDifficulty
1966  * Signature: (J)Ljava/util/Map;
1967  */
1968 JNIEXPORT jobject JNICALL Java_io_github_cvc5_api_Solver_getDifficulty(
1969     JNIEnv* env, jobject, jlong pointer)
1970 {
1971   CVC5_JAVA_API_TRY_CATCH_BEGIN;
1972   Solver* solver = reinterpret_cast<Solver*>(pointer);
1973   std::map<Term, Term> map = solver->getDifficulty();
1974   // HashMap hashMap = new HashMap();
1975   jclass hashMapClass = env->FindClass("Ljava/util/HashMap;");
1976   jmethodID constructor = env->GetMethodID(hashMapClass, "<init>", "()V");
1977   jobject hashMap = env->NewObject(hashMapClass, constructor);
1978   jmethodID putMethod = env->GetMethodID(
1979       hashMapClass,
1980       "put",
1981       "(Ljava/lang/Object;Ljava/lang/Object;)Ljava/lang/Object;");
1982
1983   // Long longObject = new Long(statPointer)
1984   jclass longClass = env->FindClass("Ljava/lang/Long;");
1985   jmethodID longConstructor = env->GetMethodID(longClass, "<init>", "(J)V");
1986
1987   for (const auto& [k, v] : map)
1988   {
1989     // hashmap.put(key, value);
1990     Term* termKey = new Term(k);
1991     Term* termValue = new Term(v);
1992     jobject key = env->NewObject(
1993         longClass, longConstructor, reinterpret_cast<jlong>(termKey));
1994     jobject value = env->NewObject(
1995         longClass, longConstructor, reinterpret_cast<jlong>(termValue));
1996     env->CallObjectMethod(hashMap, putMethod, key, value);
1997   }
1998   return hashMap;
1999   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
2000 }
2001
2002 /*
2003  * Class:     io_github_cvc5_api_Solver
2004  * Method:    getProof
2005  * Signature: (J)Ljava/lang/String;
2006  */
2007 JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Solver_getProof(JNIEnv* env,
2008                                                                   jobject,
2009                                                                   jlong pointer)
2010 {
2011   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2012   Solver* solver = reinterpret_cast<Solver*>(pointer);
2013   std::string proof = solver->getProof();
2014   return env->NewStringUTF(proof.c_str());
2015   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2016 }
2017
2018 /*
2019  * Class:     io_github_cvc5_api_Solver
2020  * Method:    getValue
2021  * Signature: (JJ)J
2022  */
2023 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getValue__JJ(
2024     JNIEnv* env, jobject, jlong pointer, jlong termPointer)
2025 {
2026   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2027   Solver* solver = reinterpret_cast<Solver*>(pointer);
2028   Term* term = reinterpret_cast<Term*>(termPointer);
2029   Term* retPointer = new Term(solver->getValue(*term));
2030   return reinterpret_cast<jlong>(retPointer);
2031   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2032 }
2033
2034 /*
2035  * Class:     io_github_cvc5_api_Solver
2036  * Method:    getValue
2037  * Signature: (J[J)[J
2038  */
2039 JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Solver_getValue__J_3J(
2040     JNIEnv* env, jobject, jlong pointer, jlongArray termPointers)
2041 {
2042   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2043   Solver* solver = reinterpret_cast<Solver*>(pointer);
2044   std::vector<Term> terms = getObjectsFromPointers<Term>(env, termPointers);
2045   std::vector<Term> values = solver->getValue(terms);
2046   jlongArray ret = getPointersFromObjects<Term>(env, values);
2047   return ret;
2048   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2049 }
2050
2051 /*
2052  * Class:     io_github_cvc5_api_Solver
2053  * Method:    getModelDomainElements
2054  * Signature: (JJ)[J
2055  */
2056 JNIEXPORT jlongArray JNICALL
2057 Java_io_github_cvc5_api_Solver_getModelDomainElements(JNIEnv* env,
2058                                                       jobject,
2059                                                       jlong pointer,
2060                                                       jlong sortPointer)
2061 {
2062   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2063   Solver* solver = reinterpret_cast<Solver*>(pointer);
2064   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
2065   std::vector<Term> terms = solver->getModelDomainElements(*sort);
2066   jlongArray ret = getPointersFromObjects<Term>(env, terms);
2067   return ret;
2068   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
2069 }
2070
2071 /*
2072  * Class:     io_github_cvc5_api_Solver
2073  * Method:    isModelCoreSymbol
2074  * Signature: (JJ)Z
2075  */
2076 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_isModelCoreSymbol(
2077     JNIEnv* env, jobject, jlong pointer, jlong termPointer)
2078 {
2079   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2080   Solver* solver = reinterpret_cast<Solver*>(pointer);
2081   Term* term = reinterpret_cast<Term*>(termPointer);
2082   return static_cast<jboolean>(solver->isModelCoreSymbol(*term));
2083   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
2084 }
2085
2086 /*
2087  * Class:     io_github_cvc5_api_Solver
2088  * Method:    getModel
2089  * Signature: (J[J[J)Ljava/lang/String;
2090  */
2091 JNIEXPORT jstring JNICALL
2092 Java_io_github_cvc5_api_Solver_getModel(JNIEnv* env,
2093                                         jobject,
2094                                         jlong pointer,
2095                                         jlongArray sortPointers,
2096                                         jlongArray varPointers)
2097 {
2098   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2099   Solver* solver = reinterpret_cast<Solver*>(pointer);
2100   std::vector<Sort> sorts = getObjectsFromPointers<Sort>(env, sortPointers);
2101   std::vector<Term> vars = getObjectsFromPointers<Term>(env, varPointers);
2102   std::string model = solver->getModel(sorts, vars);
2103   return env->NewStringUTF(model.c_str());
2104   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2105 }
2106
2107 /*
2108  * Class:     io_github_cvc5_api_Solver
2109  * Method:    getQuantifierElimination
2110  * Signature: (JJ)J
2111  */
2112 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getQuantifierElimination(
2113     JNIEnv* env, jobject, jlong pointer, jlong qPointer)
2114 {
2115   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2116   Solver* solver = reinterpret_cast<Solver*>(pointer);
2117   Term* q = reinterpret_cast<Term*>(qPointer);
2118   Term* retPointer = new Term(solver->getQuantifierElimination(*q));
2119   return reinterpret_cast<jlong>(retPointer);
2120   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2121 }
2122
2123 /*
2124  * Class:     io_github_cvc5_api_Solver
2125  * Method:    getQuantifierEliminationDisjunct
2126  * Signature: (JJ)J
2127  */
2128 JNIEXPORT jlong JNICALL
2129 Java_io_github_cvc5_api_Solver_getQuantifierEliminationDisjunct(JNIEnv* env,
2130                                                                 jobject,
2131                                                                 jlong pointer,
2132                                                                 jlong qPointer)
2133 {
2134   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2135   Solver* solver = reinterpret_cast<Solver*>(pointer);
2136   Term* q = reinterpret_cast<Term*>(qPointer);
2137   Term* retPointer = new Term(solver->getQuantifierEliminationDisjunct(*q));
2138   return reinterpret_cast<jlong>(retPointer);
2139   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2140 }
2141
2142 /*
2143  * Class:     io_github_cvc5_api_Solver
2144  * Method:    declareSepHeap
2145  * Signature: (JJJ)V
2146  */
2147 JNIEXPORT void JNICALL
2148 Java_io_github_cvc5_api_Solver_declareSepHeap(JNIEnv* env,
2149                                               jobject,
2150                                               jlong pointer,
2151                                               jlong locSortPointer,
2152                                               jlong dataSortPointer)
2153 {
2154   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2155   Solver* solver = reinterpret_cast<Solver*>(pointer);
2156   Sort* locSort = reinterpret_cast<Sort*>(locSortPointer);
2157   Sort* dataSort = reinterpret_cast<Sort*>(dataSortPointer);
2158   solver->declareSepHeap(*locSort, *dataSort);
2159   CVC5_JAVA_API_TRY_CATCH_END(env);
2160 }
2161
2162 /*
2163  * Class:     io_github_cvc5_api_Solver
2164  * Method:    getValueSepHeap
2165  * Signature: (J)J
2166  */
2167 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getValueSepHeap(
2168     JNIEnv* env, jobject, jlong pointer)
2169 {
2170   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2171   Solver* solver = reinterpret_cast<Solver*>(pointer);
2172   Term* retPointer = new Term(solver->getValueSepHeap());
2173   return reinterpret_cast<jlong>(retPointer);
2174   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2175 }
2176
2177 /*
2178  * Class:     io_github_cvc5_api_Solver
2179  * Method:    getValueSepNil
2180  * Signature: (J)J
2181  */
2182 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getValueSepNil(
2183     JNIEnv* env, jobject, jlong pointer)
2184 {
2185   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2186   Solver* solver = reinterpret_cast<Solver*>(pointer);
2187   Term* retPointer = new Term(solver->getValueSepNil());
2188   return reinterpret_cast<jlong>(retPointer);
2189   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2190 }
2191
2192 /*
2193  * Class:     io_github_cvc5_api_Solver
2194  * Method:    pop
2195  * Signature: (JI)V
2196  */
2197 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_pop(JNIEnv* env,
2198                                                           jobject,
2199                                                           jlong pointer,
2200                                                           jint nscopes)
2201 {
2202   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2203   Solver* solver = reinterpret_cast<Solver*>(pointer);
2204   solver->pop((uint32_t)nscopes);
2205   CVC5_JAVA_API_TRY_CATCH_END(env);
2206 }
2207
2208 /*
2209  * Class:     io_github_cvc5_api_Solver
2210  * Method:    getInterpolant
2211  * Signature: (JJJ)Z
2212  */
2213 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_getInterpolant__JJJ(
2214     JNIEnv* env, jobject, jlong pointer, jlong conjPointer, jlong outputPointer)
2215 {
2216   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2217   Solver* solver = reinterpret_cast<Solver*>(pointer);
2218   Term* conj = reinterpret_cast<Term*>(conjPointer);
2219   Term* output = reinterpret_cast<Term*>(outputPointer);
2220   return (jboolean)solver->getInterpolant(*conj, *output);
2221   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2222 }
2223
2224 /*
2225  * Class:     io_github_cvc5_api_Solver
2226  * Method:    getInterpolant
2227  * Signature: (JJJJ)Z
2228  */
2229 JNIEXPORT jboolean JNICALL
2230 Java_io_github_cvc5_api_Solver_getInterpolant__JJJJ(JNIEnv* env,
2231                                                     jobject,
2232                                                     jlong pointer,
2233                                                     jlong conjPointer,
2234                                                     jlong grammarPointer,
2235                                                     jlong outputPointer)
2236 {
2237   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2238   Solver* solver = reinterpret_cast<Solver*>(pointer);
2239   Term* conj = reinterpret_cast<Term*>(conjPointer);
2240   Grammar* grammar = reinterpret_cast<Grammar*>(grammarPointer);
2241   Term* output = reinterpret_cast<Term*>(outputPointer);
2242   return (jboolean)solver->getInterpolant(*conj, *grammar, *output);
2243   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2244 }
2245
2246 /*
2247  * Class:     io_github_cvc5_api_Solver
2248  * Method:    getAbduct
2249  * Signature: (JJJ)Z
2250  */
2251 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_getAbduct__JJJ(
2252     JNIEnv* env, jobject, jlong pointer, jlong conjPointer, jlong outputPointer)
2253 {
2254   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2255   Solver* solver = reinterpret_cast<Solver*>(pointer);
2256   Term* conj = reinterpret_cast<Term*>(conjPointer);
2257   Term* output = reinterpret_cast<Term*>(outputPointer);
2258   return (jboolean)solver->getAbduct(*conj, *output);
2259   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2260 }
2261
2262 /*
2263  * Class:     io_github_cvc5_api_Solver
2264  * Method:    getAbduct
2265  * Signature: (JJJJ)Z
2266  */
2267 JNIEXPORT jboolean JNICALL
2268 Java_io_github_cvc5_api_Solver_getAbduct__JJJJ(JNIEnv* env,
2269                                                jobject,
2270                                                jlong pointer,
2271                                                jlong conjPointer,
2272                                                jlong grammarPointer,
2273                                                jlong outputPointer)
2274 {
2275   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2276   Solver* solver = reinterpret_cast<Solver*>(pointer);
2277   Term* conj = reinterpret_cast<Term*>(conjPointer);
2278   Grammar* grammar = reinterpret_cast<Grammar*>(grammarPointer);
2279   Term* output = reinterpret_cast<Term*>(outputPointer);
2280   return (jboolean)solver->getAbduct(*conj, *grammar, *output);
2281   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2282 }
2283
2284 /*
2285  * Class:     io_github_cvc5_api_Solver
2286  * Method:    getAbductNext
2287  * Signature: (JJ)Z
2288  */
2289 JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Solver_getAbductNext
2290     (JNIEnv * env, jobject, jlong pointer, jlong outputPointer)
2291 {
2292   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2293   Solver* solver = reinterpret_cast<Solver*>(pointer);
2294   Term* output = reinterpret_cast<Term*>(outputPointer);
2295   return (jboolean)solver->getAbductNext(*output);
2296   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2297 }
2298
2299 /*
2300  * Class:     io_github_cvc5_api_Solver
2301  * Method:    blockModel
2302  * Signature: (J)V
2303  */
2304 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_blockModel(JNIEnv* env,
2305                                                                  jobject,
2306                                                                  jlong pointer)
2307 {
2308   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2309   Solver* solver = reinterpret_cast<Solver*>(pointer);
2310   solver->blockModel();
2311   CVC5_JAVA_API_TRY_CATCH_END(env);
2312 }
2313
2314 /*
2315  * Class:     io_github_cvc5_api_Solver
2316  * Method:    blockModelValues
2317  * Signature: (J[J)V
2318  */
2319 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_blockModelValues(
2320     JNIEnv* env, jobject, jlong pointer, jlongArray jTerms)
2321 {
2322   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2323   Solver* solver = reinterpret_cast<Solver*>(pointer);
2324   std::vector<Term> terms = getObjectsFromPointers<Term>(env, jTerms);
2325   solver->blockModelValues(terms);
2326   CVC5_JAVA_API_TRY_CATCH_END(env);
2327 }
2328
2329 /*
2330  * Class:     io_github_cvc5_api_Solver
2331  * Method:    push
2332  * Signature: (JI)V
2333  */
2334 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_push(JNIEnv* env,
2335                                                            jobject,
2336                                                            jlong pointer,
2337                                                            jint nscopes)
2338 {
2339   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2340   Solver* solver = reinterpret_cast<Solver*>(pointer);
2341   solver->push((uint32_t)nscopes);
2342   CVC5_JAVA_API_TRY_CATCH_END(env);
2343 }
2344
2345 /*
2346  * Class:     io_github_cvc5_api_Solver
2347  * Method:    resetAssertions
2348  * Signature: (J)V
2349  */
2350 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_resetAssertions(
2351     JNIEnv* env, jobject, jlong pointer)
2352 {
2353   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2354   Solver* solver = reinterpret_cast<Solver*>(pointer);
2355   solver->resetAssertions();
2356   CVC5_JAVA_API_TRY_CATCH_END(env);
2357 }
2358
2359 /*
2360  * Class:     io_github_cvc5_api_Solver
2361  * Method:    setInfo
2362  * Signature: (JLjava/lang/String;Ljava/lang/String;)V
2363  */
2364 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_setInfo(
2365     JNIEnv* env, jobject, jlong pointer, jstring jKeyword, jstring jValue)
2366 {
2367   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2368   Solver* solver = reinterpret_cast<Solver*>(pointer);
2369   const char* sKeyword = env->GetStringUTFChars(jKeyword, nullptr);
2370   const char* sValue = env->GetStringUTFChars(jValue, nullptr);
2371   std::string cKeyword(sKeyword);
2372   std::string cValue(sValue);
2373   solver->setInfo(cKeyword, cValue);
2374   env->ReleaseStringUTFChars(jKeyword, sKeyword);
2375   env->ReleaseStringUTFChars(jValue, sValue);
2376   CVC5_JAVA_API_TRY_CATCH_END(env);
2377 }
2378
2379 /*
2380  * Class:     io_github_cvc5_api_Solver
2381  * Method:    setLogic
2382  * Signature: (JLjava/lang/String;)V
2383  */
2384 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_setLogic(JNIEnv* env,
2385                                                                jobject,
2386                                                                jlong pointer,
2387                                                                jstring jLogic)
2388 {
2389   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2390
2391   Solver* solver = reinterpret_cast<Solver*>(pointer);
2392   const char* cLogic = env->GetStringUTFChars(jLogic, nullptr);
2393   solver->setLogic(std::string(cLogic));
2394
2395   CVC5_JAVA_API_TRY_CATCH_END(env);
2396 }
2397
2398 /*
2399  * Class:     io_github_cvc5_api_Solver
2400  * Method:    setOption
2401  * Signature: (JLjava/lang/String;Ljava/lang/String;)V
2402  */
2403 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_setOption(
2404     JNIEnv* env, jobject, jlong pointer, jstring jOption, jstring jValue)
2405 {
2406   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2407   Solver* solver = reinterpret_cast<Solver*>(pointer);
2408   const char* sOption = env->GetStringUTFChars(jOption, nullptr);
2409   const char* sValue = env->GetStringUTFChars(jValue, nullptr);
2410   std::string cOption(sOption);
2411   std::string cValue(sValue);
2412   solver->setOption(cOption, cValue);
2413   env->ReleaseStringUTFChars(jOption, sOption);
2414   env->ReleaseStringUTFChars(jValue, sValue);
2415   CVC5_JAVA_API_TRY_CATCH_END(env);
2416 }
2417
2418 /*
2419  * Class:     io_github_cvc5_api_Solver
2420  * Method:    ensureTermSort
2421  * Signature: (JJJ)J
2422  */
2423 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_ensureTermSort(
2424     JNIEnv* env, jobject, jlong pointer, jlong termPointer, jlong sortPointer)
2425 {
2426   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2427   Solver* solver = reinterpret_cast<Solver*>(pointer);
2428   Term* term = reinterpret_cast<Term*>(termPointer);
2429   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
2430   Term* retPointer = new Term(solver->ensureTermSort(*term, *sort));
2431   return reinterpret_cast<jlong>(retPointer);
2432   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2433 }
2434
2435 /*
2436  * Class:     io_github_cvc5_api_Solver
2437  * Method:    mkSygusVar
2438  * Signature: (JJLjava/lang/String;)J
2439  */
2440 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkSygusVar(
2441     JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jstring jSymbol)
2442 {
2443   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2444   Solver* solver = reinterpret_cast<Solver*>(pointer);
2445   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
2446   const char* s = env->GetStringUTFChars(jSymbol, nullptr);
2447   std::string cSymbol(s);
2448   Term* retPointer = new Term(solver->mkSygusVar(*sort, cSymbol));
2449   env->ReleaseStringUTFChars(jSymbol, s);
2450   return reinterpret_cast<jlong>(retPointer);
2451   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2452 }
2453
2454 /*
2455  * Class:     io_github_cvc5_api_Solver
2456  * Method:    mkSygusGrammar
2457  * Signature: (J[J[J)J
2458  */
2459 JNIEXPORT jlong JNICALL
2460 Java_io_github_cvc5_api_Solver_mkSygusGrammar(JNIEnv* env,
2461                                               jobject,
2462                                               jlong pointer,
2463                                               jlongArray jBoundVars,
2464                                               jlongArray jNtSymbols)
2465 {
2466   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2467   Solver* solver = reinterpret_cast<Solver*>(pointer);
2468   std::vector<Term> boundVars = getObjectsFromPointers<Term>(env, jBoundVars);
2469   std::vector<Term> ntSymbols = getObjectsFromPointers<Term>(env, jNtSymbols);
2470   Grammar* retPointer =
2471       new Grammar(solver->mkSygusGrammar(boundVars, ntSymbols));
2472   return reinterpret_cast<jlong>(retPointer);
2473   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2474 }
2475
2476 /*
2477  * Class:     io_github_cvc5_api_Solver
2478  * Method:    synthFun
2479  * Signature: (JLjava/lang/String;[JJ)J
2480  */
2481 JNIEXPORT jlong JNICALL
2482 Java_io_github_cvc5_api_Solver_synthFun__JLjava_lang_String_2_3JJ(
2483     JNIEnv* env,
2484     jobject,
2485     jlong pointer,
2486     jstring jSymbol,
2487     jlongArray jVars,
2488     jlong sortPointer)
2489 {
2490   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2491   Solver* solver = reinterpret_cast<Solver*>(pointer);
2492   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
2493   const char* s = env->GetStringUTFChars(jSymbol, nullptr);
2494   std::string cSymbol(s);
2495   std::vector<Term> boundVars = getObjectsFromPointers<Term>(env, jVars);
2496   Term* retPointer = new Term(solver->synthFun(cSymbol, boundVars, *sort));
2497   env->ReleaseStringUTFChars(jSymbol, s);
2498   return reinterpret_cast<jlong>(retPointer);
2499   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2500 }
2501
2502 /*
2503  * Class:     io_github_cvc5_api_Solver
2504  * Method:    synthFun
2505  * Signature: (JLjava/lang/String;[JJJ)J
2506  */
2507 JNIEXPORT jlong JNICALL
2508 Java_io_github_cvc5_api_Solver_synthFun__JLjava_lang_String_2_3JJJ(
2509     JNIEnv* env,
2510     jobject,
2511     jlong pointer,
2512     jstring jSymbol,
2513     jlongArray jVars,
2514     jlong sortPointer,
2515     jlong grammarPointer)
2516 {
2517   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2518   Solver* solver = reinterpret_cast<Solver*>(pointer);
2519   Sort* sort = reinterpret_cast<Sort*>(sortPointer);
2520   Grammar* grammar = reinterpret_cast<Grammar*>(grammarPointer);
2521   const char* s = env->GetStringUTFChars(jSymbol, nullptr);
2522   std::string cSymbol(s);
2523   std::vector<Term> boundVars = getObjectsFromPointers<Term>(env, jVars);
2524   Term* retPointer =
2525       new Term(solver->synthFun(cSymbol, boundVars, *sort, *grammar));
2526   env->ReleaseStringUTFChars(jSymbol, s);
2527   return reinterpret_cast<jlong>(retPointer);
2528   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2529 }
2530
2531 /*
2532  * Class:     io_github_cvc5_api_Solver
2533  * Method:    synthInv
2534  * Signature: (JLjava/lang/String;[J)J
2535  */
2536 JNIEXPORT jlong JNICALL
2537 Java_io_github_cvc5_api_Solver_synthInv__JLjava_lang_String_2_3J(
2538     JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jlongArray jVars)
2539 {
2540   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2541   Solver* solver = reinterpret_cast<Solver*>(pointer);
2542   const char* s = env->GetStringUTFChars(jSymbol, nullptr);
2543   std::string cSymbol(s);
2544   std::vector<Term> vars = getObjectsFromPointers<Term>(env, jVars);
2545   Term* retPointer = new Term(solver->synthInv(cSymbol, vars));
2546   env->ReleaseStringUTFChars(jSymbol, s);
2547   return reinterpret_cast<jlong>(retPointer);
2548   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2549 }
2550
2551 /*
2552  * Class:     io_github_cvc5_api_Solver
2553  * Method:    synthInv
2554  * Signature: (JLjava/lang/String;[JJ)J
2555  */
2556 JNIEXPORT jlong JNICALL
2557 Java_io_github_cvc5_api_Solver_synthInv__JLjava_lang_String_2_3JJ(
2558     JNIEnv* env,
2559     jobject,
2560     jlong pointer,
2561     jstring jSymbol,
2562     jlongArray jVars,
2563     jlong grammarPointer)
2564 {
2565   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2566   Solver* solver = reinterpret_cast<Solver*>(pointer);
2567   Grammar* grammar = reinterpret_cast<Grammar*>(grammarPointer);
2568   const char* s = env->GetStringUTFChars(jSymbol, nullptr);
2569   std::string cSymbol(s);
2570   std::vector<Term> vars = getObjectsFromPointers<Term>(env, jVars);
2571   Term* retPointer = new Term(solver->synthInv(cSymbol, vars, *grammar));
2572   env->ReleaseStringUTFChars(jSymbol, s);
2573   return reinterpret_cast<jlong>(retPointer);
2574   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2575 }
2576
2577 /*
2578  * Class:     io_github_cvc5_api_Solver
2579  * Method:    addSygusConstraint
2580  * Signature: (JJ)V
2581  */
2582 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_addSygusConstraint(
2583     JNIEnv* env, jobject, jlong pointer, jlong termPointer)
2584 {
2585   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2586   Solver* solver = reinterpret_cast<Solver*>(pointer);
2587   Term* term = reinterpret_cast<Term*>(termPointer);
2588   solver->addSygusConstraint(*term);
2589   CVC5_JAVA_API_TRY_CATCH_END(env);
2590 }
2591
2592 /*
2593  * Class:     io_github_cvc5_api_Solver
2594  * Method:    addSygusAssume
2595  * Signature: (JJ)V
2596  */
2597 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_addSygusAssume(
2598     JNIEnv* env, jobject, jlong pointer, jlong termPointer)
2599 {
2600   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2601   Solver* solver = reinterpret_cast<Solver*>(pointer);
2602   Term* term = reinterpret_cast<Term*>(termPointer);
2603   solver->addSygusAssume(*term);
2604   CVC5_JAVA_API_TRY_CATCH_END(env);
2605 }
2606
2607 /*
2608  * Class:     io_github_cvc5_api_Solver
2609  * Method:    addSygusInvConstraint
2610  * Signature: (JJJJJ)V
2611  */
2612 JNIEXPORT void JNICALL
2613 Java_io_github_cvc5_api_Solver_addSygusInvConstraint(JNIEnv* env,
2614                                                      jobject,
2615                                                      jlong pointer,
2616                                                      jlong invPointer,
2617                                                      jlong prePointer,
2618                                                      jlong transPointer,
2619                                                      jlong postPointer)
2620 {
2621   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2622   Solver* solver = reinterpret_cast<Solver*>(pointer);
2623   Term* inv = reinterpret_cast<Term*>(invPointer);
2624   Term* pre = reinterpret_cast<Term*>(prePointer);
2625   Term* trans = reinterpret_cast<Term*>(transPointer);
2626   Term* post = reinterpret_cast<Term*>(postPointer);
2627   solver->addSygusInvConstraint(*inv, *pre, *trans, *post);
2628   CVC5_JAVA_API_TRY_CATCH_END(env);
2629 }
2630
2631 /*
2632  * Class:     io_github_cvc5_api_Solver
2633  * Method:    checkSynth
2634  * Signature: (J)J
2635  */
2636 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkSynth(JNIEnv* env,
2637                                                                   jobject,
2638                                                                   jlong pointer)
2639 {
2640   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2641   Solver* solver = reinterpret_cast<Solver*>(pointer);
2642   Result* retPointer = new Result(solver->checkSynth());
2643   return reinterpret_cast<jlong>(retPointer);
2644   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2645 }
2646
2647 /*
2648  * Class:     io_github_cvc5_api_Solver
2649  * Method:    checkSynthNext
2650  * Signature: (J)J
2651  */
2652 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_checkSynthNext(
2653     JNIEnv* env, jobject, jlong pointer)
2654 {
2655   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2656   Solver* solver = reinterpret_cast<Solver*>(pointer);
2657   Result* retPointer = new Result(solver->checkSynthNext());
2658   return reinterpret_cast<jlong>(retPointer);
2659   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2660 }
2661
2662 /*
2663  * Class:     io_github_cvc5_api_Solver
2664  * Method:    getSynthSolution
2665  * Signature: (JJ)J
2666  */
2667 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getSynthSolution(
2668     JNIEnv* env, jobject, jlong pointer, jlong termPointer)
2669 {
2670   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2671   Solver* solver = reinterpret_cast<Solver*>(pointer);
2672   Term* term = reinterpret_cast<Term*>(termPointer);
2673   Term* retPointer = new Term(solver->getSynthSolution(*term));
2674   return reinterpret_cast<jlong>(retPointer);
2675   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2676 }
2677
2678 /*
2679  * Class:     io_github_cvc5_api_Solver
2680  * Method:    getSynthSolutions
2681  * Signature: (J[J)[J
2682  */
2683 JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Solver_getSynthSolutions(
2684     JNIEnv* env, jobject, jlong pointer, jlongArray jTerms)
2685 {
2686   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2687   Solver* solver = reinterpret_cast<Solver*>(pointer);
2688   std::vector<Term> terms = getObjectsFromPointers<Term>(env, jTerms);
2689   std::vector<Term> solutions = solver->getSynthSolutions(terms);
2690   jlongArray ret = getPointersFromObjects<Term>(env, solutions);
2691   return ret;
2692   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
2693 }
2694
2695 /*
2696  * Class:     io_github_cvc5_api_Solver
2697  * Method:    getStatistics
2698  * Signature: (J)J
2699  */
2700 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getStatistics(
2701     JNIEnv* env, jobject, jlong pointer)
2702 {
2703   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2704   Solver* solver = reinterpret_cast<Solver*>(pointer);
2705   Statistics* retPointer = new Statistics(solver->getStatistics());
2706   return reinterpret_cast<jlong>(retPointer);
2707   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2708 }
2709
2710 /*
2711  * Class:     io_github_cvc5_api_Solver
2712  * Method:    getNullTerm
2713  * Signature: (J)J
2714  */
2715 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getNullTerm(JNIEnv* env,
2716                                                                    jobject,
2717                                                                    jlong)
2718 {
2719   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2720   Term* ret = new Term();
2721   return reinterpret_cast<jlong>(ret);
2722   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2723 }
2724
2725 /*
2726  * Class:     io_github_cvc5_api_Solver
2727  * Method:    getNullResult
2728  * Signature: (J)J
2729  */
2730 JNIEXPORT jlong JNICALL
2731 Java_io_github_cvc5_api_Solver_getNullResult(JNIEnv* env, jobject, jlong)
2732 {
2733   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2734   Result* ret = new Result();
2735   return reinterpret_cast<jlong>(ret);
2736   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2737 }
2738
2739 /*
2740  * Class:     io_github_cvc5_api_Solver
2741  * Method:    getNullOp
2742  * Signature: (J)J
2743  */
2744 JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getNullOp(JNIEnv* env,
2745                                                                  jobject,
2746                                                                  jlong)
2747 {
2748   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2749   Op* ret = new Op();
2750   return reinterpret_cast<jlong>(ret);
2751   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2752 }
2753
2754 /*
2755  * Class:     io_github_cvc5_api_Solver
2756  * Method:    getNullDatatypeDecl
2757  * Signature: (J)J
2758  */
2759 JNIEXPORT jlong JNICALL
2760 Java_io_github_cvc5_api_Solver_getNullDatatypeDecl(JNIEnv* env, jobject, jlong)
2761 {
2762   CVC5_JAVA_API_TRY_CATCH_BEGIN;
2763   DatatypeDecl* ret = new DatatypeDecl();
2764   return reinterpret_cast<jlong>(ret);
2765   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
2766 }