New C++: Remove redundant mkBoundVar function.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 032326c268902b5950ff5d92792e5279ea8ff325..82e4ffba16c58db64bf2ea14057be9ab9790b3ea 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2408,27 +2408,13 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const
   }
 }
 
-Term Solver::mkBoundVar(const std::string& symbol, Sort sort) const
+Term Solver::mkBoundVar(Sort sort, const std::string& symbol) const
 {
   try
   {
     CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
-    Term res = d_exprMgr->mkBoundVar(symbol, *sort.d_type);
-    (void)res.d_expr->getType(true); /* kick off type checking */
-    return res;
-  }
-  catch (const CVC4::TypeCheckingException& e)
-  {
-    throw CVC4ApiException(e.getMessage());
-  }
-}
-
-Term Solver::mkBoundVar(Sort sort) const
-{
-  try
-  {
-    CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
-    Term res = d_exprMgr->mkBoundVar(*sort.d_type);
+    Term res = symbol.empty() ? d_exprMgr->mkBoundVar(*sort.d_type)
+                              : d_exprMgr->mkBoundVar(symbol, *sort.d_type);
     (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 3999dd2ede3fbbb8a397ef82623a9cd07f84207d..df26b79ea0b01e206ee97df2ec357aac4ba8b351 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2173,20 +2173,13 @@ class CVC4_PUBLIC Solver
    */
   Term mkVar(Sort sort, const std::string& symbol = std::string()) const;
 
-  /**
-   * Create bound variable.
-   * @param symbol the name of the variable
-   * @param sort the sort of the variable
-   * @return the variable
-   */
-  Term mkBoundVar(const std::string& symbol, Sort sort) const;
-
   /**
    * Create bound variable.
    * @param sort the sort of the variable
+   * @param symbol the name of the variable
    * @return the variable
    */
-  Term mkBoundVar(Sort sort) const;
+  Term mkBoundVar(Sort sort, const std::string& symbol = std::string()) const;
 
   /* .................................................................... */
   /* Formula Handling                                                     */

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index f64751d0176f106fb2985c6374fb5f5967228f1b..dfd92a8c5c4a1104506d8972d6f2a27e6491a51e 100644 (file)
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -295,12 +295,12 @@ void SolverBlack::testMkBoundVar()
   Sort boolSort = d_solver->getBooleanSort();
   Sort intSort = d_solver->getIntegerSort();
   Sort funSort = d_solver->mkFunctionSort(intSort, boolSort);
-  TS_ASSERT_THROWS(d_solver->mkBoundVar(Sort()), CVC4ApiException&);
   TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(boolSort));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(funSort));
-  TS_ASSERT_THROWS(d_solver->mkBoundVar("a", Sort()), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(std::string("b"), boolSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar("", funSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(boolSort, std::string("b")));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(funSort, ""));
+  TS_ASSERT_THROWS(d_solver->mkBoundVar(Sort()), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkBoundVar(Sort(), "a"), CVC4ApiException&);
 }
 
 void SolverBlack::testMkBoolean()
@@ -795,12 +795,12 @@ void SolverBlack::testDefineFun()
   Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
   Sort funSort2 = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"),
                                            d_solver->getIntegerSort());
-  Term b1 = d_solver->mkBoundVar("b1", bvSort);
-  Term b11 = d_solver->mkBoundVar("b1", bvSort);
-  Term b2 = d_solver->mkBoundVar("b2", d_solver->getIntegerSort());
-  Term b3 = d_solver->mkBoundVar("b3", funSort2);
-  Term v1 = d_solver->mkBoundVar("v1", bvSort);
-  Term v2 = d_solver->mkBoundVar("v2", d_solver->getIntegerSort());
+  Term b1 = d_solver->mkBoundVar(bvSort, "b1");
+  Term b11 = d_solver->mkBoundVar(bvSort, "b1");
+  Term b2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "b2");
+  Term b3 = d_solver->mkBoundVar(funSort2, "b3");
+  Term v1 = d_solver->mkBoundVar(bvSort, "v1");
+  Term v2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "v2");
   Term v3 = d_solver->mkVar(funSort2, "v3");
   Term f1 = d_solver->declareConst("f1", funSort1);
   Term f2 = d_solver->declareConst("f2", funSort2);
@@ -827,12 +827,12 @@ void SolverBlack::testDefineFunRec()
   Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
   Sort funSort2 = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"),
                                            d_solver->getIntegerSort());
-  Term b1 = d_solver->mkBoundVar("b1", bvSort);
-  Term b11 = d_solver->mkBoundVar("b1", bvSort);
-  Term b2 = d_solver->mkBoundVar("b2", d_solver->getIntegerSort());
-  Term b3 = d_solver->mkBoundVar("b3", funSort2);
-  Term v1 = d_solver->mkBoundVar("v1", bvSort);
-  Term v2 = d_solver->mkBoundVar("v2", d_solver->getIntegerSort());
+  Term b1 = d_solver->mkBoundVar(bvSort, "b1");
+  Term b11 = d_solver->mkBoundVar(bvSort, "b1");
+  Term b2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "b2");
+  Term b3 = d_solver->mkBoundVar(funSort2, "b3");
+  Term v1 = d_solver->mkBoundVar(bvSort, "v1");
+  Term v2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "v2");
   Term v3 = d_solver->mkVar(funSort2, "v3");
   Term f1 = d_solver->declareConst("f1", funSort1);
   Term f2 = d_solver->declareConst("f2", funSort2);
@@ -861,13 +861,13 @@ void SolverBlack::testDefineFunsRec()
   Sort bvSort = d_solver->mkBitVectorSort(32);
   Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
   Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort());
-  Term b1 = d_solver->mkBoundVar("b1", bvSort);
-  Term b11 = d_solver->mkBoundVar("b1", bvSort);
-  Term b2 = d_solver->mkBoundVar("b2", d_solver->getIntegerSort());
-  Term b3 = d_solver->mkBoundVar("b3", funSort2);
-  Term b4 = d_solver->mkBoundVar("b4", uSort);
-  Term v1 = d_solver->mkBoundVar("v1", bvSort);
-  Term v2 = d_solver->mkBoundVar("v2", d_solver->getIntegerSort());
+  Term b1 = d_solver->mkBoundVar(bvSort, "b1");
+  Term b11 = d_solver->mkBoundVar(bvSort, "b1");
+  Term b2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "b2");
+  Term b3 = d_solver->mkBoundVar(funSort2, "b3");
+  Term b4 = d_solver->mkBoundVar(uSort, "b4");
+  Term v1 = d_solver->mkBoundVar(bvSort, "v1");
+  Term v2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "v2");
   Term v3 = d_solver->mkVar(funSort2, "v3");
   Term v4 = d_solver->mkVar(uSort, "v4");
   Term f1 = d_solver->declareConst("f1", funSort1);