CODEWITHSUNDEEP
z3z3py
lllllllllllll
lllllllllllll

Reputation: 9140

Sum of all the bits in a Bit Vector of Z3

Given a bit vector in Z3, I am wondering how can I sum up each individual bit of this vector?

E.g.,

a = BitVecVal(3, 2)
sum_all_bit(a) = 2

Is there any pre-implemented APIs/functions that support this? Thank you!

Upvotes: 1

Views: 2919

Answers (3)

mborowczak
mborowczak

Reputation: 181

So you're computing the Hamming Weight of a bit vector. Based on a previous question I had, one of the developers had this answer. Based on that original answer, this is how I do it today:

def HW(bvec):
    return Sum([ ZeroExt(int(ceil(log2(bvec.size()))), Extract(i,i,bvec)) for i in range(bvec.size())])

Upvotes: 2

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

It isn't part of the bit-vector operations. You can create an expression as follows:

def sub(b):
    n = b.size()
    bits = [ Extract(i, i, b) for i in range(n) ]
    bvs  = [ Concat(BitVecVal(0, n - 1), b) for b in bits ]
    nb   = reduce(lambda a, b: a + b, bvs)
    return nb


print sub(BitVecVal(4,7))

Of course, log(n) bits for the result will suffice if you prefer.

Upvotes: 2

alias
alias

Reputation: 30525

The page:

https://graphics.stanford.edu/~seander/bithacks.html#CountBitsSetNaive

has various algorithms for counting the bits; which can be translated to Z3/Python with relative ease, I suppose.

My favorite is: https://graphics.stanford.edu/~seander/bithacks.html#CountBitsSetKernighan

which has the nice property that it loops as many times as there are set bits in the input. (But you shouldn't extrapolate from that to any meaningful complexity metric, as you do arithmetic in each loop, which might be costly. The same is true for all these algorithms.)

Having said that, if your input is fully symbolic, you can't really beat the simple iterative algorithm, as you can't short-cut the iteration count. Above methods might work faster if the input has concrete bits.

Upvotes: 2

Related Questions