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
Base class for all expressions.
Definition: expr.h:54
Introduce LET for common subexpressions.
Definition: letify.h:17
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.
API to expression classes.
let_count_idt(std::size_t _count, const symbol_exprt &_let_symbol)
Definition: letify.h:27
symbol_exprt let_symbol
Definition: letify.h:33
std::size_t count
Definition: letify.h:32