Add declareOracleFun to the Java API (#8815)

diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt
index 736ffddb9d365cc81f23ad4691f627a4c99a0692..93b018179ce1bfbe2e2810a8466b6528249d2a7d 100644 (file)
--- a/src/api/java/CMakeLists.txt
+++ b/src/api/java/CMakeLists.txt
@@ -75,6 +75,7 @@ set(JAVA_FILES
   ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/DatatypeDecl.java
   ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/DatatypeSelector.java
   ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/Grammar.java
+  ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/IOracle.java
   ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/IPointer.java
   ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/Op.java
   ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/OptionInfo.java

diff --git a/src/api/java/io/github/cvc5/IOracle.java b/src/api/java/io/github/cvc5/IOracle.java
new file mode 100644 (file)
index 0000000..cab3cc8
--- /dev/null
+++ b/src/api/java/io/github/cvc5/IOracle.java
@@ -0,0 +1,23 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The cvc5 java API.
+ *
+ * IOracle interface for cvc5 oracle functions.
+ */
+
+package io.github.cvc5;
+
+@FunctionalInterface
+public interface IOracle {
+  Term apply(Term[] terms) throws CVC5ApiException;
+}

diff --git a/src/api/java/io/github/cvc5/Solver.java b/src/api/java/io/github/cvc5/Solver.java
index a3fcb4ce4d154b98d86e9596bcf186a43c28d6af..c89701f9bdae403d286001ca5ff05710d09178c0 100644 (file)
--- a/src/api/java/io/github/cvc5/Solver.java
+++ b/src/api/java/io/github/cvc5/Solver.java
@@ -47,6 +47,9 @@ public class Solver implements IPointer, AutoCloseable
   // store pointers for terms, sorts, etc
   List<AbstractPointer> abstractPointers = new ArrayList<>();
 
+  // store IOracle objects
+  List<IOracle> oracles = new ArrayList<>();
+
   @Override
   public void close()
   {
@@ -57,6 +60,8 @@ public class Solver implements IPointer, AutoCloseable
     }
     // delete the heap memory for this solver
     deletePointer();
+    // clear oracles
+    oracles.clear();
   }
 
   void addAbstractPointer(AbstractPointer abstractPointer)
@@ -2180,6 +2185,42 @@ public class Solver implements IPointer, AutoCloseable
   private native long declarePool(
       long pointer, String symbol, long sortPointer, long[] termPointers);
 
+  /**
+   * Declare an oracle function with reference to an implementation.
+   *
+   * Oracle functions have a different semantics with respect to ordinary
+   * declared functions. In particular, for an input to be satisfiable,
+   * its oracle functions are implicitly universally quantified.
+   *
+   * This method is used in part for implementing this command:
+   *
+   * {@code
+   * (declare-oracle-fun <sym> (<sort>*) <sort> <sym>)
+   * }
+   *
+   *
+   * In particular, the above command is implemented by constructing a
+   * function over terms that wraps a call to binary sym via a text interface.
+   *
+   * @api.note This method is experimental and may change in future versions.
+   *
+   * @param symbol The name of the oracle
+   * @param sorts The sorts of the parameters to this function
+   * @param sort The sort of the return value of this function
+   * @param oracle An object that implements the oracle interface.
+   * @return The oracle function
+   */
+  public Term declareOracleFun(String symbol, Sort[] sorts, Sort sort, IOracle oracle)
+  {
+    oracles.add(oracle);
+    long[] sortPointers = Utils.getPointers(sorts);
+    long termPointer = declareOracleFun(pointer, symbol, sortPointers, sort.getPointer(), oracle);
+    return new Term(this, termPointer);
+  }
+
+  private native long declareOracleFun(
+      long pointer, String symbol, long[] sortPointers, long sortPointer, IOracle oracle);
+
   /**
    * Pop a level from the assertion stack.
    *
@@ -2569,16 +2610,15 @@ public class Solver implements IPointer, AutoCloseable
    * @param ntSymbols The pre-declaration of the non-terminal symbols.
    * @return The grammar.
    */
-  public Grammar mkGrammar(Term[] boundVars, Term[] ntSymbols) {
+  public Grammar mkGrammar(Term[] boundVars, Term[] ntSymbols)
+  {
     long[] boundVarPointers = Utils.getPointers(boundVars);
     long[] ntSymbolPointers = Utils.getPointers(ntSymbols);
-    long grammarPointer =
-        mkGrammar(pointer, boundVarPointers, ntSymbolPointers);
+    long grammarPointer = mkGrammar(pointer, boundVarPointers, ntSymbolPointers);
     return new Grammar(this, grammarPointer);
   }
 
-  private native long mkGrammar(
-      long pointer, long[] boundVarPointers, long[] ntSymbolPointers);
+  private native long mkGrammar(long pointer, long[] boundVarPointers, long[] ntSymbolPointers);
 
   /**
    * Synthesize n-ary function.

diff --git a/src/api/java/jni/api_utilities.cpp b/src/api/java/jni/api_utilities.cpp
index 1c5e5b5bebb36c75c9699a867f3476950cb14897..a6c986ac9625b823ef88e8916be0048b7b9e5709 100644 (file)
--- a/src/api/java/jni/api_utilities.cpp
+++ b/src/api/java/jni/api_utilities.cpp
@@ -49,4 +49,34 @@ jobject getBooleanObject(JNIEnv* env, bool cValue)
       env->GetMethodID(booleanClass, "<init>", "(Z)V");
   jobject ret = env->NewObject(booleanClass, booleanConstructor, jValue);
   return ret;
-}
\ No newline at end of file
+}
+
+cvc5::Term applyOracle(JNIEnv* env,
+                       jobject solverRef,
+                       jobject oracleRef,
+                       const std::vector<cvc5::Term>& terms)
+{
+  jclass termClass = env->FindClass("Lio/github/cvc5/Term;");
+  jmethodID termConstructor =
+      env->GetMethodID(termClass, "<init>", "(Lio/github/cvc5/Solver;J)V");
+
+  jobjectArray jTerms = env->NewObjectArray(terms.size(), termClass, NULL);
+
+  for (size_t i = 0; i < terms.size(); i++)
+  {
+    jlong termPointer = reinterpret_cast<jlong>(new cvc5::Term(terms[i]));
+    jobject jTerm =
+        env->NewObject(termClass, termConstructor, solverRef, termPointer);
+    env->SetObjectArrayElement(jTerms, i, jTerm);
+  }
+
+  jclass oracleClass = env->GetObjectClass(oracleRef);
+  jmethodID applyMethod = env->GetMethodID(
+      oracleClass, "apply", "([Lio/github/cvc5/Term;)Lio/github/cvc5/Term;");
+
+  jobject jTerm = env->CallObjectMethod(oracleRef, applyMethod, jTerms);
+  jfieldID pointer = env->GetFieldID(termClass, "pointer", "J");
+  jlong termPointer = env->GetLongField(jTerm, pointer);
+  cvc5::Term* term = reinterpret_cast<cvc5::Term*>(termPointer);
+  return *term;
+}

diff --git a/src/api/java/jni/api_utilities.h b/src/api/java/jni/api_utilities.h
index 5dfeeb7c0965c28ec22e0c630bd979106b278994..86488c740b0e72df9a1e7af302351f99a740626b 100644 (file)
--- a/src/api/java/jni/api_utilities.h
+++ b/src/api/java/jni/api_utilities.h
@@ -15,34 +15,34 @@
 
 #ifndef CVC5__API_UTILITIES_H
 #define CVC5__API_UTILITIES_H
-
 #include <jni.h>
 
 #include <string>
 #include <vector>
 
+#include "api/cpp/cvc5.h"
+
 #define CVC5_JAVA_API_TRY_CATCH_BEGIN \
   try                                 \
   {
-#define CVC5_JAVA_API_TRY_CATCH_END(env)                                  \
-  }                                                                       \
-  catch (const CVC5ApiOptionException& e)                                 \
-  {                                                                       \
-    jclass exceptionClass =                                               \
-        env->FindClass("io/github/cvc5/CVC5ApiOptionException");      \
-    env->ThrowNew(exceptionClass, e.what());                              \
-  }                                                                       \
-  catch (const CVC5ApiRecoverableException& e)                            \
-  {                                                                       \
-    jclass exceptionClass =                                               \
-        env->FindClass("io/github/cvc5/CVC5ApiRecoverableException"); \
-    env->ThrowNew(exceptionClass, e.what());                              \
-  }                                                                       \
-  catch (const CVC5ApiException& e)                                       \
-  {                                                                       \
-    jclass exceptionClass =                                               \
-        env->FindClass("io/github/cvc5/CVC5ApiException");            \
-    env->ThrowNew(exceptionClass, e.what());                              \
+#define CVC5_JAVA_API_TRY_CATCH_END(env)                                       \
+  }                                                                            \
+  catch (const CVC5ApiOptionException& e)                                      \
+  {                                                                            \
+    jclass exceptionClass =                                                    \
+        env->FindClass("io/github/cvc5/CVC5ApiOptionException");               \
+    env->ThrowNew(exceptionClass, e.what());                                   \
+  }                                                                            \
+  catch (const CVC5ApiRecoverableException& e)                                 \
+  {                                                                            \
+    jclass exceptionClass =                                                    \
+        env->FindClass("io/github/cvc5/CVC5ApiRecoverableException");          \
+    env->ThrowNew(exceptionClass, e.what());                                   \
+  }                                                                            \
+  catch (const CVC5ApiException& e)                                            \
+  {                                                                            \
+    jclass exceptionClass = env->FindClass("io/github/cvc5/CVC5ApiException"); \
+    env->ThrowNew(exceptionClass, e.what());                                   \
   }
 #define CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, returnValue) \
   CVC5_JAVA_API_TRY_CATCH_END(env)                           \
@@ -139,4 +139,22 @@ jobject getDoubleObject(JNIEnv* env, double value);
  */
 jobject getBooleanObject(JNIEnv* env, bool value);
 
+/**
+ * a map from solver pointers to global references that need to be freed when
+ * the java Solver.close method is called
+ */
+inline std::map<jlong, std::vector<jobject> > globalReferences;
+
+/**
+ * @param env jni environment
+ * @param solverRef a global reference to java Solver object
+ * @param oracleRef a global reference to java IOracle object
+ * @param terms a list of terms
+ * @return the result of calling IOracle.compute(terms)
+ */
+cvc5::Term applyOracle(JNIEnv* env,
+                       jobject solverRef,
+                       jobject oracleRef,
+                       const std::vector<cvc5::Term>& terms);
+
 #endif  // CVC5__API_UTILITIES_H

diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index e13090beadffdbbf9117c4eecda2894c047fab55..01809f7ce0ced01647f455c1692f58221a63fd39 100644 (file)
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -24,8 +24,7 @@ using namespace cvc5;
  * Method:    newSolver
  * Signature: ()J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_newSolver(JNIEnv*,
-                                                                 jobject)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_newSolver(JNIEnv*, jobject)
 {
   Solver* solver = new Solver();
   return reinterpret_cast<jlong>(solver);
@@ -36,9 +35,16 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_newSolver(JNIEnv*,
  * Method:    deletePointer
  * Signature: (J)V
  */
-JNIEXPORT void JNICALL
-Java_io_github_cvc5_Solver_deletePointer(JNIEnv*, jclass, jlong pointer)
+JNIEXPORT void JNICALL Java_io_github_cvc5_Solver_deletePointer(JNIEnv* env,
+                                                                jclass,
+                                                                jlong pointer)
 {
+  const std::vector<jobject>& refs = globalReferences[pointer];
+  for (jobject ref : refs)
+  {
+    env->DeleteGlobalRef(ref);
+  }
+  globalReferences.erase(pointer);
   delete (reinterpret_cast<Solver*>(pointer));
 }
 
@@ -47,8 +53,9 @@ Java_io_github_cvc5_Solver_deletePointer(JNIEnv*, jclass, jlong pointer)
  * Method:    getNullSort
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_Solver_getNullSort(JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getNullSort(JNIEnv* env,
+                                                               jobject,
+                                                               jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -62,8 +69,9 @@ Java_io_github_cvc5_Solver_getNullSort(JNIEnv* env, jobject, jlong pointer)
  * Method:    getBooleanSort
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getBooleanSort(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getBooleanSort(JNIEnv* env,
+                                                                  jobject,
+                                                                  jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -77,8 +85,9 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getBooleanSort(
  * Method:    getIntegerSort
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getIntegerSort(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getIntegerSort(JNIEnv* env,
+                                                                  jobject,
+                                                                  jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -92,8 +101,9 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getIntegerSort(
  * Method:    getRealSort
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_Solver_getRealSort(JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getRealSort(JNIEnv* env,
+                                                               jobject,
+                                                               jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -107,8 +117,9 @@ Java_io_github_cvc5_Solver_getRealSort(JNIEnv* env, jobject, jlong pointer)
  * Method:    getRegExpSort
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getRegExpSort(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getRegExpSort(JNIEnv* env,
+                                                                 jobject,
+                                                                 jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -137,8 +148,9 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getRoundingModeSort(
  * Method:    getStringSort
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getStringSort(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getStringSort(JNIEnv* env,
+                                                                 jobject,
+                                                                 jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -154,10 +166,10 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getStringSort(
  */
 JNIEXPORT jlong JNICALL
 Java_io_github_cvc5_Solver_mkArraySort(JNIEnv* env,
-                                           jobject,
-                                           jlong pointer,
-                                           jlong indexSortPointer,
-                                           jlong elementSortPointer)
+                                       jobject,
+                                       jlong pointer,
+                                       jlong indexSortPointer,
+                                       jlong elementSortPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -220,11 +232,8 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkDatatypeSort(
  * Method:    mkDatatypeSorts
  * Signature: (J[J)[J
  */
-JNIEXPORT jlongArray JNICALL
-Java_io_github_cvc5_Solver_mkDatatypeSorts(JNIEnv* env,
-                                                     jobject,
-                                                     jlong pointer,
-                                                     jlongArray jDecls)
+JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_Solver_mkDatatypeSorts(
+    JNIEnv* env, jobject, jlong pointer, jlongArray jDecls)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -536,8 +545,10 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkTupleSort(
  * Method:    mkTerm
  * Signature: (JI)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkTerm__JI(
-    JNIEnv* env, jobject, jlong pointer, jint kindValue)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkTerm__JI(JNIEnv* env,
+                                                              jobject,
+                                                              jlong pointer,
+                                                              jint kindValue)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -571,11 +582,11 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkTerm__JIJ(
  */
 JNIEXPORT jlong JNICALL
 Java_io_github_cvc5_Solver_mkTerm__JIJJ(JNIEnv* env,
-                                            jobject,
-                                            jlong pointer,
-                                            jint kindValue,
-                                            jlong child1Pointer,
-                                            jlong child2Pointer)
+                                        jobject,
+                                        jlong pointer,
+                                        jint kindValue,
+                                        jlong child1Pointer,
+                                        jlong child2Pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -594,12 +605,12 @@ Java_io_github_cvc5_Solver_mkTerm__JIJJ(JNIEnv* env,
  */
 JNIEXPORT jlong JNICALL
 Java_io_github_cvc5_Solver_mkTerm__JIJJJ(JNIEnv* env,
-                                             jobject,
-                                             jlong pointer,
-                                             jint kindValue,
-                                             jlong child1Pointer,
-                                             jlong child2Pointer,
-                                             jlong child3Pointer)
+                                         jobject,
+                                         jlong pointer,
+                                         jint kindValue,
+                                         jlong child1Pointer,
+                                         jlong child2Pointer,
+                                         jlong child3Pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -620,10 +631,10 @@ Java_io_github_cvc5_Solver_mkTerm__JIJJJ(JNIEnv* env,
  */
 JNIEXPORT jlong JNICALL
 Java_io_github_cvc5_Solver_mkTerm__JI_3J(JNIEnv* env,
-                                             jobject,
-                                             jlong pointer,
-                                             jint kindValue,
-                                             jlongArray childrenPointers)
+                                         jobject,
+                                         jlong pointer,
+                                         jint kindValue,
+                                         jlongArray childrenPointers)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -640,8 +651,10 @@ Java_io_github_cvc5_Solver_mkTerm__JI_3J(JNIEnv* env,
  * Method:    mkTerm
  * Signature: (JJ)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkTerm__JJ(
-    JNIEnv* env, jobject, jlong pointer, jlong opPointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkTerm__JJ(JNIEnv* env,
+                                                              jobject,
+                                                              jlong pointer,
+                                                              jlong opPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -675,11 +688,11 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkTerm__JJJ(
  */
 JNIEXPORT jlong JNICALL
 Java_io_github_cvc5_Solver_mkTerm__JJJJ(JNIEnv* env,
-                                            jobject,
-                                            jlong pointer,
-                                            jlong opPointer,
-                                            jlong child1Pointer,
-                                            jlong child2Pointer)
+                                        jobject,
+                                        jlong pointer,
+                                        jlong opPointer,
+                                        jlong child1Pointer,
+                                        jlong child2Pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -698,12 +711,12 @@ Java_io_github_cvc5_Solver_mkTerm__JJJJ(JNIEnv* env,
  */
 JNIEXPORT jlong JNICALL
 Java_io_github_cvc5_Solver_mkTerm__JJJJJ(JNIEnv* env,
-                                             jobject,
-                                             jlong pointer,
-                                             jlong opPointer,
-                                             jlong child1Pointer,
-                                             jlong child2Pointer,
-                                             jlong child3Pointer)
+                                         jobject,
+                                         jlong pointer,
+                                         jlong opPointer,
+                                         jlong child1Pointer,
+                                         jlong child2Pointer,
+                                         jlong child3Pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -723,10 +736,10 @@ Java_io_github_cvc5_Solver_mkTerm__JJJJJ(JNIEnv* env,
  */
 JNIEXPORT jlong JNICALL
 Java_io_github_cvc5_Solver_mkTerm__JJ_3J(JNIEnv* env,
-                                             jobject,
-                                             jlong pointer,
-                                             jlong opPointer,
-                                             jlongArray childrenPointers)
+                                         jobject,
+                                         jlong pointer,
+                                         jlong opPointer,
+                                         jlongArray childrenPointers)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -745,10 +758,10 @@ Java_io_github_cvc5_Solver_mkTerm__JJ_3J(JNIEnv* env,
  */
 JNIEXPORT jlong JNICALL
 Java_io_github_cvc5_Solver_mkTuple(JNIEnv* env,
-                                       jobject,
-                                       jlong pointer,
-                                       jlongArray sortPointers,
-                                       jlongArray termPointers)
+                                   jobject,
+                                   jlong pointer,
+                                   jlongArray sortPointers,
+                                   jlongArray termPointers)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -765,9 +778,9 @@ Java_io_github_cvc5_Solver_mkTuple(JNIEnv* env,
  * Signature: (JI)J
  */
 JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkOp__JI(JNIEnv* env,
-                                                                jobject,
-                                                                jlong pointer,
-                                                                jint kindValue)
+                                                            jobject,
+                                                            jlong pointer,
+                                                            jint kindValue)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -782,8 +795,7 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkOp__JI(JNIEnv* env,
  * Method:    mkOp
  * Signature: (JILjava/lang/String;)J
  */
-JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_Solver_mkOp__JILjava_lang_String_2(
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkOp__JILjava_lang_String_2(
     JNIEnv* env, jobject, jlong pointer, jint kindValue, jstring jArg)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
@@ -864,8 +876,8 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkOp__JI_3I(
  * Signature: (J)J
  */
 JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkTrue(JNIEnv* env,
-                                                              jobject,
-                                                              jlong pointer)
+                                                          jobject,
+                                                          jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -880,8 +892,8 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkTrue(JNIEnv* env,
  * Signature: (J)J
  */
 JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkFalse(JNIEnv* env,
-                                                               jobject,
-                                                               jlong pointer)
+                                                           jobject,
+                                                           jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -896,9 +908,9 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkFalse(JNIEnv* env,
  * Signature: (JZ)J
  */
 JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkBoolean(JNIEnv* env,
-                                                                 jobject,
-                                                                 jlong pointer,
-                                                                 jboolean val)
+                                                             jobject,
+                                                             jlong pointer,
+                                                             jboolean val)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -913,8 +925,8 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkBoolean(JNIEnv* env,
  * Signature: (J)J
  */
 JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkPi(JNIEnv* env,
-                                                            jobject,
-                                                            jlong pointer)
+                                                        jobject,
+                                                        jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -930,9 +942,9 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkPi(JNIEnv* env,
  */
 JNIEXPORT jlong JNICALL
 Java_io_github_cvc5_Solver_mkInteger__JLjava_lang_String_2(JNIEnv* env,
-                                                               jobject,
-                                                               jlong pointer,
-                                                               jstring jS)
+                                                           jobject,
+                                                           jlong pointer,
+                                                           jstring jS)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -949,8 +961,10 @@ Java_io_github_cvc5_Solver_mkInteger__JLjava_lang_String_2(JNIEnv* env,
  * Method:    mkInteger
  * Signature: (JJ)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkInteger__JJ(
-    JNIEnv* env, jobject, jlong pointer, jlong val)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkInteger__JJ(JNIEnv* env,
+                                                                 jobject,
+                                                                 jlong pointer,
+                                                                 jlong val)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -964,11 +978,8 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkInteger__JJ(
  * Method:    mkReal
  * Signature: (JLjava/lang/String;)J
  */
-JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_Solver_mkReal__JLjava_lang_String_2(JNIEnv* env,
-                                                            jobject,
-                                                            jlong pointer,
-                                                            jstring jS)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkReal__JLjava_lang_String_2(
+    JNIEnv* env, jobject, jlong pointer, jstring jS)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -985,8 +996,10 @@ Java_io_github_cvc5_Solver_mkReal__JLjava_lang_String_2(JNIEnv* env,
  * Method:    mkRealValue
  * Signature: (JJ)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkRealValue(
-    JNIEnv* env, jobject, jlong pointer, jlong val)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkRealValue(JNIEnv* env,
+                                                               jobject,
+                                                               jlong pointer,
+                                                               jlong val)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1015,8 +1028,9 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkReal__JJJ(
  * Method:    mkRegexpNone
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkRegexpNone(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkRegexpNone(JNIEnv* env,
+                                                                jobject,
+                                                                jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1030,8 +1044,9 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkRegexpNone(
  * Method:    mkRegexpAll
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_Solver_mkRegexpAll(JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkRegexpAll(JNIEnv* env,
+                                                               jobject,
+                                                               jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1045,8 +1060,8 @@ Java_io_github_cvc5_Solver_mkRegexpAll(JNIEnv* env, jobject, jlong pointer)
  * Method:    mkRegexpAllchar
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkRegexpAllchar(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jlong JNICALL
+Java_io_github_cvc5_Solver_mkRegexpAllchar(JNIEnv* env, jobject, jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1060,8 +1075,10 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkRegexpAllchar(
  * Method:    mkEmptySet
  * Signature: (JJ)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkEmptySet(
-    JNIEnv* env, jobject, jlong pointer, jlong sortPointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkEmptySet(JNIEnv* env,
+                                                              jobject,
+                                                              jlong pointer,
+                                                              jlong sortPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1076,8 +1093,10 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkEmptySet(
  * Method:    mkEmptyBag
  * Signature: (JJ)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkEmptyBag(
-    JNIEnv* env, jobject, jlong pointer, jlong sortPointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkEmptyBag(JNIEnv* env,
+                                                              jobject,
+                                                              jlong pointer,
+                                                              jlong sortPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1093,8 +1112,8 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkEmptyBag(
  * Signature: (J)J
  */
 JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkSepEmp(JNIEnv* env,
-                                                                jobject,
-                                                                jlong pointer)
+                                                            jobject,
+                                                            jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1108,8 +1127,10 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkSepEmp(JNIEnv* env,
  * Method:    mkSepNil
  * Signature: (JJ)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkSepNil(
-    JNIEnv* env, jobject, jlong pointer, jlong sortPointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkSepNil(JNIEnv* env,
+                                                            jobject,
+                                                            jlong pointer,
+                                                            jlong sortPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1308,8 +1329,10 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkFloatingPointNegZero(
  * Method:    mkRoundingMode
  * Signature: (JI)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkRoundingMode(
-    JNIEnv* env, jobject, jlong pointer, jint rm)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkRoundingMode(JNIEnv* env,
+                                                                  jobject,
+                                                                  jlong pointer,
+                                                                  jint rm)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1413,11 +1436,8 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkVar(
  * Method:    mkDatatypeConstructorDecl
  * Signature: (JLjava/lang/String;)J
  */
-JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_Solver_mkDatatypeConstructorDecl(JNIEnv* env,
-                                                         jobject,
-                                                         jlong pointer,
-                                                         jstring jName)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkDatatypeConstructorDecl(
+    JNIEnv* env, jobject, jlong pointer, jstring jName)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1482,8 +1502,10 @@ Java_io_github_cvc5_Solver_mkDatatypeDecl__JLjava_lang_String_2_3JZ(
  * Method:    simplify
  * Signature: (JJ)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_simplify(
-    JNIEnv* env, jobject, jlong pointer, jlong termPointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_simplify(JNIEnv* env,
+                                                            jobject,
+                                                            jlong pointer,
+                                                            jlong termPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1514,8 +1536,8 @@ JNIEXPORT void JNICALL Java_io_github_cvc5_Solver_assertFormula(
  * Signature: (J)J
  */
 JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_checkSat(JNIEnv* env,
-                                                                jobject,
-                                                                jlong pointer)
+                                                            jobject,
+                                                            jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1582,13 +1604,12 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_declareDatatype(
  * Method:    declareFun
  * Signature: (JLjava/lang/String;[JJ)J
  */
-JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_Solver_declareFun(JNIEnv* env,
-                                          jobject,
-                                          jlong pointer,
-                                          jstring jSymbol,
-                                          jlongArray jSorts,
-                                          jlong sortPointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_declareFun(JNIEnv* env,
+                                                              jobject,
+                                                              jlong pointer,
+                                                              jstring jSymbol,
+                                                              jlongArray jSorts,
+                                                              jlong sortPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1624,15 +1645,14 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_declareSort(
  * Method:    defineFun
  * Signature: (JLjava/lang/String;[JJJZ)J
  */
-JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_Solver_defineFun(JNIEnv* env,
-                                         jobject,
-                                         jlong pointer,
-                                         jstring jSymbol,
-                                         jlongArray jVars,
-                                         jlong sortPointer,
-                                         jlong termPointer,
-                                         jboolean global)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_defineFun(JNIEnv* env,
+                                                             jobject,
+                                                             jlong pointer,
+                                                             jstring jSymbol,
+                                                             jlongArray jVars,
+                                                             jlong sortPointer,
+                                                             jlong termPointer,
+                                                             jboolean global)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1685,12 +1705,12 @@ Java_io_github_cvc5_Solver_defineFunRec__JLjava_lang_String_2_3JJJZ(
  */
 JNIEXPORT jlong JNICALL
 Java_io_github_cvc5_Solver_defineFunRec__JJ_3JJZ(JNIEnv* env,
-                                                     jobject,
-                                                     jlong pointer,
-                                                     jlong funPointer,
-                                                     jlongArray jVars,
-                                                     jlong termPointer,
-                                                     jboolean global)
+                                                 jobject,
+                                                 jlong pointer,
+                                                 jlong funPointer,
+                                                 jlongArray jVars,
+                                                 jlong termPointer,
+                                                 jboolean global)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1710,12 +1730,12 @@ Java_io_github_cvc5_Solver_defineFunRec__JJ_3JJZ(JNIEnv* env,
  */
 JNIEXPORT void JNICALL
 Java_io_github_cvc5_Solver_defineFunsRec(JNIEnv* env,
-                                             jobject,
-                                             jlong pointer,
-                                             jlongArray jFuns,
-                                             jobjectArray jVars,
-                                             jlongArray jTerms,
-                                             jboolean global)
+                                         jobject,
+                                         jlong pointer,
+                                         jlongArray jFuns,
+                                         jobjectArray jVars,
+                                         jlongArray jTerms,
+                                         jboolean global)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1761,8 +1781,8 @@ JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_Solver_getLearnedLiterals(
  * Method:    getAssertions
  * Signature: (J)[J
  */
-JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_Solver_getAssertions(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jlongArray JNICALL
+Java_io_github_cvc5_Solver_getAssertions(JNIEnv* env, jobject, jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1778,9 +1798,9 @@ JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_Solver_getAssertions(
  * Signature: (JLjava/lang/String;)Ljava/lang/String;
  */
 JNIEXPORT jstring JNICALL Java_io_github_cvc5_Solver_getInfo(JNIEnv* env,
-                                                                 jobject,
-                                                                 jlong pointer,
-                                                                 jstring jFlag)
+                                                             jobject,
+                                                             jlong pointer,
+                                                             jstring jFlag)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1796,8 +1816,10 @@ JNIEXPORT jstring JNICALL Java_io_github_cvc5_Solver_getInfo(JNIEnv* env,
  * Method:    getOption
  * Signature: (JLjava/lang/String;)Ljava/lang/String;
  */
-JNIEXPORT jstring JNICALL Java_io_github_cvc5_Solver_getOption(
-    JNIEnv* env, jobject, jlong pointer, jstring jOption)
+JNIEXPORT jstring JNICALL Java_io_github_cvc5_Solver_getOption(JNIEnv* env,
+                                                               jobject,
+                                                               jlong pointer,
+                                                               jstring jOption)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1813,8 +1835,8 @@ JNIEXPORT jstring JNICALL Java_io_github_cvc5_Solver_getOption(
  * Method:    getOptionNames
  * Signature: (J)[Ljava/lang/String;
  */
-JNIEXPORT jobjectArray JNICALL Java_io_github_cvc5_Solver_getOptionNames(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jobjectArray JNICALL
+Java_io_github_cvc5_Solver_getOptionNames(JNIEnv* env, jobject, jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1845,8 +1867,8 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getOptionInfo(
  * Method:    getDriverOptions
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getDriverOptions(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jlong JNICALL
+Java_io_github_cvc5_Solver_getDriverOptions(JNIEnv* env, jobject, jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1892,8 +1914,8 @@ Java_io_github_cvc5_Solver_getUnsatCore(JNIEnv* env, jobject, jlong pointer)
  * Method:    getDifficulty
  * Signature: (J)Ljava/util/Map;
  */
-JNIEXPORT jobject JNICALL Java_io_github_cvc5_Solver_getDifficulty(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jobject JNICALL
+Java_io_github_cvc5_Solver_getDifficulty(JNIEnv* env, jobject, jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1932,8 +1954,8 @@ JNIEXPORT jobject JNICALL Java_io_github_cvc5_Solver_getDifficulty(
  * Signature: (J)Ljava/lang/String;
  */
 JNIEXPORT jstring JNICALL Java_io_github_cvc5_Solver_getProof(JNIEnv* env,
-                                                                  jobject,
-                                                                  jlong pointer)
+                                                              jobject,
+                                                              jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -1980,11 +2002,8 @@ JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_Solver_getValue__J_3J(
  * Method:    getModelDomainElements
  * Signature: (JJ)[J
  */
-JNIEXPORT jlongArray JNICALL
-Java_io_github_cvc5_Solver_getModelDomainElements(JNIEnv* env,
-                                                      jobject,
-                                                      jlong pointer,
-                                                      jlong sortPointer)
+JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_Solver_getModelDomainElements(
+    JNIEnv* env, jobject, jlong pointer, jlong sortPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2017,10 +2036,10 @@ JNIEXPORT jboolean JNICALL Java_io_github_cvc5_Solver_isModelCoreSymbol(
  */
 JNIEXPORT jstring JNICALL
 Java_io_github_cvc5_Solver_getModel(JNIEnv* env,
-                                        jobject,
-                                        jlong pointer,
-                                        jlongArray sortPointers,
-                                        jlongArray varPointers)
+                                    jobject,
+                                    jlong pointer,
+                                    jlongArray sortPointers,
+                                    jlongArray varPointers)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2054,9 +2073,9 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getQuantifierElimination(
  */
 JNIEXPORT jlong JNICALL
 Java_io_github_cvc5_Solver_getQuantifierEliminationDisjunct(JNIEnv* env,
-                                                                jobject,
-                                                                jlong pointer,
-                                                                jlong qPointer)
+                                                            jobject,
+                                                            jlong pointer,
+                                                            jlong qPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2073,10 +2092,10 @@ Java_io_github_cvc5_Solver_getQuantifierEliminationDisjunct(JNIEnv* env,
  */
 JNIEXPORT void JNICALL
 Java_io_github_cvc5_Solver_declareSepHeap(JNIEnv* env,
-                                              jobject,
-                                              jlong pointer,
-                                              jlong locSortPointer,
-                                              jlong dataSortPointer)
+                                          jobject,
+                                          jlong pointer,
+                                          jlong locSortPointer,
+                                          jlong dataSortPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2091,8 +2110,8 @@ Java_io_github_cvc5_Solver_declareSepHeap(JNIEnv* env,
  * Method:    getValueSepHeap
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getValueSepHeap(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jlong JNICALL
+Java_io_github_cvc5_Solver_getValueSepHeap(JNIEnv* env, jobject, jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2106,8 +2125,9 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getValueSepHeap(
  * Method:    getValueSepNil
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getValueSepNil(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getValueSepNil(JNIEnv* env,
+                                                                  jobject,
+                                                                  jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2121,29 +2141,70 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getValueSepNil(
  * Method:    declarePool
  * Signature: (Ljava/lang/String;J[J])J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_declarePool(
-    JNIEnv* env, jobject, jlong pointer, jstring jsymbol, jlong sort, jlongArray initValuePointers)
+JNIEXPORT jlong JNICALL
+Java_io_github_cvc5_Solver_declarePool(JNIEnv* env,
+                                       jobject,
+                                       jlong pointer,
+                                       jstring jsymbol,
+                                       jlong sort,
+                                       jlongArray initValuePointers)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
   const char* s = env->GetStringUTFChars(jsymbol, nullptr);
   std::string symbol(s);
   Sort* sortptr = reinterpret_cast<Sort*>(sort);
-  std::vector<Term> initValue = getObjectsFromPointers<Term>(env, initValuePointers);
+  std::vector<Term> initValue =
+      getObjectsFromPointers<Term>(env, initValuePointers);
   Term* retPointer = new Term(solver->declarePool(symbol, *sortptr, initValue));
   return reinterpret_cast<jlong>(retPointer);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
+/*
+ * Class:     io_github_cvc5_Solver
+ * Method:    declareOracleFun
+ * Signature: (JLjava/lang/String;[JJLio/github/cvc5/IOracle;)J
+ */
+JNIEXPORT jlong JNICALL
+Java_io_github_cvc5_Solver_declareOracleFun(JNIEnv* env,
+                                            jobject jSolver,
+                                            jlong pointer,
+                                            jstring jSymbol,
+                                            jlongArray sortPointers,
+                                            jlong sortPointer,
+                                            jobject oracle)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  jobject solverReference = env->NewGlobalRef(jSolver);
+  globalReferences[pointer].push_back(solverReference);
+  jobject oracleReference = env->NewGlobalRef(oracle);
+  globalReferences[pointer].push_back(oracleReference);
+  Solver* solver = reinterpret_cast<Solver*>(pointer);
+  const char* s = env->GetStringUTFChars(jSymbol, nullptr);
+  std::string cSymbol(s);
+  Sort* sort = reinterpret_cast<Sort*>(sortPointer);
+  std::vector<Sort> sorts = getObjectsFromPointers<Sort>(env, sortPointers);
+  std::function<Term(std::vector<Term>)> fn =
+      [env, solverReference, oracleReference](std::vector<Term> input) {
+        Term term = applyOracle(env, solverReference, oracleReference, input);
+        return term;
+      };
+  Term* retPointer =
+      new Term(solver->declareOracleFun(cSymbol, sorts, *sort, fn));
+  return reinterpret_cast<jlong>(retPointer);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
 /*
  * Class:     io_github_cvc5_Solver
  * Method:    pop
  * Signature: (JI)V
  */
 JNIEXPORT void JNICALL Java_io_github_cvc5_Solver_pop(JNIEnv* env,
-                                                          jobject,
-                                                          jlong pointer,
-                                                          jint nscopes)
+                                                      jobject,
+                                                      jlong pointer,
+                                                      jint nscopes)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2174,10 +2235,10 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getInterpolant__JJ(
  */
 JNIEXPORT jlong JNICALL
 Java_io_github_cvc5_Solver_getInterpolant__JJJ(JNIEnv* env,
-                                                   jobject,
-                                                   jlong pointer,
-                                                   jlong conjPointer,
-                                                   jlong grammarPointer)
+                                               jobject,
+                                               jlong pointer,
+                                               jlong conjPointer,
+                                               jlong grammarPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2226,10 +2287,10 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getAbduct__JJ(
  */
 JNIEXPORT jlong JNICALL
 Java_io_github_cvc5_Solver_getAbduct__JJJ(JNIEnv* env,
-                                              jobject,
-                                              jlong pointer,
-                                              jlong conjPointer,
-                                              jlong grammarPointer)
+                                          jobject,
+                                          jlong pointer,
+                                          jlong conjPointer,
+                                          jlong grammarPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2245,8 +2306,9 @@ Java_io_github_cvc5_Solver_getAbduct__JJJ(JNIEnv* env,
  * Method:    getAbductNext
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getAbductNext(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getAbductNext(JNIEnv* env,
+                                                                 jobject,
+                                                                 jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2292,10 +2354,8 @@ JNIEXPORT void JNICALL Java_io_github_cvc5_Solver_blockModelValues(
  * Method:    getInstantiations
  * Signature: (J[J[J)Ljava/lang/String;
  */
-JNIEXPORT jstring JNICALL
-Java_io_github_cvc5_Solver_getInstantiations(JNIEnv* env,
-                                        jobject,
-                                        jlong pointer)
+JNIEXPORT jstring JNICALL Java_io_github_cvc5_Solver_getInstantiations(
+    JNIEnv* env, jobject, jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2310,9 +2370,9 @@ Java_io_github_cvc5_Solver_getInstantiations(JNIEnv* env,
  * Signature: (JI)V
  */
 JNIEXPORT void JNICALL Java_io_github_cvc5_Solver_push(JNIEnv* env,
-                                                           jobject,
-                                                           jlong pointer,
-                                                           jint nscopes)
+                                                       jobject,
+                                                       jlong pointer,
+                                                       jint nscopes)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2325,8 +2385,9 @@ JNIEXPORT void JNICALL Java_io_github_cvc5_Solver_push(JNIEnv* env,
  * Method:    resetAssertions
  * Signature: (J)V
  */
-JNIEXPORT void JNICALL Java_io_github_cvc5_Solver_resetAssertions(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT void JNICALL Java_io_github_cvc5_Solver_resetAssertions(JNIEnv* env,
+                                                                  jobject,
+                                                                  jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2360,9 +2421,9 @@ JNIEXPORT void JNICALL Java_io_github_cvc5_Solver_setInfo(
  * Signature: (JLjava/lang/String;)V
  */
 JNIEXPORT void JNICALL Java_io_github_cvc5_Solver_setLogic(JNIEnv* env,
-                                                               jobject,
-                                                               jlong pointer,
-                                                               jstring jLogic)
+                                                           jobject,
+                                                           jlong pointer,
+                                                           jstring jLogic)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
 
@@ -2439,13 +2500,12 @@ Java_io_github_cvc5_Solver_mkGrammar(JNIEnv* env,
  * Signature: (JLjava/lang/String;[JJ)J
  */
 JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_Solver_synthFun__JLjava_lang_String_2_3JJ(
-    JNIEnv* env,
-    jobject,
-    jlong pointer,
-    jstring jSymbol,
-    jlongArray jVars,
-    jlong sortPointer)
+Java_io_github_cvc5_Solver_synthFun__JLjava_lang_String_2_3JJ(JNIEnv* env,
+                                                              jobject,
+                                                              jlong pointer,
+                                                              jstring jSymbol,
+                                                              jlongArray jVars,
+                                                              jlong sortPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2571,12 +2631,12 @@ JNIEXPORT void JNICALL Java_io_github_cvc5_Solver_addSygusAssume(
  */
 JNIEXPORT void JNICALL
 Java_io_github_cvc5_Solver_addSygusInvConstraint(JNIEnv* env,
-                                                     jobject,
-                                                     jlong pointer,
-                                                     jlong invPointer,
-                                                     jlong prePointer,
-                                                     jlong transPointer,
-                                                     jlong postPointer)
+                                                 jobject,
+                                                 jlong pointer,
+                                                 jlong invPointer,
+                                                 jlong prePointer,
+                                                 jlong transPointer,
+                                                 jlong postPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2594,8 +2654,8 @@ Java_io_github_cvc5_Solver_addSygusInvConstraint(JNIEnv* env,
  * Signature: (J)J
  */
 JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_checkSynth(JNIEnv* env,
-                                                                  jobject,
-                                                                  jlong pointer)
+                                                              jobject,
+                                                              jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2609,8 +2669,9 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_checkSynth(JNIEnv* env,
  * Method:    checkSynthNext
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_checkSynthNext(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_checkSynthNext(JNIEnv* env,
+                                                                  jobject,
+                                                                  jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2657,8 +2718,9 @@ JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_Solver_getSynthSolutions(
  * Method:    getStatistics
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getStatistics(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getStatistics(JNIEnv* env,
+                                                                 jobject,
+                                                                 jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2673,8 +2735,8 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getStatistics(
  * Signature: (J)J
  */
 JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getNullTerm(JNIEnv* env,
-                                                                   jobject,
-                                                                   jlong)
+                                                               jobject,
+                                                               jlong)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Term* ret = new Term();
@@ -2687,8 +2749,9 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getNullTerm(JNIEnv* env,
  * Method:    getNullResult
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_Solver_getNullResult(JNIEnv* env, jobject, jlong)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getNullResult(JNIEnv* env,
+                                                                 jobject,
+                                                                 jlong)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Result* ret = new Result();
@@ -2716,8 +2779,8 @@ Java_io_github_cvc5_Solver_getNullSynthResult(JNIEnv* env, jobject, jlong)
  * Signature: (J)J
  */
 JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getNullOp(JNIEnv* env,
-                                                                 jobject,
-                                                                 jlong)
+                                                             jobject,
+                                                             jlong)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Op* ret = new Op();

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index b52514a283f7bd3976e5437557d28a529e727320..38d41b9ef7ffe6b7034cb1dec9aeb39883c3d3c4 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -820,8 +820,7 @@ class SolverTest
 
     // list datatype
     Sort sort = d_solver.mkParamSort("T");
-    DatatypeDecl listDecl =
-        d_solver.mkDatatypeDecl("paramlist", new Sort[] {sort});
+    DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", new Sort[] {sort});
     DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
     DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
     cons.addSelector("head", sort);
@@ -915,8 +914,8 @@ class SolverTest
                                new Term[] {d_solver.mkBitVector(3, "101", 2)}));
     assertThrows(CVC5ApiException.class,
         ()
-            -> d_solver.mkTuple(new Sort[] {d_solver.getRealSort()},
-                new Term[] {d_solver.mkInteger("5")}));
+            -> d_solver.mkTuple(
+                new Sort[] {d_solver.getRealSort()}, new Term[] {d_solver.mkInteger("5")}));
 
     assertThrows(CVC5ApiException.class,
         () -> d_solver.mkTuple(new Sort[] {}, new Term[] {d_solver.mkBitVector(3, "101", 2)}));
@@ -1551,7 +1550,7 @@ class SolverTest
     Term x = d_solver.mkConst(intSort, "x");
     Term y = d_solver.mkConst(intSort, "y");
     // declare a pool with initial value { 0, x, y }
-    Term p = d_solver.declarePool("p", intSort, new Term[]{zero, x, y});
+    Term p = d_solver.declarePool("p", intSort, new Term[] {zero, x, y});
     // pool should have the same sort
     assertEquals(p.getSort(), setSort);
   }
@@ -1985,7 +1984,7 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.getValue(sum));
     assertDoesNotThrow(() -> d_solver.getValue(p_f_y));
 
-    Term[] b = d_solver.getValue(new Term[]{x, y, z});
+    Term[] b = d_solver.getValue(new Term[] {x, y, z});
 
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.getValue(x));
@@ -2659,23 +2658,21 @@ class SolverTest
   }
 
   @Test
-  void mkGrammar() throws CVC5ApiException {
+  void mkGrammar() throws CVC5ApiException
+  {
     Term nullTerm = d_solver.getNullTerm();
     Term boolTerm = d_solver.mkBoolean(true);
     Term boolVar = d_solver.mkVar(d_solver.getBooleanSort());
     Term intVar = d_solver.mkVar(d_solver.getIntegerSort());
 
-    assertDoesNotThrow(
-        () -> d_solver.mkGrammar(new Term[] {}, new Term[] {intVar}));
-    assertDoesNotThrow(
-        () -> d_solver.mkGrammar(new Term[] {boolVar}, new Term[] {intVar}));
+    assertDoesNotThrow(() -> d_solver.mkGrammar(new Term[] {}, new Term[] {intVar}));
+    assertDoesNotThrow(() -> d_solver.mkGrammar(new Term[] {boolVar}, new Term[] {intVar}));
 
-    assertThrows(CVC5ApiException.class,
-        () -> d_solver.mkGrammar(new Term[] {}, new Term[] {}));
-    assertThrows(CVC5ApiException.class,
-        () -> d_solver.mkGrammar(new Term[] {}, new Term[] {nullTerm}));
-    assertThrows(CVC5ApiException.class,
-        () -> d_solver.mkGrammar(new Term[] {}, new Term[] {boolTerm}));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkGrammar(new Term[] {}, new Term[] {}));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.mkGrammar(new Term[] {}, new Term[] {nullTerm}));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.mkGrammar(new Term[] {}, new Term[] {boolTerm}));
     assertThrows(CVC5ApiException.class,
         () -> d_solver.mkGrammar(new Term[] {boolTerm}, new Term[] {intVar}));
 
@@ -2683,13 +2680,12 @@ class SolverTest
     slv.setOption("sygus", "true");
     Term boolVar2 = slv.mkVar(slv.getBooleanSort());
     Term intVar2 = slv.mkVar(slv.getIntegerSort());
-    assertDoesNotThrow(
-        () -> slv.mkGrammar(new Term[] {boolVar2}, new Term[] {intVar2}));
+    assertDoesNotThrow(() -> slv.mkGrammar(new Term[] {boolVar2}, new Term[] {intVar2}));
 
-    assertThrows(CVC5ApiException.class,
-        () -> slv.mkGrammar(new Term[] {boolVar}, new Term[] {intVar2}));
-    assertThrows(CVC5ApiException.class,
-        () -> slv.mkGrammar(new Term[] {boolVar2}, new Term[] {intVar}));
+    assertThrows(
+        CVC5ApiException.class, () -> slv.mkGrammar(new Term[] {boolVar}, new Term[] {intVar2}));
+    assertThrows(
+        CVC5ApiException.class, () -> slv.mkGrammar(new Term[] {boolVar2}, new Term[] {intVar}));
     slv.close();
   }
 
@@ -3012,4 +3008,98 @@ class SolverTest
             + "(set.singleton \"Z\")))",
         projection.toString());
   }
+
+  @Test
+  void declareOracleFunError() throws CVC5ApiException
+  {
+    Sort iSort = d_solver.getIntegerSort();
+    // cannot declare without option
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> d_solver.declareOracleFun(
+                "f", new Sort[] {iSort}, iSort, (input) -> d_solver.mkInteger(0)));
+    d_solver.setOption("oracles", "true");
+    Sort nullSort = d_solver.getNullSort();
+    // bad sort
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> d_solver.declareOracleFun(
+                "f", new Sort[] {nullSort}, iSort, (input) -> d_solver.mkInteger(0)));
+  }
+
+  @Test
+  void declareOracleFunUnsat() throws CVC5ApiException
+  {
+    d_solver.setOption("oracles", "true");
+    Sort iSort = d_solver.getIntegerSort();
+    // f is the function implementing (lambda ((x Int)) (+ x 1))
+    Term f = d_solver.declareOracleFun("f", new Sort[] {iSort}, iSort, (input) -> {
+      if (input[0].getIntegerValue().signum() > -1)
+      {
+        return d_solver.mkInteger(input[0].getIntegerValue().add(new BigInteger("1")).toString());
+      }
+      return d_solver.mkInteger(0);
+    });
+    Term three = d_solver.mkInteger(3);
+    Term five = d_solver.mkInteger(5);
+    Term eq =
+        d_solver.mkTerm(EQUAL, new Term[] {d_solver.mkTerm(APPLY_UF, new Term[] {f, three}), five});
+    d_solver.assertFormula(eq);
+    // (f 3) = 5
+    assertTrue(d_solver.checkSat().isUnsat());
+  }
+
+  @Test
+  void declareOracleFunSat() throws CVC5ApiException
+  {
+    d_solver.setOption("oracles", "true");
+    d_solver.setOption("produce-models", "true");
+    Sort iSort = d_solver.getIntegerSort();
+
+    // f is the function implementing (lambda ((x Int)) (% x 10))
+    Term f = d_solver.declareOracleFun("f", new Sort[] {iSort}, iSort, (input) -> {
+      if (input[0].getIntegerValue().signum() > -1)
+      {
+        return d_solver.mkInteger(input[0].getIntegerValue().mod(new BigInteger("10")).toString());
+      }
+      return d_solver.mkInteger(0);
+    });
+    Term seven = d_solver.mkInteger(7);
+    Term x = d_solver.mkConst(iSort, "x");
+    Term lb = d_solver.mkTerm(Kind.GEQ, new Term[] {x, d_solver.mkInteger(0)});
+    d_solver.assertFormula(lb);
+    Term ub = d_solver.mkTerm(Kind.LEQ, new Term[] {x, d_solver.mkInteger(100)});
+    d_solver.assertFormula(ub);
+    Term eq = d_solver.mkTerm(
+        Kind.EQUAL, new Term[] {d_solver.mkTerm(APPLY_UF, new Term[] {f, x}), seven});
+    d_solver.assertFormula(eq);
+    // x >= 0 ^ x <= 100 ^ (f x) = 7
+    assertTrue(d_solver.checkSat().isSat());
+    Term xval = d_solver.getValue(x);
+    assertTrue(xval.getIntegerValue().signum() > -1);
+    assertTrue(xval.getIntegerValue().mod(new BigInteger("10")).equals(new BigInteger("7")));
+  }
+
+  @Test
+  void declareOracleFunSat2() throws CVC5ApiException
+  {
+    d_solver.setOption("oracles", "true");
+    d_solver.setOption("produce-models", "true");
+    Sort iSort = d_solver.getIntegerSort();
+    Sort bSort = d_solver.getBooleanSort();
+    // eq is the function implementing (lambda ((x Int) (y Int)) (= x y))
+    Term eq = d_solver.declareOracleFun("eq", new Sort[] {iSort, iSort}, bSort, (input) -> {
+      return d_solver.mkBoolean(input[0].equals(input[1]));
+    });
+    Term x = d_solver.mkConst(iSort, "x");
+    Term y = d_solver.mkConst(iSort, "y");
+    Term neq = d_solver.mkTerm(
+        Kind.NOT, new Term[] {d_solver.mkTerm(Kind.APPLY_UF, new Term[] {eq, x, y})});
+    d_solver.assertFormula(neq);
+    // (not (eq x y))
+    assertTrue(d_solver.checkSat().isSat());
+    Term xval = d_solver.getValue(x);
+    Term yval = d_solver.getValue(y);
+    assertFalse(xval.equals(yval));
+  }
 }

diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java
index eca76590bd7fff8c49a5a96499a626f53a78498d..84ef2727928486f1e7746f64a29daace85049776 100644 (file)
--- a/test/unit/api/java/SortTest.java
+++ b/test/unit/api/java/SortTest.java
@@ -58,8 +58,7 @@ class SortTest
   Sort create_param_datatype_sort() throws CVC5ApiException
   {
     Sort sort = d_solver.mkParamSort("T");
-    DatatypeDecl paramDtypeSpec =
-        d_solver.mkDatatypeDecl("paramlist", new Sort[] {sort});
+    DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", new Sort[] {sort});
     DatatypeConstructorDecl paramCons = d_solver.mkDatatypeConstructorDecl("cons");
     DatatypeConstructorDecl paramNil = d_solver.mkDatatypeConstructorDecl("nil");
     paramCons.addSelector("head", sort);

diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java
index b7302b7f365e061528e03fa6e83fd44fc5d8174c..b103d6b6d5e7ed73bb8e78d44e5fe1cab65d5d7d 100644 (file)
--- a/test/unit/api/java/TermTest.java
+++ b/test/unit/api/java/TermTest.java
@@ -210,8 +210,7 @@ class TermTest
 
     // Test Datatypes Ops
     Sort sort = d_solver.mkParamSort("T");
-    DatatypeDecl listDecl =
-        d_solver.mkDatatypeDecl("paramlist", new Sort[] {sort});
+    DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", new Sort[] {sort});
     DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
     DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
     cons.addSelector("head", sort);