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

5 files changed, 36 insertions, 10 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index c91b0455c..a56210fb1 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -50,6 +50,7 @@ void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString
 
 CommandExecutor::CommandExecutor(Options& options)
     : d_solver(new api::Solver(&options)),
+      d_symman(new parser::SymbolManager(d_solver.get())),
       d_smtEngine(d_solver->getSmtEngine()),
       d_options(options),
       d_stats("driver"),
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index d7899020e..c3c310380 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -21,6 +21,7 @@
 #include "api/cvc4cpp.h"
 #include "expr/expr_manager.h"
 #include "options/options.h"
+#include "parser/symbol_manager.h"
 #include "smt/smt_engine.h"
 #include "util/statistics_registry.h"
 
@@ -28,10 +29,6 @@ namespace CVC4 {
 
 class Command;
 
-namespace api {
-class Solver;
-}
-
 namespace main {
 
 class CommandExecutor
@@ -40,7 +37,22 @@ class CommandExecutor
   std::string d_lastStatistics;
 
  protected:
+  /**
+   * The solver object, which is allocated by this class and is used for
+   * executing most commands (e.g. check-sat).
+   */
   std::unique_ptr<api::Solver> d_solver;
+  /**
+   * The symbol manager, which is allocated by this class. This manages
+   * all things related to definitions of symbols and their impact on behaviors
+   * for commands (e.g. get-unsat-core, get-model, get-assignment), as well
+   * as tracking expression names. Note the symbol manager is independent from
+   * the parser, which uses this symbol manager given a text input.
+   *
+   * Certain commands (e.g. reset-assertions) have a specific impact on the
+   * symbol manager.
+   */
+  std::unique_ptr<parser::SymbolManager> d_symman;
   SmtEngine* d_smtEngine;
   Options& d_options;
   StatisticsRegistry d_stats;
@@ -67,6 +79,9 @@ class CommandExecutor
   /** Get a pointer to the solver object owned by this CommandExecutor. */
   api::Solver* getSolver() { return d_solver.get(); }
 
+  /** Get a pointer to the symbol manager owned by this CommandExecutor */
+  parser::SymbolManager* getSymbolManager() { return d_symman.get(); }
+
   api::Result getResult() const { return d_result; }
   void reset();
 
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 9fff51b93..673c5ddd9 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -213,7 +213,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
       }
-      InteractiveShell shell(pExecutor->getSolver());
+      InteractiveShell shell(pExecutor->getSolver(),
+                             pExecutor->getSymbolManager());
       if(opts.getInteractivePrompt()) {
         Message() << Configuration::getPackageName()
                   << " " << Configuration::getVersionString();
@@ -258,7 +259,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         // pExecutor->doCommand(cmd);
       }
 
-      ParserBuilder parserBuilder(pExecutor->getSolver(), filename, opts);
+      ParserBuilder parserBuilder(pExecutor->getSolver(),
+                                  pExecutor->getSymbolManager(),
+                                  filename,
+                                  opts);
 
       if( inputFromStdin ) {
 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
@@ -411,7 +415,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         pExecutor->doCommand(cmd);
       }
 
-      ParserBuilder parserBuilder(pExecutor->getSolver(), filename, opts);
+      ParserBuilder parserBuilder(pExecutor->getSolver(),
+                                  pExecutor->getSymbolManager(),
+                                  filename,
+                                  opts);
 
       if( inputFromStdin ) {
 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index b798d03ee..8d482b08e 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -43,6 +43,7 @@
 #include "parser/input.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
+#include "parser/symbol_manager.h"
 #include "smt/command.h"
 #include "theory/logic_info.h"
 
@@ -83,13 +84,14 @@ static set<string> s_declarations;
 
 #endif /* HAVE_LIBEDITLINE */
 
-InteractiveShell::InteractiveShell(api::Solver* solver)
+InteractiveShell::InteractiveShell(api::Solver* solver,
+                                   parser::SymbolManager* sm)
     : d_options(solver->getOptions()),
       d_in(*d_options.getIn()),
       d_out(*d_options.getOutConst()),
       d_quit(false)
 {
-  ParserBuilder parserBuilder(solver, INPUT_FILENAME, d_options);
+  ParserBuilder parserBuilder(solver, sm, INPUT_FILENAME, d_options);
   /* Create parser with bogus input. */
   d_parser = parserBuilder.withStringInput("").build();
   if(d_options.wasSetByUserForceLogicString()) {
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 36e6068a4..b00f8a8f4 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -33,6 +33,7 @@ class Solver;
 
 namespace parser {
   class Parser;
+  class SymbolManager;
 }/* CVC4::parser namespace */
 
 class CVC4_PUBLIC InteractiveShell
@@ -50,7 +51,7 @@ class CVC4_PUBLIC InteractiveShell
   static const unsigned s_historyLimit = 500;
 
 public:
- InteractiveShell(api::Solver* solver);
+ InteractiveShell(api::Solver* solver, parser::SymbolManager* sm);
 
  /**
   * Close out the interactive session.