Keep definitions when global-declarations enabled (#4572)

Fixes #4552. Fixes #4555. The SMT-LIB standard mandates that definitions
are kept when `:global-declarations` are enabled. Until now, CVC4 was
keeping track of the symbols of a definition correctly but lost the body
of the definition when the user context was popped. This commit fixes
the issue by adding a `global` parameter to
`SmtEngine::defineFunction()` and `SmtEngine::defineFunctionRec()`. If
that parameter is set, the definitions of functions are added at level 0
to `d_definedFunctions` and the lemmas for recursive function
definitions are kept in an additional list and asserted during each
`checkSat` call. The commit also updates new API, the commands, and the
parsers to reflect this change.

4 files changed, 55 insertions, 30 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 2c65f1ca6..88974dc69 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -4219,7 +4219,8 @@ Sort Solver::declareSort(const std::string& symbol, uint32_t arity) const
 Term Solver::defineFun(const std::string& symbol,
                        const std::vector<Term>& bound_vars,
                        Sort sort,
-                       Term term) const
+                       Term term,
+                       bool global) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)
@@ -4253,14 +4254,15 @@ Term Solver::defineFun(const std::string& symbol,
   }
   Expr fun = d_exprMgr->mkVar(symbol, type);
   std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
-  d_smtEngine->defineFunction(fun, ebound_vars, *term.d_expr);
+  d_smtEngine->defineFunction(fun, ebound_vars, *term.d_expr, global);
   return Term(this, fun);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Term Solver::defineFun(Term fun,
                        const std::vector<Term>& bound_vars,
-                       Term term) const
+                       Term term,
+                       bool global) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function";
@@ -4293,7 +4295,7 @@ Term Solver::defineFun(Term fun,
       << codomain << "'";
 
   std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
-  d_smtEngine->defineFunction(*fun.d_expr, ebound_vars, *term.d_expr);
+  d_smtEngine->defineFunction(*fun.d_expr, ebound_vars, *term.d_expr, global);
   return fun;
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -4304,7 +4306,8 @@ Term Solver::defineFun(Term fun,
 Term Solver::defineFunRec(const std::string& symbol,
                           const std::vector<Term>& bound_vars,
                           Sort sort,
-                          Term term) const
+                          Term term,
+                          bool global) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)
@@ -4340,14 +4343,15 @@ Term Solver::defineFunRec(const std::string& symbol,
   }
   Expr fun = d_exprMgr->mkVar(symbol, type);
   std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
-  d_smtEngine->defineFunctionRec(fun, ebound_vars, *term.d_expr);
+  d_smtEngine->defineFunctionRec(fun, ebound_vars, *term.d_expr, global);
   return Term(this, fun);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Term Solver::defineFunRec(Term fun,
                           const std::vector<Term>& bound_vars,
-                          Term term) const
+                          Term term,
+                          bool global) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function";
@@ -4379,7 +4383,8 @@ Term Solver::defineFunRec(Term fun,
       << "Invalid sort of function body '" << term << "', expected '"
       << codomain << "'";
   std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
-  d_smtEngine->defineFunctionRec(*fun.d_expr, ebound_vars, *term.d_expr);
+  d_smtEngine->defineFunctionRec(
+      *fun.d_expr, ebound_vars, *term.d_expr, global);
   return fun;
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -4389,7 +4394,8 @@ Term Solver::defineFunRec(Term fun,
  */
 void Solver::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) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   size_t funs_size = funs.size();
@@ -4444,7 +4450,7 @@ void Solver::defineFunsRec(const std::vector<Term>& funs,
     ebound_vars.push_back(termVectorToExprs(v));
   }
   std::vector<Expr> exprs = termVectorToExprs(terms);
-  d_smtEngine->defineFunctionsRec(efuns, ebound_vars, exprs);
+  d_smtEngine->defineFunctionsRec(efuns, ebound_vars, exprs, global);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
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.
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index cc998306d..624b3c365 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -181,14 +181,14 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         Term declareFun(const string& symbol, const vector[Sort]& sorts, Sort sort) except +
         Sort declareSort(const string& symbol, uint32_t arity) except +
         Term defineFun(const string& symbol, const vector[Term]& bound_vars,
-                       Sort sort, Term term) except +
-        Term defineFun(Term fun, const vector[Term]& bound_vars, Term term) except +
+                       Sort sort, Term term, bint glbl) except +
+        Term defineFun(Term fun, const vector[Term]& bound_vars, Term term, bint glbl) except +
         Term defineFunRec(const string& symbol, const vector[Term]& bound_vars,
-                          Sort sort, Term term) except +
+                          Sort sort, Term term, bint glbl) except +
         Term defineFunRec(Term fun, const vector[Term]& bound_vars,
-                          Term term) except +
+                          Term term, bint glbl) except +
         Term defineFunsRec(vector[Term]& funs, vector[vector[Term]]& bound_vars,
-                           vector[Term]& terms) except +
+                           vector[Term]& terms, bint glbl) except +
         vector[Term] getAssertions() except +
         vector[pair[Term, Term]] getAssignment() except +
         string getInfo(const string& flag) except +
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index 9dd9c1cde..b7593f6f1 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -797,13 +797,13 @@ cdef class Solver:
         sort.csort = self.csolver.declareSort(symbol.encode(), arity)
         return sort
 
-    def defineFun(self, sym_or_fun, bound_vars, sort_or_term, t=None):
+    def defineFun(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
         '''
         Supports two uses:
                 Term defineFun(str symbol, List[Term] bound_vars,
-                               Sort sort, Term term)
+                               Sort sort, Term term, bool glbl)
                 Term defineFun(Term fun, List[Term] bound_vars,
-                               Term term)
+                               Term term, bool glbl)
         '''
         cdef Term term = Term()
         cdef vector[c_Term] v
@@ -814,21 +814,23 @@ cdef class Solver:
             term.cterm = self.csolver.defineFun((<str?> sym_or_fun).encode(),
                                                 <const vector[c_Term] &> v,
                                                 (<Sort?> sort_or_term).csort,
-                                                (<Term?> t).cterm)
+                                                (<Term?> t).cterm,
+                                                <bint> glbl)
         else:
             term.cterm = self.csolver.defineFun((<Term?> sym_or_fun).cterm,
                                                 <const vector[c_Term]&> v,
-                                                (<Term?> sort_or_term).cterm)
+                                                (<Term?> sort_or_term).cterm,
+                                                <bint> glbl)
 
         return term
 
-    def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None):
+    def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
         '''
         Supports two uses:
                 Term defineFunRec(str symbol, List[Term] bound_vars,
-                               Sort sort, Term term)
+                               Sort sort, Term term, bool glbl)
                 Term defineFunRec(Term fun, List[Term] bound_vars,
-                               Term term)
+                               Term term, bool glbl)
         '''
         cdef Term term = Term()
         cdef vector[c_Term] v
@@ -839,11 +841,13 @@ cdef class Solver:
             term.cterm = self.csolver.defineFunRec((<str?> sym_or_fun).encode(),
                                                 <const vector[c_Term] &> v,
                                                 (<Sort?> sort_or_term).csort,
-                                                (<Term?> t).cterm)
+                                                (<Term?> t).cterm,
+                                                <bint> glbl)
         else:
             term.cterm = self.csolver.defineFunRec((<Term?> sym_or_fun).cterm,
                                                    <const vector[c_Term]&> v,
-                                                   (<Term?> sort_or_term).cterm)
+                                                   (<Term?> sort_or_term).cterm,
+                                                   <bint> glbl)
 
         return term