Skip to content

Commit 54aca0a

Browse files
kroeningkroening
committed
make substitute_symbols available outside of std_expr.cpp
1 parent 84cf140 commit 54aca0a

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
@@ -93,6 +93,7 @@ SRC = arith_tools.cpp \
9393
string_hash.cpp \
9494
string_utils.cpp \
9595
structured_data.cpp \
96+
substitute_symbols.cpp \
9697
symbol.cpp \
9798
symbol_table_base.cpp \
9899
symbol_table.cpp \

‎src/util/std_expr.cpp

Lines changed: 2 additions & 95 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
1010

1111
#include "namespace.h"
1212
#include "range.h"
13+
#include "substitute_symbols.h"
1314

1415
#include <map>
1516

@@ -137,100 +138,6 @@ void let_exprt::validate(const exprt &expr, const validation_modet vm)
137138
}
138139
}
139140

140-
static optionalt<exprt> substitute_symbols_rec(
141-
const std::map<irep_idt, exprt> &substitutions,
142-
exprt src)
143-
{
144-
if(src.id() == ID_symbol)
145-
{
146-
auto s_it = substitutions.find(to_symbol_expr(src).get_identifier());
147-
if(s_it == substitutions.end())
148-
return {};
149-
else
150-
return s_it->second;
151-
}
152-
else if(
153-
src.id() == ID_forall || src.id() == ID_exists || src.id() == ID_lambda)
154-
{
155-
const auto &binding_expr = to_binding_expr(src);
156-
157-
// bindings may be nested,
158-
// which may hide some of our substitutions
159-
auto new_substitutions = substitutions;
160-
for(const auto &variable : binding_expr.variables())
161-
new_substitutions.erase(variable.get_identifier());
162-
163-
auto op_result =
164-
substitute_symbols_rec(new_substitutions, binding_expr.where());
165-
if(op_result.has_value())
166-
return binding_exprt(
167-
src.id(),
168-
binding_expr.variables(),
169-
op_result.value(),
170-
binding_expr.type());
171-
else
172-
return {};
173-
}
174-
else if(src.id() == ID_let)
175-
{
176-
auto new_let_expr = to_let_expr(src); // copy
177-
const auto &binding_expr = to_let_expr(src).binding();
178-
179-
// bindings may be nested,
180-
// which may hide some of our substitutions
181-
auto new_substitutions = substitutions;
182-
for(const auto &variable : binding_expr.variables())
183-
new_substitutions.erase(variable.get_identifier());
184-
185-
bool op_changed = false;
186-
187-
for(auto &op : new_let_expr.values())
188-
{
189-
auto op_result = substitute_symbols_rec(new_substitutions, op);
190-
191-
if(op_result.has_value())
192-
{
193-
op = op_result.value();
194-
op_changed = true;
195-
}
196-
}
197-
198-
auto op_result =
199-
substitute_symbols_rec(new_substitutions, binding_expr.where());
200-
if(op_result.has_value())
201-
{
202-
new_let_expr.where() = op_result.value();
203-
op_changed = true;
204-
}
205-
206-
if(op_changed)
207-
return std::move(new_let_expr);
208-
else
209-
return {};
210-
}
211-
212-
if(!src.has_operands())
213-
return {};
214-
215-
bool op_changed = false;
216-
217-
for(auto &op : src.operands())
218-
{
219-
auto op_result = substitute_symbols_rec(substitutions, op);
220-
221-
if(op_result.has_value())
222-
{
223-
op = op_result.value();
224-
op_changed = true;
225-
}
226-
}
227-
228-
if(op_changed)
229-
return src;
230-
else
231-
return {};
232-
}
233-
234141
exprt binding_exprt::instantiate(const operandst &values) const
235142
{
236143
// number of values must match the number of bound variables
@@ -253,7 +160,7 @@ exprt binding_exprt::instantiate(const operandst &values) const
253160
substitutions[variables[i].get_identifier()] = values[i];
254161

255162
// now recurse downwards and substitute in 'where'
256-
auto substitute_result = substitute_symbols_rec(substitutions, where());
163+
auto substitute_result = substitute_symbols(substitutions, where());
257164

258165
if(substitute_result.has_value())
259166
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)