[API] Remove redundant version of `mkFunctionSort` (#8503)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 1 Apr 2022 04:50:25 +0000 (21:50 -0700)
committerGitHub <noreply@github.com>
Fri, 1 Apr 2022 04:50:25 +0000 (04:50 +0000)
mkFunctionSort that takes two sorts as arguments is redundant, because
the first argument is equivalent to a vector of size one passed to the
other overload of mkFunctionSort. This commit removes the method from
the C++ API but keeps the existing semantics for the Java and Python
bindings for convenience and consistency with, e.g. mkTerm.

14 files changed:
examples/api/cpp/combination.cpp
examples/simple_vc_quant_cxx.cpp
src/api/cpp/cvc5.cpp
src/api/cpp/cvc5.h
src/api/java/io/github/cvc5/Solver.java
src/api/java/jni/solver.cpp
src/api/python/cvc5.pxd
src/api/python/cvc5.pxi
src/parser/tptp/tptp.cpp
test/unit/api/cpp/solver_black.cpp
test/unit/api/cpp/sort_black.cpp
test/unit/api/cpp/term_black.cpp
test/unit/api/cpp/term_white.cpp
test/unit/parser/parser_black.cpp

index c3af0c423685a9d3fa65303842c6932beac3781e..98a460a8b1c938f3e8749c846881d93a878af9df 100644 (file)
@@ -46,8 +46,8 @@ int main()
   Sort u = slv.mkUninterpretedSort("u");
   Sort integer = slv.getIntegerSort();
   Sort boolean = slv.getBooleanSort();
-  Sort uToInt = slv.mkFunctionSort(u, integer);
-  Sort intPred = slv.mkFunctionSort(integer, boolean);
+  Sort uToInt = slv.mkFunctionSort({u}, integer);
+  Sort intPred = slv.mkFunctionSort({integer}, boolean);
 
   // Variables
   Term x = slv.mkConst(u, "x");
index 2c953b6fbcd06e2faa4f05a8f7b83908cf371483..a0e051070f5dcef71c091dccc96ae41ba3d9f5f4 100644 (file)
@@ -27,7 +27,7 @@ int main() {
 
   Sort integer = slv.getIntegerSort();
   Sort boolean = slv.getBooleanSort();
-  Sort integerPredicate = slv.mkFunctionSort(integer, boolean);
+  Sort integerPredicate = slv.mkFunctionSort({integer}, boolean);
 
   Term p = slv.mkConst(integerPredicate, "P");
   Term x = slv.mkVar(integer, "x");
index 7534eceaabe3b5a62ffa16fc07286bf36520a2e1..b7e44a85061466ef05c05d7987e2ee466a12e713 100644 (file)
@@ -5522,18 +5522,6 @@ std::vector<Sort> Solver::mkDatatypeSorts(
   CVC5_API_TRY_CATCH_END;
 }
 
-Sort Solver::mkFunctionSort(const Sort& domain, const Sort& codomain) const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_SOLVER_CHECK_DOMAIN_SORT(domain);
-  CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(codomain);
-  //////// all checks before this line
-  return Sort(
-      this, getNodeManager()->mkFunctionType(*domain.d_type, *codomain.d_type));
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
 Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts,
                             const Sort& codomain) const
 {
index 2358ee879e82fc8423d427713149594ff1ae8cf7..9f4113fb6471a64ec035f41431b7aac44ec117b2 100644 (file)
@@ -3211,14 +3211,6 @@ class CVC5_EXPORT Solver
       const std::vector<DatatypeDecl>& dtypedecls,
       const std::set<Sort>& unresolvedSorts) const;
 
-  /**
-   * Create function sort.
-   * @param domain the sort of the function argument
-   * @param codomain the sort of the function return value
-   * @return the function sort
-   */
-  Sort mkFunctionSort(const Sort& domain, const Sort& codomain) const;
-
   /**
    * Create function sort.
    * @param sorts the sort of the function arguments
index 384824e5d5a63a22c6933ca798ecc5299d842dff..92d444fe7d222b7cd455a30aaa65f35f15ad6083 100644 (file)
@@ -318,12 +318,9 @@ public class Solver implements IPointer, AutoCloseable
    */
   public Sort mkFunctionSort(Sort domain, Sort codomain)
   {
-    long sortPointer = mkFunctionSort(pointer, domain.getPointer(), codomain.getPointer());
-    return new Sort(this, sortPointer);
+    return mkFunctionSort(new Sort[] {domain}, codomain);
   }
 
-  private native long mkFunctionSort(long pointer, long domainPointer, long codomainPointer);
-
   /**
    * Create function sort.
    * @param sorts the sort of the function arguments
index f21434dd23b3248ce7fe03cdd1863b6573529ba6..41ada6adeaaee77662716129050d84e349aa8542 100644 (file)
@@ -269,38 +269,17 @@ Java_io_github_cvc5_Solver_mkDatatypeSorts__J_3J_3J(JNIEnv* env,
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 }
 
-/*
- * Class:     io_github_cvc5_Solver
- * Method:    mkFunctionSort
- * Signature: (JJJ)J
- */
-JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_Solver_mkFunctionSort__JJJ(JNIEnv* env,
-                                                   jobject,
-                                                   jlong pointer,
-                                                   jlong domainPointer,
-                                                   jlong codomainPointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  Solver* solver = reinterpret_cast<Solver*>(pointer);
-  Sort* domain = reinterpret_cast<Sort*>(domainPointer);
-  Sort* codomain = reinterpret_cast<Sort*>(codomainPointer);
-  Sort* sortPointer = new Sort(solver->mkFunctionSort(*domain, *codomain));
-  return reinterpret_cast<jlong>(sortPointer);
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-}
-
 /*
  * Class:     io_github_cvc5_Solver
  * Method:    mkFunctionSort
  * Signature: (J[JJ)J
  */
 JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_Solver_mkFunctionSort__J_3JJ(JNIEnv* env,
-                                                     jobject,
-                                                     jlong pointer,
-                                                     jlongArray sortPointers,
-                                                     jlong codomainPointer)
+Java_io_github_cvc5_Solver_mkFunctionSort(JNIEnv* env,
+                                          jobject,
+                                          jlong pointer,
+                                          jlongArray sortPointers,
+                                          jlong codomainPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
index 929c03900b72d74c9f069042b1730970fcbda63c..13e5041ca984f636c3f6c58f54f31ef6fb56aede 100644 (file)
@@ -218,7 +218,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
         Sort mkDatatypeSort(DatatypeDecl dtypedecl) except +
         vector[Sort] mkDatatypeSorts(const vector[DatatypeDecl]& dtypedecls,
                                      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 +
index eb0e749bd501b1fb973a826b864e4e4665d373bc..91b949854e7a1b76f778e154e5c4cfb33b0db046 100644 (file)
@@ -819,16 +819,14 @@ cdef class Solver:
         cdef Sort sort = Sort(self)
         # populate a vector with dereferenced c_Sorts
         cdef vector[c_Sort] v
-
         if isinstance(sorts, Sort):
-            sort.csort = self.csolver.mkFunctionSort((<Sort?> sorts).csort,
-                                                     codomain.csort)
-        elif isinstance(sorts, list):
+            v.push_back((<Sort?>sorts).csort)
+        else:
             for s in sorts:
                 v.push_back((<Sort?>s).csort)
 
-            sort.csort = self.csolver.mkFunctionSort(<const vector[c_Sort]&> v,
-                                                      codomain.csort)
+        sort.csort = self.csolver.mkFunctionSort(<const vector[c_Sort]&> v,
+                                                 codomain.csort)
         return sort
 
     def mkParamSort(self, str symbolname = None):
index 79878adfa83d8c1431fd09d2557db4bb143c4f46..3c06d81adc5330c1ae61e75a6f4adc187e2a4438 100644 (file)
@@ -487,11 +487,11 @@ cvc5::Term Tptp::convertRatToUnsorted(cvc5::Term expr)
   if (d_rtu_op.isNull()) {
     cvc5::Sort t;
     // Conversion from rational to unsorted
-    t = d_solver->mkFunctionSort(d_solver->getRealSort(), d_unsorted);
+    t = d_solver->mkFunctionSort({d_solver->getRealSort()}, d_unsorted);
     d_rtu_op = d_solver->mkConst(t, "$$rtu");
     preemptCommand(new DeclareFunctionCommand("$$rtu", d_rtu_op, t));
     // Conversion from unsorted to rational
-    t = d_solver->mkFunctionSort(d_unsorted, d_solver->getRealSort());
+    t = d_solver->mkFunctionSort({d_unsorted}, d_solver->getRealSort());
     d_utr_op = d_solver->mkConst(t, "$$utr");
     preemptCommand(new DeclareFunctionCommand("$$utr", d_utr_op, t));
   }
index 6b8d985c9f3f850c7643297f187a1fc071506f78..69bdf60c1f5752c71eca88677203abe2916cce81 100644 (file)
@@ -237,22 +237,23 @@ TEST_F(TestApiBlackSolver, mkDatatypeSorts)
 
 TEST_F(TestApiBlackSolver, mkFunctionSort)
 {
-  ASSERT_NO_THROW(d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+  ASSERT_NO_THROW(d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
                                           d_solver.getIntegerSort()));
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+  Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
                                          d_solver.getIntegerSort());
   // function arguments are allowed
-  ASSERT_NO_THROW(d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()));
+  ASSERT_NO_THROW(
+      d_solver.mkFunctionSort({funSort}, d_solver.getIntegerSort()));
   // non-first-class arguments are not allowed
   Sort reSort = d_solver.getRegExpSort();
-  ASSERT_THROW(d_solver.mkFunctionSort(reSort, d_solver.getIntegerSort()),
+  ASSERT_THROW(d_solver.mkFunctionSort({reSort}, d_solver.getIntegerSort()),
                CVC5ApiException);
-  ASSERT_THROW(d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort),
+  ASSERT_THROW(d_solver.mkFunctionSort({d_solver.getIntegerSort()}, funSort),
                CVC5ApiException);
   ASSERT_NO_THROW(d_solver.mkFunctionSort(
       {d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()},
       d_solver.getIntegerSort()));
-  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+  Sort funSort2 = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
                                           d_solver.getIntegerSort());
   // function arguments are allowed
   ASSERT_NO_THROW(
@@ -264,10 +265,10 @@ TEST_F(TestApiBlackSolver, mkFunctionSort)
                CVC5ApiException);
 
   Solver slv;
-  ASSERT_THROW(slv.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+  ASSERT_THROW(slv.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
                                   d_solver.getIntegerSort()),
                CVC5ApiException);
-  ASSERT_THROW(slv.mkFunctionSort(slv.mkUninterpretedSort("u"),
+  ASSERT_THROW(slv.mkFunctionSort({slv.mkUninterpretedSort("u")},
                                   d_solver.getIntegerSort()),
                CVC5ApiException);
   std::vector<Sort> sorts1 = {d_solver.getBooleanSort(),
@@ -291,7 +292,7 @@ TEST_F(TestApiBlackSolver, mkPredicateSort)
 {
   ASSERT_NO_THROW(d_solver.mkPredicateSort({d_solver.getIntegerSort()}));
   ASSERT_THROW(d_solver.mkPredicateSort({}), CVC5ApiException);
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+  Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
                                          d_solver.getIntegerSort());
   // functions as arguments are allowed
   ASSERT_NO_THROW(
@@ -370,7 +371,7 @@ TEST_F(TestApiBlackSolver, mkUninterpretedSortConstructorSort)
 TEST_F(TestApiBlackSolver, mkTupleSort)
 {
   ASSERT_NO_THROW(d_solver.mkTupleSort({d_solver.getIntegerSort()}));
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+  Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
                                          d_solver.getIntegerSort());
   ASSERT_THROW(d_solver.mkTupleSort({d_solver.getIntegerSort(), funSort}),
                CVC5ApiException);
@@ -431,7 +432,7 @@ TEST_F(TestApiBlackSolver, mkVar)
 {
   Sort boolSort = d_solver.getBooleanSort();
   Sort intSort = d_solver.getIntegerSort();
-  Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
+  Sort funSort = d_solver.mkFunctionSort({intSort}, boolSort);
   ASSERT_NO_THROW(d_solver.mkVar(boolSort));
   ASSERT_NO_THROW(d_solver.mkVar(funSort));
   ASSERT_NO_THROW(d_solver.mkVar(boolSort, std::string("b")));
@@ -963,7 +964,7 @@ TEST_F(TestApiBlackSolver, mkConst)
 {
   Sort boolSort = d_solver.getBooleanSort();
   Sort intSort = d_solver.getIntegerSort();
-  Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
+  Sort funSort = d_solver.mkFunctionSort({intSort}, boolSort);
   ASSERT_NO_THROW(d_solver.mkConst(boolSort));
   ASSERT_NO_THROW(d_solver.mkConst(funSort));
   ASSERT_NO_THROW(d_solver.mkConst(boolSort, std::string("b")));
@@ -1035,7 +1036,7 @@ TEST_F(TestApiBlackSolver, declareDatatype)
 TEST_F(TestApiBlackSolver, declareFun)
 {
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+  Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
                                          d_solver.getIntegerSort());
   ASSERT_NO_THROW(d_solver.declareFun("f1", {}, bvSort));
   ASSERT_NO_THROW(
@@ -1073,7 +1074,7 @@ TEST_F(TestApiBlackSolver, defineSort)
 TEST_F(TestApiBlackSolver, defineFun)
 {
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+  Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
                                          d_solver.getIntegerSort());
   Term b1 = d_solver.mkVar(bvSort, "b1");
   Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
@@ -1128,7 +1129,7 @@ TEST_F(TestApiBlackSolver, defineFunRec)
 {
   Sort bvSort = d_solver.mkBitVectorSort(32);
   Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
-  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+  Sort funSort2 = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
                                           d_solver.getIntegerSort());
   Term b1 = d_solver.mkVar(bvSort, "b1");
   Term b11 = d_solver.mkVar(bvSort, "b1");
@@ -1191,7 +1192,7 @@ TEST_F(TestApiBlackSolver, defineFunRecWrongLogic)
 TEST_F(TestApiBlackSolver, defineFunRecGlobal)
 {
   Sort bSort = d_solver.getBooleanSort();
-  Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
+  Sort fSort = d_solver.mkFunctionSort({bSort}, bSort);
 
   d_solver.push();
   Term bTrue = d_solver.mkBoolean(true);
@@ -1218,7 +1219,7 @@ TEST_F(TestApiBlackSolver, defineFunsRec)
   Sort uSort = d_solver.mkUninterpretedSort("u");
   Sort bvSort = d_solver.mkBitVectorSort(32);
   Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
-  Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
+  Sort funSort2 = d_solver.mkFunctionSort({uSort}, d_solver.getIntegerSort());
   Term b1 = d_solver.mkVar(bvSort, "b1");
   Term b11 = d_solver.mkVar(bvSort, "b1");
   Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
@@ -1248,7 +1249,7 @@ TEST_F(TestApiBlackSolver, defineFunsRec)
   Sort uSort2 = slv.mkUninterpretedSort("u");
   Sort bvSort2 = slv.mkBitVectorSort(32);
   Sort funSort12 = slv.mkFunctionSort({bvSort2, bvSort2}, bvSort2);
-  Sort funSort22 = slv.mkFunctionSort(uSort2, slv.getIntegerSort());
+  Sort funSort22 = slv.mkFunctionSort({uSort2}, slv.getIntegerSort());
   Term b12 = slv.mkVar(bvSort2, "b1");
   Term b112 = slv.mkVar(bvSort2, "b1");
   Term b42 = slv.mkVar(uSort2, "b4");
@@ -1280,7 +1281,7 @@ TEST_F(TestApiBlackSolver, defineFunsRecWrongLogic)
   Sort uSort = d_solver.mkUninterpretedSort("u");
   Sort bvSort = d_solver.mkBitVectorSort(32);
   Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
-  Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
+  Sort funSort2 = d_solver.mkFunctionSort({uSort}, d_solver.getIntegerSort());
   Term b = d_solver.mkVar(bvSort, "b");
   Term u = d_solver.mkVar(uSort, "u");
   Term v1 = d_solver.mkConst(bvSort, "v1");
@@ -1294,7 +1295,7 @@ TEST_F(TestApiBlackSolver, defineFunsRecWrongLogic)
 TEST_F(TestApiBlackSolver, defineFunsRecGlobal)
 {
   Sort bSort = d_solver.getBooleanSort();
-  Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
+  Sort fSort = d_solver.mkFunctionSort({bSort}, bSort);
 
   d_solver.push();
   Term bTrue = d_solver.mkBoolean(true);
@@ -1781,8 +1782,8 @@ TEST_F(TestApiBlackSolver, getUnsatCoreAndProof)
   Sort uSort = d_solver.mkUninterpretedSort("u");
   Sort intSort = d_solver.getIntegerSort();
   Sort boolSort = d_solver.getBooleanSort();
-  Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
-  Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
+  Sort uToIntSort = d_solver.mkFunctionSort({uSort}, intSort);
+  Sort intPredSort = d_solver.mkFunctionSort({intSort}, boolSort);
   std::vector<Term> uc;
 
   Term x = d_solver.mkConst(uSort, "x");
@@ -1906,8 +1907,8 @@ TEST_F(TestApiBlackSolver, getValue3)
   Sort uSort = d_solver.mkUninterpretedSort("u");
   Sort intSort = d_solver.getIntegerSort();
   Sort boolSort = d_solver.getBooleanSort();
-  Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
-  Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
+  Sort uToIntSort = d_solver.mkFunctionSort({uSort}, intSort);
+  Sort intPredSort = d_solver.mkFunctionSort({intSort}, boolSort);
   std::vector<Term> unsat_core;
 
   Term x = d_solver.mkConst(uSort, "x");
@@ -2343,7 +2344,7 @@ TEST_F(TestApiBlackSolver, simplify)
   Sort bvSort = d_solver.mkBitVectorSort(32);
   Sort uSort = d_solver.mkUninterpretedSort("u");
   Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
-  Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
+  Sort funSort2 = d_solver.mkFunctionSort({uSort}, d_solver.getIntegerSort());
   DatatypeDecl consListSpec = d_solver.mkDatatypeDecl("list");
   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", d_solver.getIntegerSort());
@@ -2458,8 +2459,8 @@ TEST_F(TestApiBlackSolver, checkSatAssuming2)
   Sort uSort = d_solver.mkUninterpretedSort("u");
   Sort intSort = d_solver.getIntegerSort();
   Sort boolSort = d_solver.getBooleanSort();
-  Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
-  Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
+  Sort uToIntSort = d_solver.mkFunctionSort({uSort}, intSort);
+  Sort intPredSort = d_solver.mkFunctionSort({intSort}, boolSort);
 
   Term n = Term();
   // Constants
@@ -2538,7 +2539,7 @@ TEST_F(TestApiBlackSolver, declareSygusVar)
   d_solver.setOption("sygus", "true");
   Sort boolSort = d_solver.getBooleanSort();
   Sort intSort = d_solver.getIntegerSort();
-  Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
+  Sort funSort = d_solver.mkFunctionSort({intSort}, boolSort);
 
   ASSERT_NO_THROW(d_solver.declareSygusVar("", boolSort));
   ASSERT_NO_THROW(d_solver.declareSygusVar("", funSort));
@@ -2898,7 +2899,7 @@ TEST_F(TestApiBlackSolver, Output)
 TEST_F(TestApiBlackSolver, issue7000)
 {
   Sort s1 = d_solver.getIntegerSort();
-  Sort s2 = d_solver.mkFunctionSort(s1, s1);
+  Sort s2 = d_solver.mkFunctionSort({s1}, s1);
   Sort s3 = d_solver.getRealSort();
   Term t4 = d_solver.mkPi();
   Term t7 = d_solver.mkConst(s3, "_x5");
index e388c60fa566e0a9990675bc0a636743644cdf45..ccbe23f9b7fc148a5702ee24ceb681e25ec86031 100644 (file)
@@ -180,7 +180,7 @@ TEST_F(TestApiBlackSort, isUpdater)
 
 TEST_F(TestApiBlackSort, isFunction)
 {
-  Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(),
+  Sort fun_sort = d_solver.mkFunctionSort({d_solver.getRealSort()},
                                           d_solver.getIntegerSort());
   ASSERT_TRUE(fun_sort.isFunction());
   ASSERT_NO_THROW(Sort().isFunction());
@@ -407,7 +407,7 @@ TEST_F(TestApiBlackSort, getUninterpretedSortConstructor)
 
 TEST_F(TestApiBlackSort, getFunctionArity)
 {
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort(),
+  Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
                                          d_solver.getIntegerSort());
   ASSERT_NO_THROW(funSort.getFunctionArity());
   Sort bvSort = d_solver.mkBitVectorSort(32);
@@ -416,7 +416,7 @@ TEST_F(TestApiBlackSort, getFunctionArity)
 
 TEST_F(TestApiBlackSort, getFunctionDomainSorts)
 {
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+  Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
                                          d_solver.getIntegerSort());
   ASSERT_NO_THROW(funSort.getFunctionDomainSorts());
   Sort bvSort = d_solver.mkBitVectorSort(32);
@@ -425,7 +425,7 @@ TEST_F(TestApiBlackSort, getFunctionDomainSorts)
 
 TEST_F(TestApiBlackSort, getFunctionCodomainSort)
 {
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+  Sort funSort = d_solver.mkFunctionSort({d_solver.mkUninterpretedSort("u")},
                                          d_solver.getIntegerSort());
   ASSERT_NO_THROW(funSort.getFunctionCodomainSort());
   Sort bvSort = d_solver.mkBitVectorSort(32);
index 08086d4c22de5eac9747b46e930c9e687495032e..45f53183bb4df4a6738b1c1296ad4c1d23e56d3b 100644 (file)
@@ -56,8 +56,8 @@ TEST_F(TestApiBlackTerm, getKind)
   Sort uSort = d_solver.mkUninterpretedSort("u");
   Sort intSort = d_solver.getIntegerSort();
   Sort boolSort = d_solver.getBooleanSort();
-  Sort funSort1 = d_solver.mkFunctionSort(uSort, intSort);
-  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+  Sort funSort1 = d_solver.mkFunctionSort({uSort}, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
 
   Term n;
   ASSERT_THROW(n.getKind(), CVC5ApiException);
@@ -98,8 +98,8 @@ TEST_F(TestApiBlackTerm, getSort)
   Sort bvSort = d_solver.mkBitVectorSort(8);
   Sort intSort = d_solver.getIntegerSort();
   Sort boolSort = d_solver.getBooleanSort();
-  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
-  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
 
   Term n;
   ASSERT_THROW(n.getSort(), CVC5ApiException);
@@ -143,7 +143,7 @@ TEST_F(TestApiBlackTerm, getOp)
   Sort intsort = d_solver.getIntegerSort();
   Sort bvsort = d_solver.mkBitVectorSort(8);
   Sort arrsort = d_solver.mkArraySort(bvsort, intsort);
-  Sort funsort = d_solver.mkFunctionSort(intsort, bvsort);
+  Sort funsort = d_solver.mkFunctionSort({intsort}, bvsort);
 
   Term x = d_solver.mkConst(intsort, "x");
   Term a = d_solver.mkConst(arrsort, "a");
@@ -238,8 +238,8 @@ TEST_F(TestApiBlackTerm, notTerm)
   Sort bvSort = d_solver.mkBitVectorSort(8);
   Sort intSort = d_solver.getIntegerSort();
   Sort boolSort = d_solver.getBooleanSort();
-  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
-  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
 
   ASSERT_THROW(Term().notTerm(), CVC5ApiException);
   Term b = d_solver.mkTrue();
@@ -267,8 +267,8 @@ TEST_F(TestApiBlackTerm, andTerm)
   Sort bvSort = d_solver.mkBitVectorSort(8);
   Sort intSort = d_solver.getIntegerSort();
   Sort boolSort = d_solver.getBooleanSort();
-  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
-  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
 
   Term b = d_solver.mkTrue();
   ASSERT_THROW(Term().andTerm(b), CVC5ApiException);
@@ -333,8 +333,8 @@ TEST_F(TestApiBlackTerm, orTerm)
   Sort bvSort = d_solver.mkBitVectorSort(8);
   Sort intSort = d_solver.getIntegerSort();
   Sort boolSort = d_solver.getBooleanSort();
-  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
-  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
 
   Term b = d_solver.mkTrue();
   ASSERT_THROW(Term().orTerm(b), CVC5ApiException);
@@ -399,8 +399,8 @@ TEST_F(TestApiBlackTerm, xorTerm)
   Sort bvSort = d_solver.mkBitVectorSort(8);
   Sort intSort = d_solver.getIntegerSort();
   Sort boolSort = d_solver.getBooleanSort();
-  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
-  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
 
   Term b = d_solver.mkTrue();
   ASSERT_THROW(Term().xorTerm(b), CVC5ApiException);
@@ -465,8 +465,8 @@ TEST_F(TestApiBlackTerm, eqTerm)
   Sort bvSort = d_solver.mkBitVectorSort(8);
   Sort intSort = d_solver.getIntegerSort();
   Sort boolSort = d_solver.getBooleanSort();
-  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
-  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
 
   Term b = d_solver.mkTrue();
   ASSERT_THROW(Term().eqTerm(b), CVC5ApiException);
@@ -531,8 +531,8 @@ TEST_F(TestApiBlackTerm, impTerm)
   Sort bvSort = d_solver.mkBitVectorSort(8);
   Sort intSort = d_solver.getIntegerSort();
   Sort boolSort = d_solver.getBooleanSort();
-  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
-  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
 
   Term b = d_solver.mkTrue();
   ASSERT_THROW(Term().impTerm(b), CVC5ApiException);
@@ -597,8 +597,8 @@ TEST_F(TestApiBlackTerm, iteTerm)
   Sort bvSort = d_solver.mkBitVectorSort(8);
   Sort intSort = d_solver.getIntegerSort();
   Sort boolSort = d_solver.getBooleanSort();
-  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
-  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort}, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort({intSort}, boolSort);
 
   Term b = d_solver.mkTrue();
   ASSERT_THROW(Term().iteTerm(b, b), CVC5ApiException);
@@ -669,7 +669,7 @@ TEST_F(TestApiBlackTerm, termChildren)
 
   // apply term f(2)
   Sort intSort = d_solver.getIntegerSort();
-  Sort fsort = d_solver.mkFunctionSort(intSort, intSort);
+  Sort fsort = d_solver.mkFunctionSort({intSort}, intSort);
   Term f = d_solver.mkConst(fsort, "f");
   Term t2 = d_solver.mkTerm(APPLY_UF, {f, two});
   // due to our higher-order view of terms, we treat f as a child of APPLY_UF
index ef741d35c2bc824579442eee288ec987a8fc2053..74f9baf1b6e9478d1d7a8ff9b841e694a022d6d3 100644 (file)
@@ -28,7 +28,7 @@ TEST_F(TestApiWhiteTerm, getOp)
   Sort intsort = d_solver.getIntegerSort();
   Sort bvsort = d_solver.mkBitVectorSort(8);
   Sort arrsort = d_solver.mkArraySort(bvsort, intsort);
-  Sort funsort = d_solver.mkFunctionSort(intsort, bvsort);
+  Sort funsort = d_solver.mkFunctionSort({intsort}, bvsort);
 
   Term x = d_solver.mkConst(intsort, "x");
   Term a = d_solver.mkConst(arrsort, "a");
index 7c763ddb44e10f559be27c78b0ab0a4b688d7061..5de730b45afdae6aa965fcc6c82934275d26ddde 100644 (file)
@@ -66,9 +66,9 @@ class TestParserBlackParser : public TestInternal
     cvc5::Sort u = parser.mkSort("u");
     cvc5::Sort v = parser.mkSort("v");
     /* f : t->u; g: u->v; h: v->t; */
-    parser.bindVar("f", d_solver.get()->mkFunctionSort(t, u));
-    parser.bindVar("g", d_solver.get()->mkFunctionSort(u, v));
-    parser.bindVar("h", d_solver.get()->mkFunctionSort(v, t));
+    parser.bindVar("f", d_solver.get()->mkFunctionSort({t}, u));
+    parser.bindVar("g", d_solver.get()->mkFunctionSort({u}, v));
+    parser.bindVar("h", d_solver.get()->mkFunctionSort({v}, t));
     /* x:t; y:u; z:v; */
     parser.bindVar("x", t);
     parser.bindVar("y", u);