Skip to content

Commit 865394f

Browse files
committed
make substitute_symbols available outside of std_expr.cpp
substitute_symbols is useful beyond the specific use case in std_expr.cpp (instantiating binding_exprt). This commit makes it available outside.
1 parent 612fcaa commit 865394f

File tree

4 files changed

+145
-95
lines changed

4 files changed

+145
-95
lines changed

src/util/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -92,6 +92,7 @@ SRC = arith_tools.cpp \
9292
string_hash.cpp \
9393
string_utils.cpp \
9494
structured_data.cpp \
95+
substitute_symbols.cpp \
9596
symbol.cpp \
9697
symbol_table_base.cpp \
9798
symbol_table.cpp \

src/util/std_expr.cpp

Lines changed: 2 additions & 95 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
1111
#include "namespace.h"
1212
#include "pointer_expr.h"
1313
#include "range.h"
14+
#include "substitute_symbols.h"
1415

1516
#include <map>
1617

@@ -165,100 +166,6 @@ void let_exprt::validate(const exprt &expr, const validation_modet vm)
165166
}
166167
}
167168

168-
static optionalt<exprt> substitute_symbols_rec(
169-
const std::map<irep_idt, exprt> &substitutions,
170-
exprt src)
171-
{
172-
if(src.id() == ID_symbol)
173-
{
174-
auto s_it = substitutions.find(to_symbol_expr(src).get_identifier());
175-
if(s_it == substitutions.end())
176-
return {};
177-
else
178-
return s_it->second;
179-
}
180-
else if(
181-
src.id() == ID_forall || src.id() == ID_exists || src.id() == ID_lambda)
182-
{
183-
const auto &binding_expr = to_binding_expr(src);
184-
185-
// bindings may be nested,
186-
// which may hide some of our substitutions
187-
auto new_substitutions = substitutions;
188-
for(const auto &variable : binding_expr.variables())
189-
new_substitutions.erase(variable.get_identifier());
190-
191-
auto op_result =
192-
substitute_symbols_rec(new_substitutions, binding_expr.where());
193-
if(op_result.has_value())
194-
return binding_exprt(
195-
src.id(),
196-
binding_expr.variables(),
197-
op_result.value(),
198-
binding_expr.type());
199-
else
200-
return {};
201-
}
202-
else if(src.id() == ID_let)
203-
{
204-
auto new_let_expr = to_let_expr(src); // copy
205-
const auto &binding_expr = to_let_expr(src).binding();
206-
207-
// bindings may be nested,
208-
// which may hide some of our substitutions
209-
auto new_substitutions = substitutions;
210-
for(const auto &variable : binding_expr.variables())
211-
new_substitutions.erase(variable.get_identifier());
212-
213-
bool op_changed = false;
214-
215-
for(auto &op : new_let_expr.values())
216-
{
217-
auto op_result = substitute_symbols_rec(new_substitutions, op);
218-
219-
if(op_result.has_value())
220-
{
221-
op = op_result.value();
222-
op_changed = true;
223-
}
224-
}
225-
226-
auto op_result =
227-
substitute_symbols_rec(new_substitutions, binding_expr.where());
228-
if(op_result.has_value())
229-
{
230-
new_let_expr.where() = op_result.value();
231-
op_changed = true;
232-
}
233-
234-
if(op_changed)
235-
return std::move(new_let_expr);
236-
else
237-
return {};
238-
}
239-
240-
if(!src.has_operands())
241-
return {};
242-
243-
bool op_changed = false;
244-
245-
for(auto &op : src.operands())
246-
{
247-
auto op_result = substitute_symbols_rec(substitutions, op);
248-
249-
if(op_result.has_value())
250-
{
251-
op = op_result.value();
252-
op_changed = true;
253-
}
254-
}
255-
256-
if(op_changed)
257-
return src;
258-
else
259-
return {};
260-
}
261-
262169
exprt binding_exprt::instantiate(const operandst &values) const
263170
{
264171
// number of values must match the number of bound variables
@@ -281,7 +188,7 @@ exprt binding_exprt::instantiate(const operandst &values) const
281188
substitutions[variables[i].get_identifier()] = values[i];
282189

283190
// now recurse downwards and substitute in 'where'
284-
auto substitute_result = substitute_symbols_rec(substitutions, where());
191+
auto substitute_result = substitute_symbols(substitutions, where());
285192

286193
if(substitute_result.has_value())
287194
return substitute_result.value();

src/util/substitute_symbols.cpp

Lines changed: 114 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,114 @@
1+
/*******************************************************************\
2+
3+
Module: Symbol Substitution
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file util/substitute_symbols.cpp
10+
/// Symbol Substitution
11+
12+
#include "substitute_symbols.h"
13+
14+
#include "std_expr.h"
15+
16+
static optionalt<exprt> substitute_symbols_rec(
17+
const std::map<irep_idt, exprt> &substitutions,
18+
exprt src)
19+
{
20+
if(src.id() == ID_symbol)
21+
{
22+
auto s_it = substitutions.find(to_symbol_expr(src).get_identifier());
23+
if(s_it == substitutions.end())
24+
return {};
25+
else
26+
return s_it->second;
27+
}
28+
else if(
29+
src.id() == ID_forall || src.id() == ID_exists || src.id() == ID_lambda)
30+
{
31+
const auto &binding_expr = to_binding_expr(src);
32+
33+
// bindings may be nested,
34+
// which may hide some of our substitutions
35+
auto new_substitutions = substitutions;
36+
for(const auto &variable : binding_expr.variables())
37+
new_substitutions.erase(variable.get_identifier());
38+
39+
auto op_result =
40+
substitute_symbols_rec(new_substitutions, binding_expr.where());
41+
if(op_result.has_value())
42+
return binding_exprt(
43+
src.id(),
44+
binding_expr.variables(),
45+
op_result.value(),
46+
binding_expr.type());
47+
else
48+
return {};
49+
}
50+
else if(src.id() == ID_let)
51+
{
52+
auto new_let_expr = to_let_expr(src); // copy
53+
const auto &binding_expr = to_let_expr(src).binding();
54+
55+
// bindings may be nested,
56+
// which may hide some of our substitutions
57+
auto new_substitutions = substitutions;
58+
for(const auto &variable : binding_expr.variables())
59+
new_substitutions.erase(variable.get_identifier());
60+
61+
bool op_changed = false;
62+
63+
for(auto &op : new_let_expr.values())
64+
{
65+
auto op_result = substitute_symbols_rec(new_substitutions, op);
66+
67+
if(op_result.has_value())
68+
{
69+
op = op_result.value();
70+
op_changed = true;
71+
}
72+
}
73+
74+
auto op_result =
75+
substitute_symbols_rec(new_substitutions, binding_expr.where());
76+
if(op_result.has_value())
77+
{
78+
new_let_expr.where() = op_result.value();
79+
op_changed = true;
80+
}
81+
82+
if(op_changed)
83+
return std::move(new_let_expr);
84+
else
85+
return {};
86+
}
87+
88+
if(!src.has_operands())
89+
return {};
90+
91+
bool op_changed = false;
92+
93+
for(auto &op : src.operands())
94+
{
95+
auto op_result = substitute_symbols_rec(substitutions, op);
96+
97+
if(op_result.has_value())
98+
{
99+
op = op_result.value();
100+
op_changed = true;
101+
}
102+
}
103+
104+
if(op_changed)
105+
return src;
106+
else
107+
return {};
108+
}
109+
110+
optionalt<exprt>
111+
substitute_symbols(const std::map<irep_idt, exprt> &substitutions, exprt src)
112+
{
113+
return substitute_symbols_rec(substitutions, src);
114+
}

src/util/substitute_symbols.h

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
/*******************************************************************\
2+
3+
Module: Symbol Substitution
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_UTIL_SUBSTITUTE_SYMBOLS_H
10+
#define CPROVER_UTIL_SUBSTITUTE_SYMBOLS_H
11+
12+
/// \file util/substitute_symbols.h
13+
/// Symbol Substitution
14+
15+
#include "expr.h"
16+
17+
#include <map>
18+
19+
/// Substitute free occurrences of the variables given
20+
/// by their identifiers in the keys of the map in the
21+
/// given expression. Only symbol_exprt expressions are
22+
/// substituted.
23+
/// \returns expression after substitution,
24+
/// or {} when no substitution took place
25+
optionalt<exprt>
26+
substitute_symbols(const std::map<irep_idt, exprt> &substitutions, exprt);
27+
28+
#endif // CPROVER_UTIL_SUBSTITUTE_SYMBOLS_H

0 commit comments

Comments
 (0)