#include <stdint.h>
#include <stdio.h>
#include <assert.h>

// time cbmc --trace --function check 1.c

// copypasted from https://en.wikipedia.org/wiki/Hamming_weight and reworked

const uint64_t m1  = 0x5555555555555555;
const uint64_t m2  = 0x3333333333333333;
const uint64_t m4  = 0x0f0f0f0f0f0f0f0f;
const uint64_t m8  = 0x00ff00ff00ff00ff;
const uint64_t m16 = 0x0000ffff0000ffff;
const uint64_t m32 = 0x00000000ffffffff;
const uint64_t h01 = 0x0101010101010101;

int popcount64a(uint64_t x)
{
	x = (x & m1 ) + ((x >>  1) & m1 );
	x = (x & m2 ) + ((x >>  2) & m2 );
	x = (x & m4 ) + ((x >>  4) & m4 );
	x = (x & m8 ) + ((x >>  8) & m8 );
	x = (x & m16) + ((x >> 16) & m16);
	x = (x & m32) + ((x >> 32) & m32);
	return x;
}

int popcount64b(uint64_t x)
{
	x -= (x >> 1) & m1;             
	x = (x & m2) + ((x >> 2) & m2); 
	x = (x + (x >> 4)) & m4;        
	x += x >>  8;
	x += x >> 16;
	x += x >> 32;
	return x & 0x7f;
}

int popcount64c(uint64_t x)
{
	x -= (x >> 1) & m1;             
	x = (x & m2) + ((x >> 2) & m2); 
	x = (x + (x >> 4)) & m4;        
	return (x * h01) >> 56;
}

// Kernighan's...

int popcount64d(uint64_t x)
{
	int count;
	for (count=0; x; count++)
		x &= x - 1; // x = x & (x-1)
	return count;
}

int popcount64d_my(uint64_t x)
{
	int count;
	for (count=0; count<64 && x; count++)
		x &= x - 1;
	return count;
}

// Kernighan's unrolled...

int popcount64d_unrolled(uint64_t x)
{
	int count=0;
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};
	if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};if (x) {x &= x-1; count++;};

	// be sure x==0 upon the function exit...
	assert(x==0);
	return count;
}

int popcount64_naive(uint64_t x)
{
	uint64_t rt=0, i;
	for (i=0; i<64; i++)
		rt=rt+((x>>i)&1);
	return rt;
}

int popcount64_table(uint64_t x)
{
	uint64_t tbl[16]={0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4};

	uint64_t rt=0;

	rt=rt+tbl[(x>>(0*4))&0xf];
	rt=rt+tbl[(x>>(1*4))&0xf];
	rt=rt+tbl[(x>>(2*4))&0xf];
	rt=rt+tbl[(x>>(3*4))&0xf];
	rt=rt+tbl[(x>>(4*4))&0xf];
	rt=rt+tbl[(x>>(5*4))&0xf];
	rt=rt+tbl[(x>>(6*4))&0xf];
	rt=rt+tbl[(x>>(7*4))&0xf];
	rt=rt+tbl[(x>>(8*4))&0xf];
	rt=rt+tbl[(x>>(9*4))&0xf];
	rt=rt+tbl[(x>>(10*4))&0xf];
	rt=rt+tbl[(x>>(11*4))&0xf];
	rt=rt+tbl[(x>>(12*4))&0xf];
	rt=rt+tbl[(x>>(13*4))&0xf];
	rt=rt+tbl[(x>>(14*4))&0xf];
	rt=rt+tbl[(x>>(15*4))&0xf];
	
	return rt;
}

int popcount64_table2(uint64_t x)
{
	uint64_t tbl[256]={
0, 1, 1, 2, 1, 2, 2, 3, 1, 2, 2, 3, 2, 3, 3, 4, 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5,
1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6,
1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6,
2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7,
1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6,
2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7,
2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7,
3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 4, 5, 5, 6, 5, 6, 6, 7, 5, 6, 6, 7, 6, 7, 7, 8};

	uint64_t rt=0;

	rt=rt+tbl[(x>>(0*8))&0xff];
	rt=rt+tbl[(x>>(1*8))&0xff];
	rt=rt+tbl[(x>>(2*8))&0xff];
	rt=rt+tbl[(x>>(3*8))&0xff];
	rt=rt+tbl[(x>>(4*8))&0xff];
	rt=rt+tbl[(x>>(5*8))&0xff];
	rt=rt+tbl[(x>>(6*8))&0xff];
	rt=rt+tbl[(x>>(7*8))&0xff];
	
	return rt;
}

// from https://www.chessprogramming.org/Population_Count
int hakmem169_32(uint32_t x)
{
   x = x  - ((x >> 1)  & 033333333333)
          - ((x >> 2)  & 011111111111);
   x = (x +  (x >> 3)) & 030707070707 ;
   return x % 63; /* casting out 63 */
} 

int hakmem169_64(uint64_t x)
{
	return hakmem169_32(x>>32) + hakmem169_32(x&0xffffffff);
};

void check(uint64_t c)
{
        //assert (popcount64d_unrolled(c)==popcount64a(c)); // ~980s (~16m)
        assert (popcount64a(c)==popcount64b(c)); // fast
        //assert (popcount64b(c)==popcount64c(c)); // fast
        //assert (popcount64c(c)==popcount64a(c)); // fast
        //assert (popcount64a(c)==popcount64_naive(c)); // 10s
	//assert (popcount64a(c)==popcount64_table(c)); // fast
	//assert (popcount64a(c)==hakmem169_64(c)); // 163s
	//assert (popcount64_naive(c)==popcount64_table(c)); // fast
	//assert (popcount64a(c)==popcount64_table2(c)); // fast
        //assert (popcount64a(c)==popcount64d(c)); // infinite "unwinding loop"
        //assert (popcount64a(c)==popcount64d_my(c)); // ~2520s (~42m)
};

int main()
{
};