Move symbol manager to src/expr/ (#5420)

This is required since symbol manager will use context dependent data structures (in its cpp).

This is required since classes in src/parser/ are not allowed to include private headers.

5 files changed, 4 insertions, 185 deletions

diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index 7b55c0915..8e69da34b 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -55,8 +55,6 @@ set(libcvc4parser_src_files
   smt2/smt2_input.h
   smt2/sygus_input.cpp
   smt2/sygus_input.h
-  symbol_manager.cpp
-  symbol_manager.h
   tptp/TptpLexer.c
   tptp/TptpParser.c
   tptp/tptp.cpp
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 405935165..c762fc117 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -26,11 +26,11 @@
 
 #include "api/cvc4cpp.h"
 #include "expr/kind.h"
+#include "expr/symbol_manager.h"
 #include "expr/symbol_table.h"
 #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 {
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 9d62c12a3..bf205b13a 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -26,16 +26,16 @@
 
 namespace CVC4 {
 
-class Options;
-
 namespace api {
 class Solver;
 }
 
+class Options;
+class SymbolManager;
+
 namespace parser {
 
 class Parser;
-class SymbolManager;
 
 /**
  * A builder for input language parsers. <code>build()</code> can be
diff --git a/src/parser/symbol_manager.cpp b/src/parser/symbol_manager.cpp
deleted file mode 100644
index 32e17aea8..000000000
--- a/src/parser/symbol_manager.cpp
+++ /dev/null
@@ -1,77 +0,0 @@
-/*********************                                                        */
-/*! \file symbol_manager.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The symbol manager
- **/
-
-#include "parser/symbol_manager.h"
-
-namespace CVC4 {
-namespace parser {
-
-SymbolManager::SymbolManager(api::Solver* s) : d_solver(s) {}
-
-SymbolTable* SymbolManager::getSymbolTable() { return &d_symtabAllocated; }
-
-bool SymbolManager::setExpressionName(api::Term t,
-                                      const std::string& name,
-                                      bool isAssertion)
-{
-  if (d_names.find(t) != d_names.end())
-  {
-    // already named assertion
-    return false;
-  }
-  if (isAssertion)
-  {
-    d_namedAsserts.insert(t);
-  }
-  d_names[t] = name;
-  return true;
-}
-
-bool SymbolManager::getExpressionName(api::Term t,
-                                      std::string& name,
-                                      bool isAssertion) const
-{
-  std::map<api::Term, std::string>::const_iterator it = d_names.find(t);
-  if (it == d_names.end())
-  {
-    return false;
-  }
-  if (isAssertion)
-  {
-    // must be an assertion name
-    if (d_namedAsserts.find(t) == d_namedAsserts.end())
-    {
-      return false;
-    }
-  }
-  name = it->second;
-  return true;
-}
-
-void SymbolManager::getExpressionNames(const std::vector<api::Term>& ts,
-                                       std::vector<std::string>& names,
-                                       bool areAssertions) const
-{
-  for (const api::Term& t : ts)
-  {
-    std::string name;
-    if (getExpressionName(t, name, areAssertions))
-    {
-      names.push_back(name);
-    }
-  }
-}
-
-}  // namespace parser
-}  // namespace CVC4
diff --git a/src/parser/symbol_manager.h b/src/parser/symbol_manager.h
deleted file mode 100644
index 20b0c80e4..000000000
--- a/src/parser/symbol_manager.h
+++ /dev/null
@@ -1,102 +0,0 @@
-/*********************                                                        */
-/*! \file symbol_manager.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The symbol manager
- **/
-
-#include "cvc4parser_public.h"
-
-#ifndef CVC4__PARSER__SYMBOL_MANAGER_H
-#define CVC4__PARSER__SYMBOL_MANAGER_H
-
-#include <map>
-#include <set>
-#include <string>
-
-#include "api/cvc4cpp.h"
-#include "expr/symbol_table.h"
-
-namespace CVC4 {
-namespace parser {
-
-/**
- * Symbol manager, which manages:
- * (1) The symbol table used by the parser,
- * (2) Information related to the (! ... :named s) feature in SMT-LIB version 2.
- */
-class CVC4_PUBLIC SymbolManager
-{
- public:
-  SymbolManager(api::Solver* s);
-  ~SymbolManager() {}
-  /** Get the underlying symbol table */
-  SymbolTable* getSymbolTable();
-  //---------------------------- named expressions
-  /** Set name of term t to name
-   *
-   * @param t The term to name
-   * @param name The given name
-   * @param isAssertion Whether t is being given a name in an assertion
-   * context. In particular, this is true if and only if there was an assertion
-   * command of the form (assert (! t :named name)).
-   * @return true if the name was set. This method may return false if t
-   * already has a name.
-   */
-  bool setExpressionName(api::Term t,
-                         const std::string& name,
-                         bool isAssertion = false);
-  /** Get name for term t
-   *
-   * @param t The term
-   * @param name The argument to update with the name of t
-   * @param isAssertion Whether we only wish to get the assertion name of t
-   * @return true if t has a name. If so, name is updated to that name.
-   * Otherwise, name is unchanged.
-   */
-  bool getExpressionName(api::Term t,
-                         std::string& name,
-                         bool isAssertion = false) const;
-  /**
-   * Convert list of terms to list of names. This adds to names the names of
-   * all terms in ts that has names. Terms that do not have names are not
-   * included.
-   *
-   * Notice that we do not distinguish what terms among those in ts have names.
-   * If the caller of this method wants more fine-grained information about what
-   * specific terms had names, then use the more fine grained interface above,
-   * per term.
-   *
-   * @param ts The terms
-   * @param names The name list
-   * @param areAssertions Whether we only wish to include assertion names
-   */
-  void getExpressionNames(const std::vector<api::Term>& ts,
-                          std::vector<std::string>& names,
-                          bool areAssertions = false) const;
-  //---------------------------- end named expressions
-
- private:
-  /** The API Solver object. */
-  api::Solver* d_solver;
-  /**
-   * The declaration scope that is "owned" by this symbol manager.
-   */
-  SymbolTable d_symtabAllocated;
-  /** Map terms to names */
-  std::map<api::Term, std::string> d_names;
-  /** The set of terms with assertion names */
-  std::set<api::Term> d_namedAsserts;
-};
-
-}  // namespace parser
-}  // namespace CVC4
-
-#endif /* CVC4__PARSER__SYMBOL_MANAGER_H */