diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-02-13 12:52:17 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-02-13 12:52:17 -0800 |
commit | 549fe66e9cd274784edac47203b832ff7797834f (patch) | |
tree | 3108cf767b0949427501124975d5856145f4c87e /src/api | |
parent | 83cd4823d6bf8e0c8e7d82afbfac824744491762 (diff) |
New C++ API: Remove redundant declareFun function. (#2837)
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cpp.cpp | 9 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 9 |
2 files changed, 0 insertions, 18 deletions
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 @@ -3003,15 +3003,6 @@ Sort Solver::declareDatatype( } /** - * ( 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> ) */ Term Solver::declareFun(const std::string& symbol, 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 @@ -2271,15 +2271,6 @@ class CVC4_PUBLIC Solver 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> ) * @param symbol the name of the function |