/**
 * bipart.c
 *
 * Program to remove the variables not used in a CNF file. It renames all other variables.
 *
 * Input: A CNF file name
 * Output: A renamed CNF file with a name ending in '-New.cnf'
 *
 * @author  Eduardo Rodriguez-Tello
 * @version 1.00, 10/12/2003
 */

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

/**
 * Global variables
 */

int N;										// Number of variables in the CNF file
int M;										// Number of clauses in the CNF file

int *clauseRel;								// Contains the variables readed in one line of the CNF file
int contVars = 0;							// Represent the number variables readed in one line of the CNF file

int **exist;								// Contains the actual index of each variable of the CNF file
int NActual;								// Actual number of variables used in the CNF file

char fileName[100];							// The CNF File name


/**
 * Returns a vector of n elements
 */
int *Vector(unsigned int n)  {
     int *P = (int *)malloc(n * sizeof(int));

     if (P == NULL){
        fprintf(stderr,"Memory allocation error!\n");
        exit(0);
     }
     return P;
}
/**
 * Returns a matrix
 */
int **Matrix(int nrl,int nrh,int ncl,int nch)  {
     int i;
     int **m;

     m = (int **) malloc((unsigned)(nrh-nrl+1)*sizeof(int));
     if (!m)
        fprintf(stderr,"Memory allocation error in step 1!\n");
     m -= nrl;
     for (i = nrl; i <= nrh; i++) {
        m[i]=(int*) malloc((unsigned) (nch-ncl+1)*sizeof(int));
        if (!m[i])
           fprintf(stderr,"Memory allocation error in step 2!\n");
        m[i] -= ncl;
     }
     return m;
}
/**
 * Read all the literals in a line of text; returns 1 if in the line is a 
 * complete clause (i.e. it ends with a 0)
 */
int readClause(char *l)  {
	char stringToTokenize[128]; stringToTokenize[0]='\0';
	char blancs[128]; blancs[0]='\0';
	char *tok;
    int tmp, len;
    int finished = 0;
	
    if ( ((len=strlen(l)-1) != 0)&&(l[0] != 'c')&&(l[0] != 'C') ) {
		strcpy(stringToTokenize,l);
		tok = (char *)strtok(stringToTokenize, "\t\n\r ");
		//		tok[0]='\0';
		while(tok != NULL)  {			
			tmp = atoi(tok);
			if (tmp != 0)
				clauseRel[contVars++] = tmp;
            else
				finished = 1;
			tok = (char *)strtok(NULL, "\t\n\r ");
		}
	}
    return finished;
}
/**
 * Reads the CNF File and sums all the clause lengths
 */
void readVars(char * cnfFile)  {
     char line[100], tempstr1[10], tempstr2[10];
     int i, countM, complete;
	 FILE *cnf;
	 
	 cnf = fopen(cnfFile,"r");
     if (!cnf) {
       fprintf(stderr,"Could not open the file: %s\n",cnfFile);
       exit(1);
     }
     // Ignors the comment lines
     fgets(line, 100, cnf);
     while (line[0] != 'p')  {
          fgets(line, 100, cnf);
     }
     // Now, we have the problem line in the buffer
     sscanf(line, "%s %s %d %d", tempstr1, tempstr2, &N, &M);
	 countM = 0;
	 contVars = 0;
	 clauseRel = (int *) Vector(100);
	 exist = (int **) Matrix(0, N+1, 0, 2);
	 for (i=0; i<N+1; i++)  {
		exist[i][0]=0;
		exist[i][1]=0;
	 }
	 do {
		fgets(line, 100, cnf);			
		complete = readClause(line);
		if (complete)  {
			for (i=0; i < contVars; i++)  {
				exist[abs(clauseRel[i])][0]=1;
                clauseRel[i]=0;
			}
            contVars = 0;
            complete = 0;
			countM++;
		}
	 } while ((!feof(cnf))&&(countM<M));
	 fclose(cnf);
	 NActual = 1;
	 for (i=0; i<N+1; i++)  {
		if (exist[i][0])  {
			exist[i][1]=NActual;
			//fprintf(stderr,"%i\t%i\n",i, NActual);
			NActual++;
		}
		//else
		//	fprintf(stderr,"%i\t\n",i);
	 }
	 NActual = NActual-1;
	 //if (N!=NActual) fprintf(stderr,"N: %i \t NActual: %i\n",N, NActual);
}
/**
 * Creates the new CNF file and a file which stores the variables that were renamed
 */
void createCNFFile(char *in)  {
	char line[100], tempstr1[10], tempstr2[10];
	char file1[100];
	int  i, t, countM, complete;
	FILE *cnf, *P1;

	file1[0] = '\0';
	t = strlen(in);
	strcpy(line, in);
	strncat(file1, line, t-4);
	strcat(file1, "-New.cnf");

	P1 = fopen(file1, "wt");
	if (!P1) {
		fprintf(stderr,"Could not open the file: %s\n", file1);
		exit(1);
	}
	cnf = fopen(in, "r");
    if (!cnf) {
		fprintf(stderr,"Could not open the file: %s\n", in);
		exit(1);
    }
	// Write the headings of the first CNF file
	fprintf(P1, "c\n");
	fprintf(P1, "c Originally it contains %i variables and %i did not appeared\n", N, N-NActual);
	fprintf(P1, "c\n");
	
	line[0] = 'x';
	while (line[0] != 'p')  {
		fgets(line, 100, cnf);
		if (line[0] == 'p')
			fprintf(P1, "c ");
		fprintf(P1, "%s",line);
    }
	fprintf(P1, "p\tcnf\t%i\t%i\n", NActual, M);
	// Now, we have the problem line in the buffer
    sscanf(line, "%s %s %d %d", tempstr1, tempstr2, &N, &M);
    //fprintf(stderr,"Variables: %i, Clauses: %i\n", N, M);
	countM = 0;
	contVars = 0;
	do {
		fgets(line, 100, cnf);		
		complete = readClause(line);
        if (complete)  {
			for (i=0; i < contVars; i++)  {
				if (clauseRel[i] > 0)
					fprintf(P1, "%d\t", exist[abs(clauseRel[i])][1]);
				else
					fprintf(P1, "%d\t", -exist[abs(clauseRel[i])][1]);
				clauseRel[i]=0;
			}
			fprintf(P1, "0\n");
		}
        contVars = 0;
        complete = 0;
		countM++;
	} while ((!feof(cnf))&&(countM<M));
	fclose(cnf);
	fclose(P1);
}
/**
 * Main program entry point
 */
int main(int argc, char *argv[])  {
	
	if (argc != 2) {
		fprintf(stderr,"use: clean CNFFile.CNF\n");
	    exit(1);
	}
	strcpy(fileName, argv[1]);
	readVars(fileName);
	createCNFFile(fileName);
	return 0;
}