From: Andres Noetzli Date: Fri, 1 Apr 2022 04:50:25 +0000 (-0700) Subject: [API] Remove redundant version of `mkFunctionSort` (#8503) X-Git-Tag: cvc5-1.0.0~73 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=01061af730c2805c8c1d4a7cc2a03dee6ffc0017;p=cvc5.git [API] Remove redundant version of `mkFunctionSort` (#8503) 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. --- diff --git a/examples/api/cpp/combination.cpp b/examples/api/cpp/combination.cpp index c3af0c423..98a460a8b 100644 --- a/examples/api/cpp/combination.cpp +++ b/examples/api/cpp/combination.cpp @@ -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"); diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp index 2c953b6fb..a0e051070 100644 --- a/examples/simple_vc_quant_cxx.cpp +++ b/examples/simple_vc_quant_cxx.cpp @@ -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"); diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 7534eceaa..b7e44a850 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -5522,18 +5522,6 @@ std::vector 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& sorts, const Sort& codomain) const { diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 2358ee879..9f4113fb6 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -3211,14 +3211,6 @@ class CVC5_EXPORT Solver const std::vector& dtypedecls, const std::set& 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 diff --git a/src/api/java/io/github/cvc5/Solver.java b/src/api/java/io/github/cvc5/Solver.java index 384824e5d..92d444fe7 100644 --- a/src/api/java/io/github/cvc5/Solver.java +++ b/src/api/java/io/github/cvc5/Solver.java @@ -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 diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index f21434dd2..41ada6ade 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -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(pointer); - Sort* domain = reinterpret_cast(domainPointer); - Sort* codomain = reinterpret_cast(codomainPointer); - Sort* sortPointer = new Sort(solver->mkFunctionSort(*domain, *codomain)); - return reinterpret_cast(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(pointer); diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 929c03900..13e5041ca 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -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 + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index eb0e749bd..91b949854 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -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(( sorts).csort, - codomain.csort) - elif isinstance(sorts, list): + v.push_back((sorts).csort) + else: for s in sorts: v.push_back((s).csort) - sort.csort = self.csolver.mkFunctionSort( v, - codomain.csort) + sort.csort = self.csolver.mkFunctionSort( v, + codomain.csort) return sort def mkParamSort(self, str symbolname = None): diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 79878adfa..3c06d81ad 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -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)); } diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 6b8d985c9..69bdf60c1 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -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 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 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 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"); diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp index e388c60fa..ccbe23f9b 100644 --- a/test/unit/api/cpp/sort_black.cpp +++ b/test/unit/api/cpp/sort_black.cpp @@ -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); diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp index 08086d4c2..45f53183b 100644 --- a/test/unit/api/cpp/term_black.cpp +++ b/test/unit/api/cpp/term_black.cpp @@ -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 diff --git a/test/unit/api/cpp/term_white.cpp b/test/unit/api/cpp/term_white.cpp index ef741d35c..74f9baf1b 100644 --- a/test/unit/api/cpp/term_white.cpp +++ b/test/unit/api/cpp/term_white.cpp @@ -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"); diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp index 7c763ddb4..5de730b45 100644 --- a/test/unit/parser/parser_black.cpp +++ b/test/unit/parser/parser_black.cpp @@ -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);