23 if(expr.
id()==ID_symbol ||
24 expr.
id()==ID_nondet_symbol)
28 const auto map_entry_opt =
map.get_map_entry(identifier);
30 if(map_entry_opt.has_value())
42 exprt skeleton = expr;
57 if(type.
id()==ID_bool)
61 switch(
prop.l_get(bv[offset]).get_value())
74 if(type.
id()==ID_array)
81 const typet &subtype = array_type.element_type();
82 const auto &sub_width_opt =
bv_width.get_width_opt(subtype);
84 if(sub_width_opt.has_value() && *sub_width_opt > 0)
88 std::size_t sub_width = *sub_width_opt;
91 op.reserve(width/sub_width);
93 for(std::size_t new_offset=0;
95 new_offset+=sub_width)
99 from_integer(new_offset / sub_width, array_type.index_type())};
100 op.push_back(
bv_get_rec(index, bv, offset + new_offset));
112 else if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
115 type.
id() == ID_struct
118 std::size_t new_offset=0;
120 op.reserve(components.size());
122 for(
const auto &c : components)
124 const typet &subtype = c.type();
127 op.push_back(
bv_get_rec(member, bv, offset + new_offset));
134 else if(type.
id() == ID_union || type.
id() == ID_union_tag)
137 type.
id() == ID_union
141 if(components.empty())
145 std::size_t component_nr=0;
147 const typet &subtype = components[component_nr].type();
150 expr, components[component_nr].get_name(), subtype};
152 components[component_nr].get_name(),
156 else if(type.
id()==ID_complex)
164 width == sub_width * 2,
165 "complex type has two elements of equal bit width");
178 value.reserve(width);
180 for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
184 switch(
prop.l_get(bv[bit_nr]).get_value())
197 std::reverse(value.begin(), value.end());
203 type.
id() == ID_string || type.
id() == ID_empty ||
204 type.
id() == ID_enumeration);
205 if(type.
id()==ID_string)
216 else if(type.
id() == ID_empty)
220 else if(type.
id() == ID_enumeration)
224 if(int_value >= elements.size())
253 width, [&value](
size_t i) {
return value[value.size() - i - 1] ==
'1'; });
264 skeleton.
type() = type;
274 bv_cachet::const_iterator it=
bv_cache.find(expr);
295 typedef std::map<mp_integer, exprt> valuest;
298 const auto opt_num =
arrays.get_number(expr);
299 if(opt_num.has_value())
302 const auto number =
arrays.find_number(*opt_num);
305 index_mapt::const_iterator it=
index_map.find(number);
309 for(index_sett::const_iterator it1=
311 it1!=index_set.end();
324 index_mpint.has_value() && *index_mpint >= 0 &&
325 (!size_opt.has_value() || *index_mpint < *size_opt))
328 values[*index_mpint] =
331 values[*index_mpint] = value;
339 if(!size_opt.has_value() || values.size() != *size_opt)
343 result.
operands().reserve(values.size()*2);
345 for(valuest::const_iterator it=values.begin();
356 result=
exprt(ID_array, type);
364 for(valuest::iterator it=values.begin();
386 for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
388 switch(
prop.l_get(bv[bit_nr]).get_value())
bvtypet get_bvtype(const typet &type)
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Array constructor from list of elements.
Array constructor from a list of index-element pairs Operands are index/value pairs,...
const exprt & size() const
union_find< exprt, irep_hash > arrays
std::set< exprt > index_sett
bool is_unbounded_array(const typet &type) const override
exprt bv_get(const bvt &bv, const typet &type) const
numberingt< irep_idt > string_numbering
virtual exprt bv_get_unbounded_array(const exprt &) const
virtual exprt bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset) const
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
exprt bv_get_cache(const exprt &expr) const
virtual std::size_t boolbv_width(const typet &type) const
mp_integer get_value(const bvt &bv)
Complex constructor from a pair of numbers.
Imaginary part of the expression describing a complex number.
Real part of the expression describing a complex number.
A constant literal expression.
virtual exprt get(const exprt &) const =0
Return expr with variables replaced by values from satisfying assignment if available.
Union constructor to support unions without any member (a GCC/Clang feature).
const irept::subt & elements() const
Base class for all expressions.
std::vector< exprt > operandst
bool is_boolean() const
Return whether the expression represents a Boolean.
typet & type()
Return the type of the expression.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
The Boolean constant false.
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
const std::string & get_string(const irep_idt &name) const
Extract member of struct or union.
Struct constructor from list of elements.
const componentst & components() const
std::vector< componentt > componentst
The Boolean constant true.
const typet & subtype() const
The type of an expression, extends irept.
Union constructor from single element.
std::vector< literalt > bvt
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
const mp_integer string2integer(const std::string &n, unsigned base)
const std::string integer2string(const mp_integer &n, unsigned base)
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
API to expression classes.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a typet to a enumeration_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.