Split expression names from SmtEngine (#4832)

Towards splitting SmtEngine / deleting SmtEnginePrivate.

5 files changed, 112 insertions, 29 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 61261afe4..17c4a26f5 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -230,6 +230,8 @@ libcvc4_add_sources(
   smt/dump.h
   smt/dump_manager.cpp
   smt/dump_manager.h
+  smt/expr_names.cpp
+  smt/expr_names.h
   smt/listeners.cpp
   smt/listeners.h
   smt/logic_exception.h
diff --git a/src/smt/expr_names.cpp b/src/smt/expr_names.cpp
new file mode 100644
index 000000000..78c0346e4
--- /dev/null
+++ b/src/smt/expr_names.cpp
@@ -0,0 +1,39 @@
+/*********************                                                        */
+/*! \file expr_names.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 Utility for maintaining expression names.
+ **/
+
+#include "smt/expr_names.h"
+
+namespace CVC4 {
+namespace smt {
+
+ExprNames::ExprNames(context::UserContext* u)
+    : d_exprNames(u)
+{
+}
+
+void ExprNames::setExpressionName(const Node& e, const std::string& name) {
+  d_exprNames[e] = name;
+}
+
+bool ExprNames::getExpressionName(const Node& e, std::string& name) const {
+  auto it = d_exprNames.find(e);
+  if(it!=d_exprNames.end()) {
+    name = (*it).second;
+    return true;
+  }
+  return false;
+}
+
+}  // namespace smt
+}  // namespace CVC4
diff --git a/src/smt/expr_names.h b/src/smt/expr_names.h
new file mode 100644
index 000000000..b4bb9993e
--- /dev/null
+++ b/src/smt/expr_names.h
@@ -0,0 +1,59 @@
+/*********************                                                        */
+/*! \file expr_names.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 Utility for maintaining expression names.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__EXPR_NAMES_H
+#define CVC4__SMT__EXPR_NAMES_H
+
+#include <string>
+
+#include "context/cdhashmap.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace smt {
+
+/**
+ * This utility is responsible for maintaining names for expressions.
+ */
+class ExprNames
+{
+ public:
+  ExprNames(context::UserContext* u);
+  /**
+   * Get expression name.
+   *
+   * Return true if given expression has a name in the current context.
+   * If it returns true, the name of expression 'e' is stored in 'name'.
+   */
+  bool getExpressionName(const Node& e, std::string& name) const;
+
+  /**
+   * Set name of given expression 'e' to 'name'.
+   *
+   * This information is user-context-dependent.
+   * If 'e' already has a name, it is overwritten.
+   */
+  void setExpressionName(const Node& e, const std::string& name);
+
+ private:
+  /** mapping from expressions to name */
+  context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames;
+};
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f114dba7c..6d1e7ffbc 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -82,6 +82,7 @@
 #include "prop/prop_engine.h"
 #include "smt/abduction_solver.h"
 #include "smt/abstract_values.h"
+#include "smt/expr_names.h"
 #include "smt/command.h"
 #include "smt/defined_function.h"
 #include "smt/dump_manager.h"
@@ -176,10 +177,6 @@ class SmtEnginePrivate
   /** Process assertions module */
   ProcessAssertions d_processor;
 
-  //------------------------------- expression names
-  /** mapping from expressions to name */
-  context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames;
-  //------------------------------- end expression names
  public:
   IteSkolemMap& getIteSkolemMap() { return d_assertions.getIteSkolemMap(); }
 
@@ -214,7 +211,6 @@ class SmtEnginePrivate
         d_assertions(),
         d_assertionsProcessed(smt.getUserContext(), false),
         d_processor(smt, *smt.getResourceManager()),
-        d_exprNames(smt.getUserContext()),
         d_iteRemover(smt.getUserContext()),
         d_sygusConjectureStale(smt.getUserContext(), true)
   {
@@ -299,24 +295,6 @@ class SmtEnginePrivate
     Assert(d_assertions.size() == 0);
     return applySubstitutions(n).toExpr();
   }
-
-  //------------------------------- expression names
-  // implements setExpressionName, as described in smt_engine.h
-  void setExpressionName(Expr e, std::string name) {
-    d_exprNames[Node::fromExpr(e)] = name;
-  }
-
-  // implements getExpressionName, as described in smt_engine.h
-  bool getExpressionName(Expr e, std::string& name) const {
-    context::CDHashMap< Node, std::string, NodeHashFunction >::const_iterator it = d_exprNames.find(e);
-    if(it!=d_exprNames.end()) {
-      name = (*it).second;
-      return true;
-    }else{
-      return false;
-    }
-  }
-  //------------------------------- end expression names
 };/* class SmtEnginePrivate */
 
 }/* namespace CVC4::smt */
@@ -328,6 +306,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_exprManager(em),
       d_nodeManager(d_exprManager->getNodeManager()),
       d_absValues(new AbstractValues(d_nodeManager)),
+      d_exprNames(new ExprNames(d_userContext.get())),
       d_dumpm(new DumpManager(d_userContext.get())),
       d_routListener(new ResourceOutListener(*this)),
       d_snmListener(new SmtNodeManagerListener(*d_dumpm.get())),
@@ -578,6 +557,7 @@ SmtEngine::~SmtEngine()
 #endif
 
     d_absValues.reset(nullptr);
+    d_exprNames.reset(nullptr);
     d_dumpm.reset(nullptr);
 
     d_theoryEngine.reset(nullptr);
@@ -3219,13 +3199,13 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
   return SExpr::parseAtom(d_options.getOption(key));
 }
 
-bool SmtEngine::getExpressionName(Expr e, std::string& name) const {
-  return d_private->getExpressionName(e, name);
+bool SmtEngine::getExpressionName(const Node& e, std::string& name) const {
+  return d_exprNames->getExpressionName(e, name);
 }
 
-void SmtEngine::setExpressionName(Expr e, const std::string& name) {
+void SmtEngine::setExpressionName(const Node& e, const std::string& name) {
   Trace("smt-debug") << "Set expression name " << e << " to " << name << std::endl;
-  d_private->setExpressionName(e,name);
+  d_exprNames->setExpressionName(e,name);
 }
 
 Options& SmtEngine::getOptions() { return d_options; }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 99b993e7b..f51b6759b 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -93,6 +93,7 @@ namespace prop {
 namespace smt {
 /** Utilities */
 class AbstractValues;
+class ExprNames;
 class DumpManager;
 class ResourceOutListener;
 class SmtNodeManagerListener;
@@ -858,7 +859,7 @@ class CVC4_PUBLIC SmtEngine
    * Return true if given expressoion has a name in the current context.
    * If it returns true, the name of expression 'e' is stored in 'name'.
    */
-  bool getExpressionName(Expr e, std::string& name) const;
+  bool getExpressionName(const Node& e, std::string& name) const;
 
   /**
    * Set name of given expression 'e' to 'name'.
@@ -866,7 +867,7 @@ class CVC4_PUBLIC SmtEngine
    * This information is user-context-dependent.
    * If 'e' already has a name, it is overwritten.
    */
-  void setExpressionName(Expr e, const std::string& name);
+  void setExpressionName(const Node& e, const std::string& name);
 
   /** Get the options object (const and non-const versions) */
   Options& getOptions();
@@ -1121,6 +1122,8 @@ class CVC4_PUBLIC SmtEngine
   NodeManager* d_nodeManager;
   /** Abstract values */
   std::unique_ptr<smt::AbstractValues> d_absValues;
+  /** Expression names */
+  std::unique_ptr<smt::ExprNames> d_exprNames;
   /** The dump manager */
   std::unique_ptr<smt::DumpManager> d_dumpm;
   /** Resource out listener */