From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 2 Nov 2020 13:01:19 +0000 (-0600)
Subject: Avoid dynamic allocation in symbol table implementation (#5368)
X-Git-Tag: cvc5-1.0.0~2642
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d8c692850d8d7d9963c9c207e1b20cac1ec24635;p=cvc5.git

Avoid dynamic allocation in symbol table implementation (#5368)

Encountered this while debugging the new symbol manager. This is not essential but probably a good idea to refactor.
---

diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 888434665..3d01b778c 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -342,16 +342,13 @@ class SymbolTable::Implementation {
  public:
   Implementation()
       : d_context(),
-        d_exprMap(new (true) CDHashMap<string, api::Term>(&d_context)),
-        d_typeMap(new (true) TypeMap(&d_context))
+        d_exprMap(&d_context),
+        d_typeMap(&d_context),
+        d_overload_trie(&d_context)
   {
-    d_overload_trie = new OverloadedTypeTrie(&d_context);
   }
 
   ~Implementation() {
-    d_exprMap->deleteSelf();
-    d_typeMap->deleteSelf();
-    delete d_overload_trie;
   }
 
   bool bind(const string& name, api::Term obj, bool levelZero, bool doOverload);
@@ -388,17 +385,17 @@ class SymbolTable::Implementation {
   Context d_context;
 
   /** A map for expressions. */
-  CDHashMap<string, api::Term>* d_exprMap;
+  CDHashMap<string, api::Term> d_exprMap;
 
   /** A map for types. */
   using TypeMap = CDHashMap<string, std::pair<vector<api::Sort>, api::Sort>>;
-  TypeMap* d_typeMap;
+  TypeMap d_typeMap;
 
   //------------------------ operator overloading
   // the null expression
   api::Term d_nullTerm;
   // overloaded type trie, stores all information regarding overloading
-  OverloadedTypeTrie* d_overload_trie;
+  OverloadedTypeTrie d_overload_trie;
   /** bind with overloading
    * This is called whenever obj is bound to name where overloading symbols is
    * allowed. If a symbol is previously bound to that name, it marks both as
@@ -420,21 +417,21 @@ bool SymbolTable::Implementation::bind(const string& name,
     }
   }
   if (levelZero) {
-    d_exprMap->insertAtContextLevelZero(name, obj);
+    d_exprMap.insertAtContextLevelZero(name, obj);
   } else {
-    d_exprMap->insert(name, obj);
+    d_exprMap.insert(name, obj);
   }
   return true;
 }
 
 bool SymbolTable::Implementation::isBound(const string& name) const {
-  return d_exprMap->find(name) != d_exprMap->end();
+  return d_exprMap.find(name) != d_exprMap.end();
 }
 
 api::Term SymbolTable::Implementation::lookup(const string& name) const
 {
   Assert(isBound(name));
-  api::Term expr = (*d_exprMap->find(name)).second;
+  api::Term expr = (*d_exprMap.find(name)).second;
   if (isOverloadedFunction(expr)) {
     return d_nullTerm;
   } else {
@@ -447,10 +444,9 @@ void SymbolTable::Implementation::bindType(const string& name,
                                            bool levelZero)
 {
   if (levelZero) {
-    d_typeMap->insertAtContextLevelZero(name,
-                                        make_pair(vector<api::Sort>(), t));
+    d_typeMap.insertAtContextLevelZero(name, make_pair(vector<api::Sort>(), t));
   } else {
-    d_typeMap->insert(name, make_pair(vector<api::Sort>(), t));
+    d_typeMap.insert(name, make_pair(vector<api::Sort>(), t));
   }
 }
 
@@ -470,19 +466,20 @@ void SymbolTable::Implementation::bindType(const string& name,
     Debug("sort") << "], " << t << ")" << endl;
   }
   if (levelZero) {
-    d_typeMap->insertAtContextLevelZero(name, make_pair(params, t));
+    d_typeMap.insertAtContextLevelZero(name, make_pair(params, t));
   } else {
-    d_typeMap->insert(name, make_pair(params, t));
+    d_typeMap.insert(name, make_pair(params, t));
   }
 }
 
 bool SymbolTable::Implementation::isBoundType(const string& name) const {
-  return d_typeMap->find(name) != d_typeMap->end();
+  return d_typeMap.find(name) != d_typeMap.end();
 }
 
 api::Sort SymbolTable::Implementation::lookupType(const string& name) const
 {
-  pair<vector<api::Sort>, api::Sort> p = (*d_typeMap->find(name)).second;
+  std::pair<std::vector<api::Sort>, api::Sort> p =
+      (*d_typeMap.find(name)).second;
   PrettyCheckArgument(p.first.size() == 0, name,
                       "type constructor arity is wrong: "
                       "`%s' requires %u parameters but was provided 0",
@@ -494,7 +491,7 @@ api::Sort SymbolTable::Implementation::lookupType(
     const string& name, const vector<api::Sort>& params) const
 {
   std::pair<std::vector<api::Sort>, api::Sort> p =
-      (*d_typeMap->find(name)).second;
+      (*d_typeMap.find(name)).second;
   PrettyCheckArgument(p.first.size() == params.size(), params,
                       "type constructor arity is wrong: "
                       "`%s' requires %u parameters but was provided %u",
@@ -535,7 +532,8 @@ api::Sort SymbolTable::Implementation::lookupType(
 }
 
 size_t SymbolTable::Implementation::lookupArity(const string& name) {
-  pair<vector<api::Sort>, api::Sort> p = (*d_typeMap->find(name)).second;
+  std::pair<std::vector<api::Sort>, api::Sort> p =
+      (*d_typeMap.find(name)).second;
   return p.first.size();
 }
 
@@ -559,29 +557,30 @@ void SymbolTable::Implementation::reset() {
 
 bool SymbolTable::Implementation::isOverloadedFunction(api::Term fun) const
 {
-  return d_overload_trie->isOverloadedFunction(fun);
+  return d_overload_trie.isOverloadedFunction(fun);
 }
 
 api::Term SymbolTable::Implementation::getOverloadedConstantForType(
     const std::string& name, api::Sort t) const
 {
-  return d_overload_trie->getOverloadedConstantForType(name, t);
+  return d_overload_trie.getOverloadedConstantForType(name, t);
 }
 
 api::Term SymbolTable::Implementation::getOverloadedFunctionForTypes(
     const std::string& name, const std::vector<api::Sort>& argTypes) const
 {
-  return d_overload_trie->getOverloadedFunctionForTypes(name, argTypes);
+  return d_overload_trie.getOverloadedFunctionForTypes(name, argTypes);
 }
 
 bool SymbolTable::Implementation::bindWithOverloading(const string& name,
                                                       api::Term obj)
 {
-  CDHashMap<string, api::Term>::const_iterator it = d_exprMap->find(name);
-  if (it != d_exprMap->end()) {
+  CDHashMap<string, api::Term>::const_iterator it = d_exprMap.find(name);
+  if (it != d_exprMap.end())
+  {
     const api::Term& prev_bound_obj = (*it).second;
     if (prev_bound_obj != obj) {
-      return d_overload_trie->bind(name, prev_bound_obj, obj);
+      return d_overload_trie.bind(name, prev_bound_obj, obj);
     }
   }
   return true;