#include "../includes/globals.h"
#include "dpll.h"
#include <malloc.h>
#include <assert.h>
#include <stdlib.h>

void checkStructure();

void buildSupportStructures(){
	int i;
	int j;
	DPLL_LITERAL* dpll_literals = (DPLL_LITERAL*) malloc(sizeof(DPLL_LITERAL)* numberOfLiterals);
	srandom(RAND_SEED);
	emptyClauses = NULL;
	singleVariableClauses = NULL;
	unsatisfiedClauses = numberOfClauses;
	for(i=0;i<numberOfLiterals;i++){
		literals[i].data = &dpll_literals[i];
		dpll_literals[i].depthSatisfied = -1;
		dpll_literals[i].positiveClauses = NULL;
		dpll_literals[i].negativeClauses = NULL;
	}
	DPLL_CLAUSE* dpll_clauses = (DPLL_CLAUSE*) malloc(sizeof(DPLL_CLAUSE)*numberOfClauses);
    for(i=0;i<numberOfClauses;i++){
    	clauses[i].data = &dpll_clauses[i];
    	dpll_clauses[i].isSatisfied = 0;
    	dpll_clauses[i].depthSatisfied = -1;
    	dpll_clauses[i].currentLiteralCount = clauses[i].literalCount;
    	dpll_clauses[i].currentLiterals = (int*) malloc(sizeof(int)*maxLiteralsPerClause);
    	for(j=0;j<dpll_clauses[i].currentLiteralCount;j++){
    		LITERAL* thisLiteral = getLiteral(abs(clauses[i].literals[j]));
    		DPLL_LITERAL* thisLiteralData = (DPLL_LITERAL*) thisLiteral->data;
    		CLAUSE_ENCLOSER* cl = (CLAUSE_ENCLOSER*) malloc(sizeof(CLAUSE_ENCLOSER));
    		cl->clause = &clauses[i];
    		if(clauses[i].literals[j] > 0){
    			cl->next = thisLiteralData->positiveClauses;
    			thisLiteralData->positiveClauses = cl;
    		}
    		else{
    			cl->next = thisLiteralData->negativeClauses;
    			thisLiteralData->negativeClauses = cl;
    		}
    		dpll_clauses[i].currentLiterals[j]=clauses[i].literals[j];
    	}
    	if(dpll_clauses[i].currentLiteralCount == 0){
    		CLAUSE_ENCLOSER* c1 = (CLAUSE_ENCLOSER*) malloc(sizeof(CLAUSE_ENCLOSER));
    		c1->clause = &clauses[i];
    		c1->next = emptyClauses;
    		emptyClauses = c1;
    	}
    	else if(dpll_clauses[i].currentLiteralCount == 1){
    		CLAUSE_ENCLOSER* c1 = (CLAUSE_ENCLOSER*) malloc(sizeof(CLAUSE_ENCLOSER));
    		c1->clause = &clauses[i];
    		c1->next = singleVariableClauses;
    		singleVariableClauses = c1;
    		
    	}
    }
    //checkStructure();
}

void checkStructure(){
	int i;
	int j;
	for(i=0;i<numberOfLiterals;i++){
		CLAUSE_ENCLOSER* c1 = ((DPLL_LITERAL*)(getLiteral(i+1)->data))->positiveClauses;
		while(c1 != NULL){
			printf("CHECK %d\n",c1->clause);
			c1 = c1->next;
		}
	}
}

void printLiteralState(){
	int j;
	int i;
	printf("***** DUMPING LITERAL STATE ******\n");
	for(i=0;i<numberOfLiterals;i++){
		printf("LITERAL: %d, VALUE = %d\n",literals[i].literalNumber, literals[i].value);
	}
	printf("\n\n");
}

void printSolution(int hasSolution){
	int i;
	int j;
	if(hasSolution == 0){
		printf("Solution: Fail\n");
		return;
	}
	printf("Solution: (");
	for(i=0; i<numberOfLiterals; i++){
		if(literals[i].value<0){
			j=-literals[i].literalNumber;
		}
		else{
			j=literals[i].literalNumber;
		}
		printf(" %d", j);
	}
	printf(" )\n");
}

void printState(){
	int j;
	int i;
	printf("***** DUMPING STATE ******\n");
	for(i=0;i<numberOfClauses;i++){
		DPLL_CLAUSE* dl = (DPLL_CLAUSE*) clauses[i].data;
		printf("CLAUSE %d: \n",i);
		printf("CURRENT LITERALS: ");
		for(j=0;j<dl->currentLiteralCount;j++){
			printf("%d ",dl->currentLiterals[j]);
		}
		printf("\n IS SATISFIED: %d at DEPTH %d\n",dl->isSatisfied, dl->depthSatisfied);
	}
	printf("\n\n");
}

void satisfyClauses(int literal, int depth){
	LITERAL* l = getLiteral(abs(literal));
	CLAUSE_ENCLOSER* clEn;	
	if(literal > 0){
		clEn = ((DPLL_LITERAL*)(l->data))->positiveClauses;
	}
	else{
		clEn = ((DPLL_LITERAL*)(l->data))->negativeClauses;
	}
	while(clEn != NULL){
		CLAUSE* cl = clEn->clause;
		DPLL_CLAUSE* dl = (DPLL_CLAUSE*) cl->data;
		if(dl->isSatisfied == 0){
			int i;
			dl->isSatisfied = 1;
			dl->depthSatisfied = depth;
			for(i=0;i<dl->currentLiteralCount;i++){
				if(dl->currentLiterals[i]>0){
					getLiteral(dl->currentLiterals[i])->countTrueClauses--;
				}
				else{
					getLiteral(-dl->currentLiterals[i])->countFalseClauses--;
				}
			}
			unsatisfiedClauses--;
		}
		clEn = clEn->next;
	}
}

int allSatisfied(){
	if(unsatisfiedClauses == 0){
		return 1;
	}
	return 0;
}

void shortenClauses(int literal, int depth){
	LITERAL* l = getLiteral(abs(literal));
	CLAUSE_ENCLOSER* clEn;	
	if(literal > 0){
		clEn = ((DPLL_LITERAL*)(l->data))->positiveClauses;
	}
	else{
		clEn = ((DPLL_LITERAL*)(l->data))->negativeClauses;
	}
	while(clEn != NULL){
		CLAUSE* cl = clEn->clause;
		DPLL_CLAUSE* dl = (DPLL_CLAUSE*) cl->data;
			int i;
			int j=0;
			for(i=0;i<dl->currentLiteralCount;i++){
				if(dl->currentLiterals[i]!=literal){
					dl->currentLiterals[j++]=dl->currentLiterals[i];
				}
			}
			assert(j<dl->currentLiteralCount);
			dl->currentLiteralCount=j;
		if(dl->isSatisfied == 0){
			if(dl->currentLiteralCount == 0){
	    		CLAUSE_ENCLOSER* ce = (CLAUSE_ENCLOSER*) malloc(sizeof(CLAUSE_ENCLOSER));
    			ce->clause = cl;
    			ce->next = emptyClauses;
	    		emptyClauses = ce;
			}
			else if(dl->currentLiteralCount == 1){
	    		CLAUSE_ENCLOSER* ce = (CLAUSE_ENCLOSER*) malloc(sizeof(CLAUSE_ENCLOSER));
    			ce->clause = cl;
    			ce->next = singleVariableClauses;
    			singleVariableClauses = ce;
			}
		}
		clEn = clEn->next;
	}
}

int hasEmptyClause(){
	if(emptyClauses == NULL){
		return 0;
	}
	else{
		while(emptyClauses != NULL){
			CLAUSE* cl = emptyClauses->clause;
			DPLL_CLAUSE* dl = (DPLL_CLAUSE*) cl->data;
			if(dl->currentLiteralCount!=0){
				CLAUSE_ENCLOSER* clen = emptyClauses;
				emptyClauses = emptyClauses->next;
				free(clen);
			}
			else{
				break;
			}
		}
		if(emptyClauses != NULL){	
			return 1;
		}
		return 0;
	}
}

int getUnitLiteral(){
	while(singleVariableClauses != NULL){
		DPLL_CLAUSE* dl = (DPLL_CLAUSE*) singleVariableClauses->clause->data;
		if(dl->isSatisfied == 0 && dl->currentLiteralCount == 1){
			return dl->currentLiterals[0];
		}
		else{
			CLAUSE_ENCLOSER* old = singleVariableClauses;
			singleVariableClauses = singleVariableClauses->next;
			free(old);
		}
	}
	return 0;
}

int getPureLiteral(){
	int i;
	for(i=0;i<numberOfLiterals;i++){
		if(literals[i].value == 0){
			if(literals[i].countTrueClauses == 0 && literals[i].countFalseClauses > 0){
				return -literals[i].literalNumber;
			}
			else if(literals[i].countFalseClauses == 0 && literals[i].countTrueClauses > 0){
				return literals[i].literalNumber;
			}
		}
	}
	return 0;
}

void cleanUp(int literal, int depth){
	LITERAL* l = getLiteral(abs(literal));
	l->value = 0;
	CLAUSE_ENCLOSER* clEn;	
	CLAUSE_ENCLOSER* clEnAddLiteral;
	if(literal > 0){
		clEn = ((DPLL_LITERAL*)(l->data))->positiveClauses;
		clEnAddLiteral = ((DPLL_LITERAL*)(l->data))->negativeClauses;
	}
	else{
		clEn = ((DPLL_LITERAL*)(l->data))->negativeClauses;
		clEnAddLiteral = ((DPLL_LITERAL*)(l->data))->positiveClauses;
	}
	//printf("Starting cleanup\n");
	while(clEn != NULL){
		CLAUSE* cl = clEn->clause;
		/*if(cl != NULL){
			printf("NN %d\n",cl);
		}
		else{
			printf("c1 is null\n");
		}*/
		DPLL_CLAUSE* dl = (DPLL_CLAUSE*) cl->data;
		if(dl->isSatisfied == 1 && dl->depthSatisfied == depth){
			int i;
			dl->isSatisfied = 0;
			dl->depthSatisfied = -1;
			for(i=0;i<dl->currentLiteralCount;i++){
				if(dl->currentLiterals[i]>0){
					getLiteral(dl->currentLiterals[i])->countTrueClauses++;
				}
				else{
					getLiteral(-(dl->currentLiterals[i]))->countFalseClauses++;
				}
			}
			unsatisfiedClauses++;
		}
		clEn = clEn->next;
	}
	while(clEnAddLiteral != NULL){
		CLAUSE* cl;
		DPLL_CLAUSE* dl;
 		cl = clEnAddLiteral->clause;
		dl = (DPLL_CLAUSE*) (cl->data);
		//if(dl->depthSatisfied >= depth){
			int item = dl->currentLiteralCount;	
			dl->currentLiterals[item]=-literal;
			dl->currentLiteralCount=item+1;
			assert(item + 1 <= maxLiteralsPerClause);
		//}
		clEnAddLiteral = clEnAddLiteral->next;
	}
}

int getUnsatisfiedVariable(){
	//TODO: replace by a better algorithm...
	int direction = 1;
	#ifdef RANDOMIZED_DIRECTION 
		if(random()%2 == 0){
			direction = -1;
		}
	#endif	
	#ifdef RANDOMIZED_EXPLORE 
		int i;
		int count = 0;
		int selected=0;
		for(i = 0; i<numberOfLiterals; i++){
			if(literals[i].value  == 0){
				count++;
				if(random()%count == 0){
					selected = literals[i].literalNumber;
				}
			}
		}
		return direction * selected;
	#else
	#ifdef GREEDY_SELECT
		int i;
		int selected=0;
		int max = 0;
		for(i = 0; i<numberOfLiterals; i++){
			if(literals[i].value  == 0){
				if(literals[i].countTrueClauses > max){
					selected = literals[i].literalNumber;
					max = literals[i].countTrueClauses;
				}
				if(literals[i].countFalseClauses > max){
					selected = -literals[i].literalNumber;
					max = literals[i].countFalseClauses;
				}
			}
		}
		return selected;
	#else
	#ifdef GREEDY_SELECT_2
		int i;
		int selected=0;
		int min = 10000000;
		for(i = 0; i<numberOfLiterals; i++){
			if(literals[i].value  == 0){
				if(literals[i].countFalseClauses < min){
					selected = literals[i].literalNumber;
					min = literals[i].countFalseClauses;
				}
				if(literals[i].countTrueClauses < min){
					selected = -literals[i].literalNumber;
					min = literals[i].countTrueClauses;
				}
			}
		}
		return selected;

	#else
	int i;
	for(i=0;i<numberOfLiterals;i++){
		if(literals[i].value == 0){
			return direction * literals[i].literalNumber;
		}
	}
	return 0;
	#endif
	#endif
	#endif
}

int dpllStepWithCleanUp(int literal, int depth){
	//printState();
	int returnedValue = dpllStep(literal, depth);
	if(returnedValue == 0){
		//printf("BEFORE CLEAN\n");
		//checkStructure();
		cleanUp(literal, depth);
		//printf("AFTER CLEAN\n");
		//checkStructure();
	}
	return returnedValue;
}

void runDPLL(){
	statistics.maxDepthExplored = 0;
	statistics.nodesExplored=0;
	statistics.backTracks=0;
	buildSupportStructures();
	int returned = dpllStep(0,0);
	printf("Printf Returned %d\n",returned);
	printSolution(returned);
	printLiteralState();
	#ifdef PRINT_STATISTICS
		printf("**** STATISTICS *****\n");
		printf("Max Depth: %d\n",statistics.maxDepthExplored);
		printf("Nodes Expored: %d\n",statistics.nodesExplored);
		printf("BackTracks: %d\n",statistics.backTracks);
	#endif
}

int dpllStep(int literal, int depth){
		statistics.nodesExplored++;
		if(statistics.maxDepthExplored < depth){
			statistics.maxDepthExplored = depth;
		}
		if(literal != 0){
			LITERAL* currentLiteral = getLiteral(abs(literal));
			assert(currentLiteral->value == 0);
			if(literal > 0){
				currentLiteral->value=1;
			}
			else{
				currentLiteral->value=-1;
			}
			((DPLL_LITERAL*)(currentLiteral->data))->depthSatisfied=depth;
			satisfyClauses(literal,depth);
			if(allSatisfied()){
				return 1;
			}
			else{
				//printf( "Shortening %d\n",literal);
				shortenClauses(-literal, depth);
			}
		}
		if(hasEmptyClause()){
			#ifdef DPLL_DEBUG
				printf("Has Empty Clause\n");
			#endif
			return 0;
		}
		int unitLiteral = getUnitLiteral();
		if(unitLiteral != 0){
			#ifdef DPLL_DEBUG
				printf("Accepting Unit Literal %d\n",unitLiteral);
			#endif
			return dpllStepWithCleanUp(unitLiteral, depth+1);
		}
		int pureLiteral = getPureLiteral();
		if(pureLiteral != 0){
			#ifdef DPLL_DEBUG
				printf("Accepting Pure Literal %d\n",pureLiteral);
			#endif
			return dpllStepWithCleanUp(pureLiteral, depth+1);
		}
		int selectVariable = getUnsatisfiedVariable();
		if(selectVariable == 0){
			return 0;
		}
		#ifdef DPLL_DEBUG
			printf("Selecting Variable %d\n",selectVariable);
		#endif
		if(dpllStepWithCleanUp(selectVariable, depth+1)){
				return 1;
		}
		else{
			statistics.backTracks++;
			#ifdef DPLL_DEBUG
				printf("Selecting Variable %d\n",-selectVariable);
			#endif
			return dpllStepWithCleanUp(-selectVariable, depth+1);
		}
}