49 const typet &type)
const
53 assert(bv.size()>=offset+width);
58 switch(
prop.
l_get(bv[offset]).get_value())
97 dest.operands().swap(op);
109 result.
type() = type;
116 result.
type() = type;
125 op.reserve(components.size());
127 for(
const auto &
c : components)
129 const typet &subtype =
c.type();
146 if(components.empty())
173 for(std::size_t
i=0;
i<size;
i++)
181 return std::move(value);
261 width, [&value](
size_t i) {
return value[value.size() -
i - 1] ==
'1'; });
280 bv_cachet::const_iterator it=
bv_cache.find(expr);
306 typedef std::map<mp_integer, exprt> valuest;
316 index_mapt::const_iterator it=
index_map.find(number);
320 for(index_sett::const_iterator
it1=
352 result.
operands().reserve(values.size()*2);
354 for(valuest::const_iterator it=values.begin();
373 for(valuest::iterator it=values.begin();
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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
optionalt< std::reference_wrapper< const map_entryt > > get_map_entry(const irep_idt &identifier) const
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
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
virtual exprt bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset, 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 &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Union constructor to support unions without any member (a GCC/Clang feature).
Base class for all expressions.
std::vector< exprt > operandst
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
void reserve_operands(operandst::size_type n)
typet & type()
Return the type of the expression.
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.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
virtual tvt l_get(literalt a) const =0
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
std::vector< componentt > componentst
The Boolean constant true.
const typet & subtype() const
The type of an expression, extends irept.
Union constructor from single element.
size_type find_number(const_iterator it) const
optionalt< number_type > get_number(const T &a) const
Vector constructor from list of elements.
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 PRECONDITION(CONDITION)
API to expression classes.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_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.