Remove (unused) replacement of symbol-type symbols

Any such replacement would raise questions about type consistency. The code
would also have required updating to include various tag types.

Author: tautschnig

src/util/replace_symbol.cpp

@@ -110,7 +110,7 @@ bool replace_symbolt::replace(
 
 bool replace_symbolt::have_to_replace(const exprt &dest) const
 {
-  if(expr_map.empty() && type_map.empty())
+  if(expr_map.empty())
     return false;
 
   // first look at type
@@ -186,17 +186,6 @@ bool replace_symbolt::replace(typet &dest) const
       if(!replace(*it))
         result=false;
   }
-  else if(dest.id() == ID_symbol_type)
-  {
-    type_mapt::const_iterator it =
-      type_map.find(to_symbol_type(dest).get_identifier());
-
-    if(it!=type_map.end())
-    {
-      dest=it->second;
-      result=false;
-    }
-  }
   else if(dest.id()==ID_array)
   {
     array_typet &array_type=to_array_type(dest);
@@ -209,7 +198,7 @@ bool replace_symbolt::replace(typet &dest) const
 
 bool replace_symbolt::have_to_replace(const typet &dest) const
 {
-  if(expr_map.empty() && type_map.empty())
+  if(expr_map.empty())
     return false;
 
   if(dest.has_subtype())
@@ -251,11 +240,6 @@ bool replace_symbolt::have_to_replace(const typet &dest) const
       if(have_to_replace(*it))
         return true;
   }
-  else if(dest.id() == ID_symbol_type)
-  {
-    const irep_idt &identifier = to_symbol_type(dest).get_identifier();
-    return type_map.find(identifier) != type_map.end();
-  }
   else if(dest.id()==ID_array)
     return have_to_replace(to_array_type(dest).size());
 

src/util/replace_symbol.h

@@ -24,17 +24,10 @@ class replace_symbolt
 {
 public:
   typedef std::unordered_map<irep_idt, exprt> expr_mapt;
-  typedef std::unordered_map<irep_idt, typet> type_mapt;
 
   void insert(const class symbol_exprt &old_expr,
               const exprt &new_expr);
 
-  void insert(const irep_idt &identifier,
-                     const typet &type)
-  {
-    type_map.insert(std::pair<irep_idt, typet>(identifier, type));
-  }
-
   /// \brief Replaces a symbol with a constant
   /// If you are replacing symbols with constants in an l-value, you can
   /// create something that is not an l-value.   For example if your
@@ -66,23 +59,21 @@ class replace_symbolt
   void clear()
   {
     expr_map.clear();
-    type_map.clear();
   }
 
   bool empty() const
   {
-    return expr_map.empty() && type_map.empty();
+    return expr_map.empty();
   }
 
   std::size_t erase(const irep_idt &id)
   {
-    return expr_map.erase(id) + type_map.erase(id);
+    return expr_map.erase(id);
   }
 
   bool replaces_symbol(const irep_idt &id) const
   {
-    return expr_map.find(id) != expr_map.end() ||
-           type_map.find(id) != type_map.end();
+    return expr_map.find(id) != expr_map.end();
   }
 
   replace_symbolt();
@@ -100,7 +91,6 @@ class replace_symbolt
 
 protected:
   expr_mapt expr_map;
-  type_mapt type_map;
 
 protected:
   bool have_to_replace(const exprt &dest) const;