Select one bit in BitVec

[Muxucao0812]

I want to implement two operations:

1. vector[index] = val
2. variable = vector[index]
   And val, index, vector, and variable are all terms, index is the term of one number, maybe index = BitVec("index", 4) index = 0b0100, how can I implement these operations? Thanks

[NikolajBjorner]

you can extract a range, but not a single bit. Extract(v, k, k) is a bit-vector of length 1. It is either BitVecVal(0,1) or BitVecVal(1,1). You can compare the result of extraction to get a Boolean. To update the "index"th entry of vector you have
vector_updated = Concat(Extract(vector, vector_length - 1, index+1), If(val, BitVecVal(1,1), BitVecVal(0,1)), Extract(vector, index - 1, 0)).

[Muxucao0812]

for the extract function, the index needs to be some determined number, but I want to use the symbolic expression as the index, if it can build some functions to achieve that

[NikolajBjorner]

For bit-vectors you can't use symbolic indices. You can use a big if-then-else statement to dispatch on the symbolic index.

[Muxucao0812]

Thanks! You provide a feasible solution. But i want to know why vector couldn't extract by symbolic expression, I think that like the operation Select of Array.

[NikolajBjorner]

bit-vectors are typically not used in the same domains as arrays. Extraction at variable offsets isn't built-in as the main use case for bit-vectors is that they have fixed (and relatively small) sizes.
There are also "sequences", that enjoy some intersections with arrays. In z3, sequences are tuned towards theories where you want extensional equality between objects of sequence sort.