From 6c64864fc261a9849ddbb7595af7ae9a69466291 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 29 Mar 2022 13:57:07 -0500 Subject: [PATCH] Add information for cardinality constraint to the API (#8422) Python API is not implemented yet, as it requires new infrastructure for returning pairs. --- src/api/cpp/cvc5.cpp | 34 ++++++++++++++++++ src/api/cpp/cvc5.h | 10 ++++++ src/api/java/io/github/cvc5/api/Term.java | 23 ++++++++++++ src/api/java/jni/term.cpp | 43 +++++++++++++++++++++++ test/unit/api/cpp/term_black.cpp | 15 ++++++++ test/unit/api/java/TermTest.java | 15 ++++++++ 6 files changed, 140 insertions(+) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 4f92c98c6..d0f0957d2 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -3228,6 +3228,40 @@ std::vector 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 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( + d_node->getOperator() + .getConst() + .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(); + 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 3fd0dad4a..9c7bc0c98 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -1607,6 +1607,16 @@ class CVC5_EXPORT Term */ std::vector 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 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 ba95d3458..02fb42cf4 100644 --- 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, 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 getCardinalityConstraint() + { + Pair pair = getCardinalityConstraint(pointer); + Sort sort = new Sort(solver, pair.first); + return new Pair(sort, pair.second); + } + + private native Pair getCardinalityConstraint(long pointer); + public class ConstIterator implements Iterator { private int currentIndex; diff --git a/src/api/java/jni/term.cpp b/src/api/java/jni/term.cpp index a0f5f1bc4..e5bb02b22 100644 --- 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(pointer); + return static_cast(current->isCardinalityConstraint()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(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(pointer); + auto [sort, upperBound] = current->getCardinalityConstraint(); + Sort* sortPointer = new Sort(sort); + jobject u = getBigIntegerObject(env, upperBound); + + // Long s = new Long(sortPointer); + jclass longClass = env->FindClass("Ljava/lang/Long;"); + jmethodID longConstructor = env->GetMethodID(longClass, "", "(J)V"); + jobject s = env->NewObject(longClass, longConstructor, sortPointer); + + // Pair pair = new Pair(s, u); + jclass pairClass = env->FindClass("Lio/github/cvc5/api/Pair;"); + jmethodID pairConstructor = env->GetMethodID( + pairClass, "", "(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 070ccacab..e5be408eb 100644 --- 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 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 e9875d362..ee5d1429d 100644 --- 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 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"); -- 2.30.2