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

/* Transforms SAT instance to a CA instance (in CATS format) *
 * via a simple NP-completeness reduction  (pretty cool :-)  */

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

int main(int argc, char **argv)
{
   int n, m;
   int *nXs, **Xs, **Xsgns, **xlitnums;
   int *nCs, **Cs, **Csgns, **clitnums;
   int *litx, *litc, *lits;
   int **goods, *nGs;

   int x, c, s, lit, numlits, i, j, maxnCs;
   int b, g, G, bb;

	 FILE *in, *out;
   char ch;
	 int fnum;
	 char outname[10000];
	 char *outputDir;
	 char* lastslash;

	 if (argc < 3) {
		 printf("Incorrect number of arguments.\n");
		 printf("Usage: cnf2cats <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, '.'), ".cats");


		 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);
	
	   nXs = (int *) malloc(m * sizeof(int));
	   Xs = (int **) malloc(m * sizeof(int *));
	   for (c = 0; c < m; c++) Xs[c] = (int *) malloc(n * sizeof(int));
	   Xsgns = (int **) malloc(m * sizeof(int *));
	   for (c = 0; c < m; c++) Xsgns[c] = (int *) malloc(n * sizeof(int));
	   clitnums = (int **) malloc(m * sizeof(int *));
	   for (c = 0; c < m; c++) clitnums[c] = (int *) malloc(n * sizeof(int));
	
	   nCs = (int *) malloc((n+1) * sizeof(int));
	   Cs = (int **) malloc((n+1) * sizeof(int *));
	   for (x = 1; x <= n; x++) Cs[x] = (int *) malloc(m * sizeof(int));
	   Csgns = (int **) malloc((n+1) * sizeof(int *));
	   for (x = 1; x <= n; x++) Csgns[x] = (int *) malloc(m * sizeof(int));
	   xlitnums = (int **) malloc((n+1) * sizeof(int *));
	   for (x = 1; x <= n; x++) xlitnums[x] = (int *) malloc(m * sizeof(int));
	   
	   litx = (int *) malloc(n * m * sizeof(int));
	   litc = (int *) malloc(n * m * sizeof(int));
	   lits = (int *) malloc(n * m * sizeof(int));
	
	   numlits = 0;
	   for (c = 0; c < m; c++)
	      for (fscanf(in, "%d", &lit); lit; fscanf(in, "%d", &lit)) {
	         x = abs(lit);
	         s = (lit > 0) ? 1 : -1;
	         Xs[c][nXs[c]] = x;
	         Xsgns[c][nXs[c]] = s;
	         clitnums[c][nXs[c]] = numlits;
	         nXs[c]++;
	         Cs[x][nCs[x]] = c;
	         Csgns[x][nCs[x]] = s;
	         xlitnums[x][nCs[x]] = numlits;
	         nCs[x]++;
	         litx[numlits] = x;
	         litc[numlits] = c;
	         lits[numlits] = s;
	         numlits++;
	      };
	
	   maxnCs = 0;
	   for (x = 1; x <= n; x++) if (nCs[x] > maxnCs) maxnCs = nCs[x];
	   G = maxnCs;
	   nGs = (int *) calloc(numlits, sizeof(int));
	   goods = (int **) malloc(numlits * sizeof(int *));
	   for (b = 0; b < numlits; b++) goods[b] = (int *) malloc(G * sizeof(int));
	
	   g  = 0;
	   for (b = 0; b < numlits-1; b++) {
	      x = litx[b];
	      s = lits[b];
	      for (bb = b+1; bb < numlits; bb++) 
	         if (litx[bb] == x && lits[bb] != s) {
	            goods[b][nGs[b]++] = g;
	            goods[bb][nGs[bb]++] = g;
	            g++;
	         };
	   }
	   for (c = 0; c < m; c++) {
	      for (i = 0; i < nXs[c]; i++) {
	         bb = clitnums[c][i];
	         goods[bb][nGs[bb]++] = g;
	      }
	      g++;
	   }
	   
	   fprintf(out, "goods %d\n", g);
	   fprintf(out, "bids %d\n", numlits);
	   
	   for (b = 0; b < numlits; b++) {
	      fprintf(out, "%d	1	", b);
	      for (j = 0; j < nGs[b]; j++) fprintf(out, "%d	", goods[b][j]);
	      fprintf(out, "#\n");
	   }
	 }
	 return 0;
}