Java and python unit tests for mkCardinalityConstraint (#7486)

Adds leftover missing unit tests for new API call for mkCardinalityConstraint from eeb78c8.

8 files changed, 74 insertions, 16 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 280b07bb2..5e38096c8 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -6054,16 +6054,16 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
   CVC5_API_TRY_CATCH_END;
 }
 
-Term Solver::mkCardinalityConstraint(const Sort& sort, uint32_t ubound) const
+Term Solver::mkCardinalityConstraint(const Sort& sort, uint32_t upperBound) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORT(sort);
   CVC5_API_ARG_CHECK_EXPECTED(sort.isUninterpretedSort(), sort)
       << "an uninterpreted sort";
-  CVC5_API_ARG_CHECK_EXPECTED(ubound > 0, ubound) << "a value > 0";
+  CVC5_API_ARG_CHECK_EXPECTED(upperBound > 0, upperBound) << "a value > 0";
   //////// all checks before this line
   Node cco =
-      d_nodeMgr->mkConst(cvc5::CardinalityConstraint(*sort.d_type, ubound));
+      d_nodeMgr->mkConst(cvc5::CardinalityConstraint(*sort.d_type, upperBound));
   Node cc = d_nodeMgr->mkNode(cvc5::Kind::CARDINALITY_CONSTRAINT, cco);
   return Term(this, cc);
   ////////
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 57c3f311d..c618106a6 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3600,10 +3600,10 @@ class CVC5_EXPORT Solver
   /**
    * Create a cardinality constraint for an uninterpreted sort.
    * @param sort the sort the cardinality constraint is for
-   * @param val the upper bound on the cardinality of the sort
+   * @param upperBound the upper bound on the cardinality of the sort
    * @return the cardinality constraint
    */
-  Term mkCardinalityConstraint(const Sort& sort, uint32_t ubound) const;
+  Term mkCardinalityConstraint(const Sort& sort, uint32_t upperBound) const;
 
   /* .................................................................... */
   /* Create Variables                                                     */
diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index 670ab7cbd..3a9f450a4 100644
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -1184,6 +1184,21 @@ public class Solver implements IPointer
 
   private native long mkFloatingPoint(long pointer, int exp, int sig, long valPointer);
 
+  /**
+   * Create a cardinality constraint for an uninterpreted sort.
+   * @param sort the sort the cardinality constraint is for
+   * @param upperBound the upper bound on the cardinality of the sort
+   * @return the cardinality constraint
+   */
+  public Term mkCardinalityConstraint(Sort sort, int upperBound) throws CVC5ApiException
+  {
+    Utils.validateUnsigned(upperBound, "upperBound");
+    long termPointer = mkCardinalityConstraint(pointer, sort.getPointer(), upperBound);
+    return new Term(this, termPointer);
+  }
+
+  private native long mkCardinalityConstraint(long pointer, long sortPointer, int upperBound);
+
   /* .................................................................... */
   /* Create Variables                                                     */
   /* .................................................................... */
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
+}
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 02b572120..cf405b519 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -241,6 +241,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Term mkUninterpretedConst(Sort sort, int32_t index) except +
         Term mkAbstractValue(const string& index) except +
         Term mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) except +
+        Term mkCardinalityConstraint(Sort sort, int32_t index) except +
         Term mkConst(Sort sort, const string& symbol) except +
         # default value for symbol defined in cpp/cvc5.h
         Term mkConst(Sort sort) except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 4627859b9..9391dbdd1 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1391,6 +1391,16 @@ cdef class Solver:
         term.cterm = self.csolver.mkFloatingPoint(exp, sig, val.cterm)
         return term
 
+    def mkCardinalityConstraint(self, Sort sort, int index):
+        """Create cardinality constraint.
+
+        :param sort: Sort of the constraint
+        :param index: The upper bound for the cardinality of the sort
+        """
+        cdef Term term = Term(self)
+        term.cterm = self.csolver.mkCardinalityConstraint(sort.csort, index)
+        return term
+
     def mkConst(self, Sort sort, symbol=None):
         """
         Create (first-order) constant (0-arity function symbol).
diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
index 6052a057f..04a275741 100644
--- a/test/python/unit/api/test_solver.py
+++ b/test/python/unit/api/test_solver.py
@@ -422,6 +422,17 @@ def test_mk_floating_point(solver):
     with pytest.raises(RuntimeError):
         slv.mkFloatingPoint(3, 5, t1)
 
+def test_mk_cardinality_constraint(solver):
+    su = solver.mkUninterpretedSort("u")
+    si = solver.getIntegerSort()
+    solver.mkCardinalityConstraint(su, 3)
+    with pytest.raises(RuntimeError):
+        solver.mkEmptySet(solver.mkCardinalityConstraint(si, 3))
+    with pytest.raises(RuntimeError):
+        solver.mkEmptySet(solver.mkCardinalityConstraint(su, 0))
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkCardinalityConstraint(su, 3)
 
 def test_mk_empty_set(solver):
     slv = pycvc5.Solver()
diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 8511827a8..1f88add2d 100644
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -387,16 +387,6 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO));
   }
 
-  @Test void mkUninterpretedConst() throws CVC5ApiException
-  {
-    assertDoesNotThrow(() -> d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
-    assertThrows(
-        CVC5ApiException.class, () -> d_solver.mkUninterpretedConst(d_solver.getNullSort(), 1));
-    Solver slv = new Solver();
-    assertThrows(
-        CVC5ApiException.class, () -> slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
-  }
-
   @Test void mkAbstractValue() throws CVC5ApiException
   {
     assertDoesNotThrow(() -> d_solver.mkAbstractValue(("1")));
@@ -434,6 +424,20 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> slv.mkFloatingPoint(3, 5, t1));
   }
 
+  @Test void mkCardinalityConstraint() throws CVC5ApiException
+  {
+    Sort su = d_solver.mkUninterpretedSort("u");
+    Sort si = d_solver.getIntegerSort();
+    assertDoesNotThrow(() -> d_solver.mkCardinalityConstraint(su, 3));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.mkCardinalityConstraint(si, 3));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.mkCardinalityConstraint(su, 0));
+    Solver slv = new Solver();
+    assertThrows(
+        CVC5ApiException.class, () -> slv.mkCardinalityConstraint(su, 3));
+  }
+
   @Test void mkEmptySet() throws CVC5ApiException
   {
     Solver slv = new Solver();