Add information for cardinality constraint to the API (#8422)

Python API is not implemented yet, as it requires new infrastructure for returning pairs.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 4f92c98c6c90fff0b978449eefa847e36661034e..d0f0957d2e8c9b7b78af4205099941c1279001b2 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -3228,6 +3228,40 @@ std::vector<Term> Term::getSequenceValue() const
   CVC5_API_TRY_CATCH_END;
 }
 
+bool Term::isCardinalityConstraint() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  //////// all checks before this line
+  return d_node->getKind() == cvc5::Kind::CARDINALITY_CONSTRAINT;
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+std::pair<Sort, uint32_t> Term::getCardinalityConstraint() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_ARG_CHECK_EXPECTED(
+      d_node->getKind() == cvc5::Kind::CARDINALITY_CONSTRAINT, *d_node)
+      << "Term to be a cardinality constraint when calling "
+         "getCardinalityConstraint()";
+  // this should never happen since we restrict what the user can create
+  CVC5_API_ARG_CHECK_EXPECTED(detail::checkIntegerBounds<std::uint32_t>(
+                                  d_node->getOperator()
+                                      .getConst<CardinalityConstraint>()
+                                      .getUpperBound()),
+                              *d_node)
+      << "Upper bound for cardinality constraint does not fit uint32_t";
+  //////// all checks before this line
+  const CardinalityConstraint& cc =
+      d_node->getOperator().getConst<CardinalityConstraint>();
+  return std::make_pair(Sort(d_solver, cc.getType()),
+                        cc.getUpperBound().getUnsignedInt());
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 std::ostream& operator<<(std::ostream& out, const Term& t)
 {
   out << t.toString();

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 3fd0dad4a557fddb5c2f733f032f512f71c0880f..9c7bc0c98ddfd72c04990f08a7736cb13a2677b2 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -1607,6 +1607,16 @@ class CVC5_EXPORT Term
    */
   std::vector<Term> getSequenceValue() const;
 
+  /**
+   * @return true if the term is a cardinality constraint
+   */
+  bool isCardinalityConstraint() const;
+  /**
+   * Asserts isCardinalityConstraint().
+   * @return the sort the cardinality constraint is for and its upper bound.
+   */
+  std::pair<Sort, uint32_t> getCardinalityConstraint() const;
+
  protected:
   /**
    * The associated solver object.

diff --git a/src/api/java/io/github/cvc5/api/Term.java b/src/api/java/io/github/cvc5/api/Term.java
index ba95d3458bf340f248020138dda770dcd6061623..02fb42cf4f412596552a2d49b612ba35a097f531 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Term.java
+++ b/src/api/java/io/github/cvc5/api/Term.java
@@ -682,6 +682,29 @@ public class Term extends AbstractPointer implements Comparable<Term>, Iterable<
 
   private native long[] getSequenceValue(long pointer);
 
+  /**
+   * @return true if the term is a cardinality constraint
+   */
+  public boolean isCardinalityConstraint()
+  {
+    return isCardinalityConstraint(pointer);
+  }
+
+  private native boolean isCardinalityConstraint(long pointer);
+
+ /**
+   * Asserts isCardinalityConstraint().
+   * @return the sort the cardinality constraint is for and its upper bound.
+   */
+  public Pair<Sort, BigInteger> getCardinalityConstraint()
+  {
+    Pair<Long, BigInteger> pair = getCardinalityConstraint(pointer);
+    Sort sort = new Sort(solver, pair.first);
+    return new Pair<Sort, BigInteger>(sort, pair.second);
+  }
+
+  private native Pair<Long, BigInteger> getCardinalityConstraint(long pointer);
+
   public class ConstIterator implements Iterator<Term>
   {
     private int currentIndex;

diff --git a/src/api/java/jni/term.cpp b/src/api/java/jni/term.cpp
index a0f5f1bc4eeb01176e861be0d70d6f34a5480720..e5bb02b22892c9af0679f8f90da5970f2a1f37c7 100644 (file)
--- a/src/api/java/jni/term.cpp
+++ b/src/api/java/jni/term.cpp
@@ -905,6 +905,49 @@ JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Term_getSequenceValue(
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 }
 
+/*
+ * Class:     io_github_cvc5_api_Term
+ * Method:    isCardinalityConstraint
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isCardinalityConstraint(
+    JNIEnv* env, jobject, jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  return static_cast<jboolean>(current->isCardinalityConstraint());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
+}
+
+/*
+ * Class:     io_github_cvc5_api_Term
+ * Method:    getCardinalityConstraint
+ * Signature: (J)Lio/github/cvc5/api/Pair;
+ */
+JNIEXPORT jobject JNICALL Java_io_github_cvc5_api_Term_getCardinalityConstraint(
+    JNIEnv* env, jobject, jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Term* current = reinterpret_cast<Term*>(pointer);
+  auto [sort, upperBound] = current->getCardinalityConstraint();
+  Sort* sortPointer = new Sort(sort);
+  jobject u = getBigIntegerObject<std::uint32_t>(env, upperBound);
+
+  // Long s = new Long(sortPointer);
+  jclass longClass = env->FindClass("Ljava/lang/Long;");
+  jmethodID longConstructor = env->GetMethodID(longClass, "<init>", "(J)V");
+  jobject s = env->NewObject(longClass, longConstructor, sortPointer);
+
+  // Pair pair = new Pair<Long, BigInteger>(s, u);
+  jclass pairClass = env->FindClass("Lio/github/cvc5/api/Pair;");
+  jmethodID pairConstructor = env->GetMethodID(
+      pairClass, "<init>", "(Ljava/lang/Object;Ljava/lang/Object;)V");
+  jobject pair = env->NewObject(pairClass, pairConstructor, s, u);
+
+  return pair;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
 /*
  * Class:     io_github_cvc5_api_Term
  * Method:    iterator

diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp
index 070ccacab3eb5a49714eb8158c8395873176c4fc..e5be408eb6e898dc371e66830da03ea0ec8c0169 100644 (file)
--- a/test/unit/api/cpp/term_black.cpp
+++ b/test/unit/api/cpp/term_black.cpp
@@ -1137,6 +1137,21 @@ TEST_F(TestApiBlackTerm, getSequenceValue)
   ASSERT_THROW(su.getSequenceValue(), CVC5ApiException);
 }
 
+TEST_F(TestApiBlackTerm, getCardinalityConstraint)
+{
+  Sort su = d_solver.mkUninterpretedSort("u");
+  Term t = d_solver.mkCardinalityConstraint(su, 3);
+  ASSERT_TRUE(t.isCardinalityConstraint());
+  std::pair<Sort, uint32_t> cc = t.getCardinalityConstraint();
+  ASSERT_EQ(cc.first, su);
+  ASSERT_EQ(cc.second, 3);
+  Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
+  ASSERT_FALSE(x.isCardinalityConstraint());
+  ASSERT_THROW(x.getCardinalityConstraint(), CVC5ApiException);
+  Term nullt;
+  ASSERT_THROW(nullt.isCardinalityConstraint(), CVC5ApiException);
+}
+
 TEST_F(TestApiBlackTerm, termScopedToString)
 {
   Sort intsort = d_solver.getIntegerSort();

diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java
index e9875d362bfe84eeb1994356e587a2685805ce6b..ee5d1429da5f40b72007f626a05e59f93793a80b 100644 (file)
--- a/test/unit/api/java/TermTest.java
+++ b/test/unit/api/java/TermTest.java
@@ -997,6 +997,21 @@ class TermTest
     assertEquals(Arrays.asList(new Term[] {i1, i1, i2}), Arrays.asList(s5.getSequenceValue()));
   }
 
+  @Test void getCardinalityConstraint() throws CVC5ApiException
+  {
+    Sort su = d_solver.mkUninterpretedSort("u");
+    Term t = d_solver.mkCardinalityConstraint(su, 3);
+    assertTrue(t.isCardinalityConstraint());
+    Pair<Sort, BigInteger> cc = t.getCardinalityConstraint();
+    assertEquals(cc.first, su);
+    assertEquals(cc.second, new BigInteger("3"));
+    Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
+    assertFalse(x.isCardinalityConstraint());
+    assertThrows(CVC5ApiException.class, () -> x.getCardinalityConstraint());
+    Term nullt = d_solver.getNullTerm();
+    assertThrows(CVC5ApiException.class, () -> nullt.isCardinalityConstraint());
+  }
+
   @Test void substitute()
   {
     Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");