diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-03-18 15:58:43 -0700 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-03-18 17:26:29 -0700 |
| commit | cd2a319d14b1ec7598e8e774cec012b4ce990274 (patch) | |
| tree | 1abd651b33513441ebbc51281b1f8cdd8a9eaf11 /src/api | |
| parent | a4f76da78653e80c28740b2ad4bf3929110d5a25 (diff) | |
New C++: Remove redundant mkBoundVar function.
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 20 | ||||
| -rw-r--r-- | src/api/cvc4cpp.h | 11 |
2 files changed, 5 insertions, 26 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 @@ -2175,18 +2175,11 @@ class CVC4_PUBLIC Solver /** * 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 */ |