Hacker News Reader

Comment by axman6 | Hacker News Reader

Is that second implementation in Hacker's Delight? Also it'd be interesting to see how z3 handles the examples shown there too (the logarithmic time algorithms using

    x'  = (x  & b10101010) >> 1 + x  & b01010101
    x'' = (x' & b11001100) >> 2 + x' & b00110011

or whatever it is)

View on HN

No: Z3 proves the Hacker's Delight* trick almost instantly. The implementation above is not actually faster in practice, so it's rarely used; but its equivalence to popcount relies on Z/2^64Z properties that solvers do not seem familiar with.

* This sort of trick is much older than Hacker's Delight, by the way; Knuth tracks it down to the 1950s in Volume 4A.

Reply on news.ycombinator.com