New C++ API: Remove redundant mkTerm function. (#2836)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index ea70fc0566ed18845d485a3723c552b69ea6fd27..5d1f853e07a8e3717001d7bdab091b00039ccf80 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2531,21 +2531,6 @@ Term Solver::mkTerm(Kind kind) const
   }
 }
 
-Term Solver::mkTerm(Kind kind, Sort sort) const
-{
-  try
-  {
-    CVC4_API_KIND_CHECK_EXPECTED(kind == SEP_NIL, kind) << "SEP_NIL";
-    Term res = d_exprMgr->mkNullaryOperator(*sort.d_type, extToIntKind(kind));
-    (void)res.d_expr->getType(true); /* kick off type checking */
-    return res;
-  }
-  catch (const CVC4::TypeCheckingException& e)
-  {
-    throw CVC4ApiException(e.getMessage());
-  }
-}
-
 Term Solver::mkTerm(Kind kind, Term child) const
 {
   try

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 955aff21a2ca0bd3d5919fcda3d5671b20d21501..2ac762b3e405ca93c95b8eb47b89cf2fcc17bc5a 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -1702,14 +1702,6 @@ class CVC4_PUBLIC Solver
    */
   Term mkTerm(Kind kind) const;
 
-  /**
-   * Create 0-ary term of given kind and sort.
-   * @param kind the kind of the term
-   * @param sort the sort argument to this kind
-   * @return the Term
-   */
-  Term mkTerm(Kind kind, Sort sort) const;
-
   /**
    * Create a unary term of given kind.
    * @param kind the kind of the term

diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 4e69ddfe11a46b56fce366e82a329624a3a6db49..3184da78ec62156c2f1b4f70e627fb09d5674499 100644 (file)
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -1755,7 +1755,6 @@ enum CVC4_PUBLIC Kind : int32_t
    * Parameters: 0
    * Create with:
    *   mkSepNil(Sort sort)
-   *   mkTerm(Kind kind, Sort sort)
    */
   SEP_NIL,
   /**

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 169a9948dba25501bb25474843b08a2fc5a86309..0a3eb46c3cda3b9b667b0e08e939c2b33bb52458 100644 (file)
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -550,11 +550,6 @@ void SolverBlack::testMkTerm()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(REGEXP_SIGMA));
   TS_ASSERT_THROWS(d_solver->mkTerm(CONST_BITVECTOR), CVC4ApiException&);
 
-  // mkTerm(Kind kind, Sort sort) const
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver->mkTerm(SEP_NIL, d_solver->getBooleanSort()));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(SEP_NIL, Sort()));
-
   // mkTerm(Kind kind, Term child) const
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(NOT, d_solver->mkTrue()));
   TS_ASSERT_THROWS(d_solver->mkTerm(NOT, Term()), CVC4ApiException&);