CBMC
replace_symbol.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_REPLACE_SYMBOL_H
11 #define CPROVER_UTIL_REPLACE_SYMBOL_H
12 
13 //
14 // true: did nothing
15 // false: replaced something
16 //
17 
18 #include "expr.h"
19 
20 #include <set>
21 #include <unordered_map>
22 
28 {
29 public:
30  typedef std::unordered_map<irep_idt, exprt> expr_mapt;
31 
35  void insert(const class symbol_exprt &old_expr,
36  const exprt &new_expr);
37 
39  void set(const class symbol_exprt &old_expr, const exprt &new_expr);
40 
41  virtual bool replace(exprt &dest) const;
42  virtual bool replace(typet &dest) const;
43 
44  void operator()(exprt &dest) const
45  {
46  replace(dest);
47  }
48 
49  void operator()(typet &dest) const
50  {
51  replace(dest);
52  }
53 
54  void clear()
55  {
56  expr_map.clear();
57  }
58 
59  bool empty() const
60  {
61  return expr_map.empty();
62  }
63 
64  std::size_t erase(const irep_idt &id)
65  {
66  return expr_map.erase(id);
67  }
68 
69  expr_mapt::iterator erase(expr_mapt::iterator it)
70  {
71  return expr_map.erase(it);
72  }
73 
74  bool replaces_symbol(const irep_idt &id) const
75  {
76  return expr_map.find(id) != expr_map.end();
77  }
78 
80  virtual ~replace_symbolt();
81 
82  const expr_mapt &get_expr_map() const
83  {
84  return expr_map;
85  }
86 
88  {
89  return expr_map;
90  }
91 
92 protected:
94  mutable std::set<irep_idt> bindings;
95 
96  virtual bool replace_symbol_expr(symbol_exprt &dest) const;
97 
98  bool have_to_replace(const exprt &dest) const;
99  bool have_to_replace(const typet &type) const;
100 };
101 
103 {
104 public:
106  {
107  }
108 
109  void insert(const symbol_exprt &old_expr, const exprt &new_expr);
110 
111 protected:
112  bool replace_symbol_expr(symbol_exprt &dest) const override;
113 };
114 
124 {
125 public:
126  bool replace(exprt &dest) const override;
127 
128 private:
129  mutable bool require_lvalue = false;
130 
132  {
133  public:
136  {
137  require_lvalue = value;
138  }
139 
141  {
143  }
144 
145  private:
148  };
149 
150  bool replace_symbol_expr(symbol_exprt &dest) const override;
151 };
152 
153 #endif // CPROVER_UTIL_REPLACE_SYMBOL_H
set_require_lvalue_and_backupt(bool &require_lvalue, const bool value)
Replace symbols with constants while maintaining syntactically valid expressions.
bool replace_symbol_expr(symbol_exprt &dest) const override
bool replace(exprt &dest) const override
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
Replace a symbol expression by a given expression.
virtual bool replace(exprt &dest) const
bool empty() const
std::size_t erase(const irep_idt &id)
bool have_to_replace(const exprt &dest) const
void set(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr.
const expr_mapt & get_expr_map() const
void operator()(exprt &dest) const
expr_mapt & get_expr_map()
expr_mapt::iterator erase(expr_mapt::iterator it)
std::set< irep_idt > bindings
virtual ~replace_symbolt()
virtual bool replace_symbol_expr(symbol_exprt &dest) const
std::unordered_map< irep_idt, exprt > expr_mapt
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
bool replaces_symbol(const irep_idt &id) const
expr_mapt expr_map
void operator()(typet &dest) const
Expression to hold a symbol (variable)
Definition: std_expr.h:131
The type of an expression, extends irept.
Definition: type.h:29
bool replace_symbol_expr(symbol_exprt &dest) const override
void insert(const symbol_exprt &old_expr, const exprt &new_expr)