diff options
Diffstat (limited to 'src/api/cvc4cpp.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 25 |
1 files changed, 20 insertions, 5 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index adf3691ab..aa51a4134 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2860,12 +2860,15 @@ class CVC4_PUBLIC Solver * @param bound_vars the parameters to this function * @param sort the sort of the return value of this function * @param term the function body + * @param global determines whether this definition is global (i.e. persists + * when popping the context) * @return the function */ Term defineFun(const std::string& symbol, const std::vector<Term>& bound_vars, Sort sort, - Term term) const; + Term term, + bool global = false) const; /** * Define n-ary function. * SMT-LIB: ( define-fun <function_def> ) @@ -2873,11 +2876,14 @@ class CVC4_PUBLIC Solver * @param fun the sorted function * @param bound_vars the parameters to this function * @param term the function body + * @param global determines whether this definition is global (i.e. persists + * when popping the context) * @return the function */ Term defineFun(Term fun, const std::vector<Term>& bound_vars, - Term term) const; + Term term, + bool global = false) const; /** * Define recursive function. @@ -2886,12 +2892,15 @@ class CVC4_PUBLIC Solver * @param bound_vars the parameters to this function * @param sort the sort of the return value of this function * @param term the function body + * @param global determines whether this definition is global (i.e. persists + * when popping the context) * @return the function */ Term defineFunRec(const std::string& symbol, const std::vector<Term>& bound_vars, Sort sort, - Term term) const; + Term term, + bool global = false) const; /** * Define recursive function. @@ -2900,11 +2909,14 @@ class CVC4_PUBLIC Solver * @param fun the sorted function * @param bound_vars the parameters to this function * @param term the function body + * @param global determines whether this definition is global (i.e. persists + * when popping the context) * @return the function */ Term defineFunRec(Term fun, const std::vector<Term>& bound_vars, - Term term) const; + Term term, + bool global = false) const; /** * Define recursive functions. @@ -2913,11 +2925,14 @@ class CVC4_PUBLIC Solver * @param funs the sorted functions * @param bound_vars the list of parameters to the functions * @param term the list of function bodies of the functions + * @param global determines whether this definition is global (i.e. persists + * when popping the context) * @return the function */ void defineFunsRec(const std::vector<Term>& funs, const std::vector<std::vector<Term>>& bound_vars, - const std::vector<Term>& terms) const; + const std::vector<Term>& terms, + bool global = false) const; /** * Echo a given string to the given output stream. |