19 using valuest = std::map<irep_idt, exprt>;
26 for(
auto &expr : constraints)
43 values.insert({symbol_expr.get_identifier(),
equal_expr.rhs()});
59 for(
auto &expr : constraints)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
void equality_propagation(std::vector< exprt > &constraints)
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
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...