Refactor get_identifier as member function of decision procedure

This already reads large parts of the internal state, so the refactor
cuts down on parameters passed and enables use of other member
functions.

Author: thomasspriggs

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -343,13 +343,8 @@ exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
   return expr;
 }
 
-static optionalt<smt_termt> get_identifier(
-  const exprt &expr,
-  const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
-    &expression_handle_identifiers,
-  const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
-    &expression_identifiers,
-  const namespacet &ns)
+optionalt<smt_termt>
+smt2_incremental_decision_proceduret::get_identifier(const exprt &expr) const
 {
   // Lookup the non-lowered form first.
   const auto handle_find_result = expression_handle_identifiers.find(expr);
@@ -457,23 +452,13 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
   auto descriptor = [&]() -> optionalt<smt_termt> {
     if(const auto index_expr = expr_try_dynamic_cast<index_exprt>(expr))
     {
-      const auto array = get_identifier(
-        index_expr->array(),
-        expression_handle_identifiers,
-        expression_identifiers,
-        ns);
-      const auto index = get_identifier(
-        index_expr->index(),
-        expression_handle_identifiers,
-        expression_identifiers,
-        ns);
+      const auto array = get_identifier(index_expr->array());
+      const auto index = get_identifier(index_expr->index());
       if(!array || !index)
         return {};
       return smt_array_theoryt::select(*array, *index);
     }
-    if(
-      auto identifier_descriptor = get_identifier(
-        expr, expression_handle_identifiers, expression_identifiers, ns))
+    if(auto identifier_descriptor = get_identifier(expr))
     {
       return identifier_descriptor;
     }

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -98,6 +98,7 @@ class smt2_incremental_decision_proceduret final
   /// possible expression forms by expressing these in terms of the remaining
   /// language features.
   exprt lower(exprt expression);
+  optionalt<smt_termt> get_identifier(const exprt &expr) const;
 
   /// Namespace for looking up the expressions which symbol_exprts relate to.
   /// This includes the symbols defined outside of the decision procedure but