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 }
irep_hash_mapt::end
const_iterator end() const
Definition: irep_hash_container.h:133
letifyt::let_id_count
std::size_t let_id_count
Definition: letify.h:23
exprt
Base class for all expressions.
Definition: expr.h:53
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
letifyt::collect_bindings
void collect_bindings(const exprt &expr, seen_expressionst &map, std::vector< exprt > &let_order)
Definition: letify.cpp:17
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
irep_hash_container.h
IREP Hash Container.
letifyt::let_count_idt::count
std::size_t count
Definition: letify.h:32
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
irep_hash_mapt
Definition: irep_hash_container.h:102
letifyt::substitute_let
static exprt substitute_let(const exprt &expr, const seen_expressionst &map)
Definition: letify.cpp:90
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
letifyt::let_count_idt
Definition: letify.h:26
irep_hash_mapt::find
const_iterator find(const Key &key) const
Definition: irep_hash_container.h:113
letifyt::operator()
exprt operator()(const exprt &)
Definition: letify.cpp:80
letifyt::letify
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
irep_hash_mapt::const_iterator
typename mapt::const_iterator const_iterator
Definition: irep_hash_container.h:110
irep_hash_mapt::insert
std::pair< iterator, bool > insert(const value_type &value)
Definition: irep_hash_container.h:165
exprt::visit_pre
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:311
exprt::operands
operandst & operands()
Definition: expr.h:95
letify.h
irep_hash_mapt::iterator
typename mapt::iterator iterator
Definition: irep_hash_container.h:111
std_expr.h
API to expression classes.
let_exprt
A let expression.
Definition: std_expr.h:4165
validation_modet::INVARIANT
@ INVARIANT