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)
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(struct_typet::componentst::const_iterator
145 it=components.begin();
146 it!=components.end();
156 op.back()=
bv_get_rec(bv, unknown, offset+new_offset, subtype);
157 new_offset+=sub_width;
165 else if(type.
id()==ID_union)
170 assert(!components.empty());
173 std::size_t component_nr=0;
178 components[component_nr].get_name());
180 const typet &subtype=components[component_nr].type();
186 else if(type.
id()==ID_vector)
191 if(sub_width!=0 && width%sub_width==0)
193 std::size_t size=width/sub_width;
194 exprt value(ID_vector, type);
197 for(std::size_t i=0; i<size; i++)
199 bv_get_rec(bv, unknown, i*sub_width, subtype));
204 else if(type.
id()==ID_complex)
209 if(sub_width!=0 && width==sub_width*2)
211 exprt value(ID_complex, type);
224 for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
236 default: assert(
false);
246 if(type.
id()==ID_string)
282 std::vector<bool> unknown;
283 unknown.resize(bv.size(),
false);
289 if(expr.
type().
id()==ID_bool)
293 bv_cachet::const_iterator it=
bv_cache.find(expr);
315 if(size.
id()!=ID_infinity)
329 typedef std::map<mp_integer, exprt> valuest;
342 index_mapt::const_iterator it=
index_map.find(number);
346 for(index_sett::const_iterator it1=
348 it1!=index_set.end();
368 values[index_mpint]=value;
376 if(size_mpint>100 || size.
id()==ID_infinity)
381 result.operands().reserve(values.size()*2);
383 for(valuest::const_iterator it=values.begin();
388 result.copy_to_operands(index, it->second);
395 result.type().set(ID_size, size);
400 result.operands().resize(size_int);
402 for(std::size_t i=0; i<size_int; i++)
407 for(valuest::iterator it=values.begin();
410 if(it->first>=0 && it->first<size_mpint)
425 for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
427 assert(bit_nr<bv.size());
433 default: assert(
false);
The type of an expression.
const typet & follow(const typet &src) const
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
virtual 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
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
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
A constant literal expression.
const typet & follow_tag(const union_tag_typet &src) const
const irep_idt & id() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
bool get_number(const T &a, number_type &n) const
void set_value(const irep_idt &value)
The boolean constant true.
union constructor from single element
API to expression classes.
const irep_idt & get(const irep_namet &name) const
numbering< irep_idt > string_numbering
const exprt & size() const
bvtypet get_bvtype(const typet &type)
The boolean constant false.
std::vector< exprt > operandst
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
mp_integer get_value(const bvt &bv)
exprt get(const exprt &expr) const override
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_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
virtual tvt l_get(literalt a) const =0
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
std::size_t integer2size_t(const mp_integer &n)
const typet & subtype() const
struct constructor from list of elements
std::vector< literalt > bvt
void reserve_operands(operandst::size_type n)