cprover
Loading...
Searching...
No Matches
replace_symbol.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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 <unordered_map>
21
25{
26public:
27 typedef std::unordered_map<irep_idt, exprt> expr_mapt;
28
32 void insert(const class symbol_exprt &old_expr,
33 const exprt &new_expr);
34
36 void set(const class symbol_exprt &old_expr, const exprt &new_expr);
37
38 virtual bool replace(exprt &dest) const;
39 virtual bool replace(typet &dest) const;
40
41 void operator()(exprt &dest) const
42 {
43 replace(dest);
44 }
45
46 void operator()(typet &dest) const
47 {
48 replace(dest);
49 }
50
51 void clear()
52 {
53 expr_map.clear();
54 }
55
56 bool empty() const
57 {
58 return expr_map.empty();
59 }
60
61 std::size_t erase(const irep_idt &id)
62 {
63 return expr_map.erase(id);
64 }
65
66 expr_mapt::iterator erase(expr_mapt::iterator it)
67 {
68 return expr_map.erase(it);
69 }
70
71 bool replaces_symbol(const irep_idt &id) const
72 {
73 return expr_map.find(id) != expr_map.end();
74 }
75
77 virtual ~replace_symbolt();
78
79 const expr_mapt &get_expr_map() const
80 {
81 return expr_map;
82 }
83
85 {
86 return expr_map;
87 }
88
89protected:
91
92 virtual bool replace_symbol_expr(symbol_exprt &dest) const;
93
94 bool have_to_replace(const exprt &dest) const;
95 bool have_to_replace(const typet &type) const;
96};
97
99{
100public:
102 {
103 }
104
105 void insert(const symbol_exprt &old_expr, const exprt &new_expr);
106
107protected:
108 bool replace_symbol_expr(symbol_exprt &dest) const override;
109};
110
120{
121public:
122 bool replace(exprt &dest) const override;
123
124private:
125 mutable bool require_lvalue = false;
126
128 {
129 public:
132 {
133 require_lvalue = value;
134 }
135
137 {
139 }
140
141 private:
144 };
145
146 bool replace_symbol_expr(symbol_exprt &dest) const override;
147};
148
149#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:37
Base class for all expressions.
Definition: expr.h:54
Replace expression or type symbols by an expression or type, respectively.
virtual bool replace(exprt &dest) const
bool empty() const
std::size_t erase(const irep_idt &id)
const expr_mapt & get_expr_map() const
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.
void operator()(exprt &dest) const
expr_mapt::iterator erase(expr_mapt::iterator it)
expr_mapt & get_expr_map()
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:80
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)