Go to the documentation of this file.
19 return val.find_first_not_of(
'0')==std::string::npos;
49 -> decltype(struct_expr.op0())
52 std::is_base_of<struct_exprt, T>::value,
"T must be a struct_exprt.");
56 index < struct_expr.operands().size(),
57 "component matching index should exist");
58 return struct_expr.operands()[index];
90 const typet &compound_type = ns.
follow(member_expr.compound().type());
91 const auto *struct_union_type =
92 type_try_dynamic_cast<struct_union_typet>(compound_type);
95 struct_union_type !=
nullptr,
96 "member must address a struct, union or compatible type");
99 struct_union_type->get_component(member_expr.get_component_name());
104 "member component '" +
id2string(member_expr.get_component_name()) +
105 "' must exist on addressed type");
110 "member expression's type must match the addressed struct or union "
122 let_expr.values().size() == let_expr.variables().size(),
123 "number of variables must match number of values");
126 make_range(let_expr.variables()).zip(let_expr.values()))
131 "let binding symbols must be symbols");
136 "let bindings must be type consistent");
141 const std::map<irep_idt, exprt> &substitutions,
144 if(src.
id() == ID_symbol)
146 auto s_it = substitutions.find(
to_symbol_expr(src).get_identifier());
147 if(s_it == substitutions.end())
153 src.
id() == ID_forall || src.
id() == ID_exists || src.
id() == ID_lambda)
159 auto new_substitutions = substitutions;
160 for(
const auto &variable : binding_expr.variables())
161 new_substitutions.erase(variable.get_identifier());
165 if(op_result.has_value())
168 binding_expr.variables(),
170 binding_expr.type());
174 else if(src.
id() == ID_let)
181 auto new_substitutions = substitutions;
182 for(
const auto &variable : binding_expr.variables())
183 new_substitutions.erase(variable.get_identifier());
185 bool op_changed =
false;
187 for(
auto &op : new_let_expr.values())
191 if(op_result.has_value())
193 op = op_result.value();
200 if(op_result.has_value())
202 new_let_expr.where() = op_result.value();
207 return std::move(new_let_expr);
215 bool op_changed =
false;
221 if(op_result.has_value())
223 op = op_result.value();
240 std::map<symbol_exprt, exprt> value_map;
242 for(std::size_t i = 0; i <
variables.size(); i++)
250 std::map<irep_idt, exprt> substitutions;
252 for(std::size_t i = 0; i <
variables.size(); i++)
253 substitutions[
variables[i].get_identifier()] = values[i];
258 if(substitute_result.has_value())
259 return substitute_result.value();
266 std::vector<exprt> values;
267 values.reserve(new_variables.size());
268 for(
const auto &new_variable : new_variables)
269 values.push_back(new_variable);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
The type of an expression, extends irept.
Base class for all expressions.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
static void validate(const exprt &, validation_modet)
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
static optionalt< exprt > substitute_symbols_rec(const std::map< irep_idt, exprt > &substitutions, exprt src)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
bool has_operands() const
Return true if there is at least one operand.
const std::string & id2string(const irep_idt &d)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
#define PRECONDITION(CONDITION)
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
std::vector< symbol_exprt > variablest
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the member expression has the right number of operands, refers to a component that exists ...
const irep_idt & id() const
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
A base class for variable bindings (quantifiers, let, lambda)
std::vector< exprt > operandst
The Boolean constant false.
nonstd::optional< T > optionalt
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bool value_is_zero_string() const
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
exprt & component(const irep_idt &name, const namespacet &ns)
The Boolean constant true.
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
API to expression classes.
binding_exprt & binding()
const irep_idt & get_value() const
ranget< iteratort > make_range(iteratort begin, iteratort end)