move letification into separate class

src/solvers/Makefile

@@ -181,6 +181,7 @@ SRC = $(BOOLEFORCE_SRC) \
       sat/dimacs_cnf.cpp \
       sat/pbs_dimacs_cnf.cpp \
       sat/resolution_proof.cpp \
+      smt2/letify.cpp \
       smt2/smt2_conv.cpp \
       smt2/smt2_dec.cpp \
       smt2/smt2_format.cpp \

src/solvers/smt2/letify.cpp

@@ -0,0 +1,92 @@
+/*******************************************************************\
+
+Module: Introduce LET for common subexpressions
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \file
+/// Introduce LET for common subexpressions
+
+#include "letify.h"
+
+#include <util/irep_hash_container.h>
+#include <util/std_expr.h>
+
+void letifyt::collect_bindings(
+  exprt &expr,
+  seen_expressionst &map,
+  std::vector<exprt> &let_order)
+{
+  seen_expressionst::iterator entry = map.find(expr);
+
+  if(entry != map.end())
+  {
+    let_count_idt &count_id = entry->second;
+    ++(count_id.count);
+    return;
+  }
+
+  // do not letify things with no children
+  if(expr.operands().empty())
+    return;
+
+  Forall_operands(it, expr)
+    collect_bindings(*it, map, let_order);
+
+  INVARIANT(
+    map.find(expr) == map.end(), "expression should not have been seen yet");
+
+  symbol_exprt let =
+    symbol_exprt("_let_" + std::to_string(++let_id_count), expr.type());
+
+  map.insert(std::make_pair(expr, let_count_idt(1, let)));
+
+  let_order.push_back(expr);
+}
+
+exprt letifyt::letify_rec(
+  exprt &expr,
+  std::vector<exprt> &let_order,
+  const seen_expressionst &map,
+  std::size_t i)
+{
+  if(i >= let_order.size())
+    return substitute_let(expr, map);
+
+  exprt current = let_order[i];
+  INVARIANT(
+    map.find(current) != map.end(), "expression should have been seen already");
+
+  if(map.find(current)->second.count < LET_COUNT)
+    return letify_rec(expr, let_order, map, i + 1);
+
+  return let_exprt(
+    map.find(current)->second.let_symbol,
+    substitute_let(current, map),
+    letify_rec(expr, let_order, map, i + 1));
+}
+
+exprt letifyt::operator()(exprt &expr)
+{
+  seen_expressionst map;
+  std::vector<exprt> let_order;
+
+  collect_bindings(expr, map, let_order);
+
+  return letify_rec(expr, let_order, map, 0);
+}
+
+exprt letifyt::substitute_let(exprt &expr, const seen_expressionst &map)
+{
+  if(expr.operands().empty())
+    return expr;
+
+  let_visitort lv(map);
+
+  Forall_operands(it, expr)
+    it->visit(lv);
+
+  return expr;
+}

src/solvers/smt2/letify.h

@@ -0,0 +1,78 @@
+/*******************************************************************\
+
+Module: Introduce LET for common subexpressions
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_SOLVERS_SMT2_LETIFY_H
+#define CPROVER_SOLVERS_SMT2_LETIFY_H
+
+#include <util/irep_hash_container.h>
+#include <util/std_expr.h>
+
+/// Introduce LET for common subexpressions
+class letifyt
+{
+public:
+  exprt operator()(exprt &expr);
+
+protected:
+  // to produce a fresh ID for each new let
+  std::size_t let_id_count = 0;
+
+  static const std::size_t LET_COUNT = 2;
+
+  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;
+  };
+
+#ifdef HASH_CODE
+  using seen_expressionst = std::unordered_map<exprt, let_count_idt, irep_hash>;
+#else
+  using seen_expressionst = irep_hash_mapt<exprt, let_count_idt>;
+#endif
+
+  class let_visitort : public expr_visitort
+  {
+    const seen_expressionst &let_map;
+
+  public:
+    explicit let_visitort(const seen_expressionst &map) : let_map(map)
+    {
+    }
+
+    void operator()(exprt &expr)
+    {
+      seen_expressionst::const_iterator it = let_map.find(expr);
+      if(it != let_map.end() && it->second.count >= letifyt::LET_COUNT)
+      {
+        const symbol_exprt &symb = it->second.let_symbol;
+        expr = symb;
+      }
+    }
+  };
+
+  void collect_bindings(
+    exprt &expr,
+    seen_expressionst &map,
+    std::vector<exprt> &let_order);
+
+  exprt letify_rec(
+    exprt &expr,
+    std::vector<exprt> &let_order,
+    const seen_expressionst &map,
+    std::size_t i);
+
+  exprt substitute_let(exprt &expr, const seen_expressionst &map);
+};
+
+#endif // CPROVER_SOLVERS_SMT2_LETIFY_H

src/solvers/smt2/smt2_conv.cpp

@@ -4713,85 +4713,6 @@ void smt2_convt::find_symbols_rec(
   }
 }
 
-exprt smt2_convt::letify(exprt &expr)
-{
-  seen_expressionst map;
-  std::vector<exprt> let_order;
-
-  collect_bindings(expr, map, let_order);
-
-  return letify_rec(expr, let_order, map, 0);
-}
-
-exprt smt2_convt::letify_rec(
-  exprt &expr,
-  std::vector<exprt> &let_order,
-  const seen_expressionst &map,
-  std::size_t i)
-{
-  if(i>=let_order.size())
-    return substitute_let(expr, map);
-
-  exprt current=let_order[i];
-  INVARIANT(
-    map.find(current) != map.end(), "expression should have been seen already");
-
-  if(map.find(current)->second.count < LET_COUNT)
-    return letify_rec(expr, let_order, map, i+1);
-
-  return let_exprt(
-    map.find(current)->second.let_symbol,
-    substitute_let(current, map),
-    letify_rec(expr, let_order, map, i + 1));
-}
-
-void smt2_convt::collect_bindings(
-  exprt &expr,
-  seen_expressionst &map,
-  std::vector<exprt> &let_order)
-{
-  seen_expressionst::iterator entry = map.find(expr);
-
-  if(entry != map.end())
-  {
-    let_count_idt &count_id = entry->second;
-    ++(count_id.count);
-    return;
-  }
-
-  // do not letify things with no children
-  if(expr.operands().empty())
-    return;
-
-  Forall_operands(it, expr)
-    collect_bindings(*it, map, let_order);
-
-  INVARIANT(
-    map.find(expr) == map.end(), "expression should not have been seen yet");
-
-  symbol_exprt let=
-    symbol_exprt("_let_"+std::to_string(++let_id_count), expr.type());
-
-  map.insert(std::make_pair(expr, let_count_idt(1, let)));
-
-  let_order.push_back(expr);
-}
-
-exprt smt2_convt::substitute_let(
-  exprt &expr,
-  const seen_expressionst &map)
-{
-  if(expr.operands().empty())
-    return expr;
-
-  let_visitort lv(map);
-
-  Forall_operands(it, expr)
-    it->visit(lv);
-
-  return expr;
-}
-
 std::size_t smt2_convt::get_number_of_solver_calls() const
 {
   return number_of_solver_calls;

src/solvers/smt2/smt2_conv.h

@@ -24,6 +24,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <solvers/flattening/boolbv_width.h>
 #include <solvers/flattening/pointer_logic.h>
 
+#include "letify.h"
+
 class typecast_exprt;
 class constant_exprt;
 class index_exprt;
@@ -62,7 +64,6 @@ class smt2_convt:public prop_convt
       logic(_logic),
       solver(_solver),
       boolbv_width(_ns),
-      let_id_count(0),
       pointer_logic(_ns),
       no_boolean_variables(0)
   {
@@ -187,59 +188,7 @@ class smt2_convt:public prop_convt
   void find_symbols_rec(const typet &type, std::set<irep_idt> &recstack);
 
   // letification
-  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;
-  };
-
-#ifdef HASH_CODE
-  typedef std::unordered_map<exprt, let_count_idt, irep_hash> seen_expressionst;
-#else
-  typedef irep_hash_mapt<exprt, let_count_idt> seen_expressionst;
-#endif
-
-  std::size_t let_id_count;
-  static const std::size_t LET_COUNT = 2;
-
-  class let_visitort:public expr_visitort
-  {
-    const seen_expressionst &let_map;
-
-  public:
-    explicit let_visitort(const seen_expressionst &map):let_map(map) { }
-
-    void operator()(exprt &expr)
-    {
-      seen_expressionst::const_iterator it=let_map.find(expr);
-      if(it != let_map.end() && it->second.count >= LET_COUNT)
-      {
-        const symbol_exprt &symb = it->second.let_symbol;
-        expr=symb;
-      }
-    }
-  };
-
-  exprt letify(exprt &expr);
-  exprt letify_rec(
-    exprt &expr,
-    std::vector<exprt> &let_order,
-    const seen_expressionst &map,
-    std::size_t i);
-
-  void collect_bindings(
-    exprt &expr,
-    seen_expressionst &map,
-    std::vector<exprt> &let_order);
-
-  exprt substitute_let(
-    exprt &expr,
-    const seen_expressionst &map);
+  letifyt letify;
 
   // Parsing solver responses
   constant_exprt parse_literal(const irept &, const typet &type);