kdrag.theories.bitvec.UnConcat

kdrag.theories.bitvec.UnConcat(x: BitVecRef, lane_num: int) → list[BitVecRef]

Unpack a bitvector into lanes.

>>> x,y = smt.BitVecs("x y", 32)
>>> kd.prove(smt.Concat(UnConcat(x, 4)) == x)
|= Concat(Concat(Concat(Extract(31, 24, x), Extract(23, 16, x)),
              Extract(15, 8, x)),
       Extract(7, 0, x)) == x
>>> kd.prove(UnConcat(smt.Concat(x,y), 2)[0] == x)
|= Extract(63, 32, Concat(x, y)) == x

Parameters:

x (BitVecRef)
lane_num (int)

Return type:

list[BitVecRef]