Go to the documentation of this file.
18 const auto &values = expr.
values();
22 "let must have the type of the 'where' operand");
25 for(
auto &binding :
make_range(variables).zip(values))
28 binding.first.type() == binding.second.type(),
29 "let value must have the type of the let symbol");
37 std::vector<bvt> converted_values;
38 converted_values.reserve(variables.size());
40 for(
auto &value : values)
47 for(
const auto &binding :
make_range(fresh_variables).zip(converted_values))
49 bool is_boolean = binding.first.type().id() == ID_bool;
50 const auto &identifier = binding.first.get_identifier();
55 DATA_INVARIANT(binding.second.size() == 1,
"boolean values have one bit");
56 symbols[identifier] = binding.second[0];
65 for(
const auto &pair :
make_range(variables).zip(fresh_variables))
66 replace_symbol.
insert(pair.first, pair.second);
70 replace_symbol(where_renamed);
76 for(
const auto &entry : fresh_variables)
78 const auto &type = entry.type();
79 if(type.id() == ID_bool)
80 symbols.erase(entry.get_identifier());
void erase_literals(const irep_idt &identifier, const typet &type)
std::vector< literalt > bvt
binding_exprt::variablest fresh_binding(const binding_exprt &)
create new, unique variables for the given binding
Base class for all expressions.
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
typet & type()
Return the type of the expression.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Ranges: pair of begin and end iterators, which can be initialized from containers,...
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
virtual bvt convert_let(const let_exprt &)
exprt & where()
convenience accessor for binding().where()
API to expression classes.
binding_exprt & binding()
ranget< iteratort > make_range(iteratort begin, iteratort end)
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Replace expression or type symbols by an expression or type, respectively.