4 ms·
SMT solvers have been getting better and better, but they still fail at relatively simple things. I often use them to prove certain low-level optimizations are
by pbsd 12y ago
SMT solvers have been getting better and better, but they still fail at relatively simple things. I often use them to prove certain low-level optimizations are correct, and sometimes simple things completely choke the solver.
The following is a simple example of a popcount implementation, relatively easy to prove correct by a human, but that Z3 (and presumably others, but I haven't tried) is unable to solve in a reasonable amount of time. Using z3py for convenience:
from z3 import *
def popcount1(x):
return Sum([ ZeroExt(6, Extract(i,i,x)) for i in range(64) ])
def popcount2(x):
return Extract(6, 0, -Sum([ RotateLeft(x, i) for i in range(64) ]))
x = BitVec("x", 64)
prove(popcount1(x) == popcount2(x))
- axman6 12y agoIs 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.