28 if(index_as_integer < 0 || index_as_integer >= src_bv.size())
31 return src_bv[numeric_cast_v<std::size_t>(index_as_integer)];
35 expr.
src().
type().
id() == ID_verilog_signedbv ||
36 expr.
src().
type().
id() == ID_verilog_unsignedbv)
39 "extractbit expression not implemented for verilog integers in " 47 if(src_bv_width == 0 || index_bv_width == 0)
50 std::size_t index_width =
66 for(std::size_t i = 0; i < src_bv.size(); i++)
79 for(std::size_t i = 0; i < src_bv.size(); i++)
Fixed-width bit-vector with unsigned binary interpretation.
literalt convert(const exprt &expr) override
boolbv_widtht boolbv_width
Thrown when we encounter an instruction, parameters to an instruction etc.
typet & type()
Return the type of the expression.
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
const irep_idt & id() const
virtual literalt new_variable()=0
API to expression classes.
virtual bool literal(const exprt &expr, std::size_t bit, literalt &literal) const
bitvector_typet index_type()
bool is_constant() const
Return whether the expression is a constant.
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt equality(const exprt &e1, const exprt &e2)
virtual bool has_set_to() const
virtual literalt convert_rest(const exprt &expr)
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual literalt convert_extractbit(const extractbit_exprt &expr)
std::vector< literalt > bvt