CBMC
Loading...
Searching...
No Matches
equality_propagation.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Equality Propagation
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
13
14#include <util/std_expr.h>
16
17void equality_propagation(std::vector<exprt> &constraints)
18{
19 using valuest = std::map<irep_idt, exprt>;
20 valuest values;
21
22 std::vector<exprt> new_constraints;
23 new_constraints.reserve(constraints.size());
24
25 // forward-propagation of equalities
26 for(auto &expr : constraints)
27 {
28 bool retain_constraint = true;
29
30 // apply the map
31 auto substitution_result = substitute_symbols(values, expr);
32 if(substitution_result.has_value())
33 expr = std::move(substitution_result.value());
34
35 if(expr.id() == ID_equal)
36 {
37 const auto &equal_expr = to_equal_expr(expr);
38 if(equal_expr.lhs().id() == ID_symbol)
39 {
40 const auto &symbol_expr = to_symbol_expr(equal_expr.lhs());
41 // this is a (deliberate) no-op when the symbol is already in the map
42 auto insert_result =
43 values.insert({symbol_expr.get_identifier(), equal_expr.rhs()});
44 if(insert_result.second)
45 {
46 // insertion has happened
47 retain_constraint = false;
48 }
49 }
50 }
51
53 new_constraints.push_back(std::move(expr));
54 }
55
56 constraints = std::move(new_constraints);
57
58 // apply the map again, to catch any backwards definitions
59 for(auto &expr : constraints)
60 {
61 if(expr.id() == ID_equal && to_equal_expr(expr).lhs().id() == ID_symbol)
62 {
63 // it's a definition
64 }
65 else
66 {
67 // apply the map
68 auto substitution_result = substitute_symbols(values, expr);
69 if(substitution_result.has_value())
70 expr = std::move(substitution_result.value());
71 }
72 }
73}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
void equality_propagation(std::vector< exprt > &constraints)
Equality Propagation.
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1407
std::optional< 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...
Symbol Substitution.