17 const std::map<irep_idt, exprt> &substitutions,
20 if(src.
id() == ID_symbol)
22 auto s_it = substitutions.find(
to_symbol_expr(src).get_identifier());
23 if(s_it == substitutions.end())
29 src.
id() == ID_forall || src.
id() == ID_exists || src.
id() == ID_lambda)
35 auto new_substitutions = substitutions;
36 for(
const auto &variable : binding_expr.variables())
37 new_substitutions.erase(variable.get_identifier());
41 if(op_result.has_value())
43 auto new_binding_expr = binding_expr;
44 new_binding_expr.where() = std::move(op_result.value());
45 return std::move(new_binding_expr);
50 else if(src.
id() == ID_let)
57 auto new_substitutions = substitutions;
58 for(
const auto &variable : binding_expr.variables())
59 new_substitutions.erase(variable.get_identifier());
61 bool op_changed =
false;
63 for(
auto &op : new_let_expr.values())
67 if(op_result.has_value())
69 op = op_result.value();
76 if(op_result.has_value())
78 new_let_expr.where() = op_result.value();
83 return std::move(new_let_expr);
91 bool op_changed =
false;
97 if(op_result.has_value())
99 op = op_result.value();
optionalt< exprt > substitute_symbols(const std::map< irep_idt, exprt > &substitutions, exprt src)
Substitute free occurrences of the variables given by their identifiers in the keys of the map in the...