18 const std::size_t _distance)
33 const std::size_t _upper,
34 const std::size_t _lower,
76 const auto new_value_width =
82 return index >= new_value_width;
119 const std::size_t new_width = numeric_cast_v<std::size_t>(
power(2, bits));
121 const bool need_typecast =
122 new_width > x_width || x.
type().
id() != ID_unsignedbv;
128 for(std::size_t shift = 1; shift < new_width; shift <<= 1)
135 std::string bitstring;
136 bitstring.reserve(new_width);
137 for(std::size_t i = 0; i < new_width / (2 * shift); ++i)
138 bitstring += std::string(shift,
'0') + std::string(shift,
'1');
163 const std::size_t new_width = numeric_cast_v<std::size_t>(
power(2, bits));
165 const bool need_typecast =
166 new_width > x_width || x.
type().
id() != ID_unsignedbv;
172 for(std::size_t shift = 1; shift < new_width; shift <<= 1)
205 result_bits.reserve(int_width);
208 for(std::size_t i = 0; i < int_width; ++i)
217 if(
lhs().
type().
id() == ID_unsignedbv)
220 if(
rhs().
type().
id() == ID_unsignedbv)
223 std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1;
236 if(
lhs().
type().
id() == ID_unsignedbv)
239 if(
rhs().
type().
id() == ID_unsignedbv)
242 std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1;
255 if(
lhs().
type().
id() == ID_unsignedbv)
258 if(
rhs().
type().
id() == ID_unsignedbv)
261 std::size_t ssize = lhs_ssize + rhs_ssize;
API to expression classes for bitvectors.
Pre-defined bitvector types.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
A base class for binary expressions.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Bit-wise negation of bit-vectors.
exprt lower() const
Lower a bitreverse_exprt to arithmetic and logic expressions.
std::size_t get_width() const
Fixed-width bit-vector without numerical interpretation.
Concatenation of bit-vector operands.
A constant literal expression.
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
exprt lower() const
Lower a count_leading_zeros_exprt to arithmetic and logic expressions.
exprt lower() const
Lower a count_trailing_zeros_exprt to arithmetic and logic expressions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
exprt lower() const
Lower a find_first_set_exprt to arithmetic and logic expressions.
Unbounded, signed integers (mathematical integers, not bitvectors)
const irep_idt & id() const
exprt lower() const
Lower a minus_overflow_exprt to arithmetic and logic expressions.
Binary multiplication Associativity is not specified.
exprt lower() const
Lower a mult_overflow_exprt to arithmetic and logic expressions.
The plus expression Associativity is not specified.
exprt lower() const
Lower a plus_overflow_exprt to arithmetic and logic expressions.
The popcount (counting the number of bits set to 1) expression.
exprt lower() const
Lower a popcount_exprt to arithmetic and logic expressions.
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
Fixed-width bit-vector with two's complement interpretation.
Expression to hold a symbol (variable)
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Fixed-width bit-vector with unsigned binary interpretation.
exprt lower() const
A lowering to masking, shifting, or.
exprt lower() const
A lowering to masking, shifting, or.
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)