kdrag.theories.bitvec.vmap

kdrag.theories.bitvec.vmap(f, n)

>>> x,y = smt.BitVecs("x y", 16)
>>> kd.prove(vmap(lambda a: a, 2)(x) == x)
|= Concat(Extract(15, 8, x), Extract(7, 0, x)) == x
>>> vmap(lambda a,b: a - b, 2)(x, y)
Concat(Extract(15, 8, x) - Extract(15, 8, y),
       Extract(7, 0, x) - Extract(7, 0, y))