[Back] We can use Z3 to prove claims. For example, we can prove that "And(x != 0, x & (x - 1) == 0)" can be used as a quick test for x to see if it is a powers of 2:

Equation: And(x!=0,x&(x-1)==0)

In this case we are proving against:

powers = [ 2**i for i in range(32) ] slow = Or([ x == p for p in powers ])

The following a sample run:

Equ01: And(x != 0, x & (x - 1) == 0) Equ02: Or([ x == p for p in powers ]) Is it proven? proved None [1, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32768, 65536, 131072, 262144, 524288, 1048576, 2097152, 4194304, 8388608, 16777216, 33554432, 67108864, 134217728, 268435456, 536870912, 1073741824, 2147483648L]

In the following code we take the random numbers and then mask of the least significant bit and define it as a "Head" or a "Tail":

from z3 import * import sys eq = 'And(x != 0, x & (x - 1) == 0)' if (len(sys.argv)>1): eq=str(sys.argv[1]) x = BitVec('x', 32) powers = [ 2**i for i in range(32) ] fast = eval(eq) slow = Or([ x == p for p in powers ]) print ("Is it proven?",prove(fast == slow)) print (powers)