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
+}