diff options
-rw-r--r-- | examples/api/datatypes-new.cpp | 2 | ||||
-rw-r--r-- | src/api/cvc4cpp.cpp | 9 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 9 | ||||
-rw-r--r-- | test/unit/api/solver_black.h | 24 |
4 files changed, 13 insertions, 31 deletions
diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp index 14ddcd383..58b23bcc2 100644 --- a/examples/api/datatypes-new.cpp +++ b/examples/api/datatypes-new.cpp @@ -115,7 +115,7 @@ void test(Solver& slv, Sort& consListSort) } } - Term a = slv.declareFun("a", paramConsIntListSort); + Term a = slv.declareConst("a", paramConsIntListSort); std::cout << "term " << a << " is of sort " << a.getSort() << std::endl; Term head_a = slv.mkTerm( diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 5d1f853e0..9d56bb88a 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3003,15 +3003,6 @@ Sort Solver::declareDatatype( } /** - * ( declare-fun <symbol> () <sort> ) - */ -Term Solver::declareFun(const std::string& symbol, Sort sort) const -{ - Type type = *sort.d_type; - return d_exprMgr->mkVar(symbol, type); -} - -/** * ( declare-fun <symbol> ( <sort>* ) <sort> ) */ Term Solver::declareFun(const std::string& symbol, diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 2ac762b3e..b6049d5b3 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2271,15 +2271,6 @@ class CVC4_PUBLIC Solver const std::vector<DatatypeConstructorDecl>& ctors) const; /** - * Declare 0-arity function symbol. - * SMT-LIB: ( declare-fun <symbol> ( ) <sort> ) - * @param symbol the name of the function - * @param sort the sort of the return value of this function - * @return the function - */ - Term declareFun(const std::string& symbol, Sort sort) const; - - /** * Declare n-ary function symbol. * SMT-LIB: ( declare-fun <symbol> ( <sort>* ) <sort> ) * @param symbol the name of the function diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 0a3eb46c3..e3f9e0852 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -611,7 +611,7 @@ void SolverBlack::testMkTermFromOpTerm() Sort listSort = d_solver->mkDatatypeSort(listDecl); Sort intListSort = listSort.instantiate(std::vector<Sort>{d_solver->getIntegerSort()}); - Term c = d_solver->declareFun("c", intListSort); + Term c = d_solver->declareConst("c", intListSort); Datatype list = listSort.getDatatype(); // list datatype constructor and selector operator terms OpTerm consTerm1 = list.getConstructorTerm("cons"); @@ -765,10 +765,10 @@ void SolverBlack::testDeclareFun() Sort bvSort = d_solver->mkBitVectorSort(32); Sort funSort = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"), d_solver->getIntegerSort()); - TS_ASSERT_THROWS_NOTHING(d_solver->declareFun("f1", bvSort)); - TS_ASSERT_THROWS_NOTHING(d_solver->declareFun("f2", funSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->declareFun("f1", {}, bvSort)); TS_ASSERT_THROWS_NOTHING( d_solver->declareFun("f3", {bvSort, d_solver->getIntegerSort()}, bvSort)); + TS_ASSERT_THROWS(d_solver->declareFun("f2", {}, funSort), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->declareFun("f4", {bvSort, funSort}, bvSort), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->declareFun("f5", {bvSort, bvSort}, funSort), @@ -795,9 +795,9 @@ void SolverBlack::testDefineFun() Term v1 = d_solver->mkBoundVar("v1", bvSort); Term v2 = d_solver->mkBoundVar("v2", d_solver->getIntegerSort()); Term v3 = d_solver->mkVar("v3", funSort2); - Term f1 = d_solver->declareFun("f1", funSort1); - Term f2 = d_solver->declareFun("f2", funSort2); - Term f3 = d_solver->declareFun("f3", bvSort); + Term f1 = d_solver->declareConst("f1", funSort1); + Term f2 = d_solver->declareConst("f2", funSort2); + Term f3 = d_solver->declareConst("f3", bvSort); TS_ASSERT_THROWS_NOTHING(d_solver->defineFun("f", {}, bvSort, v1)); TS_ASSERT_THROWS_NOTHING(d_solver->defineFun("ff", {b1, b2}, bvSort, v1)); TS_ASSERT_THROWS_NOTHING(d_solver->defineFun(f1, {b1, b11}, v1)); @@ -827,9 +827,9 @@ void SolverBlack::testDefineFunRec() Term v1 = d_solver->mkBoundVar("v1", bvSort); Term v2 = d_solver->mkBoundVar("v2", d_solver->getIntegerSort()); Term v3 = d_solver->mkVar("v3", funSort2); - Term f1 = d_solver->declareFun("f1", funSort1); - Term f2 = d_solver->declareFun("f2", funSort2); - Term f3 = d_solver->declareFun("f3", bvSort); + Term f1 = d_solver->declareConst("f1", funSort1); + Term f2 = d_solver->declareConst("f2", funSort2); + Term f3 = d_solver->declareConst("f3", bvSort); TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec("f", {}, bvSort, v1)); TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec("ff", {b1, b2}, bvSort, v1)); TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec(f1, {b1, b11}, v1)); @@ -863,9 +863,9 @@ void SolverBlack::testDefineFunsRec() Term v2 = d_solver->mkBoundVar("v2", d_solver->getIntegerSort()); Term v3 = d_solver->mkVar("v3", funSort2); Term v4 = d_solver->mkVar("v4", uSort); - Term f1 = d_solver->declareFun("f1", funSort1); - Term f2 = d_solver->declareFun("f2", funSort2); - Term f3 = d_solver->declareFun("f3", bvSort); + Term f1 = d_solver->declareConst("f1", funSort1); + Term f2 = d_solver->declareConst("f2", funSort2); + Term f3 = d_solver->declareConst("f3", bvSort); TS_ASSERT_THROWS_NOTHING( d_solver->defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2})); TS_ASSERT_THROWS( |