/* Copyright (C) 2001  Dale Schuurmans, Finnegan Southey                     */
/* This work is licensed under the Gnu General Public License (see gpl.txt). */

/* Converts CNF to COP format. */

#define CNF_MAX_LITERALS 100
#define CNF_MAX_CLAUSES  500

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

int main(int argc, char **argv);
void showUsage();
void checkAlloc(void *ptr, char *msg);

int main(int argc, char **argv)
{
	FILE *in, *out;
	int n, m, Nmax, Mmax;
	int *nXs, **Xs, **Xsgns;
	int *nYs, **Ys, **Ysgns;

	int x, y, lit, s, j;
	char ch;
	int fnum;
	char outname[10000];
	char *outputDir;
	char *lastslash;
	long clauseStart;
	long memReq;

	if (argc < 3) {
		printf("Incorrect number of arguments.\n");
		showUsage();
		exit(EXIT_FAILURE);
	}

	outputDir = argv[1];

	for (fnum = 2; fnum < argc; fnum++) {

		in = fopen(argv[fnum], "r");
		if (in == NULL) {
			printf("Error opening input file: %s\n", argv[fnum]);
			showUsage();
			exit(EXIT_FAILURE);
		}

		strcpy(outname, outputDir);
		if (outputDir[strlen(outputDir)-1] != '/')
			strcat(outname, "/");
		lastslash = strrchr(argv[fnum], '/');
		if (lastslash == NULL)
			strcat(outname, argv[fnum]);
		else
			strcat(outname, lastslash + 1);
		strcpy(strrchr(outname, '.'), ".cop");

		out = fopen(outname, "w");
		if (out == NULL) {
			printf("Error opening output file: %s\n", outname);
			showUsage();
			exit(EXIT_FAILURE);
		}

		ch = fgetc(in);
		while (ch == 'c' || ch == '#') {
			while (fgetc(in) != '\n');
			ch = fgetc(in);
		}


		fscanf(in, " cnf %d %d", &n, &m);

		fprintf(stderr, "Vars: %d\tClauses: %d\n", n, m);
		memReq = (m + n) * sizeof(int) + (2 * m + 2 * n) * sizeof(int*);
		fprintf(stderr, "Initial memory required (B): %ld\n", memReq);

		/***** allocate cnf *****/
		nXs = (int *) calloc(m, sizeof(int));
		checkAlloc(nXs, "Out of memory (1).");
		Xs = (int **) calloc(m, sizeof(int *));
		checkAlloc(nXs, "Out of memory (2).");
		Xsgns = (int **) calloc(m, sizeof(int *));
		checkAlloc(Xsgns, "Out of memory (3).");

		nYs = (int *) calloc(n, sizeof(int));
		checkAlloc(nYs, "Out of memory (4).");
		Ys = (int **) calloc(n, sizeof(int *));
		checkAlloc(Ys, "Out of memory (5).");
		Ysgns = (int **) calloc(n, sizeof(int *));
		checkAlloc(Ysgns, "Out of memory (6).");

		/***** read cnf for sizes *****/
		clauseStart = ftell(in);
		Nmax = 0;
		for (y = 0; y < m; y++) {
			for (fscanf(in, "%d", &lit); lit; fscanf(in, "%d", &lit)) {
				x = abs(lit) - 1;
				nXs[y]++;
				nYs[x]++;
			}
			if (nXs[y] > Nmax) 
				Nmax = nXs[y];
		}

		/***** allocate arrays for variable length portions *****/
		for (y = 0; y < m; y++) {
			memReq += 2 * nXs[y] * sizeof(int);
		}
		for (x = 0; x < n; x++) {
			memReq += 2 * nYs[x] * sizeof(int);
		}
		fprintf(stderr, "Total memory required (B): %ld\n", memReq);



		/***** allocate arrays for variable length portions *****/
		for (y = 0; y < m; y++) {
			Xs[y] = (int *) calloc(nXs[y], sizeof(int));
			checkAlloc(Xs[y], "Out of memory (7).");
			Xsgns[y] = (int *) calloc(nXs[y], sizeof(int));
			checkAlloc(Xsgns[y], "Out of memory (8).");
			nXs[y] = 0;
		}
		for (x = 0; x < n; x++) {
			Ys[x] = (int *) calloc(nYs[x], sizeof(int));
			checkAlloc(Ys[x], "Out of memory (9).");
			Ysgns[x] = (int *) calloc(nYs[x], sizeof(int));
			checkAlloc(Ysgns[x], "Out of memory (10).");
			nYs[x] = 0;
		}


		/***** read cnf again for actual values *****/
		fseek(in, clauseStart, SEEK_SET);
		Nmax = 0;
		for (y = 0; y < m; y++) {

			for (fscanf(in, "%d", &lit); lit; fscanf(in, "%d", &lit)) {
				x = abs(lit) - 1;
				s = (lit > 0) ? 1 : -1;
				Xs[y][nXs[y]] = x + 1;
				Xsgns[y][nXs[y]] = s;
				nXs[y]++;
				Ys[x][nYs[x]] = y;
				Ysgns[x][nYs[x]] = s;
				nYs[x]++;
			}
			if (nXs[y] > Nmax) 
				Nmax = nXs[y];
		}

		/***** print cop *****/
			/* Write number of vars and constraints. */
		fprintf(out, "(%d %d)\n", n, m);

			/* Write max-vars-per-constraint and max-constraints-per-var. */
		Mmax = 0;
		for (x = 0; x < n; x++) 
			if (nYs[x] > Mmax) 
				Mmax = nYs[x];
		fprintf(out, "(%d %d)\n", Nmax, Mmax);

			/* Write objective function values (A). */
		fprintf(out, "(");
		for (x = 0; x < n-1; x++) 
			fprintf(out, "0 ");
		fprintf(out, "0)\n");

			/* Write constraints. (B[y] nXs[y] () () () ). */
		for (y = 0; y < m; y++) {
			fprintf(out, "(%d %d ", nXs[y]-2, nXs[y]);
			for (j = 0; j < nXs[y]; j++) 
				fprintf(out, "(%d %d)", Xs[y][j]-1, -Xsgns[y][j]);
			fprintf(out, ")\n");
		}

		/***** deallocate cnf *****/
		free(nXs);
		for (y = 0; y < m; y++) 
			free(Xs[y]);
		free(Xs);
		for (y = 0; y < m; y++) 
			free(Xsgns[y]);
		free(Xsgns);

		free(nYs);
		for (x = 0; x < n; x++) 
			free(Ys[x]);
		free(Ys);
		for (x = 0; x < n; x++) 
			free(Ysgns[x]);
		free(Ysgns);

		fclose(in);
	}

	return 0;
}

void showUsage()
{
	printf("Usage: cnf2cop <output dir> <cnf file> [cnf file] ...\n");
}

void checkAlloc(void *ptr, char *msg)
{
	if (ptr == NULL) {
		fprintf(stderr, "%s\n", msg);
		exit(EXIT_FAILURE);
	}
}