From cd2a319d14b1ec7598e8e774cec012b4ce990274 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 18 Mar 2019 15:58:43 -0700 Subject: [PATCH] New C++: Remove redundant mkBoundVar function. --- src/api/cvc4cpp.cpp | 20 +++------------- src/api/cvc4cpp.h | 11 ++------- test/unit/api/solver_black.h | 46 ++++++++++++++++++------------------ 3 files changed, 28 insertions(+), 49 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 032326c26..82e4ffba1 100644 --- 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 3999dd2ed..df26b79ea 100644 --- 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 f64751d01..dfd92a8c5 100644 --- 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); -- 2.30.2