api: Use std::optional for symbols in mk* functions. (#8495)

Makes all symbols in mk* functions optional.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 2d10f8e92244169b19f1345ee3aefb602f28d7ae..3cc67a0c7ca891d5dc0a9b3cfe56abb0ca765665 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -5550,13 +5550,17 @@ Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts,
   CVC5_API_TRY_CATCH_END;
 }
 
-Sort Solver::mkParamSort(const std::string& symbol) const
+Sort Solver::mkParamSort(const std::optional<std::string>& 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<std::string>& 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<std::string>& 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<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(*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<std::string>& 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 3c8de6c18c1c2021d7263c97d07fa5ae1a9d54fa..96fe3775f6b9b268683d9efe92a5f0fe9b6e9cd6 100644 (file)
--- 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<std::string>& 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<std::string>& 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<std::string>& 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<std::string>& 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<std::string>& 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 686a16c7200ebaa2e52871aba22f5110f5362255..885ccc359c5a52d31da84d58dc21072fc0ae09d5 100644 (file)
--- 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 ee9f6affbf74b841b85f99fc57c42a9613cdbfd3..b83560e9f302a94297ef943c42f03bd4106fd388 100644 (file)
--- 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<Solver*>(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<Solver*>(pointer);
+  Sort* retPointer = new Sort(solver->mkParamSort());
+  return reinterpret_cast<jlong>(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<Solver*>(pointer);
+  Sort* sort = new Sort(solver->mkUninterpretedSort());
+  return reinterpret_cast<jlong>(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<jlong>(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<Solver*>(pointer);
+  Sort* retPointer =
+      new Sort(solver->mkUninterpretedSortConstructorSort((size_t)arity));
+  return reinterpret_cast<jlong>(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 7c40ce3afb77dabc4c96d040b1056c6557974a10..05e06b6954f179693926d21bc278902481675d39 100644 (file)
--- 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 ce4c994396f6d222859401b0b648aed0dcb93679..a5c3c3f7edd4e62c127dcea40e5c570646fb63c2 100644 (file)
--- 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 72a9182592833ed5bf74e2dbf343e8a2fb7684d2..5dacfc8a8ddbd6c3bdbafcd8203d73f442e271b2 100644 (file)
--- 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<cvc5::Sort>(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<cvc5::Sort>(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 04811d3b4557ab5f4b2c8f97b2a78cd25ea342ef..510eca60ed79d5a52ccc6b05d6ecef8c84dbe1aa 100644 (file)
--- 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<Sort> v;
@@ -520,7 +520,7 @@ TEST_F(TestApiBlackDatatype, datatypeSpecializedCons)
    */
   // Make unresolved types as placeholders
   std::set<Sort> unresTypes;
-  Sort unresList = d_solver.mkUninterpretedSortConstructorSort("plist", 1);
+  Sort unresList = d_solver.mkUninterpretedSortConstructorSort(1, "plist");
   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 4c1c0c833bb99bb47678ae58b1fdf9fcdee66c2f..d7f30cbe18d16e2dcccfb6d9857961d251a066fb 100644 (file)
--- 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 651b432a717d31410620510814ad39df9f1cfef4..c728c72e9ca783b1e9732fc329c285badf34766e 100644 (file)
--- 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 3f02933db0c37ef9b06319adfff4b889bdfcbd90..e388c60fa566e0a9990675bc0a636743644cdf45 100644 (file)
--- 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 4d0074b759a290812b06999a494b14941d1c04b1..93e38fa99c2044c47a0b8e245f40b92ec62520cd 100644 (file)
--- 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<Sort> v = new ArrayList<>();
@@ -514,7 +514,7 @@ class DatatypeTest
      */
     // Make unresolved types as placeholders
     Set<Sort> unresTypes = new HashSet<>();
-    Sort unresList = d_solver.mkUninterpretedSortConstructorSort("plist", 1);
+    Sort unresList = d_solver.mkUninterpretedSortConstructorSort(1, "plist");
     unresTypes.add(unresList);
 
     List<Sort> v = new ArrayList<>();

diff --git a/test/unit/api/java/ResultTest.java b/test/unit/api/java/ResultTest.java
index 9a2b1af328b18910a041f91078691f1c8b1b17c0..cca0c4244cb7ef87ac49151c340c3b97f97605ec 100644 (file)
--- 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 f5ca65c9f58bce87df83301a377801307e411491..7942b75f406501c73c65e1d358bd16369b76066f 100644 (file)
--- 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 3884dc35b990828c4d971504a8231de131493d30..bc3376ab7fb6f1b8d0f0e6d541ce88378a9ff9db 100644 (file)
--- 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 5b2ac50b52957899beb417029e3c64f7b11dd160..483243a9f1e60c65936292d4a229934f10fc263d 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.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 f07aa8e7438f4127152d7f62c83d642bbe8c11e7..5960c6cfe65434fcbffe369dc1cd1b95a0acd44c 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.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 941e948bb003c8deff4b214bb07c0dd9de1e5c00..3f2ecf444f4b4426b44bc65da8d3e6ccaf93d7d9 100644 (file)
--- 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):