Remove definition of propagationt

This was just a wrapper around a map, which was making access to the map
heavier without any benefit.

Author: romainbrenguier

src/goto-instrument/accelerate/scratch_program.cpp

@@ -35,7 +35,7 @@ bool scratch_programt::check_sat(bool do_slice)
   output(ns, "scratch", std::cout);
 #endif
 
-  goto_symex_statet::propagationt::valuest constants;
+  std::map<irep_idt, exprt> constants;
 
   symex.symex_with_state(symex_state, functions, symex_symbol_table);
 

src/goto-symex/goto_symex_state.cpp

@@ -227,9 +227,9 @@ void goto_symex_statet::assignment(
   // for value propagation -- the RHS is L2
 
   if(!is_shared && record_value && goto_symex_is_constantt()(rhs))
-    propagation.values[l1_identifier]=rhs;
+    propagation[l1_identifier] = rhs;
   else
-    propagation.remove(l1_identifier);
+    propagation.erase(l1_identifier);
 
   {
     // update value sets
@@ -322,10 +322,9 @@ void goto_symex_statet::rename(
       {
         // We also consider propagation if we go up to L2.
         // L1 identifiers are used for propagation!
-        propagationt::valuest::const_iterator p_it=
-          propagation.values.find(ssa.get_identifier());
+        auto p_it = propagation.find(ssa.get_identifier());
 
-        if(p_it!=propagation.values.end())
+        if(p_it != propagation.end())
           expr=p_it->second; // already L2
         else
           set_ssa_indices(ssa, ns, L2);

src/goto-symex/goto_symex_state.h

@@ -65,17 +65,8 @@ class goto_symex_statet final
   symex_level1t level1;
   symex_level2t level2;
 
-  // this maps L1 names to (L2) constants
-  class propagationt
-  {
-  public:
-    typedef std::map<irep_idt, exprt> valuest;
-    valuest values;
-    void remove(const irep_idt &identifier)
-    {
-      values.erase(identifier);
-    }
-  } propagation;
+  // Map L1 names to (L2) constants
+  std::map<irep_idt, exprt> propagation;
 
   enum levelt { L0=0, L1=1, L2=2 };
 
@@ -124,7 +115,7 @@ class goto_symex_statet final
     value_sett value_set;
     guardt guard;
     symex_targett::sourcet source;
-    propagationt propagation;
+    std::map<irep_idt, exprt> propagation;
     unsigned atomic_section_id;
     std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;
     unsigned total_vccs, remaining_vccs;

src/goto-symex/symex_dead.cpp

@@ -49,7 +49,7 @@ void goto_symext::symex_dead(statet &state)
   const irep_idt &l1_identifier=ssa_lhs.get_identifier();
 
   // prevent propagation
-  state.propagation.remove(l1_identifier);
+  state.propagation.erase(l1_identifier);
 
   // L2 renaming
   if(state.level2.current_names.find(l1_identifier)!=

src/goto-symex/symex_decl.cpp

@@ -63,7 +63,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   }
 
   // prevent propagation
-  state.propagation.remove(l1_identifier);
+  state.propagation.erase(l1_identifier);
 
   // L2 renaming
   // inlining may yield multiple declarations of the same identifier

src/goto-symex/symex_goto.cpp

@@ -413,21 +413,19 @@ void goto_symext::phi_function(
     exprt goto_state_rhs=*it, dest_state_rhs=*it;
 
     {
-      goto_symex_statet::propagationt::valuest::const_iterator p_it=
-        goto_state.propagation.values.find(l1_identifier);
+      const auto p_it = goto_state.propagation.find(l1_identifier);
 
-      if(p_it!=goto_state.propagation.values.end())
+      if(p_it != goto_state.propagation.end())
         goto_state_rhs=p_it->second;
       else
         to_ssa_expr(goto_state_rhs).set_level_2(
           goto_state.level2_current_count(l1_identifier));
     }
 
     {
-      goto_symex_statet::propagationt::valuest::const_iterator p_it=
-        dest_state.propagation.values.find(l1_identifier);
+      const auto p_it = dest_state.propagation.find(l1_identifier);
 
-      if(p_it!=dest_state.propagation.values.end())
+      if(p_it != dest_state.propagation.end())
         dest_state_rhs=p_it->second;
       else
         to_ssa_expr(dest_state_rhs).set_level_2(