9 #ifndef CPROVER_UTIL_BITVECTOR_EXPR_H
10 #define CPROVER_UTIL_BITVECTOR_EXPR_H
22 :
unary_exprt(ID_bswap, std::move(_op), std::move(_type))
40 set(ID_bits_per_byte, narrow_cast<long long>(bits_per_byte));
47 return base.
id() == ID_bswap;
54 value.
op().
type() == value.
type(),
"bswap type must match operand type");
92 return base.
id() == ID_bitnot;
136 return base.
id() == ID_bitor;
171 return base.
id() == ID_bitxor;
206 return base.
id() == ID_bitand;
233 :
binary_exprt(std::move(_src), _id, std::move(_distance))
263 return base.
id() == ID_shl || base.
id() == ID_ashr || base.
id() == ID_lshr ||
264 base.
id() == ID_ror || base.
id() == ID_rol;
298 :
shift_exprt(std::move(_src), ID_shl, std::move(_distance))
336 :
shift_exprt(std::move(_src), ID_ashr, std::move(_distance))
351 :
shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
356 :
shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
397 return base.
id() == ID_extractbit;
441 {std::move(_src), std::move(_upper), std::move(_lower)})
447 const std::size_t _upper,
448 const std::size_t _lower,
485 return base.
id() == ID_extractbits;
553 return base.
id() == ID_replication;
593 :
multi_ary_exprt(ID_concatenation, std::move(_operands), std::move(_type))
600 {std::move(_op0), std::move(_op1)},
609 return base.
id() == ID_concatenation;
636 :
unary_exprt(ID_popcount, std::move(_op), std::move(_type))
649 return base.
id() == ID_popcount;
bool can_cast_expr< replication_exprt >(const exprt &base)
bool can_cast_expr< bswap_exprt >(const exprt &base)
bool can_cast_expr< shift_exprt >(const exprt &base)
bool can_cast_expr< bitand_exprt >(const exprt &base)
bool can_cast_expr< popcount_exprt >(const exprt &base)
bool can_cast_expr< extractbits_exprt >(const exprt &base)
bool can_cast_expr< bitxor_exprt >(const exprt &base)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
bool can_cast_expr< bitor_exprt >(const exprt &base)
void validate_expr(const bswap_exprt &value)
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast an exprt to a bitxor_exprt.
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast an exprt to a bitand_exprt.
bool can_cast_expr< concatenation_exprt >(const exprt &base)
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
bool can_cast_expr< bitnot_exprt >(const exprt &base)
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
bool can_cast_expr< extractbit_exprt >(const exprt &base)
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast an exprt to a bitor_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
ashr_exprt(exprt _src, exprt _distance)
ashr_exprt(exprt _src, const std::size_t _distance)
A base class for binary expressions.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
bitand_exprt(const exprt &_op0, exprt _op1)
Bit-wise negation of bit-vectors.
bitor_exprt(const exprt &_op0, exprt _op1)
bitxor_exprt(exprt _op0, exprt _op1)
The byte swap expression.
bswap_exprt(exprt _op, std::size_t bits_per_byte)
std::size_t get_bits_per_byte() const
bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
void set_bits_per_byte(std::size_t bits_per_byte)
Concatenation of bit-vector operands.
concatenation_exprt(operandst _operands, typet _type)
concatenation_exprt(exprt _op0, exprt _op1, typet _type)
A constant literal expression.
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.
std::size_t get_size_t(const irep_namet &name) const
void set(const irep_namet &name, const irep_idt &value)
const irep_idt & id() const
lshr_exprt(exprt _src, const std::size_t _distance)
lshr_exprt(exprt _src, exprt _distance)
A base class for multi-ary expressions Associativity is not specified.
The popcount (counting the number of bits set to 1) expression.
popcount_exprt(exprt _op, typet _type)
popcount_exprt(const exprt &_op)
const constant_exprt & times() const
replication_exprt(constant_exprt _times, exprt _src, typet _type)
A base class for shift and rotate operators.
const exprt & distance() const
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
shl_exprt(exprt _src, const std::size_t _distance)
shl_exprt(exprt _src, exprt _distance)
The type of an expression, extends irept.
Generic base class for unary expressions.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
API to expression classes.