#include <u.h>
#include <libc.h>
#include <sat.h>

typedef struct Port Port;
typedef struct Link Link;

struct Port {
	int gate;
	uchar type;
	uchar pin;
	int num;
	char let;
};
enum {
	PORTIN,
	PORTOUT,
	PORTNAND,
};

struct Link {
	Port *i, *o;
	int num;
};

Port *ports, *ins, *outs, *gpins;
int nports, nins, nouts;
Link *links;
int nlinks;

int ngates;
int varnum = 1;

u64int truth;

void
mklink(Port *a, Port *b)
{
	Link *lp;
	
	links = realloc(links, (nlinks + 1) * sizeof(Link));
	memset(&links[nlinks], 0, sizeof(Link));
	links[nlinks].i = a;
	links[nlinks].o = b;
	links[nlinks++].num = varnum++;
}

void
linksat(SATSolve *s)
{
	Link *l;
	Port *p;
	int *a, n;
	int i;
	
	for(l = links; l < links + nlinks; l++)
		for(i = 0; i < 1<<nins; i++){
//			print("link %d in %d out %d\n", l->num, l->i->num + i, l->o->num + i);
			sataddv(s, -l->num, l->i->num + i, -(l->o->num + i), 0);
			sataddv(s, -l->num, -(l->i->num + i), l->o->num + i, 0);
		}
	a = nil;
	for(p = ports; p < ports + nports; p++){
		n = 0;
		for(l = links; l < links + nlinks; l++)
			if(l->o == p){
				a = realloc(a, sizeof(int) * (n + 1));
				a[n++] = l->num;
			}
		if(n > 0)
			satrange1(s, a, n, 1, 1);
	}
	free(a);
}

void
insat(SATSolve *s)
{
	int i;
	Port *p;
	
	for(p = ins; p < ins + nins; p++)
		for(i = 0; i < 1<<nins; i++){
//			print("in %d state %x val %d (var %d)\n", p->gate, i, (i&1<<p-ins)!=0, p->num + i);
			if((i&1<<p->gate) != 0)
				sataddv(s, p->num + i, 0);
			else
				sataddv(s, -(p->num + i), 0);
		}
}

void
outsat(SATSolve *s)
{
	int i;
	Port *p;
	
	for(p = outs; p < outs + nouts; p++)
		for(i = 0; i < 1<<nins; i++){
//			print("out %d state %x val %d (var %d)\n", p->gate, i, (truth>>i&1)!=0, p->num + i);
			if(truth >> i & 1)
				sataddv(s, p->num + i, 0);
			else
				sataddv(s, -(p->num + i), 0);
		}
}

void
gatesat(SATSolve *s)
{
	int i, j;
	
	for(i = 0; i < ngates; i++)
		for(j = 0; j < 1<<nins; j++){
//			print("gate %d state %x vars %d, %d, %d\n", i, j, gpins[3*i].num + j, gpins[3*i+1].num + j, gpins[3*i+2].num + j);
			sataddv(s, gpins[3*i].num + j, gpins[3*i+2].num + j, 0);
			sataddv(s, gpins[3*i+1].num + j, gpins[3*i+2].num + j, 0);
			sataddv(s, -gpins[3*i].num-j, -gpins[3*i+1].num-j, -gpins[3*i+2].num-j, 0);
		}
}

char *
portstr(Port *p)
{
	switch(p->type){
	case PORTIN: return smprint("I%d", p->gate);
	case PORTOUT: return smprint("O%d", p->gate);
	case PORTNAND: return smprint("G%d", p->gate);
	}
	return "???";
}

void
parsearg(char *a)
{
	int n;
	
	n = strlen(a);
	if(n == 0 || n & n-1) sysfatal("length not a power of 2");
	for(; *a != 0; a++){
		if((uint)(*a-'0') > 1) sysfatal("not binary");
		truth = (*a-'0')<<n-1 | truth >> 1;
	}
	for(nins = 0; n != 1; nins++)
		n >>= 1;
}

Port *
findfrom(SATSolve *s, Port *t)
{
	Link *l;
	
	for(l = links; l < links + nlinks; l++)
		if(l->o == t && satval(s, l->num) > 0)
			return l->i;
	return nil;
}

char *
printconn(SATSolve *s, Port *t)
{
	char *n;
	static char tempchr = 'n';
	
	if(t == nil)
		return "<nil>";
	if(t->type == PORTIN)
		return smprint("%c", 'a' + t->gate);
	if(t->type == PORTNAND){
		if(t->let != 0)
			return smprint("%c", t->let);
		t->let = tempchr++;
		n = smprint("%c", t->let);
		print("%s = %s NAND %s\n", n, printconn(s, findfrom(s, &t[-2])), printconn(s, findfrom(s, &t[-1])));
	}else{
		n = smprint("z");
		print("%s = %s\n", n, printconn(s, findfrom(s, t)));
	}
	return n;
}

void
main(int argc, char **argv)
{
	int i, j;
	SATSolve *s;
	
	if(argc != 2) sysfatal("usage");
	parsearg(argv[1]);
	
	nouts = 1;
	
	for(ngates = 0; ; ngates++){
	
	nports = nins + nouts + 3 * ngates;
	ports = calloc(sizeof(Port), nports);
	ins = ports;
	outs = ports + nins;
	gpins = ports + nins + nouts;
	for(i = 0; i < nins; i++){
		ins[i].gate = i;
		ins[i].type = PORTIN;
		ins[i].num = varnum;
		varnum += 1<<nins;
	}
	for(i = 0; i < nouts; i++){
		outs[i].gate = i;
		outs[i].type = PORTOUT;
		outs[i].num = varnum;
		varnum += 1<<nins;
	}
	for(i = 0; i < 3*ngates; i++){
		gpins[i].gate = i/3;
		gpins[i].type = PORTNAND;
		gpins[i].pin = i%3;
		gpins[i].num = varnum;
		varnum += 1<<nins;
	}
	for(i = 0; i < nports; i++)
		for(j = 0; j < nports; j++)
			if((ports[i].type == PORTIN || ports[i].type == PORTNAND && ports[i].pin == 2) &&
			   (ports[j].type == PORTOUT || ports[j].type == PORTNAND && ports[j].pin < 2) &&
			   (ports[i].type != PORTNAND || ports[j].type != PORTNAND || ports[i].gate < ports[j].gate))
				mklink(&ports[i], &ports[j]);
	
	s = satnew();
	linksat(s);
	insat(s);
	outsat(s);
	gatesat(s);
	if(satsolve(s))
		break;
	}

	printconn(s, &outs[0]);
}