26 expr.
id() == ID_byte_update_little_endian ||
27 expr.
id() == ID_byte_update_big_endian);
28 const bool little_endian = expr.
id() == ID_byte_update_little_endian;
33 std::size_t update_width=value_bv.size();
34 std::size_t byte_width=8;
36 if(update_width>bv.size())
37 update_width=bv.size();
41 const auto index = numeric_cast<mp_integer>(offset_expr);
47 if(offset+update_width>
mp_integer(bv.size()) || offset<0)
55 for(std::size_t i=0; i<update_width; i++)
56 bv[numeric_cast_v<std::size_t>(offset + i)] = value_bv[i];
63 const std::size_t offset_i = numeric_cast_v<std::size_t>(offset);
65 for(std::size_t i=0; i<update_width; i++)
67 size_t index_op=map_op.map_bit(offset_i+i);
68 size_t index_value=map_value.map_bit(i);
71 index_op < bv.size(),
"bit vector index shall be within bounds");
73 index_value < value_bv.size(),
74 "bit vector index shall be within bounds");
76 bv[index_op]=value_bv[index_value];
85 for(std::size_t offset=0; offset<bv.size(); offset+=byte_width)
96 for(std::size_t bit=0; bit<update_width; bit++)
97 if(offset+bit<bv.size())
99 std::size_t bv_o=map_op.
map_bit(offset+bit);
100 std::size_t value_bv_o=map_value.map_bit(bit);
102 bv[bv_o]=
prop.
lselect(equal, value_bv[value_bv_o], bv[bv_o]);