19 std::vector<exprt> &let_order)
28 if(entry != map.
end())
41 map.
find(expr) == map.
end(),
"expression should not have been seen yet");
48 let_order.push_back(expr);
55 const std::vector<exprt> &let_order,
61 for(
auto r_it = let_order.rbegin(); r_it != let_order.rend(); r_it++)
63 const exprt ¤t = *r_it;
65 auto m_it = map.
find(current);
69 if(m_it->second.count > 1)
82 std::vector<exprt> let_order;
86 return letify(expr, let_order, map);
98 op.visit_pre([&map](
exprt &expr) {
102 if(it != map.
end() && it->second.count > 1)
103 expr = it->second.let_symbol;
Base class for all expressions.
typet & type()
Return the type of the expression.
typename mapt::iterator iterator
const_iterator find(const Key &key) const
const_iterator end() const
typename mapt::const_iterator const_iterator
std::pair< iterator, bool > insert(const value_type &value)
static exprt letify(const exprt &expr, const std::vector< exprt > &let_order, const seen_expressionst &map)
Construct a nested let expression for expressions in let_order that are used more than once.
void collect_bindings(const exprt &expr, seen_expressionst &map, std::vector< exprt > &let_order)
static exprt substitute_let(const exprt &expr, const seen_expressionst &map)
exprt operator()(const exprt &)
Expression to hold a symbol (variable)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.