26 seen_expressionst::iterator entry = map.find(expr);
28 if(entry != map.end())
41 map.find(expr) == map.end(),
"expression should not have been seen yet");
65 auto m_it = map.find(current);
69 if(
m_it->second.count > 1)
96 for(
auto &op :
tmp.operands())
99 seen_expressionst::const_iterator it = map.find(expr);
102 if(it != map.end() && it->second.count > 1)
103 expr = it->second.let_symbol;
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Base class for all expressions.
void visit_pre(std::function< void(exprt &)>)
typet & type()
Return the type of the expression.
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)
std::unordered_map< exprt, let_count_idt, irep_hash > seen_expressionst
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.