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.

1 files changed, 28 insertions, 19 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 20f2dcff9..9fd0122fc 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1266,22 +1266,27 @@ std::string DefineTypeCommand::getCommandName() const { return "define-sort"; }
 
 DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
                                              Expr func,
-                                             Expr formula)
+                                             Expr formula,
+                                             bool global)
     : DeclarationDefinitionCommand(id),
       d_func(func),
       d_formals(),
-      d_formula(formula)
+      d_formula(formula),
+      d_global(global)
 {
 }
 
 DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
                                              Expr func,
                                              const std::vector<Expr>& formals,
-                                             Expr formula)
+                                             Expr formula,
+                                             bool global)
     : DeclarationDefinitionCommand(id),
       d_func(func),
       d_formals(formals),
-      d_formula(formula)
+      d_formula(formula),
+      d_global(global)
+
 {
 }
 
@@ -1298,7 +1303,7 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine)
   {
     if (!d_func.isNull())
     {
-      smtEngine->defineFunction(d_func, d_formals, d_formula);
+      smtEngine->defineFunction(d_func, d_formals, d_formula, d_global);
     }
     d_commandStatus = CommandSuccess::instance();
   }
@@ -1319,12 +1324,13 @@ Command* DefineFunctionCommand::exportTo(ExprManager* exprManager,
             back_inserter(formals),
             ExportTransformer(exprManager, variableMap));
   Expr formula = d_formula.exportTo(exprManager, variableMap);
-  return new DefineFunctionCommand(d_symbol, func, formals, formula);
+  return new DefineFunctionCommand(d_symbol, func, formals, formula, d_global);
 }
 
 Command* DefineFunctionCommand::clone() const
 {
-  return new DefineFunctionCommand(d_symbol, d_func, d_formals, d_formula);
+  return new DefineFunctionCommand(
+      d_symbol, d_func, d_formals, d_formula, d_global);
 }
 
 std::string DefineFunctionCommand::getCommandName() const
@@ -1340,8 +1346,9 @@ DefineNamedFunctionCommand::DefineNamedFunctionCommand(
     const std::string& id,
     Expr func,
     const std::vector<Expr>& formals,
-    Expr formula)
-    : DefineFunctionCommand(id, func, formals, formula)
+    Expr formula,
+    bool global)
+    : DefineFunctionCommand(id, func, formals, formula, global)
 {
 }
 
@@ -1365,12 +1372,14 @@ Command* DefineNamedFunctionCommand::exportTo(
             back_inserter(formals),
             ExportTransformer(exprManager, variableMap));
   Expr formula = d_formula.exportTo(exprManager, variableMap);
-  return new DefineNamedFunctionCommand(d_symbol, func, formals, formula);
+  return new DefineNamedFunctionCommand(
+      d_symbol, func, formals, formula, d_global);
 }
 
 Command* DefineNamedFunctionCommand::clone() const
 {
-  return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula);
+  return new DefineNamedFunctionCommand(
+      d_symbol, d_func, d_formals, d_formula, d_global);
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1378,7 +1387,8 @@ Command* DefineNamedFunctionCommand::clone() const
 /* -------------------------------------------------------------------------- */
 
 DefineFunctionRecCommand::DefineFunctionRecCommand(
-    Expr func, const std::vector<Expr>& formals, Expr formula)
+    Expr func, const std::vector<Expr>& formals, Expr formula, bool global)
+    : d_global(global)
 {
   d_funcs.push_back(func);
   d_formals.push_back(formals);
@@ -1388,11 +1398,10 @@ DefineFunctionRecCommand::DefineFunctionRecCommand(
 DefineFunctionRecCommand::DefineFunctionRecCommand(
     const std::vector<Expr>& funcs,
     const std::vector<std::vector<Expr>>& formals,
-    const std::vector<Expr>& formulas)
+    const std::vector<Expr>& formulas,
+    bool global)
+    : d_funcs(funcs), d_formals(formals), d_formulas(formulas), d_global(global)
 {
-  d_funcs.insert(d_funcs.end(), funcs.begin(), funcs.end());
-  d_formals.insert(d_formals.end(), formals.begin(), formals.end());
-  d_formulas.insert(d_formulas.end(), formulas.begin(), formulas.end());
 }
 
 const std::vector<Expr>& DefineFunctionRecCommand::getFunctions() const
@@ -1415,7 +1424,7 @@ void DefineFunctionRecCommand::invoke(SmtEngine* smtEngine)
 {
   try
   {
-    smtEngine->defineFunctionsRec(d_funcs, d_formals, d_formulas);
+    smtEngine->defineFunctionsRec(d_funcs, d_formals, d_formulas, d_global);
     d_commandStatus = CommandSuccess::instance();
   }
   catch (exception& e)
@@ -1450,12 +1459,12 @@ Command* DefineFunctionRecCommand::exportTo(
     Expr formula = d_formulas[i].exportTo(exprManager, variableMap);
     formulas.push_back(formula);
   }
-  return new DefineFunctionRecCommand(funcs, formals, formulas);
+  return new DefineFunctionRecCommand(funcs, formals, formulas, d_global);
 }
 
 Command* DefineFunctionRecCommand::clone() const
 {
-  return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas);
+  return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas, d_global);
 }
 
 std::string DefineFunctionRecCommand::getCommandName() const