replace recursion in letify_rec by loop

This avoids stack overflow in the case of expressions with many unique
subexpressions.  PR #4395 is an exemplar.

Author: Daniel Kroening

src/solvers/smt2/letify.cpp

@@ -46,26 +46,29 @@ void letifyt::collect_bindings(
   let_order.push_back(expr);
 }
 
-exprt letifyt::letify_rec(
+exprt letifyt::letify(
   const exprt &expr,
-  std::vector<exprt> &let_order,
-  const seen_expressionst &map,
-  std::size_t i)
+  const std::vector<exprt> &let_order,
+  const seen_expressionst &map)
 {
-  if(i >= let_order.size())
-    return substitute_let(expr, map);
+  exprt result = substitute_let(expr, map);
 
-  exprt current = let_order[i];
-  INVARIANT(
-    map.find(current) != map.end(), "expression should have been seen already");
+  // go backwards in let order
+  for(auto r_it = let_order.rbegin(); r_it != let_order.rend(); r_it++)
+  {
+    const exprt &current = *r_it;
 
-  if(map.find(current)->second.count < LET_COUNT)
-    return letify_rec(expr, let_order, map, i + 1);
+    auto m_it = map.find(current);
+    INVARIANT(m_it != map.end(), "expression should have been seen already");
+
+    if(m_it->second.count >= LET_COUNT)
+    {
+      result = let_exprt(
+        m_it->second.let_symbol, substitute_let(current, map), result);
+    }
+  }
 
-  return let_exprt(
-    map.find(current)->second.let_symbol,
-    substitute_let(current, map),
-    letify_rec(expr, let_order, map, i + 1));
+  return result;
 }
 
 exprt letifyt::operator()(const exprt &expr)
@@ -75,7 +78,7 @@ exprt letifyt::operator()(const exprt &expr)
 
   collect_bindings(expr, map, let_order);
 
-  return letify_rec(expr, let_order, map, 0);
+  return letify(expr, let_order, map);
 }
 
 exprt letifyt::substitute_let(const exprt &expr, const seen_expressionst &map)

src/solvers/smt2/letify.h

@@ -46,11 +46,10 @@ class letifyt
     seen_expressionst &map,
     std::vector<exprt> &let_order);
 
-  static exprt letify_rec(
+  static exprt letify(
     const exprt &expr,
-    std::vector<exprt> &let_order,
-    const seen_expressionst &map,
-    std::size_t i);
+    const std::vector<exprt> &let_order,
+    const seen_expressionst &map);
 
   static exprt substitute_let(const exprt &expr, const seen_expressionst &map);
 };