9 #ifndef CPROVER_SOLVERS_SMT2_LETIFY_H
10 #define CPROVER_SOLVERS_SMT2_LETIFY_H
45 std::vector<exprt> &let_order);
49 const std::vector<exprt> &let_order,
Base class for all expressions.
Introduce LET for common subexpressions.
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)
API to expression classes.
let_count_idt(std::size_t _count, const symbol_exprt &_let_symbol)