Add symbol manager (#5380)

This add the symbol manager class, which is a Term-level utility, separate of the API. This class manages things like expression and assertion names, which is intentionally done outside the solver.

The symbol manager is intended to live at the same level as the Solver. When parsing input, the symbol manager will be used to model any interaction of e.g. named expressions and assertions. It also stores the symbol table of the parser.

This PR adds the basic interface for the symbol manager and passes it to the parser.

Later PRs will migrate the functionality for named expression out of e.g. SmtEngine and into SymbolManager. Commands will take Solver+SymbolManager instead of Solver. This will allow the parser to be fully migrated to the new API.

Marking "complex" since this impacts further design of the parser and the code that lives in src/main.

FYI @4tXJ7f

1 files changed, 8 insertions, 8 deletions

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 260ab33cf..405935165 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -30,6 +30,7 @@
 #include "parser/input.h"
 #include "parser/parse_op.h"
 #include "parser/parser_exception.h"
+#include "parser/symbol_manager.h"
 #include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
@@ -109,16 +110,13 @@ private:
  Input* d_input;
 
  /**
-  * The declaration scope that is "owned" by this parser.  May or
-  * may not be the current declaration scope in use.
+  * Reference to the symbol manager, which manages the symbol table used by
+  * this parser.
   */
- SymbolTable d_symtabAllocated;
+ SymbolManager* d_symman;
 
  /**
-  * This current symbol table used by this parser.  Initially points
-  * to d_symtabAllocated, but can be changed (making this parser
-  * delegate its definitions and lookups to another parser).
-  * See useDeclarationsFrom().
+  * This current symbol table used by this parser, from symbol manager.
   */
  SymbolTable* d_symtab;
 
@@ -215,7 +213,8 @@ protected:
   * @attention The parser takes "ownership" of the given
   * input and will delete it on destruction.
   *
-  * @param the solver API object
+  * @param solver solver API object
+  * @param symm reference to the symbol manager
   * @param input the parser input
   * @param strictMode whether to incorporate strict(er) compliance checks
   * @param parseOnly whether we are parsing only (and therefore certain checks
@@ -223,6 +222,7 @@ protected:
   * unimplementedFeature())
   */
  Parser(api::Solver* solver,
+        SymbolManager* sm,
         Input* input,
         bool strictMode = false,
         bool parseOnly = false);