diff options
Diffstat (limited to 'src/api/java/jni/cvc5_Solver.cpp')
| -rw-r--r-- | src/api/java/jni/cvc5_Solver.cpp | 159 |
1 files changed, 158 insertions, 1 deletions
diff --git a/src/api/java/jni/cvc5_Solver.cpp b/src/api/java/jni/cvc5_Solver.cpp index c28ea412f..cdbb48db0 100644 --- a/src/api/java/jni/cvc5_Solver.cpp +++ b/src/api/java/jni/cvc5_Solver.cpp @@ -1061,6 +1061,22 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkEmptyBag(JNIEnv* env, /* * Class: cvc5_Solver + * Method: mkSepEmp + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSepEmp(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = new Term(solver->mkSepEmp()); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver * Method: mkSepNil * Signature: (JJ)J */ @@ -1871,6 +1887,57 @@ JNIEXPORT jstring JNICALL Java_cvc5_Solver_getOption(JNIEnv* env, /* * Class: cvc5_Solver + * Method: getOptionNames + * Signature: (J)[Ljava/lang/String; + */ +JNIEXPORT jobjectArray JNICALL Java_cvc5_Solver_getOptionNames(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::vector<std::string> options = solver->getOptionNames(); + jobjectArray ret = getStringArrayFromStringVector(env, options); + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: cvc5_Solver + * Method: getOptionInfo + * Signature: (JLjava/lang/String;)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getOptionInfo(JNIEnv* env, + jobject, + jlong pointer, + jstring jOption) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::string cOption(env->GetStringUTFChars(jOption, nullptr)); + OptionInfo* ret = new OptionInfo(solver->getOptionInfo(cOption)); + return reinterpret_cast<jlong>(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getDriverOptions + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getDriverOptions(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + DriverOptions* ret = new DriverOptions(solver->getDriverOptions()); + return reinterpret_cast<jlong>(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver * Method: getUnsatAssumptions * Signature: (J)[J */ @@ -1905,6 +1972,62 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getUnsatCore(JNIEnv* env, /* * Class: cvc5_Solver + * Method: getDifficulty + * Signature: (J)Ljava/util/Map; + */ +JNIEXPORT jobject JNICALL Java_cvc5_Solver_getDifficulty(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::map<Term, Term> map = solver->getDifficulty(); + // HashMap hashMap = new HashMap(); + jclass hashMapClass = env->FindClass("Ljava/util/HashMap;"); + jmethodID constructor = env->GetMethodID(hashMapClass, "<init>", "()V"); + jobject hashMap = env->NewObject(hashMapClass, constructor); + jmethodID putMethod = env->GetMethodID( + hashMapClass, + "put", + "(Ljava/lang/Object;Ljava/lang/Object;)Ljava/lang/Object;"); + + // Long longObject = new Long(statPointer) + jclass longClass = env->FindClass("Ljava/lang/Long;"); + jmethodID longConstructor = env->GetMethodID(longClass, "<init>", "(J)V"); + + for (const auto& [k, v] : map) + { + // hashmap.put(key, value); + Term* termKey = new Term(k); + Term* termValue = new Term(v); + jobject key = env->NewObject( + longClass, longConstructor, reinterpret_cast<jlong>(termKey)); + jobject value = env->NewObject( + longClass, longConstructor, reinterpret_cast<jlong>(termValue)); + env->CallObjectMethod(hashMap, putMethod, key, value); + } + return hashMap; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: cvc5_Solver + * Method: getProof + * Signature: (J)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_cvc5_Solver_getProof(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::string proof = solver->getProof(); + return env->NewStringUTF(proof.c_str()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver * Method: getValue * Signature: (JJ)J */ @@ -1940,6 +2063,23 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getValue__J_3J( /* * Class: cvc5_Solver + * Method: getModelDomainElements + * Signature: (JJ)[J + */ +JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getModelDomainElements( + JNIEnv* env, jobject, jlong pointer, jlong sortPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + std::vector<Term> terms = solver->getModelDomainElements(*sort); + jlongArray ret = getPointersFromObjects<Term>(env, terms); + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: cvc5_Solver * Method: isModelCoreSymbol * Signature: (JJ)Z */ @@ -2446,6 +2586,23 @@ JNIEXPORT void JNICALL Java_cvc5_Solver_addSygusConstraint(JNIEnv* env, /* * Class: cvc5_Solver + * Method: addSygusAssume + * Signature: (JJ)V + */ +JNIEXPORT void JNICALL Java_cvc5_Solver_addSygusAssume(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* term = reinterpret_cast<Term*>(termPointer); + solver->addSygusAssume(*term); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Solver * Method: addSygusInvConstraint * Signature: (JJJJJ)V */ @@ -2591,4 +2748,4 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullDatatypeDecl(JNIEnv* env, DatatypeDecl* ret = new DatatypeDecl(); return reinterpret_cast<jlong>(ret); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); -}
\ No newline at end of file +} |