diff options
Diffstat (limited to 'src/api/java/jni/solver.cpp')
-rw-r--r-- | src/api/java/jni/solver.cpp | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index 882a74794..af3d7e59e 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -1333,6 +1333,23 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkFloatingPoint( /* * Class: io_github_cvc5_api_Solver + * Method: mkCardinalityConstraint + * Signature: (JJI)J + */ +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkCardinalityConstraint( + JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jint upperBound) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + Term* retPointer = + new Term(solver->mkCardinalityConstraint(*sort, (int32_t)upperBound)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: io_github_cvc5_api_Solver * Method: mkConst * Signature: (JJLjava/lang/String;)J */ @@ -2707,4 +2724,4 @@ Java_io_github_cvc5_api_Solver_getNullDatatypeDecl(JNIEnv* env, jobject, jlong) DatatypeDecl* ret = new DatatypeDecl(); return reinterpret_cast<jlong>(ret); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); -}
\ No newline at end of file +} |