Go to the documentation of this file.
20 std::vector<exprt> &let_order)
29 if(entry != map.
end())
42 map.
find(expr) == map.
end(),
"expression should not have been seen yet");
49 let_order.push_back(expr);
56 const std::vector<exprt> &let_order,
62 for(
auto r_it = let_order.rbegin(); r_it != let_order.rend(); r_it++)
64 const exprt ¤t = *r_it;
66 auto m_it = map.
find(current);
70 if(m_it->second.count > 1)
83 std::vector<exprt> let_order;
87 return letify(expr, let_order, map);
103 if(it != map.
end() && it->second.count > 1)
104 expr = it->second.let_symbol;
const_iterator end() const
Base class for all expressions.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void collect_bindings(const exprt &expr, seen_expressionst &map, std::vector< exprt > &let_order)
Expression to hold a symbol (variable)
typet & type()
Return the type of the expression.
static exprt substitute_let(const exprt &expr, const seen_expressionst &map)
#define PRECONDITION(CONDITION)
const_iterator find(const Key &key) const
exprt operator()(const exprt &)
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.
typename mapt::const_iterator const_iterator
std::pair< iterator, bool > insert(const value_type &value)
void visit_pre(std::function< void(exprt &)>)
typename mapt::iterator iterator
API to expression classes.