From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 13 Feb 2019 20:52:17 +0000 (-0800)
Subject: New C++ API: Remove redundant declareFun function. (#2837)
X-Git-Tag: cvc5-1.0.0~4259
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=549fe66e9cd274784edac47203b832ff7797834f;p=cvc5.git

New C++ API: Remove redundant declareFun function. (#2837)
---

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
@@ -3002,15 +3002,6 @@ Sort Solver::declareDatatype(
   return d_exprMgr->mkDatatypeType(*dtdecl.d_dtype);
 }
 
-/**
- *  ( 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> )
  */
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
@@ -2270,15 +2270,6 @@ class CVC4_PUBLIC Solver
   Sort declareDatatype(const std::string& symbol,
                        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> )
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(