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, 2 insertions, 0 deletions

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 681404efa..0bdf23dcd 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -812,6 +812,8 @@ public:
     d_globalDeclarations = flag;
   }
 
+  bool getGlobalDeclarations() { return d_globalDeclarations; }
+
   inline SymbolTable* getSymbolTable() const {
     return d_symtab;
   }