#include "../includes/globals.h"
#include <assert.h>
#include <stdio.h>
#include <malloc.h>
#include <math.h>

void sortLiterals(CLAUSE* clause, int literals){
	int i,j;
	for(i=0;i<literals-1;i++){
		for(j=i+1;j<literals;j++){
			if(abs(clause->literals[i]) > abs(clause->literals[j])){
				int temp=clause->literals[j];
				clause->literals[j]=clause->literals[i];
				clause->literals[i]=temp;
			}
		}
	}
}

void readInputFile(char* filename){
	int counter = 0;
	int i;
	int j;
	FILE* f = fopen(filename,"r");
	int* literalSpace = NULL;
	if(f == NULL){
		printf("Input file not found\n");
		exit(1);
	}
	fscanf(f,"%d\n",&numberOfLiterals);
	fscanf(f,"%d\n",&numberOfClauses);
	fscanf(f,"%d\n",&maxLiteralsPerClause);
	assert(numberOfLiterals>=0);
	assert(numberOfClauses>=0);
	assert(maxLiteralsPerClause>=0);
	literals = (LITERAL*) malloc(numberOfLiterals*sizeof(LITERAL));
	clauses = (CLAUSE*) malloc(numberOfClauses*sizeof(CLAUSE));
	literalSpace = (int*) malloc(numberOfClauses*maxLiteralsPerClause*sizeof(int));
	for(i = 0; i < numberOfLiterals; i++){
		literals[i].literalNumber = i+1;
		literals[i].countTrueClauses=0;
		literals[i].countFalseClauses = 0;
		literals[i].data = NULL;
		literals[i].value = 0;
	}
	while(!feof(f)){
		int readComplete=0;
		int clauseIsTrue = 0;
		while(1){
			char chars = getc(f);
			if(chars == '('){
				ungetc('(', f);
				break;
			}
			if(feof(f)){
				readComplete = 1;
				break;
			}
		}
		if(readComplete == 1){
			break;
		}
		fscanf(f,"(");
		assert(counter<numberOfClauses);
		clauses[counter].literals=literalSpace+counter*maxLiteralsPerClause;
		for(i=0;i<maxLiteralsPerClause;i++){
			fscanf(f,"%d",&(clauses[counter].literals[i]));
		}
		sortLiterals(&clauses[counter], maxLiteralsPerClause);
		j = 1;
		for(i=1;i<maxLiteralsPerClause;i++){
			if(clauses[counter].literals[i-1] == - clauses[counter].literals[i]){
				//clauses is true..
				clauseIsTrue = 1;
				break;
			}
			else if(clauses[counter].literals[i-1] != clauses[counter].literals[i]){
				clauses[counter].literals[j++]=clauses[counter].literals[i];
			}
			
		}
		clauses[counter].literalCount = j;//maxLiteralsPerClause;
		clauses[counter].data=NULL;
		fscanf(f,")\n");
		if(clauseIsTrue == 1){
			numberOfClauses--;
			continue;
		}
		else{
			counter++;
		}
	}
	assert(counter == numberOfClauses);
	for(i=0;i<numberOfClauses;i++){
		for(j=0;j<clauses[i].literalCount;j++){
			int thisLiteral = clauses[i].literals[j];
			assert(abs(thisLiteral)<=numberOfLiterals);
			if(thisLiteral<0){
				literals[-thisLiteral-1].countFalseClauses++;
			}
			else{
				literals[thisLiteral-1].countTrueClauses++;
			}	
		}
	}
}

int binarySearchLiteral(CLAUSE* clause, int literalNumber, int start, int end){
	if(start == end){
		return 0;
	}
	else{
		int valueChecked = clause->literals[start+(int)((end-start)/2)];
		if(abs(valueChecked) == abs(literalNumber)){
			return valueChecked;
		}
		else if(abs(valueChecked) < literalNumber){
			return binarySearchLiteral(clause, literalNumber, start+(int)((end-start)/2)+1,end);
		}
		else{
			return binarySearchLiteral(clause, literalNumber, start, start+(int)((end-start)/2));
		}
	}
}

int hasLiteral(CLAUSE* clause, int literalNumber){
	return binarySearchLiteral(clause, literalNumber, 0, clause->literalCount);
}

LITERAL* getLiteral(int literalNumber){
	int arrayIndex = literalNumber - 1;
	assert(arrayIndex >= 0);
	assert(arrayIndex < numberOfLiterals);
	return &literals[arrayIndex];
}

int setLiteral(int literalNumber, int value){
	LITERAL* literal = getLiteral(literalNumber);
	int oldValue = literal->value;
	if(value == TRUE){
		literal->value = literalNumber;
	}
	else{
		literal->value = -literalNumber;
	}
	if(oldValue == 0){
		return 0;
	}
	return ((int)(oldValue/abs(oldValue)));
}


int resetLiteral(int literalNumber){
	return setLiteral(literalNumber,0);
}