24 if(expr.
id()==ID_symbol ||
25 expr.
id()==ID_nondet_symbol)
29 boolbv_mapt::mappingt::const_iterator it=
41 std::vector<bool> unknown;
43 std::size_t width=map_entry.
width;
46 unknown.resize(width);
48 for(std::size_t bit_nr=0; bit_nr<width; bit_nr++)
54 unknown[bit_nr]=
false;
74 const std::vector<bool> &unknown,
76 const typet &type)
const
80 assert(bv.size()==unknown.size());
81 assert(bv.size()>=offset+width);
83 if(type.
id()==ID_bool)
104 if(type.
id()==ID_array)
115 op.reserve(width/sub_width);
117 for(std::size_t new_offset=0;
119 new_offset+=sub_width)
124 bv_get_rec(index, bv, unknown, offset + new_offset, subtype));
132 else if(type.
id()==ID_struct_tag)
136 result.
type() = type;
139 else if(type.
id()==ID_union_tag)
143 result.
type() = type;
146 else if(type.
id()==ID_struct)
150 std::size_t new_offset=0;
152 op.reserve(components.size());
154 for(
const auto &c : components)
156 const typet &subtype = c.type();
160 bv_get_rec(member, bv, unknown, offset + new_offset, subtype));
164 new_offset+=sub_width;
169 else if(type.
id()==ID_union)
174 assert(!components.empty());
177 std::size_t component_nr=0;
179 const typet &subtype = components[component_nr].type();
182 expr, components[component_nr].get_name(), subtype};
184 components[component_nr].get_name(),
185 bv_get_rec(member, bv, unknown, offset, subtype),
188 else if(type.
id()==ID_vector)
193 if(sub_width!=0 && width%sub_width==0)
195 std::size_t size=width/sub_width;
199 for(std::size_t i=0; i<size; i++)
203 bv_get_rec(index, bv, unknown, i * sub_width, subtype));
206 return std::move(value);
209 else if(type.
id()==ID_complex)
214 if(sub_width!=0 && width==sub_width*2)
231 for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
252 if(type.
id()==ID_string)
263 else if(type.
id() == ID_empty)
290 width, [&value](
size_t i) {
return value[value.size() - i - 1] ==
'1'; });
300 std::vector<bool> unknown;
301 unknown.resize(bv.size(),
false);
307 if(expr.
type().
id()==ID_bool)
311 bv_cachet::const_iterator it=
bv_cache.find(expr);
330 const auto size_opt = numeric_cast<mp_integer>(size);
331 if(size_opt.has_value() && *size_opt >= 0)
332 size_mpint = *size_opt;
337 typedef std::map<mp_integer, exprt> valuest;
341 if(opt_num.has_value())
347 index_mapt::const_iterator it=
index_map.find(number);
351 for(index_sett::const_iterator it1=
353 it1!=index_set.end();
363 const auto index_mpint = numeric_cast<mp_integer>(index_value);
365 if(index_mpint.has_value())
368 values[*index_mpint] =
exprt(ID_unknown, type.
subtype());
370 values[*index_mpint] = value;
378 if(values.size() != size_mpint)
382 result.
operands().reserve(values.size()*2);
384 for(valuest::const_iterator it=values.begin();
395 result=
exprt(ID_array, type);
398 std::size_t size_int = numeric_cast_v<std::size_t>(size_mpint);
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);