22 if(operands.size()!=2)
23 throw "extractbit takes two operands";
28 if(operands[1].is_constant())
33 throw "extractbit failed to convert constant index";
35 if(o<0 || o>=bv0.size())
41 if(operands[0].type().
id()==ID_verilog_signedbv ||
42 operands[0].type().
id()==ID_verilog_unsignedbv)
52 if(width_op0==0 || width_op1==0)
55 std::size_t index_width = std::max(
address_bits(width_op0), width_op1);
70 for(std::size_t i=0; i<bv0.size(); i++)
83 for(std::size_t i=0; i<bv0.size(); i++)
Fixed-width bit-vector with unsigned binary interpretation.
literalt convert(const exprt &expr) override
boolbv_widtht boolbv_width
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
virtual literalt new_variable()=0
virtual const bvt & convert_bv(const exprt &expr)
API to expression classes.
bitvector_typet index_type()
std::vector< exprt > operandst
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
std::size_t integer2size_t(const mp_integer &n)
virtual literalt convert_extractbit(const extractbit_exprt &expr)
std::vector< literalt > bvt