function to get nibbles using Z3 and bitvector theory

Question

I'm trying to learn a little about z3 and the bit vector theory. My intention is to make a function to get the nibble from a position of the bitvector

This code returns the nibble:

(define-fun g_nibble(
   (l ( _ BitVec 12))
   (idx (Int))
) ( _ BitVec 4)

(ite
    (= idx 1) ((_ extract 11 8) l)
    (ite
        (= idx 2) ((_ extract 7 4) l)
        (ite
            (= idx 3) ((_ extract 3 0) l)     
            (_ bv0 4)
        )
    )
))

the problem is that i want avoid the multiples ite calls. I tried to replace ((_ extract 3 0) l) for somthing like ((_ extract (+ 4 idx) idx l) but it doesn't work.

Thanks

P.S: The idea is use z3 from command line (without using any library).

Answer 1

The extract function only takes numerals as arguments, not arbitrary expressions. However, we can shift the expression to one direction and then extract the first or last four bits, e.g. along the lines of

((_ extract 11 8) (bvshl l (bvmul idx four)))

(where idx and four are bit-vector expressions of size 12).