/**
 * test.c
 *
 * Program that test a CNF file for finding tautologies and missing variables
 *
 * Input: A CNF file name
 * Output: 
 *
 * @author  Eduardo Rodriguez-Tello
 * @version 1.00, 18/02/2004
 */

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

/**
 * Global variables
 */

int N;										// Number of variables in the CNF file
int M;										// Number of clauses in the CNF file
int sumAllClauseLengths;					// Sum of all the clause lenghts
int clauseRel[100];							// Contains the variables readed in one line of the CNF file
int contVars;								// 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

/**
 * Function Prototypes
 */
int **Matrix(int nrl,int nrh,int ncl,int nch);
int readClauseWithoutRepetition(char *l, int clause);
void checkCNF(char * cnfFile);

/**
 * 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) and warns if there is a tautology
 */
int readClauseWithoutRepetition(char *l, int clause)  {	
	char stringToTokenize[128]; stringToTokenize[0]='\0';
	char blancs[128]; blancs[0]='\0';
	char *tok; 
    int tmp, len, i, found;
    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 "));
		while(tok != NULL)  {			
			tmp = atoi(tok);
			if (tmp != 0) {
				found = 0;
				for (i=0; i<contVars; i++)  {
					if (abs(clauseRel[i]) == abs(tmp)) {
						found = 1;
						fprintf(stderr,"Tautology: \t%d\t%d\tClause:%d\n",tmp,-tmp, clause+1);
						break;					
					}
				}
				if (!found)
					clauseRel[contVars++] = tmp;
			}
            else
				finished = 1;
			tok = (char *)strtok(NULL, "\t\n\r ");
		}
	}
    return finished;
}
/**
 * Checks a CNF File
 */
void checkCNF(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);
	 fprintf(stderr,"CNF File: %s, Variables: %d, Clauses: %d\n\n",cnfFile, N, M);
	 sumAllClauseLengths = 0;
	 countM = 0;
	 contVars = 0;
	 exist = (int **) Matrix(0, N+1, 0, 2);
	 for (i=1; i<N+1; i++)  {
		exist[i][0]=0;
		exist[i][1]=0;
	 }	 
	 do {
		fgets(line, 100, cnf);			
		complete = readClauseWithoutRepetition(line,countM);		
		if (complete)  {
			sumAllClauseLengths = sumAllClauseLengths + contVars;
			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=1; i<N+1; i++)  {
		if (exist[i][0])  {
			exist[i][1]=NActual;
			NActual++;
		}
	 }
	 NActual = NActual-1;
	 if (N!=NActual)  {
		 fprintf(stderr,"\nMissing variables: ");
		 for (i=1; i<N+1; i++) 
			 if (exist[i][0] == 0) 
				fprintf(stderr,"%d ", i);
		 fprintf(stderr,"\n\nVariables: %d, Actual number of Variables: %d\n",N, NActual);
	 }
}
/**
 * Free memory
 */
void cleanMemory(void)  {
	free(exist);
}
/**
 * Main program entry point
 */
int main(int argc, char *argv[])  {
	 
	 if (argc != 2) {
		fprintf(stderr,"use: testcnf CNFFile.CNF\n");
	    exit(1);
	 }
	 checkCNF(argv[1]);
	 cleanMemory();
	 return 0;
}