Add a has method to symex_level1t

This will be used when we make the map for old L1 name be a
symex_level1t as well.

Author: romainbrenguier

src/goto-symex/renaming_level.cpp

@@ -78,6 +78,11 @@ optionalt<std::pair<ssa_exprt, unsigned>> symex_level1t::insert_or_replace(
   return {};
 }
 
+bool symex_level1t::has(const renamedt<ssa_exprt, L0> &ssa) const
+{
+  return current_names.has_key(ssa.get().get_identifier());
+}
+
 renamedt<ssa_exprt, L1> symex_level1t::
 operator()(renamedt<ssa_exprt, L0> l0_expr) const
 {

src/goto-symex/renaming_level.h

@@ -65,6 +65,9 @@ struct symex_level1t
   optionalt<std::pair<ssa_exprt, unsigned>>
   insert_or_replace(const renamedt<ssa_exprt, L0> &ssa, unsigned index);
 
+  /// \return true if \p ssa has an associated index
+  bool has(const renamedt<ssa_exprt, L0> &ssa) const;
+
   /// \return an SSA expression similar to \p l0_expr where the L1 tag has been
   ///   set to the value in \ref current_names of the l1 object identifier of
   ///   \p l0_expr