/* Count Boolean theories of up to n = 4 variables,
   modulo complementation of literals and interchange of variables
   Author: V.R. Pratt
   Date:   6/12/05
*/

#include <stdio.h>
#include <stdlib.h>

uint p[4] = {0xaaaa, 0xcccc, 0xf0f0, 0xff00}; /* p_0 through p_3 */
uint r[65536];                                /* r[t] = reduct of theory t */
uint chng;

#define min(a,b)	((a)<(b)? (a): (b))

void
join(uint t, uint s)
{
    chng |= (r[s] != r[t]);		/* record pending change in r */
    r[s] = r[t] = min(r[s], r[t]);	/* join the reducts of s and t */
}

int
main(int argc, char **argv)
{
    uint i, j, t, cnt, n;
    n = (argc > 1)? atoi(argv[1]): 4;
    if (n < 0 || n > 4)
    	printf("%s n  where n is between 0 and 4\n", argv[0]), exit(1);
    for (t = 1; t < (1<<(1<<n)) - 1; t++)
    	r[t] = t;            /* initially every theory reduces to itself */
    do {
	chng = 0;
	for (t = 1; t < (1<<(1<<n)) - 1; t++)
	    for (i = 0; i < n; i++) {
		/* complement p_i */
		join(t, ((t & p[i]) >> (1<<i)) | ((t & ~p[i]) << (1<<i)));
		for (j = i+1; j < n; j++)
		    /* interchange p_i and p_j */
		    join(t, ((t & ~p[j] & p[i]) << ((1<<j) - (1<<i))) |
			    ((t & p[j] & ~p[i]) >> ((1<<j) - (1<<i))) |
			    (t & ~(p[j] ^ p[i])));
	    }
    } while (chng);
    for (t = 1, cnt = 0; t < (1<<(1<<n)) - 1; t++)
	cnt += (r[t] == t);  /* count the theories that reduce to themselves */
    printf("%d\n", cnt);
    return 0;
}