/* 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)
{
   FILE *in, *out;
   int n, m, 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;

	 if (argc < 3) {
		 printf("Incorrect number of arguments.\n");
		 printf("Usage: cnf2cop <output dir> <cnf file> [cnf file] ...\n");
		 exit(1);
	 }

	 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]);
			 exit(1);
		 }

		 	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);
			 exit(1);
		 }
	
		 ch = fgetc(in);
	   while (ch == 'c' || ch == '#') {
	      while (fgetc(in) != '\n');
	      ch = fgetc(in);
	   }
	
	
	   fscanf(in, " cnf %d %d", &n, &m);
	
		 M = (m < CNF_MAX_CLAUSES) ? m : CNF_MAX_CLAUSES;
	   N = (n < CNF_MAX_LITERALS) ? n : CNF_MAX_LITERALS;
	
	   /***** allocate cnf *****/
	   nXs = (int *) calloc(m, sizeof(int));
	   Xs = (int **) calloc(m, sizeof(int *));
	   for (y = 0; y < m; y++) 
	      Xs[y] = (int *) calloc(N, sizeof(int));
	   Xsgns = (int **) calloc(m, sizeof(int *));
	   for (y = 0; y < m; y++) 
	      Xsgns[y] = (int *) calloc(N, sizeof(int));
	
	   nYs = (int *) calloc(n+1, sizeof(int));
	   Ys = (int **) calloc(n+1, sizeof(int *));
	   for (x = 1; x <= n; x++) 
	      Ys[x] = (int *) calloc(M, sizeof(int));
	   Ysgns = (int **) calloc(n+1, sizeof(int *));
	   for (x = 1; x <= n; x++) 
	      Ysgns[x] = (int *) calloc(M, sizeof(int));
	
	   /***** read cnf *****/
	   Nmax = 0;
	   for (y = 0; y < m; y++) {
	      for (fscanf(in, "%d", &lit); lit; fscanf(in, "%d", &lit)) {
	         if (nXs[y] >= N) {
	            printf("Error: #literals exceeds max lits=%d\n", N);
	            exit(1);
	         }
	         x = abs(lit);
	         s = (lit > 0) ? 1 : -1;
	         Xs[y][nXs[y]] = x;
	         Xsgns[y][nXs[y]] = s;
	         nXs[y]++;
	         Ys[x][nYs[x]] = y;
	         Ysgns[x][nYs[x]] = s;
	         nYs[x]++;
	         if (nYs[x] > M) {
	            printf("Error: #clauses exceeds max clauses=%d\n", M);
	            exit(1);
	         }
	      }
	      if (nXs[y] > Nmax) Nmax = nXs[y];
	   }
	
	   /***** print cop *****/
	   fprintf(out, "(%d %d)\n", n, m);
	   Mmax = 0;
	   for (x = 1; x <= n; x++) if (nYs[x] > Mmax) Mmax = nYs[x];
	   fprintf(out, "(%d %d)\n", Nmax, Mmax);
	   fprintf(out, "(");
	   for (x = 1; x < n; x++) fprintf(out, "0 ");
	   fprintf(out, "0)\n");
	   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 = 1; x <= n; x++) 
	      free(Ys[x]);
		 free(Ys);
	   for (x = 1; x <= n; x++) 
	      free(Ysgns[x]);
		 free(Ysgns);

		 fclose(in);
   }

	 return 0;
}