cprover
letify.h
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 
9 #ifndef CPROVER_SOLVERS_SMT2_LETIFY_H
10 #define CPROVER_SOLVERS_SMT2_LETIFY_H
11 
13 #include <util/std_expr.h>
14 
16 class letifyt
17 {
18 public:
19  exprt operator()(const exprt &);
20 
21 protected:
22  // to produce a fresh ID for each new let
23  std::size_t let_id_count = 0;
24 
26  {
27  let_count_idt(std::size_t _count, const symbol_exprt &_let_symbol)
28  : count(_count), let_symbol(_let_symbol)
29  {
30  }
31 
32  std::size_t count;
34  };
35 
36 #if HASH_CODE
37  using seen_expressionst = std::unordered_map<exprt, let_count_idt, irep_hash>;
38 #else
40 #endif
41 
42  void collect_bindings(
43  const exprt &expr,
44  seen_expressionst &map,
45  std::vector<exprt> &let_order);
46 
47  static exprt letify(
48  const exprt &expr,
49  const std::vector<exprt> &let_order,
50  const seen_expressionst &map);
51 
52  static exprt substitute_let(const exprt &expr, const seen_expressionst &map);
53 };
54 
55 #endif // CPROVER_SOLVERS_SMT2_LETIFY_H
letifyt
Introduce LET for common subexpressions.
Definition: letify.h:17
letifyt::let_count_idt::let_count_idt
let_count_idt(std::size_t _count, const symbol_exprt &_let_symbol)
Definition: letify.h:27
letifyt::let_id_count
std::size_t let_id_count
Definition: letify.h:23
exprt
Base class for all expressions.
Definition: expr.h:53
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
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
letifyt::let_count_idt
Definition: letify.h:26
letifyt::let_count_idt::let_symbol
symbol_exprt let_symbol
Definition: letify.h:33
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
std_expr.h
API to expression classes.