diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cpp/cvc5.cpp | 6 | ||||
-rw-r--r-- | src/api/cpp/cvc5.h | 4 | ||||
-rw-r--r-- | src/api/java/io/github/cvc5/api/Solver.java | 15 | ||||
-rw-r--r-- | src/api/java/jni/solver.cpp | 19 | ||||
-rw-r--r-- | src/api/python/cvc5.pxd | 1 | ||||
-rw-r--r-- | src/api/python/cvc5.pxi | 10 |
6 files changed, 49 insertions, 6 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). |