4 ms·
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
by axman6 12y ago
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)
- pbsd 12y agoNo: 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.