From f5a9a12b2188a0d2476502aa9619e2c83de99ce5 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Mon, 6 Jun 2022 13:58:22 -0500 Subject: [PATCH] Add declareOracleFun to the Java API (#8815) --- src/api/java/CMakeLists.txt | 1 + src/api/java/io/github/cvc5/IOracle.java | 23 + src/api/java/io/github/cvc5/Solver.java | 50 ++- src/api/java/jni/api_utilities.cpp | 32 +- src/api/java/jni/api_utilities.h | 58 ++- src/api/java/jni/solver.cpp | 523 +++++++++++++---------- test/unit/api/java/SolverTest.java | 136 +++++- test/unit/api/java/SortTest.java | 3 +- test/unit/api/java/TermTest.java | 3 +- 9 files changed, 546 insertions(+), 283 deletions(-) create mode 100644 src/api/java/io/github/cvc5/IOracle.java diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index 736ffddb9..93b018179 100644 --- 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 index 000000000..cab3cc861 --- /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 a3fcb4ce4..c89701f9b 100644 --- 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 abstractPointers = new ArrayList<>(); + // store IOracle objects + List 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 (*) ) + * } + * + * + * 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 1c5e5b5be..a6c986ac9 100644 --- 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, "", "(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& terms) +{ + jclass termClass = env->FindClass("Lio/github/cvc5/Term;"); + jmethodID termConstructor = + env->GetMethodID(termClass, "", "(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(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(termPointer); + return *term; +} diff --git a/src/api/java/jni/api_utilities.h b/src/api/java/jni/api_utilities.h index 5dfeeb7c0..86488c740 100644 --- 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 #include #include +#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 > 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& terms); + #endif // CVC5__API_UTILITIES_H diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index e13090bea..01809f7ce 100644 --- 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(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& refs = globalReferences[pointer]; + for (jobject ref : refs) + { + env->DeleteGlobalRef(ref); + } + globalReferences.erase(pointer); delete (reinterpret_cast(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(pointer); const char* s = env->GetStringUTFChars(jsymbol, nullptr); std::string symbol(s); Sort* sortptr = reinterpret_cast(sort); - std::vector initValue = getObjectsFromPointers(env, initValuePointers); + std::vector initValue = + getObjectsFromPointers(env, initValuePointers); Term* retPointer = new Term(solver->declarePool(symbol, *sortptr, initValue)); return reinterpret_cast(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(pointer); + const char* s = env->GetStringUTFChars(jSymbol, nullptr); + std::string cSymbol(s); + Sort* sort = reinterpret_cast(sortPointer); + std::vector sorts = getObjectsFromPointers(env, sortPointers); + std::function)> fn = + [env, solverReference, oracleReference](std::vector input) { + Term term = applyOracle(env, solverReference, oracleReference, input); + return term; + }; + Term* retPointer = + new Term(solver->declareOracleFun(cSymbol, sorts, *sort, fn)); + return reinterpret_cast(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(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(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(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(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(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(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(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(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(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(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(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(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 b52514a28..38d41b9ef 100644 --- 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 eca76590b..84ef27279 100644 --- 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 b7302b7f3..b103d6b6d 100644 --- 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); -- 2.30.2