23 if(expr.
id()==ID_symbol ||
24 expr.
id()==ID_nondet_symbol)
28 boolbv_mapt::mappingt::const_iterator it=
38 std::vector<bool> unknown;
40 std::size_t width=map_entry.
width;
43 unknown.resize(width);
45 for(std::size_t bit_nr=0; bit_nr<width; bit_nr++)
51 unknown[bit_nr]=
false;
70 const std::vector<bool> &unknown,
72 const typet &type)
const 74 if(type.
id() == ID_symbol_type)
79 assert(bv.size()==unknown.size());
80 assert(bv.size()>=offset+width);
82 if(type.
id()==ID_bool)
101 if(type.
id()==ID_array)
109 op.reserve(width/sub_width);
111 for(std::size_t new_offset=0;
113 new_offset+=sub_width)
116 bv_get_rec(bv, unknown, offset+new_offset, subtype));
124 else if(type.
id()==ID_struct_tag)
130 else if(type.
id()==ID_union_tag)
136 else if(type.
id()==ID_struct)
140 std::size_t new_offset=0;
142 op.reserve(components.size());
144 for(
const auto &c : components)
153 op.back()=
bv_get_rec(bv, unknown, offset+new_offset, subtype);
154 new_offset+=sub_width;
160 return std::move(dest);
162 else if(type.
id()==ID_union)
167 assert(!components.empty());
170 std::size_t component_nr=0;
175 components[component_nr].get_name());
177 const typet &subtype=components[component_nr].type();
181 return std::move(value);
183 else if(type.
id()==ID_vector)
188 if(sub_width!=0 && width%sub_width==0)
190 std::size_t size=width/sub_width;
194 for(std::size_t i=0; i<size; i++)
196 bv_get_rec(bv, unknown, i*sub_width, subtype));
198 return std::move(value);
201 else if(type.
id()==ID_complex)
206 if(sub_width!=0 && width==sub_width*2)
209 bv_get_rec(bv, unknown, 0 * sub_width, subtype),
210 bv_get_rec(bv, unknown, 1 * sub_width, subtype),
221 for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
241 if(type.
id()==ID_string)
267 width, [&value](
size_t i) {
return value[value.size() - i - 1] ==
'1'; });
277 std::vector<bool> unknown;
278 unknown.resize(bv.size(),
false);
284 if(expr.
type().
id()==ID_bool)
288 bv_cachet::const_iterator it=
bv_cache.find(expr);
310 if(size.
id()!=ID_infinity)
324 typedef std::map<mp_integer, exprt> valuest;
338 index_mapt::const_iterator it=
index_map.find(number);
342 for(index_sett::const_iterator it1=
344 it1!=index_set.end();
364 values[index_mpint]=value;
372 if(size_mpint>100 || size.
id()==ID_infinity)
377 result.operands().reserve(values.size()*2);
379 for(valuest::const_iterator it=values.begin();
384 result.copy_to_operands(index, it->second);
391 result.type().set(ID_size, size);
393 std::size_t size_int = numeric_cast_v<std::size_t>(size_mpint);
396 result.operands().resize(size_int);
398 for(std::size_t i=0; i<size_int; i++)
403 for(valuest::iterator it=values.begin();
406 if(it->first>=0 && it->first<size_mpint)
407 result.operands()[numeric_cast_v<std::size_t>(it->first)].swap(
422 for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
424 assert(bit_nr<bv.size());
430 default: assert(
false);
The type of an expression, extends irept.
union_find< exprt > arrays
const mp_integer string2integer(const std::string &n, unsigned base)
const std::string integer2string(const mp_integer &n, unsigned base)
virtual exprt bv_get_unbounded_array(const exprt &) const
exprt get(const exprt &expr) const override
size_type find_number(typename numbering< T >::const_iterator it) const
exprt simplify_expr(const exprt &src, const namespacet &ns)
std::set< exprt > index_sett
boolbv_widtht boolbv_width
bool is_unbounded_array(const typet &type) const override
std::vector< componentt > componentst
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
const componentst & components() const
typet & type()
Return the type of the expression.
A constant literal expression.
Structure type, corresponds to C style structs.
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
const irep_idt & id() const
The Boolean constant true.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Union constructor from single element.
API to expression classes.
const irep_idt & get(const irep_namet &name) const
numbering< irep_idt > string_numbering
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const exprt & size() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Vector constructor from list of elements.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bvtypet get_bvtype(const typet &type)
The Boolean constant false.
std::vector< exprt > operandst
mp_integer get_value(const bvt &bv)
optionalt< number_type > get_number(const T &a) const
exprt get(const exprt &expr) const override
mstreamt & result() const
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Base class for all expressions.
virtual exprt bv_get_rec(const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
virtual tvt l_get(literalt a) const =0
#define UNREACHABLE
This should be used to mark dead code.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const std::string & get_string(const irep_namet &name) const
void set_component_name(const irep_idt &component_name)
tv_enumt get_value() const
exprt bv_get(const bvt &bv, const typet &type) const
exprt bv_get_cache(const exprt &expr) const
const typet & subtype() const
Struct constructor from list of elements.
std::vector< literalt > bvt
Complex constructor from a pair of numbers.
void reserve_operands(operandst::size_type n)
Array constructor from a list of index-element pairs Operands are index/value pairs,...