From 467c95cffba499ef9c1fd542c5f3bb87cd385c5e Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Thu, 31 Mar 2022 18:10:29 -0700 Subject: [PATCH] api: Use std::optional for symbols in mk* functions. (#8495) Makes all symbols in mk* functions optional. --- src/api/cpp/cvc5.cpp | 55 +++++++------- src/api/cpp/cvc5.h | 29 ++++---- src/api/java/io/github/cvc5/Solver.java | 52 +++++++++++++- src/api/java/jni/solver.cpp | 72 +++++++++++++++++-- src/api/python/cvc5.pxd | 5 +- src/api/python/cvc5.pxi | 23 ++++-- src/parser/parser.cpp | 6 +- test/unit/api/cpp/datatype_api_black.cpp | 4 +- .../api/cpp/parametric_datatype_black.cpp | 4 +- test/unit/api/cpp/solver_black.cpp | 6 +- test/unit/api/cpp/sort_black.cpp | 20 +++--- test/unit/api/java/DatatypeTest.java | 4 +- test/unit/api/java/ResultTest.java | 4 +- test/unit/api/java/SolverTest.java | 6 +- test/unit/api/java/SortTest.java | 14 ++-- test/unit/api/python/test_datatype_api.py | 4 +- test/unit/api/python/test_solver.py | 6 +- test/unit/api/python/test_sort.py | 14 ++-- 18 files changed, 222 insertions(+), 106 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 2d10f8e92..3cc67a0c7 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -5550,13 +5550,17 @@ Sort Solver::mkFunctionSort(const std::vector& sorts, CVC5_API_TRY_CATCH_END; } -Sort Solver::mkParamSort(const std::string& symbol) const +Sort Solver::mkParamSort(const std::optional& symbol) const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - return Sort(this, - getNodeManager()->mkSort( - symbol, internal::NodeManager::SORT_FLAG_PLACEHOLDER)); + + internal::TypeNode tn = + symbol ? getNodeManager()->mkSort( + *symbol, internal::NodeManager::SORT_FLAG_PLACEHOLDER) + : getNodeManager()->mkSort( + internal::NodeManager::SORT_FLAG_PLACEHOLDER); + return Sort(this, tn); //////// CVC5_API_TRY_CATCH_END; } @@ -5626,11 +5630,13 @@ Sort Solver::mkSequenceSort(const Sort& elemSort) const CVC5_API_TRY_CATCH_END; } -Sort Solver::mkUninterpretedSort(const std::string& symbol) const +Sort Solver::mkUninterpretedSort(const std::optional& symbol) const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - return Sort(this, getNodeManager()->mkSort(symbol)); + internal::TypeNode tn = + symbol ? getNodeManager()->mkSort(*symbol) : getNodeManager()->mkSort(); + return Sort(this, tn); //////// CVC5_API_TRY_CATCH_END; } @@ -5648,13 +5654,17 @@ Sort Solver::mkUnresolvedSort(const std::string& symbol, size_t arity) const CVC5_API_TRY_CATCH_END; } -Sort Solver::mkUninterpretedSortConstructorSort(const std::string& symbol, - size_t arity) const +Sort Solver::mkUninterpretedSortConstructorSort( + size_t arity, const std::optional& symbol) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_ARG_CHECK_EXPECTED(arity > 0, arity) << "an arity > 0"; //////// all checks before this line - return Sort(this, getNodeManager()->mkSortConstructor(symbol, arity)); + if (symbol) + { + return Sort(this, getNodeManager()->mkSortConstructor(*symbol, arity)); + } + return Sort(this, getNodeManager()->mkSortConstructor("", arity)); //////// CVC5_API_TRY_CATCH_END; } @@ -6042,25 +6052,14 @@ Term Solver::mkCardinalityConstraint(const Sort& sort, uint32_t upperBound) cons /* Create constants */ /* -------------------------------------------------------------------------- */ -Term Solver::mkConst(const Sort& sort, const std::string& symbol) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_SOLVER_CHECK_SORT(sort); - //////// all checks before this line - internal::Node res = d_nodeMgr->mkVar(symbol, *sort.d_type); - (void)res.getType(true); /* kick off type checking */ - increment_vars_consts_stats(sort, false); - return Term(this, res); - //////// - CVC5_API_TRY_CATCH_END; -} - -Term Solver::mkConst(const Sort& sort) const +Term Solver::mkConst(const Sort& sort, + const std::optional& symbol) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORT(sort); //////// all checks before this line - internal::Node res = d_nodeMgr->mkVar(*sort.d_type); + internal::Node res = symbol ? d_nodeMgr->mkVar(*symbol, *sort.d_type) + : d_nodeMgr->mkVar(*sort.d_type); (void)res.getType(true); /* kick off type checking */ increment_vars_consts_stats(sort, false); return Term(this, res); @@ -6071,14 +6070,14 @@ Term Solver::mkConst(const Sort& sort) const /* Create variables */ /* -------------------------------------------------------------------------- */ -Term Solver::mkVar(const Sort& sort, const std::string& symbol) const +Term Solver::mkVar(const Sort& sort, + const std::optional& symbol) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORT(sort); //////// all checks before this line - internal::Node res = symbol.empty() - ? d_nodeMgr->mkBoundVar(*sort.d_type) - : d_nodeMgr->mkBoundVar(symbol, *sort.d_type); + internal::Node res = symbol ? d_nodeMgr->mkBoundVar(*symbol, *sort.d_type) + : d_nodeMgr->mkBoundVar(*sort.d_type); (void)res.getType(true); /* kick off type checking */ increment_vars_consts_stats(sort, true); return Term(this, res); diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 3c8de6c18..96fe3775f 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -3236,7 +3236,8 @@ class CVC5_EXPORT Solver * @param symbol the name of the sort * @return the sort parameter */ - Sort mkParamSort(const std::string& symbol) const; + Sort mkParamSort( + const std::optional& symbol = std::nullopt) const; /** * Create a predicate sort. @@ -3282,7 +3283,8 @@ class CVC5_EXPORT Solver * @param symbol the name of the sort * @return the uninterpreted sort */ - Sort mkUninterpretedSort(const std::string& symbol) const; + Sort mkUninterpretedSort( + const std::optional& symbol = std::nullopt) const; /** * Create an unresolved sort. @@ -3305,8 +3307,9 @@ class CVC5_EXPORT Solver * @param arity the arity of the sort (must be > 0) * @return the uninterpreted sort constructor sort */ - Sort mkUninterpretedSortConstructorSort(const std::string& symbol, - size_t arity) const; + Sort mkUninterpretedSortConstructorSort( + size_t arity, + const std::optional& symbol = std::nullopt) const; /** * Create a tuple sort. @@ -3658,27 +3661,21 @@ class CVC5_EXPORT Solver * \endverbatim * * @param sort the sort of the constant - * @param symbol the name of the constant + * @param symbol the name of the constant (optional) * @return the first-order constant */ - Term mkConst(const Sort& sort, const std::string& symbol) const; - /** - * Create (first-order) constant (0-arity function symbol), with a default - * symbol name. - * - * @param sort the sort of the constant - * @return the first-order constant - */ - Term mkConst(const Sort& sort) const; + Term mkConst(const Sort& sort, + const std::optional& symbol = std::nullopt) const; /** * Create a bound variable to be used in a binder (i.e. a quantifier, a * lambda, or a witness binder). * @param sort the sort of the variable - * @param symbol the name of the variable + * @param symbol the name of the variable (optional) * @return the variable */ - Term mkVar(const Sort& sort, const std::string& symbol = std::string()) const; + Term mkVar(const Sort& sort, + const std::optional& symbol = std::nullopt) const; /* .................................................................... */ /* Create datatype constructor declarations */ diff --git a/src/api/java/io/github/cvc5/Solver.java b/src/api/java/io/github/cvc5/Solver.java index 686a16c72..885ccc359 100644 --- a/src/api/java/io/github/cvc5/Solver.java +++ b/src/api/java/io/github/cvc5/Solver.java @@ -354,6 +354,21 @@ public class Solver implements IPointer, AutoCloseable private native long mkParamSort(long pointer, String symbol); + /** + * Create a sort parameter. + * + * @apiNote This method is experimental and may change in future versions. + * + * @return the sort parameter + */ + public Sort mkParamSort() + { + long sortPointer = mkParamSort(pointer); + return new Sort(this, sortPointer); + } + + private native long mkParamSort(long pointer); + /** * Create a predicate sort. * @param sorts the list of sorts of the predicate @@ -434,6 +449,18 @@ public class Solver implements IPointer, AutoCloseable private native long mkUninterpretedSort(long pointer, String symbol); + /** + * Create an uninterpreted sort. + * @return the uninterpreted sort + */ + public Sort mkUninterpretedSort() + { + long sortPointer = mkUninterpretedSort(pointer); + return new Sort(this, sortPointer); + } + + private native long mkUninterpretedSort(long pointer); + /** * Create an unresolved sort. * @@ -475,19 +502,38 @@ public class Solver implements IPointer, AutoCloseable * An uninterpreted sort constructor is an uninterpreted sort with * arity > 0. * + * @param arity the arity of the sort (must be > 0) * @param symbol the symbol of the sort + * @return the sort constructor sort + * @throws CVC5ApiException + */ + public Sort mkUninterpretedSortConstructorSort(int arity, String symbol) throws CVC5ApiException + { + Utils.validateUnsigned(arity, "arity"); + long sortPointer = mkUninterpretedSortConstructorSort(pointer, arity, symbol); + return new Sort(this, sortPointer); + } + + private native long mkUninterpretedSortConstructorSort(long pointer, int arity, String symbol); + + /** + * Create a sort constructor sort. + * + * An uninterpreted sort constructor is an uninterpreted sort with + * arity > 0. + * * @param arity the arity of the sort (must be > 0) * @return the sort constructor sort * @throws CVC5ApiException */ - public Sort mkUninterpretedSortConstructorSort(String symbol, int arity) throws CVC5ApiException + public Sort mkUninterpretedSortConstructorSort(int arity) throws CVC5ApiException { Utils.validateUnsigned(arity, "arity"); - long sortPointer = mkUninterpretedSortConstructorSort(pointer, symbol, arity); + long sortPointer = mkUninterpretedSortConstructorSort(pointer, arity); return new Sort(this, sortPointer); } - private native long mkUninterpretedSortConstructorSort(long pointer, String symbol, int arity); + private native long mkUninterpretedSortConstructorSort(long pointer, int arity); /** * Create a tuple sort. diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index ee9f6affb..b83560e9f 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -316,8 +316,11 @@ Java_io_github_cvc5_Solver_mkFunctionSort__J_3JJ(JNIEnv* env, * Method: mkParamSort * Signature: (JLjava/lang/String;)J */ -JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkParamSort( - JNIEnv* env, jobject, jlong pointer, jstring jSymbol) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_Solver_mkParamSort__JLjava_lang_String_2(JNIEnv* env, + jobject, + jlong pointer, + jstring jSymbol) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast(pointer); @@ -329,6 +332,22 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkParamSort( CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } +/* + * Class: io_github_cvc5_Solver + * Method: mkParamSort + * Signature: (JL)J + */ +JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkParamSort__J(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast(pointer); + Sort* retPointer = new Sort(solver->mkParamSort()); + return reinterpret_cast(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + /* * Class: io_github_cvc5_Solver * Method: mkPredicateSort @@ -446,7 +465,8 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkSequenceSort( * Method: mkUninterpretedSort * Signature: (JLjava/lang/String;)J */ -JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkUninterpretedSort( +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_Solver_mkUninterpretedSort__JLjava_lang_String_2( JNIEnv* env, jobject, jlong pointer, jstring jSymbol) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -460,6 +480,23 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkUninterpretedSort( CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } +/* + * Class: io_github_cvc5_Solver + * Method: mkUninterpretedSort + * Signature: (JL)J + */ +JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkUninterpretedSort__J( + JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + + Solver* solver = reinterpret_cast(pointer); + Sort* sort = new Sort(solver->mkUninterpretedSort()); + return reinterpret_cast(sort); + + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + /* * Class: io_github_cvc5_Solver * Method: mkUnresolvedSort @@ -483,11 +520,11 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkUnresolvedSort( /* * Class: io_github_cvc5_Solver * Method: mkUninterpretedSortConstructorSort - * Signature: (JLjava/lang/String;I)J + * Signature: (JLIjava/lang/String;)J */ JNIEXPORT jlong JNICALL -Java_io_github_cvc5_Solver_mkUninterpretedSortConstructorSort( - JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jint arity) +Java_io_github_cvc5_Solver_mkUninterpretedSortConstructorSort__JILjava_lang_String_2( + JNIEnv* env, jobject, jlong pointer, jint arity, jstring jSymbol) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -495,13 +532,34 @@ Java_io_github_cvc5_Solver_mkUninterpretedSortConstructorSort( const char* s = env->GetStringUTFChars(jSymbol, nullptr); std::string cSymbol(s); Sort* retPointer = new Sort( - solver->mkUninterpretedSortConstructorSort(cSymbol, (size_t)arity)); + solver->mkUninterpretedSortConstructorSort((size_t)arity, cSymbol)); env->ReleaseStringUTFChars(jSymbol, s); return reinterpret_cast(retPointer); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } +/* + * Class: io_github_cvc5_Solver + * Method: mkUninterpretedSortConstructorSort + * Signature: (JLI)J + */ +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_Solver_mkUninterpretedSortConstructorSort__JI(JNIEnv* env, + jobject, + jlong pointer, + jint arity) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + + Solver* solver = reinterpret_cast(pointer); + Sort* retPointer = + new Sort(solver->mkUninterpretedSortConstructorSort((size_t)arity)); + return reinterpret_cast(retPointer); + + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + /* * Class: io_github_cvc5_Solver * Method: mkTupleSort diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 7c40ce3af..05e06b695 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -220,15 +220,18 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5": const set[Sort]& unresolvedSorts) except + Sort mkFunctionSort(Sort domain, Sort codomain) except + Sort mkFunctionSort(const vector[Sort]& sorts, Sort codomain) except + + Sort mkParamSort() except + Sort mkParamSort(const string& symbol) except + Sort mkPredicateSort(const vector[Sort]& sorts) except + Sort mkRecordSort(const vector[pair[string, Sort]]& fields) except + Sort mkSetSort(Sort elemSort) except + Sort mkBagSort(Sort elemSort) except + Sort mkSequenceSort(Sort elemSort) except + + Sort mkUninterpretedSort() except + Sort mkUninterpretedSort(const string& symbol) except + Sort mkUnresolvedSort(const string& symbol, size_t arity) except + - Sort mkUninterpretedSortConstructorSort(const string& symbol, size_t arity) except + + Sort mkUninterpretedSortConstructorSort(size_t arity) except + + Sort mkUninterpretedSortConstructorSort(size_t arity, const string& symbol) except + Sort mkTupleSort(const vector[Sort]& sorts) except + Term mkTerm(Op op) except + Term mkTerm(Op op, const vector[Term]& children) except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index ce4c99439..a5c3c3f7e 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -831,7 +831,7 @@ cdef class Solver: codomain.csort) return sort - def mkParamSort(self, symbolname): + def mkParamSort(self, str symbolname = None): """ Create a sort parameter. .. warning:: This method is experimental and may change in future @@ -841,7 +841,10 @@ cdef class Solver: :return: the sort parameter """ cdef Sort sort = Sort(self) - sort.csort = self.csolver.mkParamSort(symbolname.encode()) + if symbolname is None: + sort.csort = self.csolver.mkParamSort() + else: + sort.csort = self.csolver.mkParamSort(symbolname.encode()) return sort @expand_list_arg(num_req_args=0) @@ -910,14 +913,17 @@ cdef class Solver: sort.csort = self.csolver.mkSequenceSort(elemSort.csort) return sort - def mkUninterpretedSort(self, str name): + def mkUninterpretedSort(self, str name = None): """Create an uninterpreted sort. :param symbol: the name of the sort :return: the uninterpreted sort """ cdef Sort sort = Sort(self) - sort.csort = self.csolver.mkUninterpretedSort(name.encode()) + if name is None: + sort.csort = self.csolver.mkUninterpretedSort() + else: + sort.csort = self.csolver.mkUninterpretedSort(name.encode()) return sort def mkUnresolvedSort(self, str name, size_t arity = 0): @@ -934,7 +940,7 @@ cdef class Solver: sort.csort = self.csolver.mkUnresolvedSort(name.encode(), arity) return sort - def mkUninterpretedSortConstructorSort(self, str symbol, size_t arity): + def mkUninterpretedSortConstructorSort(self, size_t arity, str symbol = None): """Create a sort constructor sort. An uninterpreted sort constructor is an uninterpreted sort with @@ -945,8 +951,11 @@ cdef class Solver: :return: the sort constructor sort """ cdef Sort sort = Sort(self) - sort.csort = self.csolver.mkUninterpretedSortConstructorSort( - symbol.encode(), arity) + if symbol is None: + sort.csort = self.csolver.mkUninterpretedSortConstructorSort(arity) + else: + sort.csort = self.csolver.mkUninterpretedSortConstructorSort( + arity, symbol.encode()) return sort @expand_list_arg(num_req_args=0) diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 72a918259..5dacfc8a8 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -317,7 +317,7 @@ cvc5::Sort Parser::mkSortConstructor(const std::string& name, size_t arity) { Trace("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; - cvc5::Sort type = d_solver->mkUninterpretedSortConstructorSort(name, arity); + cvc5::Sort type = d_solver->mkUninterpretedSortConstructorSort(arity, name); defineType(name, vector(arity), type); return type; } @@ -334,7 +334,7 @@ cvc5::Sort Parser::mkUnresolvedTypeConstructor(const std::string& name, size_t arity) { cvc5::Sort unresolved = - d_solver->mkUninterpretedSortConstructorSort(name, arity); + d_solver->mkUninterpretedSortConstructorSort(arity, name); defineType(name, vector(arity), unresolved); d_unresolved.insert(unresolved); return unresolved; @@ -346,7 +346,7 @@ cvc5::Sort Parser::mkUnresolvedTypeConstructor( Trace("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" << std::endl; cvc5::Sort unresolved = - d_solver->mkUninterpretedSortConstructorSort(name, params.size()); + d_solver->mkUninterpretedSortConstructorSort(params.size(), name); defineType(name, params, unresolved); cvc5::Sort t = getSort(name, params); d_unresolved.insert(unresolved); diff --git a/test/unit/api/cpp/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp index 04811d3b4..510eca60e 100644 --- a/test/unit/api/cpp/datatype_api_black.cpp +++ b/test/unit/api/cpp/datatype_api_black.cpp @@ -481,7 +481,7 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec) * END; */ unresTypes.clear(); - Sort unresList5 = d_solver.mkUninterpretedSortConstructorSort("list5", 1); + Sort unresList5 = d_solver.mkUninterpretedSortConstructorSort(1, "list5"); unresTypes.insert(unresList5); std::vector v; @@ -520,7 +520,7 @@ TEST_F(TestApiBlackDatatype, datatypeSpecializedCons) */ // Make unresolved types as placeholders std::set unresTypes; - Sort unresList = d_solver.mkUninterpretedSortConstructorSort("plist", 1); + Sort unresList = d_solver.mkUninterpretedSortConstructorSort(1, "plist"); unresTypes.insert(unresList); std::vector v; diff --git a/test/unit/api/cpp/parametric_datatype_black.cpp b/test/unit/api/cpp/parametric_datatype_black.cpp index 4c1c0c833..d7f30cbe1 100644 --- a/test/unit/api/cpp/parametric_datatype_black.cpp +++ b/test/unit/api/cpp/parametric_datatype_black.cpp @@ -28,8 +28,8 @@ TEST_F(TestApiBlackParametricDatatype, proj_issue387) { Sort s1 = d_solver.getBooleanSort(); - Sort u1 = d_solver.mkUninterpretedSortConstructorSort("_x0", 1); - Sort u2 = d_solver.mkUninterpretedSortConstructorSort("_x1", 1); + Sort u1 = d_solver.mkUninterpretedSortConstructorSort(1, "_x0"); + Sort u2 = d_solver.mkUninterpretedSortConstructorSort(1); Sort p1 = d_solver.mkParamSort("_x4"); Sort p2 = d_solver.mkParamSort("_x27"); Sort p3 = d_solver.mkParamSort("_x3"); diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 651b432a7..c728c72e9 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -361,9 +361,9 @@ TEST_F(TestApiBlackSolver, mkUnresolvedSort) TEST_F(TestApiBlackSolver, mkUninterpretedSortConstructorSort) { - ASSERT_NO_THROW(d_solver.mkUninterpretedSortConstructorSort("s", 2)); - ASSERT_NO_THROW(d_solver.mkUninterpretedSortConstructorSort("", 2)); - ASSERT_THROW(d_solver.mkUninterpretedSortConstructorSort("", 0), + ASSERT_NO_THROW(d_solver.mkUninterpretedSortConstructorSort(2, "s")); + ASSERT_NO_THROW(d_solver.mkUninterpretedSortConstructorSort(2, "")); + ASSERT_THROW(d_solver.mkUninterpretedSortConstructorSort(0), CVC5ApiException); } diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp index 3f02933db..e388c60fa 100644 --- a/test/unit/api/cpp/sort_black.cpp +++ b/test/unit/api/cpp/sort_black.cpp @@ -242,13 +242,17 @@ TEST_F(TestApiBlackSort, isUninterpreted) Sort un_sort = d_solver.mkUninterpretedSort("asdf"); ASSERT_TRUE(un_sort.isUninterpretedSort()); ASSERT_NO_THROW(Sort().isUninterpretedSort()); + Sort un_sort2 = d_solver.mkUninterpretedSort(); + ASSERT_TRUE(un_sort2.isUninterpretedSort()); } TEST_F(TestApiBlackSort, isUninterpretedSortConstructor) { - Sort sc_sort = d_solver.mkUninterpretedSortConstructorSort("asdf", 1); + Sort sc_sort = d_solver.mkUninterpretedSortConstructorSort(1, "asdf"); ASSERT_TRUE(sc_sort.isUninterpretedSortConstructor()); ASSERT_NO_THROW(Sort().isUninterpretedSortConstructor()); + Sort sc_sort2 = d_solver.mkUninterpretedSortConstructorSort(2); + ASSERT_TRUE(sc_sort2.isUninterpretedSortConstructor()); } TEST_F(TestApiBlackSort, getDatatype) @@ -319,7 +323,7 @@ TEST_F(TestApiBlackSort, instantiate) ASSERT_THROW(dtypeSort.instantiate({d_solver.getIntegerSort()}), CVC5ApiException); // instantiate uninterpreted sort constructor - Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 1); + Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort(1, "s"); ASSERT_NO_THROW(sortConsSort.instantiate({d_solver.getIntegerSort()})); } @@ -331,7 +335,7 @@ TEST_F(TestApiBlackSort, isInstantiated) paramDtypeSort.instantiate({d_solver.getIntegerSort()}); ASSERT_TRUE(instParamDtypeSort.isInstantiated()); - Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 1); + Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort(1, "s"); ASSERT_FALSE(sortConsSort.isInstantiated()); Sort instSortConsSort = sortConsSort.instantiate({d_solver.getIntegerSort()}); ASSERT_TRUE(instSortConsSort.isInstantiated()); @@ -371,7 +375,7 @@ TEST_F(TestApiBlackSort, getInstantiatedParameters) ASSERT_EQ(instSorts[1], boolSort); // uninterpreted sort constructor sort instantiation - Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 4); + Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort(4, "s"); ASSERT_THROW(sortConsSort.getInstantiatedParameters(), CVC5ApiException); Sort instSortConsSort = @@ -393,7 +397,7 @@ TEST_F(TestApiBlackSort, getUninterpretedSortConstructor) Sort realSort = d_solver.getRealSort(); Sort boolSort = d_solver.getBooleanSort(); Sort bvSort = d_solver.mkBitVectorSort(8); - Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 4); + Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort(4, "s"); ASSERT_THROW(sortConsSort.getUninterpretedSortConstructor(), CVC5ApiException); Sort instSortConsSort = @@ -403,7 +407,7 @@ TEST_F(TestApiBlackSort, getUninterpretedSortConstructor) TEST_F(TestApiBlackSort, getFunctionArity) { - Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort(), d_solver.getIntegerSort()); ASSERT_NO_THROW(funSort.getFunctionArity()); Sort bvSort = d_solver.mkBitVectorSort(32); @@ -486,7 +490,7 @@ TEST_F(TestApiBlackSort, getSymbol) TEST_F(TestApiBlackSort, getUninterpretedSortConstructorName) { - Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2); + Sort sSort = d_solver.mkUninterpretedSortConstructorSort(2, "s"); ASSERT_NO_THROW(sSort.getSymbol()); Sort bvSort = d_solver.mkBitVectorSort(32); ASSERT_THROW(bvSort.getSymbol(), CVC5ApiException); @@ -494,7 +498,7 @@ TEST_F(TestApiBlackSort, getUninterpretedSortConstructorName) TEST_F(TestApiBlackSort, getUninterpretedSortConstructorArity) { - Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2); + Sort sSort = d_solver.mkUninterpretedSortConstructorSort(2, "s"); ASSERT_NO_THROW(sSort.getUninterpretedSortConstructorArity()); Sort bvSort = d_solver.mkBitVectorSort(32); ASSERT_THROW(bvSort.getUninterpretedSortConstructorArity(), CVC5ApiException); diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java index 4d0074b75..93e38fa99 100644 --- a/test/unit/api/java/DatatypeTest.java +++ b/test/unit/api/java/DatatypeTest.java @@ -473,7 +473,7 @@ class DatatypeTest * END; */ unresTypes.clear(); - Sort unresList5 = d_solver.mkUninterpretedSortConstructorSort("list5", 1); + Sort unresList5 = d_solver.mkUninterpretedSortConstructorSort(1, "list5"); unresTypes.add(unresList5); List v = new ArrayList<>(); @@ -514,7 +514,7 @@ class DatatypeTest */ // Make unresolved types as placeholders Set unresTypes = new HashSet<>(); - Sort unresList = d_solver.mkUninterpretedSortConstructorSort("plist", 1); + Sort unresList = d_solver.mkUninterpretedSortConstructorSort(1, "plist"); unresTypes.add(unresList); List v = new ArrayList<>(); diff --git a/test/unit/api/java/ResultTest.java b/test/unit/api/java/ResultTest.java index 9a2b1af32..cca0c4244 100644 --- a/test/unit/api/java/ResultTest.java +++ b/test/unit/api/java/ResultTest.java @@ -56,7 +56,7 @@ class ResultTest @Test void eq() { - Sort u_sort = d_solver.mkUninterpretedSort("u"); + Sort u_sort = d_solver.mkUninterpretedSort(); Term x = d_solver.mkConst(u_sort, "x"); d_solver.assertFormula(x.eqTerm(x)); Result res; @@ -81,7 +81,7 @@ class ResultTest @Test void isUnsat() { - Sort u_sort = d_solver.mkUninterpretedSort("u"); + Sort u_sort = d_solver.mkUninterpretedSort(); Term x = d_solver.mkConst(u_sort, "x"); d_solver.assertFormula(x.eqTerm(x).notTerm()); Result res = d_solver.checkSat(); diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index f5ca65c9f..7942b75f4 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -370,9 +370,9 @@ class SolverTest @Test void mkUninterpretedSortConstructorSort() throws CVC5ApiException { - assertDoesNotThrow(() -> d_solver.mkUninterpretedSortConstructorSort("s", 2)); - assertDoesNotThrow(() -> d_solver.mkUninterpretedSortConstructorSort("", 2)); - assertThrows(CVC5ApiException.class, () -> d_solver.mkUninterpretedSortConstructorSort("", 0)); + assertDoesNotThrow(() -> d_solver.mkUninterpretedSortConstructorSort(2, "s")); + assertDoesNotThrow(() -> d_solver.mkUninterpretedSortConstructorSort(2)); + assertThrows(CVC5ApiException.class, () -> d_solver.mkUninterpretedSortConstructorSort(0)); } @Test diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java index 3884dc35b..bc3376ab7 100644 --- a/test/unit/api/java/SortTest.java +++ b/test/unit/api/java/SortTest.java @@ -266,7 +266,7 @@ class SortTest @Test void isUninterpretedSortSortConstructor() throws CVC5ApiException { - Sort sc_sort = d_solver.mkUninterpretedSortConstructorSort("asdf", 1); + Sort sc_sort = d_solver.mkUninterpretedSortConstructorSort(1, "asdf"); assertTrue(sc_sort.isUninterpretedSortConstructor()); assertDoesNotThrow(() -> d_solver.getNullSort().isUninterpretedSortConstructor()); } @@ -341,7 +341,7 @@ class SortTest assertThrows(CVC5ApiException.class, () -> dtypeSort.instantiate(new Sort[] {d_solver.getIntegerSort()})); // instantiate uninterpreted sort constructor - Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 1); + Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort(1, "s"); assertDoesNotThrow(() -> sortConsSort.instantiate(new Sort[] {d_solver.getIntegerSort()})); } @@ -353,7 +353,7 @@ class SortTest Sort instParamDtypeSort = paramDtypeSort.instantiate(new Sort[] {d_solver.getIntegerSort()}); assertTrue(instParamDtypeSort.isInstantiated()); - Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 1); + Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort(1, "s"); assertFalse(sortConsSort.isInstantiated()); Sort instSortConsSort = sortConsSort.instantiate(new Sort[] {d_solver.getIntegerSort()}); assertTrue(instSortConsSort.isInstantiated()); @@ -394,7 +394,7 @@ class SortTest assertEquals(instSorts[1], boolSort); // uninterpreted sort constructor sort instantiation - Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 4); + Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort(4, "s"); assertThrows(CVC5ApiException.class, () -> sortConsSort.getInstantiatedParameters()); Sort instSortConsSort = @@ -417,7 +417,7 @@ class SortTest Sort realSort = d_solver.getRealSort(); Sort boolSort = d_solver.getBooleanSort(); Sort bvSort = d_solver.mkBitVectorSort(8); - Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 4); + Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort(4); assertThrows(CVC5ApiException.class, () -> sortConsSort.getUninterpretedSortConstructor()); Sort instSortConsSort = sortConsSort.instantiate(new Sort[] {boolSort, intSort, bvSort, realSort}); @@ -519,7 +519,7 @@ class SortTest @Test void getUninterpretedSortConstructorName() throws CVC5ApiException { - Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2); + Sort sSort = d_solver.mkUninterpretedSortConstructorSort(2); assertDoesNotThrow(() -> sSort.getSymbol()); Sort bvSort = d_solver.mkBitVectorSort(32); assertThrows(CVC5ApiException.class, () -> bvSort.getSymbol()); @@ -528,7 +528,7 @@ class SortTest @Test void getUninterpretedSortConstructorArity() throws CVC5ApiException { - Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2); + Sort sSort = d_solver.mkUninterpretedSortConstructorSort(2, "s"); assertDoesNotThrow(() -> sSort.getUninterpretedSortConstructorArity()); Sort bvSort = d_solver.mkBitVectorSort(32); assertThrows(CVC5ApiException.class, () -> bvSort.getUninterpretedSortConstructorArity()); diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py index 5b2ac50b5..483243a9f 100644 --- a/test/unit/api/python/test_datatype_api.py +++ b/test/unit/api/python/test_datatype_api.py @@ -466,7 +466,7 @@ def test_datatype_simply_rec(solver): # list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil # END unresTypes.clear() - unresList5 = solver.mkUninterpretedSortConstructorSort("list5", 1) + unresList5 = solver.mkUninterpretedSortConstructorSort(1, "list5") unresTypes.add(unresList5) v = [] @@ -503,7 +503,7 @@ def test_datatype_specialized_cons(solver): # Make unresolved types as placeholders unresTypes = set([]) - unresList = solver.mkUninterpretedSortConstructorSort("plist", 1) + unresList = solver.mkUninterpretedSortConstructorSort(1, "plist") unresTypes.add(unresList) v = [] diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index f07aa8e74..5960c6cfe 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -300,10 +300,10 @@ def test_mk_unresolved_sort(solver): def test_mk_sort_constructor_sort(solver): - solver.mkUninterpretedSortConstructorSort("s", 2) - solver.mkUninterpretedSortConstructorSort("", 2) + solver.mkUninterpretedSortConstructorSort(2, "s") + solver.mkUninterpretedSortConstructorSort(2) with pytest.raises(RuntimeError): - solver.mkUninterpretedSortConstructorSort("", 0) + solver.mkUninterpretedSortConstructorSort(0) def test_mk_tuple_sort(solver): diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py index 941e948bb..3f2ecf444 100644 --- a/test/unit/api/python/test_sort.py +++ b/test/unit/api/python/test_sort.py @@ -222,7 +222,7 @@ def test_is_uninterpreted(solver): def test_is_sort_constructor(solver): - sc_sort = solver.mkUninterpretedSortConstructorSort("asdf", 1) + sc_sort = solver.mkUninterpretedSortConstructorSort(1, "asdf") assert sc_sort.isUninterpretedSortConstructor() Sort(solver).isUninterpretedSortConstructor() @@ -300,7 +300,7 @@ def test_instantiate(solver): with pytest.raises(RuntimeError): dtypeSort.instantiate([solver.getIntegerSort()]) # instantiate uninterpreted sort constructor - sortConsSort = solver.mkUninterpretedSortConstructorSort("s", 1) + sortConsSort = solver.mkUninterpretedSortConstructorSort(1, "s") sortConsSort.instantiate([solver.getIntegerSort()]) def test_is_instantiated(solver): @@ -309,7 +309,7 @@ def test_is_instantiated(solver): instParamDtypeSort = paramDtypeSort.instantiate([solver.getIntegerSort()]); assert instParamDtypeSort.isInstantiated() - sortConsSort = solver.mkUninterpretedSortConstructorSort("s", 1) + sortConsSort = solver.mkUninterpretedSortConstructorSort(1, "s") assert not sortConsSort.isInstantiated() instSortConsSort = sortConsSort.instantiate([solver.getIntegerSort()]) assert instSortConsSort.isInstantiated() @@ -348,7 +348,7 @@ def test_get_instantiated_parameters(solver): assert instSorts[1] == boolSort # uninterpreted sort constructor sort instantiation - sortConsSort = solver.mkUninterpretedSortConstructorSort("s", 4) + sortConsSort = solver.mkUninterpretedSortConstructorSort(4, "s") with pytest.raises(RuntimeError): sortConsSort.getInstantiatedParameters() @@ -371,7 +371,7 @@ def test_get_uninterpreted_sort_constructor(solver): realSort = solver.getRealSort() boolSort = solver.getBooleanSort() bvSort = solver.mkBitVectorSort(8) - sortConsSort = solver.mkUninterpretedSortConstructorSort("s", 4) + sortConsSort = solver.mkUninterpretedSortConstructorSort(4, "s") with pytest.raises(RuntimeError): sortConsSort.getUninterpretedSortConstructor() instSortConsSort = \ @@ -462,7 +462,7 @@ def test_get_uninterpreted_sort_name(solver): def test_get_uninterpreted_sort_constructor_name(solver): - sSort = solver.mkUninterpretedSortConstructorSort("s", 2) + sSort = solver.mkUninterpretedSortConstructorSort(2, "s") sSort.getSymbol() bvSort = solver.mkBitVectorSort(32) with pytest.raises(RuntimeError): @@ -470,7 +470,7 @@ def test_get_uninterpreted_sort_constructor_name(solver): def test_get_uninterpreted_sort_constructor_arity(solver): - sSort = solver.mkUninterpretedSortConstructorSort("s", 2) + sSort = solver.mkUninterpretedSortConstructorSort(2, "s") sSort.getUninterpretedSortConstructorArity() bvSort = solver.mkBitVectorSort(32) with pytest.raises(RuntimeError): -- 2.30.2