/*
Генератор Verilog из таблиц истинности, в том числе минимизированных. 
Реализация для сумматоров и умножителей по модулю (регулируется дефайном MUL)
*/

#include <stdio.h>
#include <math.h>
#include <stdlib.h>
#include <time.h>
#include <string.h>

// Минимальное количество термов для слияния
#define THOLD 30
#define MUL 1

int get_bit(int x, int pos) {
	return (x >> pos) & 1;
}

int set_bit(int x, int bit_val, int pos) {
	if (bit_val == 1)
		return (x | (1 << pos));
	else
		return (x & ~(1 << pos));
}

int invert_bit(int x) {
	if (x == 1)
		return 0;
	else
		return 1;
}

int find_bit(int p) {
	int i, k;
	k = 1;
	for (i = 0; i < 32; i++) {
		if (k > p)
			return i;
		k *= 2;
	}
	return -1;
}

int pow2(int p) {
	return (1 << p);
}

/*
void print_sum_mod(FILE *out, int p) {
	int i, k;
	int a, b;
	int bit, max, max2;
	int val, res;
	
	bit = find_bit(p-1);
	max = pow2(bit);
	max2 = pow2(2*bit);

	for (i = 0; i < bit; i++)
		fprintf(out, "A%d,", i);
	for (i = 0; i < bit; i++)
		fprintf(out, "B%d,", i);
	for (i = 0; i < bit; i++)
		fprintf(out, ",X%d", i);
	fprintf(out, "\n");
	
	// Заполняем минтермы и донткары
	for (i = 0; i < max2; i++) {
		a = 0;
		for (k = bit-1; k >= 0; k--) {
			val = get_bit(i, k);
			a += val*pow2(k);
			fprintf(out, "%d,", val);
		}
		b = 0;
		for (k = bit-1; k >= 0; k--) {
			val = get_bit(i, bit + k);
			b += val*pow2(k);
			fprintf(out, "%d,", val);
		}
		res = (a + b)%p;
		if (a >= p || b >= p) {
			for (k = bit-1; k >= 0; k--) {
				fprintf(out, ",X");
			}
		} else {
			for (k = bit-1; k >= 0; k--) {
				fprintf(out, ",%d", get_bit(res, k));
			}
		}
		fprintf(out, "\n");
	}
}
*/

#define NL 10000

struct variables
{
	char a[32];
	struct variables *node1;
	struct variables *node2;
	char type1;
	char type2;
	int swnum;
} inps[64], outs[64], gens[NL];
int ilen, olen, glen;

struct var_array {
	(struct variables *) node[64];
	char type[64];
	int num;
	struct variables *out;
} proc[100000];
int procnum;

int find_num_of_includes (
		struct variables *var1,
		int vartype1,
		struct variables *var2,
		int vartype2)
{
	int i, z;
	int flag1, flag2;
	int num = 0;

	for (z = 0; z < procnum; z++)
	{
		flag1 = 0;
		flag2 = 0;
		for (i = 0; i < proc[z].num; i++) {
			if (proc[z].node[i] == var1 && proc[z].type[i] == vartype1)
				flag1 = 1;
			if (proc[z].node[i] == var2 && proc[z].type[i] == vartype2)
				flag2 = 1;
		}
		if (flag1 == 1 && flag2 == 1)
			num++;
	}
	return num;
}

void replace_variables_with_new
	(struct variables *g)
{
	struct variables *var1;
	int vartype1;
	struct variables *var2;
	int vartype2;
	struct variables * node[64];
	char temptype[64];
	int nnum;
	int i, j, z;
	int flag1, flag2;
	int num = 0;

	var1 = g->node1;
	var2 = g->node2;
	vartype1 = g->type1;
	vartype2 = g->type2;

	for (z = 0; z < procnum; z++)
	{
		flag1 = 0;
		flag2 = 0;
		for (i = 0; i < proc[z].num; i++) {
			if (proc[z].node[i] == var1 && proc[z].type[i] == vartype1)
				flag1 = 1;
			if (proc[z].node[i] == var2 && proc[z].type[i] == vartype2)
				flag2 = 1;
		}
		// Здесь есть искомая пара заменяем
		if (flag1 == 1 && flag2 == 1) {
			nnum = 0;
			for (i = 0; i < proc[z].num; i++) {
				if (proc[z].node[i] == var1 && proc[z].type[i] == vartype1)
					continue;
				if (proc[z].node[i] == var2 && proc[z].type[i] == vartype2)
					continue;
				node[nnum] = proc[z].node[i];
				temptype[nnum] = proc[z].type[i];
				nnum++;
			}
			// Записываем новую
			node[nnum] = g;
			temptype[nnum] = 1;
			nnum++;
			// Перезаписываем массив
			for (i = 0; i < 64; i++) {
				proc[z].node[i] = NULL;
				proc[z].type[i] = 0;
			}
			for (i = 0; i < nnum; i++) {
				proc[z].node[i] = node[i];
				proc[z].type[i] = temptype[i];
			}
			proc[z].num = nnum;
		}
	}
}

void print_data(int p) {
	int i, j, k;
	int flag1, flag2;

#ifdef MUL
	printf("// Mul modulo %d\n", p);
	printf("module mul_modulo_%d (A, B, X);\n", p);
#else if 
	printf("// Sum modulo %d\n", p);
	printf("module sum_modulo_%d (A, B, X);\n", p);
#endif
	printf("	input [%d:0] A;\n", olen-1);
	printf("	input [%d:0] B;\n", olen-1);
	printf("	output[%d:0] X;\n", olen-1);

	for (i = 0; i < glen; i++) {
		printf("wire %s;\n", gens[i].a);
	}

	for (i = 0; i < glen; i++) {
		printf("assign %s = %c%s&%c%s; // Replaced = %d\n", 
				gens[i].a, 
				(gens[i].type1 == 0)?'~':' ', 
				gens[i].node1->a, 
				(gens[i].type2 == 0)?'~':' ', 
				gens[i].node2->a, 
				gens[i].swnum);
	}
	printf("\n");
	for (i = 0; i < olen; i++) {
		printf("assign %s = ", outs[i].a);
		flag1 = 0;
		for (j = 0; j < procnum; j++)
		{
			if (proc[j].out == &(outs[i])) {
				if (flag1 > 0)
					printf(" | ");
				flag2 = 0;
				printf("(");
				for (k = 0; k < proc[j].num; k++) {
					if (flag2 > 0)
						printf("&");
					printf("%c%s", (proc[j].type[k] == 0)?'~':' ', proc[j].node[k]->a);
					flag2++;
				}
				printf(")");
				flag1++;
			}
		}
		printf(";\n\n");
	}
	printf("endmodule\n\n");

	printf("module atest_bench();\n");
	printf("reg [%d:0] in1;\n", olen-1);
	printf("reg [%d:0] in2;\n", olen-1);
	printf("wire [%d:0] out;\n", olen-1);
	printf("integer i, j, l, m, t;\n");
	printf("reg dummy;\n");
	printf("wire complete;\n");
	printf("integer fori, forj;\n");
	printf("\n");
#ifdef MUL
	printf("mul_modulo_%d sm1(in1, in2, out);\n", p);
#else if 
	printf("sum_modulo_%d sm1(in1, in2, out);\n", p);
#endif
	printf("\n");
	printf("initial\n");
	printf("begin\n");
	printf("for (fori = 0; fori < %d; fori = fori + 1)\n", p);
	printf("begin\n");
	printf("for (forj = 0; forj < %d; forj = forj + 1)\n", p);
	printf("begin\n");
	printf("	in1 = fori;\n");
	printf("	in2 = forj;\n");
#ifdef MUL
	printf("	m = (fori * forj) %% %d;\n", p);
#else if 
	printf("	m = (fori + forj) %% %d;\n", p);
#endif
	printf("	#1 dummy = 1;\n");
	printf("	$display (\"!!! IN1=(%%d) IN2=(%%d) Res=(%%d) Expect=(%%d)\", fori, forj, out, m);\n");
	printf("	l = out;\n");
	printf("	if (l != m)\n");
	printf("	begin\n");
	printf("		$display (\"!!! Error (%%d, %%d)!!!\", l, m);\n");
	printf("	end\n");
	printf("	#1 dummy = 1;\n");
	printf("end\n");
	printf("end\n");
	printf("end\n");
	printf("endmodule\n");
}

int file_exists (char *buf) {
	FILE *fp = fopen(buf,"r");
	if (fp) {
		fclose(fp);
		return 1;
	} else {
		return 0;
	}
	return 0;
}

int main ()
{
	FILE *out;
	int i, j, k, m, l1, num, varnum, mod, p;
	char buf[1024];
	struct variables *max1, *max2;
	char maxvartype1, maxvartype2;
	struct variables *var1, *var2;
	char vartype1, vartype2;
	int curmax;

	for (p = 131; p <= 131; p++) {
	fprintf(stderr, "Starting module: %d\n", p);
#ifdef MUL
	sprintf(buf, "./TablesNotProc/mul_mod_%d.csv", p);
#else if
	sprintf(buf, "./TablesNotProc/sum_mod_%d.csv", p);
#endif
	if (!file_exists(buf))
		continue;
	freopen(buf, "r", stdin); 

#ifdef MUL
	sprintf(buf, "./TablesProc/mul_mod_%d.v", p);
#else if
	sprintf(buf, "./TablesProc/sum_mod_%d.v", p);
#endif
	freopen(buf, "w", stdout);
	
	// Заполняем массивы входов и выходов
	scanf("%s", buf);
	l1 = strlen(buf);
	
	ilen = 0;
	olen = 0;
	glen = 0;
	k = 0;
	for (i = 0; i < l1; i++)
	{
		// Коррекция скобок в массиве
		if (buf[i] == ',') {
			inps[ilen].a[k] = ']';
			k++;
		}
		if (buf[i] == ',' && buf[i+1] == ',') {
			inps[ilen].a[k] = 0;
			ilen++;
			k = 0;
			i += 2;
			break;
		}
		if (buf[i] == ',')
		{
			inps[ilen].a[k] = 0;
			k = 0;
			ilen++;
			continue;
		}
		inps[ilen].a[k++] = buf[i];
		// Коррекция скобок в массиве
		if (buf[i] >= 'A' && buf[i] <= 'Z' && buf[i+1] >= '0' && buf[i+1] <= '9')
			inps[ilen].a[k++] = '[';
	}
	for (; i < l1; i++)
	{
		// Коррекция скобок в массиве
		if (buf[i] == ',') {
			outs[olen].a[k] = ']';
			k++;
		}
		if (buf[i] == ',')
		{
			outs[olen].a[k] = 0;
			k = 0;
			olen++;
			continue;
		}
		outs[olen].a[k++] = buf[i];
		// Коррекция скобок в массиве
		if (buf[i] >= 'A' && buf[i] <= 'Z' && buf[i+1] >= '0' && buf[i+1] <= '9')
			outs[olen].a[k++] = '[';
	}
	outs[olen].a[k] = ']';
	k++;
	outs[olen].a[k] = 0;
	olen++;

	// Переставляем местами переменные (какой-то глюк в файле)
	for (i = 0; i < ilen/4; i++)
	{
		strcpy(buf, inps[i].a);
		strcpy(inps[i].a, inps[ilen/2 - 1 - i].a);
		strcpy(inps[ilen/2 - 1 - i].a, buf);
	}
	for (i = ilen/2; i < (3*ilen)/4; i++)
	{
		strcpy(buf, inps[i].a);
		strcpy(inps[i].a, inps[(3*ilen)/2 - 1 - i].a);
		strcpy(inps[(3*ilen)/2 - 1 - i].a, buf);
	}
	for (i = 0; i < olen/2; i++)
	{
		strcpy(buf, outs[i].a);
		strcpy(outs[i].a, outs[olen - 1 - i].a);
		strcpy(outs[olen - 1 - i].a, buf);
	}

	// Читаем большой массив с начальными переменными
	procnum = 0;
	while (scanf("%s", buf) != EOF) {
		l1 = strlen(buf);
		varnum = 0;
		k = 0;
		for (i = 0; i < l1; i++)
		{
			if (buf[i] == ',' && buf[i+1] == ',') {
				i += 2;
				break;
			}
			if (buf[i] == ',')
			{
				varnum++;
				continue;
			}
			if (buf[i] == '0') {
				proc[procnum].node[k] = &(inps[varnum]);
				proc[procnum].type[k] = 0;
				k++;
			} else if (buf[i] == '1') {
				proc[procnum].node[k] = &(inps[varnum]);
				proc[procnum].type[k] = 1;
				k++;
			}
		}
		// Читаем к какому выходу относится правило
		varnum = 0;
		proc[procnum].out = NULL;
		for (; i < l1; i++)
		{
			if (buf[i] == ',')
			{
				varnum++;
				continue;
			}
			if (buf[i] == '1') {
				proc[procnum].out = &(outs[varnum]);
				break;
			}
		}
		proc[procnum].num = k;
		procnum++;
	}

	// Основной алгоритм минимизации. Цикл по всем возможным парам
	while (1) {
		max1 = NULL;
		max2 = NULL;
		curmax = 0;
		for (i = 0; i < ilen; i++) {
			// Входы с входами
			for (j = i+1; j < ilen; j++) {
				for (k = 0; k < 2; k++) {
					for (m = 0; m < 2; m++) {
						if (i == j) // Одна переменная два раза не может быть
							continue;
						var1 = &inps[i];
						vartype1 = k;
						var2 = &inps[j];
						vartype2 = m;

						num = find_num_of_includes(var1, vartype1, var2, vartype2);
						
						if (num > curmax) {
							curmax = num;
							max1 = var1;
							max2 = var2;
							maxvartype1 = vartype1;
							maxvartype2 = vartype2;
						}
					}
				}
			}
			
			// Входы с генеренными узлами
			for (j = 0; j < glen; j++) {
				for (k = 0; k < 2; k++) {
					m = 1; // У генеренного одно состояние
					var1 = &inps[i];
					vartype1 = k;
					var2 = &gens[j];
					vartype2 = m;
					
					num = find_num_of_includes(var1, vartype1, var2, vartype2);
					
					if (num > curmax) {
						curmax = num;
						max1 = var1;
						max2 = var2;
						maxvartype1 = vartype1;
						maxvartype2 = vartype2;
					}
				}
			}
		}

		// Генеренные узлы с генеренными
		for (i = 0; i < glen; i++) {
			for (j = i+1; j < glen; j++) {
				k = 1; // У генеренного одно состояние
				m = 1; // У генеренного одно состояние
				var1 = &gens[i];
				vartype1 = k;
				var2 = &gens[j];
				vartype2 = m;
				
				num = find_num_of_includes(var1, vartype1, var2, vartype2);
				
				if (num > curmax) {
					curmax = num;
					max1 = var1;
					max2 = var2;
					maxvartype1 = vartype1;
					maxvartype2 = vartype2;
				}
			}
		}

		// Если всего THOLD или меньше копий каждой пары, то выходим
		if (curmax <= THOLD) {
			break;
		}

		// Записываем промежуточные результаты
		if (0) {
			#ifdef MUL
				sprintf(buf, "./TablesProc/mul_mod_%d_%d_PR_%d.v", p, glen, curmax);
			#else if
				sprintf(buf, "./TablesProc/sum_mod_%d_%d_PR_%d.v", p, glen, curmax);
			#endif
			freopen(buf, "w", stdout);
			print_data(p);
		}

		// Создаем новую переменную
		sprintf(gens[glen].a, "GEN%d", glen);
		gens[glen].node1 = max1;
		gens[glen].node2 = max2;
		gens[glen].type1 = maxvartype1;
		gens[glen].type2 = maxvartype2;
		gens[glen].swnum = curmax;
				
		fprintf(stderr, "New variable: %s (Replacement level: %d)\n", gens[glen].a, curmax);

		// Заменяем переменные с максимальным числом вхождений на новую
		replace_variables_with_new(&gens[glen]);
		glen++;
	}

	print_data(p);
	}

	return 0;
}