cprover
letify.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Introduce LET for common subexpressions
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "letify.h"
13 
15 #include <util/std_expr.h>
16 
18  const exprt &expr,
19  seen_expressionst &map,
20  std::vector<exprt> &let_order)
21 {
22  // do not letify things with no children
23  if(expr.operands().empty())
24  return;
25 
26  // did we already see the expression?
27  seen_expressionst::iterator entry = map.find(expr);
28 
29  if(entry != map.end())
30  {
31  // yes, seen before, increase counter
32  let_count_idt &count_id = entry->second;
33  ++(count_id.count);
34  return;
35  }
36 
37  // not seen before
38  for(auto &op : expr.operands())
39  collect_bindings(op, map, let_order);
40 
41  INVARIANT(
42  map.find(expr) == map.end(), "expression should not have been seen yet");
43 
44  symbol_exprt let =
45  symbol_exprt("_let_" + std::to_string(++let_id_count), expr.type());
46 
47  map.insert(std::make_pair(expr, let_count_idt(1, let)));
48 
49  let_order.push_back(expr);
50 }
51 
55  const exprt &expr,
56  const std::vector<exprt> &let_order,
57  const seen_expressionst &map)
58 {
59  exprt result = substitute_let(expr, map);
60 
61  // we build inside out, so go backwards in let order
62  for(auto r_it = let_order.rbegin(); r_it != let_order.rend(); r_it++)
63  {
64  const exprt &current = *r_it;
65 
66  auto m_it = map.find(current);
67  PRECONDITION(m_it != map.end());
68 
69  // Used more than once? Then a let pays off.
70  if(m_it->second.count > 1)
71  {
72  result = let_exprt(
73  m_it->second.let_symbol, substitute_let(current, map), result);
74  }
75  }
76 
77  return result;
78 }
79 
81 {
83  std::vector<exprt> let_order;
84 
85  collect_bindings(expr, map, let_order);
86 
87  return letify(expr, let_order, map);
88 }
89 
91 {
92  if(expr.operands().empty())
93  return expr;
94 
95  exprt tmp = expr;
96 
97  for(auto &op : tmp.operands())
98  {
99  op.visit_pre([&map](exprt &expr) {
101 
102  // replace subexpression by let symbol if used more than once
103  if(it != map.end() && it->second.count > 1)
104  expr = it->second.let_symbol;
105  });
106  }
107 
108  return tmp;
109 }
Base class for all expressions.
Definition: expr.h:54
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:259
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:96
typename mapt::iterator iterator
const_iterator find(const Key &key) const
std::pair< iterator, bool > insert(const value_type &value)
const_iterator end() const
typename mapt::const_iterator const_iterator
A let expression.
Definition: std_expr.h:2816
static exprt letify(const exprt &expr, const std::vector< exprt > &let_order, const seen_expressionst &map)
Construct a nested let expression for expressions in let_order that are used more than once.
Definition: letify.cpp:54
std::size_t let_id_count
Definition: letify.h:23
void collect_bindings(const exprt &expr, seen_expressionst &map, std::vector< exprt > &let_order)
Definition: letify.cpp:17
static exprt substitute_let(const exprt &expr, const seen_expressionst &map)
Definition: letify.cpp:90
exprt operator()(const exprt &)
Definition: letify.cpp:80
Expression to hold a symbol (variable)
Definition: std_expr.h:81
IREP Hash Container.
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
API to expression classes.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::size_t count
Definition: letify.h:32