From f3a2e3814d0a3f32fe1e9e24de954bc2d9ff999e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 25 Oct 2021 15:23:31 -0500 Subject: [PATCH] Java and python unit tests for mkCardinalityConstraint (#7486) Adds leftover missing unit tests for new API call for mkCardinalityConstraint from eeb78c8. --- src/api/cpp/cvc5.cpp | 6 +++--- src/api/cpp/cvc5.h | 4 ++-- src/api/java/io/github/cvc5/api/Solver.java | 15 +++++++++++++ src/api/java/jni/solver.cpp | 19 +++++++++++++++- src/api/python/cvc5.pxd | 1 + src/api/python/cvc5.pxi | 10 +++++++++ test/python/unit/api/test_solver.py | 11 ++++++++++ test/unit/api/java/SolverTest.java | 24 ++++++++++++--------- 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 @@ -1331,6 +1331,23 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkFloatingPoint( CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } +/* + * 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(pointer); + Sort* sort = reinterpret_cast(sortPointer); + Term* retPointer = + new Term(solver->mkCardinalityConstraint(*sort, (int32_t)upperBound)); + return reinterpret_cast(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + /* * Class: io_github_cvc5_api_Solver * Method: mkConst @@ -2707,4 +2724,4 @@ Java_io_github_cvc5_api_Solver_getNullDatatypeDecl(JNIEnv* env, jobject, jlong) DatatypeDecl* ret = new DatatypeDecl(); return reinterpret_cast(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(); -- 2.30.2