Go to the documentation of this file.
22 if(expr.
id()==ID_symbol ||
23 expr.
id()==ID_nondet_symbol)
29 if(map_entry_opt.has_value())
49 const typet &type)
const
53 assert(bv.size()>=offset+width);
55 if(type.
id()==ID_bool)
69 if(bvtype==bvtypet::IS_UNKNOWN)
71 if(type.
id()==ID_array)
82 op.reserve(width/sub_width);
84 for(std::size_t new_offset=0;
86 new_offset+=sub_width)
90 op.push_back(
bv_get_rec(index, bv, offset + new_offset, subtype));
102 else if(type.
id()==ID_struct_tag)
106 result.
type() = type;
109 else if(type.
id()==ID_union_tag)
113 result.
type() = type;
116 else if(type.
id()==ID_struct)
120 std::size_t new_offset=0;
122 op.reserve(components.size());
124 for(
const auto &c : components)
126 const typet &subtype = c.type();
129 op.push_back(
bv_get_rec(member, bv, offset + new_offset, subtype));
133 new_offset+=sub_width;
138 else if(type.
id()==ID_union)
143 assert(!components.empty());
146 std::size_t component_nr=0;
148 const typet &subtype = components[component_nr].type();
151 expr, components[component_nr].get_name(), subtype};
153 components[component_nr].get_name(),
157 else if(type.
id()==ID_vector)
162 if(sub_width!=0 && width%sub_width==0)
164 std::size_t size=width/sub_width;
168 for(std::size_t i=0; i<size; i++)
172 bv_get_rec(index, bv, i * sub_width, subtype));
175 return std::move(value);
178 else if(type.
id()==ID_complex)
183 if(sub_width!=0 && width==sub_width*2)
198 for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
215 case bvtypet::IS_UNKNOWN:
217 if(type.
id()==ID_string)
228 else if(type.
id() == ID_empty)
234 case bvtypet::IS_RANGE:
244 case bvtypet::IS_VERILOG_UNSIGNED:
245 case bvtypet::IS_VERILOG_SIGNED:
246 case bvtypet::IS_C_BOOL:
247 case bvtypet::IS_FIXED:
248 case bvtypet::IS_FLOAT:
249 case bvtypet::IS_UNSIGNED:
250 case bvtypet::IS_SIGNED:
252 case bvtypet::IS_C_ENUM:
255 width, [&value](
size_t i) {
return value[value.size() - i - 1] ==
'1'; });
270 if(expr.
type().
id()==ID_bool)
274 bv_cachet::const_iterator it=
bv_cache.find(expr);
293 const auto size_opt = numeric_cast<mp_integer>(size);
294 if(size_opt.has_value() && *size_opt >= 0)
295 size_mpint = *size_opt;
300 typedef std::map<mp_integer, exprt> valuest;
304 if(opt_num.has_value())
310 index_mapt::const_iterator it=
index_map.find(number);
314 for(index_sett::const_iterator it1=
316 it1!=index_set.end();
326 const auto index_mpint = numeric_cast<mp_integer>(index_value);
328 if(index_mpint.has_value())
331 values[*index_mpint] =
exprt(ID_unknown, type.
subtype());
333 values[*index_mpint] = value;
341 if(values.size() != size_mpint)
345 result.
operands().reserve(values.size()*2);
347 for(valuest::const_iterator it=values.begin();
358 result=
exprt(ID_array, type);
361 std::size_t size_int = numeric_cast_v<std::size_t>(size_mpint);
366 for(valuest::iterator it=values.begin();
369 if(it->first>=0 && it->first<size_mpint)
370 result.
operands()[numeric_cast_v<std::size_t>(it->first)].swap(
385 for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
387 assert(bit_nr<bv.size());
393 default: assert(
false);
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
#define UNREACHABLE
This should be used to mark dead code.
const componentst & components() const
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const typet & subtype() const
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
bool is_unbounded_array(const typet &type) const override
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
std::vector< literalt > bvt
const mp_integer string2integer(const std::string &n, unsigned base)
virtual exprt bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset, const typet &type) const
Real part of the expression describing a complex number.
Union constructor from single element.
bvtypet get_bvtype(const typet &type)
Base class for all expressions.
std::vector< componentt > componentst
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Vector constructor from list of elements.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
optionalt< number_type > get_number(const T &a) const
bitvector_typet index_type()
Struct constructor from list of elements.
const exprt & size() const
typet & type()
Return the type of the expression.
size_type find_number(const_iterator it) const
virtual std::size_t boolbv_width(const typet &type) const
#define PRECONDITION(CONDITION)
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
exprt simplify_expr(exprt src, const namespacet &ns)
std::set< exprt > index_sett
exprt bv_get_cache(const exprt &expr) const
const irep_idt & id() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
std::vector< exprt > operandst
Complex constructor from a pair of numbers.
The Boolean constant false.
mp_integer get_value(const bvt &bv)
virtual exprt bv_get_unbounded_array(const exprt &) const
optionalt< std::reference_wrapper< const map_entryt > > get_map_entry(const irep_idt &identifier) const
Extract member of struct or union.
const std::string & get_string(const irep_namet &name) const
Structure type, corresponds to C style structs.
virtual tvt l_get(literalt a) const =0
const irep_idt & get(const irep_namet &name) const
exprt bv_get(const bvt &bv, const typet &type) const
numberingt< irep_idt > string_numbering
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Imaginary part of the expression describing a complex number.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Array constructor from a list of index-element pairs Operands are index/value pairs,...
union_find< exprt, irep_hash > arrays
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
tv_enumt get_value() const
The Boolean constant true.
A constant literal expression.
void reserve_operands(operandst::size_type n)
API to expression classes.
Array constructor from list of elements.
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
const std::string integer2string(const mp_integer &n, unsigned base)