api: Rename *SortConstructor* to *UninterpretedSortConstructor*. (#8406)

diff --git a/docs/api/java/CMakeLists.txt b/docs/api/java/CMakeLists.txt
index 974f15e0fe6a719c264d899e77e51051d0a33fa1..2fcf74767ac4ccebbcb9426312e4a836a31389cd 100644 (file)
--- a/docs/api/java/CMakeLists.txt
+++ b/docs/api/java/CMakeLists.txt
@@ -33,7 +33,6 @@ if(BUILD_BINDINGS_JAVA)
       -cp ${CVC5_JAR_FILE}
       -tag "apiNote:a:Note:"
       -notimestamp
-      --no-module-directories
     COMMAND find ${JAVADOC_OUTPUT_DIR} -type f -exec sed -i'orig' 's/<!-- Generated by javadoc [^>]* -->//' {} "\;"
     COMMAND find ${SPHINX_GH_OUTPUT_DIR} -name '*orig' -delete
     DEPENDS cvc5jar ${CVC5_JAR_FILE}

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 7c39e991cb4ce15d1a5bdadea2f95c7e71ea05dc..b739201821b1df5dc922f87f1cc413cfcb2e2b38 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -1365,7 +1365,7 @@ bool Sort::isUninterpretedSort() const
   CVC5_API_TRY_CATCH_END;
 }
 
-bool Sort::isSortConstructor() const
+bool Sort::isUninterpretedSortConstructor() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
@@ -1395,7 +1395,7 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
   CVC5_API_CHECK(!d_type->isParametricDatatype()
                  || d_type->getNumChildren() == params.size() + 1)
       << "Arity mismatch for instantiated parametric datatype";
-  CVC5_API_CHECK(!isSortConstructor()
+  CVC5_API_CHECK(!d_type->isSortConstructor()
                  || d_type->getSortConstructorArity() == params.size())
       << "Arity mismatch for instantiated sort constructor";
   //////// all checks before this line
@@ -1674,11 +1674,11 @@ std::vector<Sort> Sort::getUninterpretedSortParamSorts() const
 
 /* Sort constructor sort ----------------------------------------------- */
 
-size_t Sort::getSortConstructorArity() const
+size_t Sort::getUninterpretedSortConstructorArity() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
+  CVC5_API_CHECK(d_type->isSortConstructor()) << "Not a sort constructor sort.";
   //////// all checks before this line
   return d_type->getSortConstructorArity();
   ////////
@@ -5600,8 +5600,8 @@ Sort Solver::mkUnresolvedSort(const std::string& symbol, size_t arity) const
   CVC5_API_TRY_CATCH_END;
 }
 
-Sort Solver::mkSortConstructorSort(const std::string& symbol,
-                                   size_t arity) const
+Sort Solver::mkUninterpretedSortConstructorSort(const std::string& symbol,
+                                                size_t arity) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_ARG_CHECK_EXPECTED(arity > 0, arity) << "an arity > 0";

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index f2156f13bf337763f0c5e319fe601b0bc9639716..e2f3d943a9869803dc3960e3ae10e79028cf7ba5 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -584,10 +584,14 @@ class CVC5_EXPORT Sort
   bool isUninterpretedSort() const;
 
   /**
-   * Is this a sort constructor kind?
+   * Is this an uninterpreted sort constructor kind?
+   *
+   * An uninterpreted sort constructor has arity > 0 and can be instantiated to
+   * construct uninterpreted sorts with given sort parameters.
+   *
    * @return true if this is a sort constructor kind
    */
-  bool isSortConstructor() const;
+  bool isUninterpretedSortConstructor() const;
 
   /**
    * @return the underlying datatype of a datatype sort
@@ -595,8 +599,11 @@ class CVC5_EXPORT Sort
   Datatype getDatatype() const;
 
   /**
-   * Instantiate a parameterized datatype/sort sort.
+   * Instantiate a parameterized datatype sort or uninterpreted sort
+   * constructor sort.
+   *
    * Create sorts parameter with Solver::mkParamSort().
+   *
    * @param params the list of sort parameters to instantiate with
    */
   Sort instantiate(const std::vector<Sort>& params) const;
@@ -753,9 +760,9 @@ class CVC5_EXPORT Sort
   /* Sort constructor sort ----------------------------------------------- */
 
   /**
-   * @return the arity of a sort constructor sort
+   * @return the arity of an uninterpreted sort constructor sort
    */
-  size_t getSortConstructorArity() const;
+  size_t getUninterpretedSortConstructorArity() const;
 
   /* Bit-vector sort ----------------------------------------------------- */
 
@@ -3282,12 +3289,16 @@ class CVC5_EXPORT Solver
   Sort mkUnresolvedSort(const std::string& symbol, size_t arity = 0) const;
 
   /**
-   * Create a sort constructor sort.
+   * Create an uninterpreted sort constructor sort.
+   *
+   * An uninterpreted sort constructor is an uninterpreted sort with arity > 0.
+   *
    * @param symbol the symbol of the sort
-   * @param arity the arity of the sort
-   * @return the sort constructor sort
+   * @param arity the arity of the sort (must be > 0)
+   * @return the uninterpreted sort constructor sort
    */
-  Sort mkSortConstructorSort(const std::string& symbol, size_t arity) const;
+  Sort mkUninterpretedSortConstructorSort(const std::string& symbol,
+                                          size_t arity) const;
 
   /**
    * Create a tuple sort.
@@ -3820,6 +3831,11 @@ class CVC5_EXPORT Solver
    *     (declare-sort <symbol> <numeral>)
    * \endverbatim
    *
+   * @note This corresponds to mkUninterpretedSort(const std::string&) const if
+   *       arity = 0, and to
+   *       mkUninterpretedSortConstructorSort(const std::string&, size_t arity) const
+   *       if arity > 0.
+   *
    * @param symbol the name of the sort
    * @param arity the arity of the sort
    * @return the sort

diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index 01fe033b41426aee825c0606042c4975d96fc54f..5b462bc2f18c64da83691d8cf68e5643590e6ba3 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -464,19 +464,23 @@ public class Solver implements IPointer, AutoCloseable
 
   /**
    * Create a sort constructor sort.
+   *
+   * An uninterpreted sort constructor is an uninterpreted sort with
+   * arity > 0.
+   *
    * @param symbol the symbol of the sort
-   * @param arity the arity of the sort
+   * @param arity the arity of the sort (must be > 0)
    * @return the sort constructor sort
    * @throws CVC5ApiException
    */
-  public Sort mkSortConstructorSort(String symbol, int arity) throws CVC5ApiException
+  public Sort mkUninterpretedSortConstructorSort(String symbol, int arity) throws CVC5ApiException
   {
     Utils.validateUnsigned(arity, "arity");
-    long sortPointer = mkSortConstructorSort(pointer, symbol, arity);
+    long sortPointer = mkUninterpretedSortConstructorSort(pointer, symbol, arity);
     return new Sort(this, sortPointer);
   }
 
-  private native long mkSortConstructorSort(long pointer, String symbol, int arity);
+  private native long mkUninterpretedSortConstructorSort(long pointer, String symbol, int arity);
 
   /**
    * Create a tuple sort.
@@ -1555,6 +1559,8 @@ public class Solver implements IPointer, AutoCloseable
    * {@code
    *   ( declare-sort <symbol> <numeral> )
    * }
+   * @apiNote This corresponds to mkUninterpretedSort() const if arity = 0, and
+   *          to mkUninterpretedSortConstructorSort() const if arity &gt; 0.
    * @param symbol the name of the sort
    * @param arity the arity of the sort
    * @return the sort

diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java
index e600fbaeb49a74c177be8409a6caffd6a229b86b..bf85107f66131068a9f16718ebb2bd03acee8270 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Sort.java
+++ b/src/api/java/io/github/cvc5/api/Sort.java
@@ -345,15 +345,19 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
   private native boolean isUninterpretedSort(long pointer);
 
   /**
-   * Is this a sort constructor kind?
+   * Is this an uninterpreted sort constructor kind?
+   *
+   * An uninterpreted sort constructor is an uninterpreted sort with arity
+   * &gt; 0.
+   *
    * @return true if this is a sort constructor kind
    */
-  public boolean isSortConstructor()
+  public boolean isUninterpretedSortConstructor()
   {
-    return isSortConstructor(pointer);
+    return isUninterpretedSortConstructor(pointer);
   }
 
-  private native boolean isSortConstructor(long pointer);
+  private native boolean isUninterpretedSortConstructor(long pointer);
 
   /**
    * @return the underlying datatype of a datatype sort
@@ -367,7 +371,8 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
   private native long getDatatype(long pointer);
 
   /**
-   * Instantiate a parameterized datatype/sort sort.
+   * Instantiate a parameterized datatype sort or uninterpreted sort
+   * constructor sort.
    * Create sorts parameter with Solver.mkParamSort().
    * @param params the list of sort parameters to instantiate with
    */
@@ -647,14 +652,14 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
   /* Sort constructor sort ----------------------------------------------- */
 
   /**
-   * @return the arity of a sort constructor sort
+   * @return the arity of an uninterpreted sort constructor sort
    */
-  public int getSortConstructorArity()
+  public int getUninterpretedSortConstructorArity()
   {
-    return getSortConstructorArity(pointer);
+    return getUninterpretedSortConstructorArity(pointer);
   }
 
-  private native int getSortConstructorArity(long pointer);
+  private native int getUninterpretedSortConstructorArity(long pointer);
 
   /* Bit-vector sort ----------------------------------------------------- */
 

diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index 718d63da8cccffa222a8ae47d225abae9dbb3df0..7eccbf2606fe9d2e18215317fb2650e2bae038fc 100644 (file)
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -482,10 +482,11 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkUnresolvedSort(
 
 /*
  * Class:     io_github_cvc5_api_Solver
- * Method:    mkSortConstructorSort
+ * Method:    mkUninterpretedSortConstructorSort
  * Signature: (JLjava/lang/String;I)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkSortConstructorSort(
+JNIEXPORT jlong JNICALL
+Java_io_github_cvc5_api_Solver_mkUninterpretedSortConstructorSort(
     JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jint arity)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
@@ -493,8 +494,8 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkSortConstructorSort(
   Solver* solver = reinterpret_cast<Solver*>(pointer);
   const char* s = env->GetStringUTFChars(jSymbol, nullptr);
   std::string cSymbol(s);
-  Sort* retPointer =
-      new Sort(solver->mkSortConstructorSort(cSymbol, (size_t)arity));
+  Sort* retPointer = new Sort(
+      solver->mkUninterpretedSortConstructorSort(cSymbol, (size_t)arity));
   env->ReleaseStringUTFChars(jSymbol, s);
   return reinterpret_cast<jlong>(retPointer);
 

diff --git a/src/api/java/jni/sort.cpp b/src/api/java/jni/sort.cpp
index 12ce60ae069aa8c83a053098ce2f5bcadcea26c5..a3d1f135f7ba00b4aff4a67e2dd45dd36df2904f 100644 (file)
--- a/src/api/java/jni/sort.cpp
+++ b/src/api/java/jni/sort.cpp
@@ -440,15 +440,17 @@ JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isUninterpretedSort(
 
 /*
  * Class:     io_github_cvc5_api_Sort
- * Method:    isSortConstructor
+ * Method:    isUninterpretedSortConstructor
  * Signature: (J)Z
  */
-JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isSortConstructor(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jboolean JNICALL
+Java_io_github_cvc5_api_Sort_isUninterpretedSortConstructor(JNIEnv* env,
+                                                            jobject,
+                                                            jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Sort* current = reinterpret_cast<Sort*>(pointer);
-  return static_cast<jboolean>(current->isSortConstructor());
+  return static_cast<jboolean>(current->isUninterpretedSortConstructor());
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 }
 
@@ -866,15 +868,17 @@ Java_io_github_cvc5_api_Sort_getUninterpretedSortParamSorts(JNIEnv* env,
 
 /*
  * Class:     io_github_cvc5_api_Sort
- * Method:    getSortConstructorArity
+ * Method:    getUninterpretedSortConstructorArity
  * Signature: (J)I
  */
-JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Sort_getSortConstructorArity(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jint JNICALL
+Java_io_github_cvc5_api_Sort_getUninterpretedSortConstructorArity(JNIEnv* env,
+                                                                  jobject,
+                                                                  jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Sort* current = reinterpret_cast<Sort*>(pointer);
-  return static_cast<jint>(current->getSortConstructorArity());
+  return static_cast<jint>(current->getUninterpretedSortConstructorArity());
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 4f482da9ed458656e91c9c0da1c7627babfa0cc7..b5cbdf7cc5e82302c2cb46750b6c0f5c141bdbbf 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -234,7 +234,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Sort mkSequenceSort(Sort elemSort) except +
         Sort mkUninterpretedSort(const string& symbol) except +
         Sort mkUnresolvedSort(const string& symbol, size_t arity) except +
-        Sort mkSortConstructorSort(const string& symbol, size_t arity) except +
+        Sort mkUninterpretedSortConstructorSort(const string& symbol, size_t arity) except +
         Sort mkTupleSort(const vector[Sort]& sorts) except +
         Term mkTerm(Op op) except +
         Term mkTerm(Op op, const vector[Term]& children) except +
@@ -398,7 +398,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint isBag() except +
         bint isSequence() except +
         bint isUninterpretedSort() except +
-        bint isSortConstructor() except +
+        bint isUninterpretedSortConstructor() except +
         Datatype getDatatype() except +
         Sort instantiate(const vector[Sort]& params) except +
         Sort substitute(const vector[Sort] & es, const vector[Sort] & reps) except +
@@ -419,7 +419,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Sort getSequenceElementSort() except +
         bint isUninterpretedSortParameterized() except +
         vector[Sort] getUninterpretedSortParamSorts() except +
-        size_t getSortConstructorArity() except +
+        size_t getUninterpretedSortConstructorArity() except +
         uint32_t getBitVectorSize() except +
         uint32_t getFloatingPointExponentSize() except +
         uint32_t getFloatingPointSignificandSize() except +

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 18e6a1e79d3706cc232322cf40b34647c56ecc35..09749b3d532f13d83d938ac925cf6308cb0380b3 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -988,15 +988,19 @@ cdef class Solver:
         sort.csort = self.csolver.mkUnresolvedSort(name.encode(), arity)
         return sort
 
-    def mkSortConstructorSort(self, str symbol, size_t arity):
+    def mkUninterpretedSortConstructorSort(self, str symbol, size_t arity):
         """Create a sort constructor sort.
 
+        An uninterpreted sort constructor is an uninterpreted sort with
+        arity > 0.
+
         :param symbol: the symbol of the sort
-        :param arity: the arity of the sort
+        :param arity: the arity of the sort (must be > 0)
         :return: the sort constructor sort
         """
         cdef Sort sort = Sort(self)
-        sort.csort =self.csolver.mkSortConstructorSort(symbol.encode(), arity)
+        sort.csort = self.csolver.mkUninterpretedSortConstructorSort(
+            symbol.encode(), arity)
         return sort
 
     @expand_list_arg(num_req_args=0)
@@ -1830,6 +1834,11 @@ cdef class Solver:
 
             ( declare-sort <symbol> <numeral> )
 
+        .. note::
+          This corresponds to :py:meth:`Solver.mkUninterpretedSort()` if
+          arity = 0, and to
+          :py:meth:`Solver.mkUninterpretedSortConstructorSort()` if arity > 0.
+
         :param symbol: the name of the sort
         :param arity: the arity of the sort
         :return: the sort
@@ -2749,13 +2758,16 @@ cdef class Sort:
         """
         return self.csort.isUninterpretedSort()
 
-    def isSortConstructor(self):
+    def isUninterpretedSortConstructor(self):
         """
             Is this a sort constructor kind?
 
+            An uninterpreted sort constructor is an uninterpreted sort with
+            arity > 0.
+
             :return: True if this a sort constructor kind.
         """
-        return self.csort.isSortConstructor()
+        return self.csort.isUninterpretedSortConstructor()
 
     def getDatatype(self):
         """
@@ -2767,7 +2779,8 @@ cdef class Sort:
 
     def instantiate(self, params):
         """
-            Instantiate a parameterized datatype/sort sort.
+            Instantiate a parameterized datatype sort or uninterpreted sort
+            constructor sort.
             Create sorts parameter with :py:meth:`Solver.mkParamSort()`
 
             :param params: the list of sort parameters to instantiate with
@@ -2965,11 +2978,11 @@ cdef class Sort:
             param_sorts.append(sort)
         return param_sorts
 
-    def getSortConstructorArity(self):
+    def getUninterpretedSortConstructorArity(self):
         """
             :return: the arity of a sort constructor sort
         """
-        return self.csort.getSortConstructorArity()
+        return self.csort.getUninterpretedSortConstructorArity()
 
     def getBitVectorSize(self):
         """

diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 7aabb20557466f8e04907f9aa96aefa731fd978c..1b0e679ca7d160fff5275eca36db7b0ffd9fd979 100644 (file)
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -490,7 +490,7 @@ api::Sort SymbolTable::Implementation::lookupType(
                         "expected parametric datatype");
     return p.second.instantiate(params);
   }
-  bool isSortConstructor = p.second.isSortConstructor();
+  bool isSortConstructor = p.second.isUninterpretedSortConstructor();
   if (TraceIsOn("sort"))
   {
     Trace("sort") << "instantiating using a sort "

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 9c38772654475e6b9c99df609858f37014773a43..a7bf82fb77dc6822472a4797dc632557e885035f 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -317,7 +317,7 @@ api::Sort Parser::mkSortConstructor(const std::string& name, size_t arity)
 {
   Trace("parser") << "newSortConstructor(" << name << ", " << arity << ")"
                   << std::endl;
-  api::Sort type = d_solver->mkSortConstructorSort(name, arity);
+  api::Sort type = d_solver->mkUninterpretedSortConstructorSort(name, arity);
   defineType(name, vector<api::Sort>(arity), type);
   return type;
 }
@@ -333,7 +333,8 @@ api::Sort Parser::mkUnresolvedType(const std::string& name)
 api::Sort Parser::mkUnresolvedTypeConstructor(const std::string& name,
                                               size_t arity)
 {
-  api::Sort unresolved = d_solver->mkSortConstructorSort(name, arity);
+  api::Sort unresolved =
+      d_solver->mkUninterpretedSortConstructorSort(name, arity);
   defineType(name, vector<api::Sort>(arity), unresolved);
   d_unresolved.insert(unresolved);
   return unresolved;
@@ -344,7 +345,8 @@ api::Sort Parser::mkUnresolvedTypeConstructor(
 {
   Trace("parser") << "newSortConstructor(P)(" << name << ", " << params.size()
                   << ")" << std::endl;
-  api::Sort unresolved = d_solver->mkSortConstructorSort(name, params.size());
+  api::Sort unresolved =
+      d_solver->mkUninterpretedSortConstructorSort(name, params.size());
   defineType(name, params, unresolved);
   api::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 c783f2fa29422157795ffb31fe3248b8a53a1c14..79956f67962c60d9cef685c1ee3dc3b8697f7358 100644 (file)
--- a/test/unit/api/cpp/datatype_api_black.cpp
+++ b/test/unit/api/cpp/datatype_api_black.cpp
@@ -483,7 +483,7 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec)
    *   END;
    */
   unresTypes.clear();
-  Sort unresList5 = d_solver.mkSortConstructorSort("list5", 1);
+  Sort unresList5 = d_solver.mkUninterpretedSortConstructorSort("list5", 1);
   unresTypes.insert(unresList5);
 
   std::vector<Sort> v;
@@ -522,7 +522,7 @@ TEST_F(TestApiBlackDatatype, datatypeSpecializedCons)
    */
   // Make unresolved types as placeholders
   std::set<Sort> unresTypes;
-  Sort unresList = d_solver.mkSortConstructorSort("plist", 1);
+  Sort unresList = d_solver.mkUninterpretedSortConstructorSort("plist", 1);
   unresTypes.insert(unresList);
 
   std::vector<Sort> v;

diff --git a/test/unit/api/cpp/parametric_datatype_black.cpp b/test/unit/api/cpp/parametric_datatype_black.cpp
index 6c4bb80e94b173126522df36811d268ebbc57d8a..219f007ec494eaecb604c28ea606f38f0ce058e9 100644 (file)
--- a/test/unit/api/cpp/parametric_datatype_black.cpp
+++ b/test/unit/api/cpp/parametric_datatype_black.cpp
@@ -30,8 +30,8 @@ TEST_F(TestApiBlackParametricDatatype, proj_issue387)
 {
   Sort s1 = d_solver.getBooleanSort();
 
-  Sort u1 = d_solver.mkSortConstructorSort("_x0", 1);
-  Sort u2 = d_solver.mkSortConstructorSort("_x1", 1);
+  Sort u1 = d_solver.mkUninterpretedSortConstructorSort("_x0", 1);
+  Sort u2 = d_solver.mkUninterpretedSortConstructorSort("_x1", 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 e32f4a8e971c4152dce394186ff8f720a061f42a..717865c71f877e8d8fe84c943841778611c2156f 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -361,11 +361,12 @@ TEST_F(TestApiBlackSolver, mkUnresolvedSort)
   ASSERT_NO_THROW(d_solver.mkUnresolvedSort("", 1));
 }
 
-TEST_F(TestApiBlackSolver, mkSortConstructorSort)
+TEST_F(TestApiBlackSolver, mkUninterpretedSortConstructorSort)
 {
-  ASSERT_NO_THROW(d_solver.mkSortConstructorSort("s", 2));
-  ASSERT_NO_THROW(d_solver.mkSortConstructorSort("", 2));
-  ASSERT_THROW(d_solver.mkSortConstructorSort("", 0), CVC5ApiException);
+  ASSERT_NO_THROW(d_solver.mkUninterpretedSortConstructorSort("s", 2));
+  ASSERT_NO_THROW(d_solver.mkUninterpretedSortConstructorSort("", 2));
+  ASSERT_THROW(d_solver.mkUninterpretedSortConstructorSort("", 0),
+               CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkTupleSort)

diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp
index 40e00d996db8662eb578ece0c04e4b8f46583c59..d14d2f4a1ef1df77c8869ec2b592d110bfafe93d 100644 (file)
--- a/test/unit/api/cpp/sort_black.cpp
+++ b/test/unit/api/cpp/sort_black.cpp
@@ -246,11 +246,11 @@ TEST_F(TestApiBlackSort, isUninterpreted)
   ASSERT_NO_THROW(Sort().isUninterpretedSort());
 }
 
-TEST_F(TestApiBlackSort, isSortConstructor)
+TEST_F(TestApiBlackSort, isUninterpretedSortConstructor)
 {
-  Sort sc_sort = d_solver.mkSortConstructorSort("asdf", 1);
-  ASSERT_TRUE(sc_sort.isSortConstructor());
-  ASSERT_NO_THROW(Sort().isSortConstructor());
+  Sort sc_sort = d_solver.mkUninterpretedSortConstructorSort("asdf", 1);
+  ASSERT_TRUE(sc_sort.isUninterpretedSortConstructor());
+  ASSERT_NO_THROW(Sort().isUninterpretedSortConstructor());
 }
 
 TEST_F(TestApiBlackSort, getDatatype)
@@ -410,7 +410,7 @@ TEST_F(TestApiBlackSort, isUninterpretedSortParameterized)
 {
   Sort uSort = d_solver.mkUninterpretedSort("u");
   ASSERT_FALSE(uSort.isUninterpretedSortParameterized());
-  Sort sSort = d_solver.mkSortConstructorSort("s", 1);
+  Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 1);
   Sort siSort = sSort.instantiate({uSort});
   ASSERT_TRUE(siSort.isUninterpretedSortParameterized());
   Sort bvSort = d_solver.mkBitVectorSort(32);
@@ -421,7 +421,7 @@ TEST_F(TestApiBlackSort, getUninterpretedSortParamSorts)
 {
   Sort uSort = d_solver.mkUninterpretedSort("u");
   ASSERT_NO_THROW(uSort.getUninterpretedSortParamSorts());
-  Sort sSort = d_solver.mkSortConstructorSort("s", 2);
+  Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2);
   Sort siSort = sSort.instantiate({uSort, uSort});
   ASSERT_EQ(siSort.getUninterpretedSortParamSorts().size(), 2);
   Sort bvSort = d_solver.mkBitVectorSort(32);
@@ -430,7 +430,7 @@ TEST_F(TestApiBlackSort, getUninterpretedSortParamSorts)
 
 TEST_F(TestApiBlackSort, getUninterpretedSortConstructorName)
 {
-  Sort sSort = d_solver.mkSortConstructorSort("s", 2);
+  Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2);
   ASSERT_NO_THROW(sSort.getSymbol());
   Sort bvSort = d_solver.mkBitVectorSort(32);
   ASSERT_THROW(bvSort.getSymbol(), CVC5ApiException);
@@ -438,10 +438,10 @@ TEST_F(TestApiBlackSort, getUninterpretedSortConstructorName)
 
 TEST_F(TestApiBlackSort, getUninterpretedSortConstructorArity)
 {
-  Sort sSort = d_solver.mkSortConstructorSort("s", 2);
-  ASSERT_NO_THROW(sSort.getSortConstructorArity());
+  Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2);
+  ASSERT_NO_THROW(sSort.getUninterpretedSortConstructorArity());
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  ASSERT_THROW(bvSort.getSortConstructorArity(), CVC5ApiException);
+  ASSERT_THROW(bvSort.getUninterpretedSortConstructorArity(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getBitVectorSize)

diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java
index 74e4e1cebedb1af8c10c57909241890eafb19bbd..8e05cb16475f143df4e74126b51fd5f9cedba17f 100644 (file)
--- a/test/unit/api/java/DatatypeTest.java
+++ b/test/unit/api/java/DatatypeTest.java
@@ -464,7 +464,7 @@ class DatatypeTest
      *   END;
      */
     unresTypes.clear();
-    Sort unresList5 = d_solver.mkSortConstructorSort("list5", 1);
+    Sort unresList5 = d_solver.mkUninterpretedSortConstructorSort("list5", 1);
     unresTypes.add(unresList5);
 
     List<Sort> v = new ArrayList<>();
@@ -504,7 +504,7 @@ class DatatypeTest
      */
     // Make unresolved types as placeholders
     Set<Sort> unresTypes = new HashSet<>();
-    Sort unresList = d_solver.mkSortConstructorSort("plist", 1);
+    Sort unresList = d_solver.mkUninterpretedSortConstructorSort("plist", 1);
     unresTypes.add(unresList);
 
     List<Sort> v = new ArrayList<>();

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 5c759b9ea7e7217f39d0fdc106e05eda36942331..77cd3b09fe8b3a553b2020a5dd4acb5049807daf 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -342,11 +342,11 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("", 1));
   }
 
-  @Test void mkSortConstructorSort() throws CVC5ApiException
+  @Test void mkUninterpretedSortConstructorSort() throws CVC5ApiException
   {
-    assertDoesNotThrow(() -> d_solver.mkSortConstructorSort("s", 2));
-    assertDoesNotThrow(() -> d_solver.mkSortConstructorSort("", 2));
-    assertThrows(CVC5ApiException.class, () -> d_solver.mkSortConstructorSort("", 0));
+    assertDoesNotThrow(() -> d_solver.mkUninterpretedSortConstructorSort("s", 2));
+    assertDoesNotThrow(() -> d_solver.mkUninterpretedSortConstructorSort("", 2));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkUninterpretedSortConstructorSort("", 0));
   }
 
   @Test void mkTupleSort() throws CVC5ApiException

diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java
index 87016a0e348259487507220368f8be3b40bd8a3a..0455f207ab1d533dfc196ce04ae95e815d9656ab 100644 (file)
--- a/test/unit/api/java/SortTest.java
+++ b/test/unit/api/java/SortTest.java
@@ -238,11 +238,11 @@ class SortTest
     assertDoesNotThrow(() -> d_solver.getNullSort().isUninterpretedSort());
   }
 
-  @Test void isSortConstructor() throws CVC5ApiException
+  @Test void isUninterpretedSortSortConstructor() throws CVC5ApiException
   {
-    Sort sc_sort = d_solver.mkSortConstructorSort("asdf", 1);
-    assertTrue(sc_sort.isSortConstructor());
-    assertDoesNotThrow(() -> d_solver.getNullSort().isSortConstructor());
+    Sort sc_sort = d_solver.mkUninterpretedSortConstructorSort("asdf", 1);
+    assertTrue(sc_sort.isUninterpretedSortConstructor());
+    assertDoesNotThrow(() -> d_solver.getNullSort().isUninterpretedSortConstructor());
   }
 
   @Test void getDatatype() throws CVC5ApiException
@@ -400,7 +400,7 @@ class SortTest
   {
     Sort uSort = d_solver.mkUninterpretedSort("u");
     assertFalse(uSort.isUninterpretedSortParameterized());
-    Sort sSort = d_solver.mkSortConstructorSort("s", 1);
+    Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 1);
     Sort siSort = sSort.instantiate(new Sort[] {uSort});
     assertTrue(siSort.isUninterpretedSortParameterized());
     Sort bvSort = d_solver.mkBitVectorSort(32);
@@ -411,7 +411,7 @@ class SortTest
   {
     Sort uSort = d_solver.mkUninterpretedSort("u");
     assertDoesNotThrow(() -> uSort.getUninterpretedSortParamSorts());
-    Sort sSort = d_solver.mkSortConstructorSort("s", 2);
+    Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2);
     Sort siSort = sSort.instantiate(new Sort[] {uSort, uSort});
     assertEquals(siSort.getUninterpretedSortParamSorts().length, 2);
     Sort bvSort = d_solver.mkBitVectorSort(32);
@@ -420,7 +420,7 @@ class SortTest
 
   @Test void getUninterpretedSortConstructorName() throws CVC5ApiException
   {
-    Sort sSort = d_solver.mkSortConstructorSort("s", 2);
+    Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2);
     assertDoesNotThrow(() -> sSort.getSymbol());
     Sort bvSort = d_solver.mkBitVectorSort(32);
     assertThrows(CVC5ApiException.class, () -> bvSort.getSymbol());
@@ -428,10 +428,10 @@ class SortTest
 
   @Test void getUninterpretedSortConstructorArity() throws CVC5ApiException
   {
-    Sort sSort = d_solver.mkSortConstructorSort("s", 2);
-    assertDoesNotThrow(() -> sSort.getSortConstructorArity());
+    Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2);
+    assertDoesNotThrow(() -> sSort.getUninterpretedSortConstructorArity());
     Sort bvSort = d_solver.mkBitVectorSort(32);
-    assertThrows(CVC5ApiException.class, () -> bvSort.getSortConstructorArity());
+    assertThrows(CVC5ApiException.class, () -> bvSort.getUninterpretedSortConstructorArity());
   }
 
   @Test void getBitVectorSize() throws CVC5ApiException

diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py
index 89b307bf71985dad028a434db910e43e09c67b50..5b2ac50b52957899beb417029e3c64f7b11dd160 100644 (file)
--- 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.mkSortConstructorSort("list5", 1)
+    unresList5 = solver.mkUninterpretedSortConstructorSort("list5", 1)
     unresTypes.add(unresList5)
 
     v = []
@@ -503,7 +503,7 @@ def test_datatype_specialized_cons(solver):
 
     # Make unresolved types as placeholders
     unresTypes = set([])
-    unresList = solver.mkSortConstructorSort("plist", 1)
+    unresList = solver.mkUninterpretedSortConstructorSort("plist", 1)
     unresTypes.add(unresList)
 
     v = []

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index de82dd1a49526e5e2d16a8c7a714154924bf2778..ca38628194d7395e042fc5e013e28364401f5769 100644 (file)
--- 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.mkSortConstructorSort("s", 2)
-    solver.mkSortConstructorSort("", 2)
+    solver.mkUninterpretedSortConstructorSort("s", 2)
+    solver.mkUninterpretedSortConstructorSort("", 2)
     with pytest.raises(RuntimeError):
-        solver.mkSortConstructorSort("", 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 83c60b312dd554f7a701c5bb1290433fe40a7cb5..b530f2c37f914cdba8ae00ec213781cfe175f689 100644 (file)
--- a/test/unit/api/python/test_sort.py
+++ b/test/unit/api/python/test_sort.py
@@ -222,9 +222,9 @@ def test_is_uninterpreted(solver):
 
 
 def test_is_sort_constructor(solver):
-    sc_sort = solver.mkSortConstructorSort("asdf", 1)
-    assert sc_sort.isSortConstructor()
-    Sort(solver).isSortConstructor()
+    sc_sort = solver.mkUninterpretedSortConstructorSort("asdf", 1)
+    assert sc_sort.isUninterpretedSortConstructor()
+    Sort(solver).isUninterpretedSortConstructor()
 
 
 def test_get_datatype(solver):
@@ -387,7 +387,7 @@ def test_get_uninterpreted_sort_name(solver):
 def test_is_uninterpreted_sort_parameterized(solver):
     uSort = solver.mkUninterpretedSort("u")
     assert not uSort.isUninterpretedSortParameterized()
-    sSort = solver.mkSortConstructorSort("s", 1)
+    sSort = solver.mkUninterpretedSortConstructorSort("s", 1)
     siSort = sSort.instantiate([uSort])
     assert siSort.isUninterpretedSortParameterized()
     bvSort = solver.mkBitVectorSort(32)
@@ -398,7 +398,7 @@ def test_is_uninterpreted_sort_parameterized(solver):
 def test_get_uninterpreted_sort_paramsorts(solver):
     uSort = solver.mkUninterpretedSort("u")
     uSort.getUninterpretedSortParamSorts()
-    sSort = solver.mkSortConstructorSort("s", 2)
+    sSort = solver.mkUninterpretedSortConstructorSort("s", 2)
     siSort = sSort.instantiate([uSort, uSort])
     assert len(siSort.getUninterpretedSortParamSorts()) == 2
     bvSort = solver.mkBitVectorSort(32)
@@ -407,7 +407,7 @@ def test_get_uninterpreted_sort_paramsorts(solver):
 
 
 def test_get_uninterpreted_sort_constructor_name(solver):
-    sSort = solver.mkSortConstructorSort("s", 2)
+    sSort = solver.mkUninterpretedSortConstructorSort("s", 2)
     sSort.getSymbol()
     bvSort = solver.mkBitVectorSort(32)
     with pytest.raises(RuntimeError):
@@ -415,11 +415,11 @@ def test_get_uninterpreted_sort_constructor_name(solver):
 
 
 def test_get_uninterpreted_sort_constructor_arity(solver):
-    sSort = solver.mkSortConstructorSort("s", 2)
-    sSort.getSortConstructorArity()
+    sSort = solver.mkUninterpretedSortConstructorSort("s", 2)
+    sSort.getUninterpretedSortConstructorArity()
     bvSort = solver.mkBitVectorSort(32)
     with pytest.raises(RuntimeError):
-        bvSort.getSortConstructorArity()
+        bvSort.getUninterpretedSortConstructorArity()
 
 
 def test_get_bv_size(solver):