let_count_idt is now a struct

Author: Daniel Kroening

src/solvers/smt2/smt2_conv.cpp

@@ -4759,12 +4759,12 @@ exprt smt2_convt::letify_rec(
   exprt current=let_order[i];
   assert(map.find(current)!=map.end());
 
-  if(map.find(current)->second.first<LET_COUNT)
+  if(map.find(current)->second.count < LET_COUNT)
     return letify_rec(expr, let_order, map, i+1);
 
   let_exprt let;
 
-  let.symbol() = map.find(current)->second.second;
+  let.symbol() = map.find(current)->second.let_symbol;
   let.value() = substitute_let(current, map);
   let.where() = letify_rec(expr, let_order, map, i+1);
 
@@ -4781,7 +4781,7 @@ void smt2_convt::collect_bindings(
   if(it!=map.end())
   {
     let_count_idt &count_id=it->second;
-    ++(count_id.first);
+    ++(count_id.count);
     return;
   }
 
@@ -4797,7 +4797,7 @@ void smt2_convt::collect_bindings(
   symbol_exprt let=
     symbol_exprt("_let_"+std::to_string(++let_id_count), expr.type());
 
-  map.insert(std::make_pair(expr, std::make_pair(1, let)));
+  map.insert(std::make_pair(expr, let_count_idt(1, let)));
 
   let_order.push_back(expr);
 }

src/solvers/smt2/smt2_conv.h

@@ -170,7 +170,17 @@ class smt2_convt:public prop_convt
   void find_symbols_rec(const typet &type, std::set<irep_idt> &recstack);
 
   // letification
-  typedef std::pair<unsigned, symbol_exprt> let_count_idt;
+  struct let_count_idt
+  {
+    let_count_idt(std::size_t _count, const symbol_exprt &_let_symbol)
+      : count(_count), let_symbol(_let_symbol)
+    {
+    }
+
+    std::size_t count;
+    symbol_exprt let_symbol;
+  };
+
   typedef std::unordered_map<exprt, let_count_idt, irep_hash> seen_expressionst;
   unsigned let_id_count;
   static const unsigned LET_COUNT=2;
@@ -185,10 +195,9 @@ class smt2_convt:public prop_convt
     void operator()(exprt &expr)
     {
       seen_expressionst::const_iterator it=let_map.find(expr);
-      if(it!=let_map.end() &&
-         it->second.first>=LET_COUNT)
+      if(it != let_map.end() && it->second.count >= LET_COUNT)
       {
-        symbol_exprt symb=it->second.second;
+        const symbol_exprt &symb = it->second.let_symbol;
         expr=symb;
       }
     }