Move increase_generation onto goto_statet

This enables us to more conveniently allocate a new generation on a non-current
state, such as a state copy that will be used on a pending branch.

No behavioural change.

Author: smowton

src/goto-symex/goto_state.cpp

@@ -20,3 +20,17 @@ void goto_statet::output_propagation_map(std::ostream &out)
     out << name_value.first << " <- " << format(name_value.second) << "\n";
   }
 }
+
+std::size_t goto_statet::increase_generation(
+  const irep_idt l1_identifier,
+  const ssa_exprt &lhs,
+  std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider)
+{
+  auto current_emplace_res =
+    level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0));
+
+  current_emplace_res.first->second.second =
+    fresh_l2_name_provider(l1_identifier);
+
+  return current_emplace_res.first->second.second;
+}

src/goto-symex/goto_state.h

@@ -74,6 +74,11 @@ class goto_statet
     : guard(true_exprt(), guard_manager)
   {
   }
+
+  std::size_t increase_generation(
+    const irep_idt l1_identifier,
+    const ssa_exprt &lhs,
+    std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider);
 };
 
 #endif // CPROVER_GOTO_SYMEX_GOTO_STATE_H

src/goto-symex/goto_symex_state.cpp

@@ -459,22 +459,6 @@ bool goto_symex_statet::l2_thread_read_encoding(
   return true;
 }
 
-/// Allocates a fresh L2 name for the given L1 identifier, and makes it the
-/// latest generation on this path.
-/// \return the newly allocated generation number
-std::size_t goto_symex_statet::increase_generation(
-  const irep_idt l1_identifier,
-  const ssa_exprt &lhs)
-{
-  auto current_emplace_res =
-    level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0));
-
-  current_emplace_res.first->second.second =
-    fresh_l2_name_provider(l1_identifier);
-
-  return current_emplace_res.first->second.second;
-}
-
 /// Allocates a fresh L2 name for the given L1 identifier, and makes it the
 /// latest generation on this path. Does nothing if there isn't an expression
 /// keyed by the l1 identifier.

src/goto-symex/goto_symex_state.h

@@ -208,7 +208,11 @@ class goto_symex_statet final : public goto_statet
   /// Allocates a fresh L2 name for the given L1 identifier, and makes it the
   //  latest generation on this path.
   std::size_t
-  increase_generation(const irep_idt l1_identifier, const ssa_exprt &lhs);
+  increase_generation(const irep_idt l1_identifier, const ssa_exprt &lhs)
+  {
+    return goto_statet::increase_generation(
+      l1_identifier, lhs, fresh_l2_name_provider);
+  }
 
   /// Increases the generation of the L1 identifier. Does nothing if there
   /// isn't an expression keyed by it.