#include "csflocref.h"
/*
============================================================================
 Name        : csfloc.c
 Author      : Gábor Kusper
 Version     : 1.0
 Copyright   : Gábor Kusper
 Description : CSFLOC in C, Ansi-style
 ============================================================================
 */


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


char* fileName;
int doSorting = 1;
int doIndexing = 1; // can be true only if doSorting is also true
int addLongTailClauses = 0; // can be greater than 0 only if doIndexing is true
int howManyClausesAddMaximumPerClauses = 0;

unsigned int MAXINTINDEX;
unsigned int MAXBITINDEX;
unsigned int MAXVALUE;

unsigned int* counter;
unsigned int* clauses;

int* numxsAtEnd;
int* indexClausesByNumxsAtEnd;

int numOfClauses;
int numOfVariables;

int lentghOfBitArray;


void printBitArray(unsigned int* toPrint)
{
	int i;
	for(i = numOfVariables-1; i>=0; i--)
	{
		int intIndex = i / (sizeof(int)*8);
		int bitIndex = i % (sizeof(int)*8);
		int mask = 1 << bitIndex;
		if((toPrint[intIndex] & mask) > 0) printf("%d ", numOfVariables-i);
		else printf("-%d ", numOfVariables-i);
	}
	printf("0 \n");
}

void printClause(int clauseIndex)
{
	printf("clauseIndex:%d\n",clauseIndex);
	printf("numxsAtEnd[clauseIndex]:%d\n",numxsAtEnd[clauseIndex]);
	int index = clauseIndex * lentghOfBitArray * 2;
	int i;
	for(i = numOfVariables-1; i>=0; i--)
	{
		int intIndex = i / (sizeof(int)*8);
		int bitIndex = i % (sizeof(int)*8);
		int mask = 1 << bitIndex;
		if((clauses[index + intIndex*2] & mask) > 0) printf("%d ", numOfVariables-i);
		else printf("-%d ", numOfVariables-i);
	}
	printf("0 \n");
	for(i = numOfVariables-1; i>=0; i--)
		{
			int intIndex = i / (sizeof(int)*8);
			int bitIndex = i % (sizeof(int)*8);
			int mask = 1 << bitIndex;
			if((clauses[index + intIndex*2 + 1] & mask) > 0) printf("%d ", numOfVariables-i);
			else printf("-%d ", numOfVariables-i);
		}
		printf("0 \n");
}


void printClauses()
{
	int clauseIndex;
	for(clauseIndex=0; clauseIndex < numOfClauses; clauseIndex++)
	{
		printClause(clauseIndex);
	}
}

// coin: http://graphics.stanford.edu/~seander/bithacks.html#ZerosOnRightBinSearch
int countZeroBitsOnTheRight(unsigned int v)
{
	int c;
	// NOTE: if 0 == v, then c = 31.
	if (v & 0x1)
	{
		// special case for odd v (assumed to happen half of the time)
		c = 0;
	}
	else
	{
		c = 1;
		if ((v & 0xffff) == 0)
		{
			v >>= 16;
			c += 16;
		}
		if ((v & 0xff) == 0)
		{
			v >>= 8;
			c += 8;
		}
		if ((v & 0xf) == 0)
		{
			v >>= 4;
			c += 4;
		}
		if ((v & 0x3) == 0)
		{
			v >>= 2;
			c += 2;
		}
		c -= v & 0x1;
	}
	return c;
}


int countZeroBitsOnTheRightInBitArray(int clauseIndex)
{
	int countZeroBits = 0;
	int index = clauseIndex * lentghOfBitArray * 2;
	int intIndex;
	for(intIndex=0; intIndex<lentghOfBitArray; intIndex++)
	{
		if(clauses[index + intIndex*2]!=0) break;
		countZeroBits += sizeof(unsigned int)*8;
	}
	if (intIndex == lentghOfBitArray) return numOfVariables-1;
	countZeroBits += countZeroBitsOnTheRight(clauses[index + intIndex*2]);
	return countZeroBits;
}

int countZeroBitsOnTheRightInBitArrayOldOne(unsigned int* bits)
{
	int countZeroBits = 0;
	int intIndex ;
	for(intIndex=0; intIndex<lentghOfBitArray; intIndex++)
	{
		if(bits[intIndex]!=0) break;
		countZeroBits += sizeof(unsigned int)*8;
	}
	if (intIndex == lentghOfBitArray) return numOfVariables-1;
	countZeroBits += countZeroBitsOnTheRight(bits[intIndex]);
	return countZeroBits;
}


void resolution(int clauseIndexC, int clauseIndexA, int clauseIndexB, int intIndex, int bitIndex)
{

	//printf("Start of Resolution\n");
	//printf("intIndex: %d\n", intIndex);
	//printf("bitIndex: %d\n",  bitIndex);
	//printClause(clauseIndexA);
	//printClause(clauseIndexB);

	numxsAtEnd[clauseIndexC] = -1;
	int indexA = clauseIndexA * lentghOfBitArray * 2;
	int indexB = clauseIndexB * lentghOfBitArray * 2;
	if ((clauses[indexA + intIndex*2 +1] & 1 << bitIndex) == (clauses[indexB + intIndex*2 +1] & 1 << bitIndex)) return;
	int i;
	for(i=0; i<lentghOfBitArray; i++)
	{
		unsigned int tesztA, tesztB, tesztMask;
		tesztMask = clauses[indexA + i*2] & clauses[indexB + i*2];
		tesztA = clauses[indexA + i*2 + 1] & tesztMask;
		tesztB = clauses[indexB + i*2 + 1] & tesztMask;
		if (i==intIndex) { tesztA |= 1<<bitIndex; tesztB |= 1<<bitIndex; }
		if (tesztA != tesztB) return;
	}

	int indexC = clauseIndexC * lentghOfBitArray * 2;
	for(i=0; i<lentghOfBitArray; i++)
	{
		clauses[indexC + i*2] = clauses[indexA + i*2] | clauses[indexB + i*2];
		clauses[indexC + i*2 + 1] = clauses[indexA + i*2 + 1] | clauses[indexB + i*2 + 1];
	}
	clauses[indexC + intIndex*2] &= ~(1<<bitIndex);
	clauses[indexC + intIndex*2 + 1] &= ~(1<<bitIndex);
	numxsAtEnd[clauseIndexC] = countZeroBitsOnTheRightInBitArray(clauseIndexC);

	//printf("End of Resolution\n");
	//printClause(clauseIndexA);
	//printClause(clauseIndexB);
	//printClause(clauseIndexC);
}

void readDIMACScsfloc(char* fileName) {
	char c[1000];
	FILE *fptr;
	if ((fptr=fopen(fileName,"r"))==NULL)
	{
		printf("Error! opening file");
		exit(1);
	}
	int clauseIndex = 0;
	while (fgets(c,1000, fptr)!=NULL) {
		if (c[0]=='c' || c[0]=='%' || c[0]=='0' || c[0]=='\n') continue;
		if (c[0]=='p'){
			char* token = strtok(c, " ");
			token = strtok(NULL, " ");
			token = strtok(NULL, " ");
			numOfVariables = atoi(token);
			MAXINTINDEX = numOfVariables/(sizeof(int)*8);
			MAXBITINDEX = numOfVariables%(sizeof(int)*8);
			MAXVALUE = 1 << MAXBITINDEX;
			lentghOfBitArray =  numOfVariables/(sizeof(int)*8)+1;
			token = strtok(NULL, " ");
			numOfClauses = atoi(token);
			numxsAtEnd = malloc(sizeof(int) * (numOfClauses+addLongTailClauses));
			clauses = malloc(sizeof(int) * (numOfClauses+addLongTailClauses) * lentghOfBitArray * 2);
			indexClausesByNumxsAtEnd = malloc(sizeof(int) * numOfVariables);
			int i;
			for(i=0; i<numOfVariables; i++)
			{
				indexClausesByNumxsAtEnd[i] = 0;
			}
			continue;
		}

		int index = clauseIndex * lentghOfBitArray * 2;
		int i;
		for(i=0; i<lentghOfBitArray; i++)
		{
			clauses[index + i*2] = 0;
			clauses[index + i*2 +1] = 0;
		}

		int maxLiteral = 0;
		char* token = strtok(c, " ");
		while (token) {
			int literal = atoi(token);
			token = strtok(NULL, " ");
			if (literal == 0) continue;

			int literalIndex = numOfVariables - abs(literal);
			int intIndex = literalIndex / (sizeof(int)*8);
			int bitIndex = literalIndex % (sizeof(int)*8);

			unsigned int setMask = 1 << bitIndex;

			clauses[index + intIndex * 2] |= setMask;
			if (literal > 0) clauses[index + intIndex * 2 +1] |= setMask;
			if (abs(literal) > maxLiteral) maxLiteral = abs(literal);
		}
		numxsAtEnd[clauseIndex] = numOfVariables - maxLiteral;
		clauseIndex++;
		if (clauseIndex == numOfClauses) break;
	}
	fclose(fptr);

    /*
    for (uint i = 0; i < numOfClauses; ++i) {
        printf("%u ", numxsAtEnd[i]);
    }
    printf("\n");
    printf("numxsAtEnd\n");
     */
}

void sortClausesByNumxsAtEnd()
{
	//printf("Before sorting:\n");
	//printClauses();
	int i;
	for(i=1; i<numOfClauses; i++)
	{
		int clauseIndex;
		for(clauseIndex=0; clauseIndex<numOfClauses-i; clauseIndex++)
		{
			if (numxsAtEnd[clauseIndex]<numxsAtEnd[clauseIndex+1])
			{
				unsigned int temp = numxsAtEnd[clauseIndex];
				numxsAtEnd[clauseIndex] = numxsAtEnd[clauseIndex+1];
				numxsAtEnd[clauseIndex+1] = temp;

				int indexA = clauseIndex * lentghOfBitArray * 2;
				int indexB = (clauseIndex+1) * lentghOfBitArray * 2;
				int relIndex;
				for(relIndex=0; relIndex<lentghOfBitArray*2; relIndex++)
				{
					temp = clauses[indexA+relIndex];
					clauses[indexA+relIndex] = clauses[indexB+relIndex];
					clauses[indexB+relIndex] = temp;
				}
			}
		}
	}
	//printf("After sorting:\n");
	//printClauses();
}

void createIndexClausesByNumxsAtEnd()
{
	int i;
	int lastValue = 0;
	for(i=numOfClauses-1; i>=0; i--)
	{
		if (numxsAtEnd[i] > lastValue)
		{
			while(lastValue != numxsAtEnd[i])
			{
				indexClausesByNumxsAtEnd[lastValue] = i+1;
				lastValue++;
			}
		}
	}

	// it might be, that we over index if there is no clause with numxAtEnd == 0
	// this part corrects this if needed
	int correctioningIndex = 0;
	while (indexClausesByNumxsAtEnd[correctioningIndex] == numOfClauses)
	{
		correctioningIndex++;
	}
	if (correctioningIndex!=0)
	{
		int goodValue = indexClausesByNumxsAtEnd[correctioningIndex];
		do
		{
			correctioningIndex--;
			indexClausesByNumxsAtEnd[correctioningIndex] = goodValue;
		}
		while(correctioningIndex!=0);
	}
}


void addClausesByResolution()
{
	int numberOfNewClauses = 0;
	int numOfZerosAtEnd = 0;
	while (numberOfNewClauses<addLongTailClauses) // While adding clauses
	{
		int clauseIndexA= numOfClauses-1;
		if(numOfZerosAtEnd!=0)
		{
			clauseIndexA = indexClausesByNumxsAtEnd[numOfZerosAtEnd-1]-1;
		}
		for( ; clauseIndexA>=indexClausesByNumxsAtEnd[numOfZerosAtEnd]; clauseIndexA--)
		{
			int clauseIndexB;
			int newClausesPerClause = 0;
			for(clauseIndexB=clauseIndexA-1; clauseIndexB>=indexClausesByNumxsAtEnd[numOfZerosAtEnd]; clauseIndexB--)
			{
				resolution(numOfClauses+numberOfNewClauses, clauseIndexA, clauseIndexB,
									  numOfZerosAtEnd/(sizeof(unsigned int)*8),
									  numOfZerosAtEnd%(sizeof(unsigned int)*8));
				if (numxsAtEnd[numOfClauses+numberOfNewClauses] == -1) continue;

				//printf("numOfZerosAtEnd: %d\n", numOfZerosAtEnd);
				//printf("numberOfNewClauses: %d\n", numberOfNewClauses);
				//printf("numxsAtEnd[numOfClauses+numberOfNewClauses]: %d\n", numxsAtEnd[numOfClauses+numberOfNewClauses]);

				numberOfNewClauses++;
				newClausesPerClause++;

				if (newClausesPerClause==howManyClausesAddMaximumPerClauses) break;
				if (numberOfNewClauses==addLongTailClauses) break;
			}
			if (numberOfNewClauses==addLongTailClauses) break;


			// +1 m?lys?g eleje
			int numOfZerosAtEnd2 = numxsAtEnd[numOfClauses+numberOfNewClauses-1];
			int clauseIndexC = numOfClauses+numberOfNewClauses-1;
			int clauseIndexD;
			for(clauseIndexD=indexClausesByNumxsAtEnd[numOfZerosAtEnd2-1]-1;
					clauseIndexD>=indexClausesByNumxsAtEnd[numOfZerosAtEnd2]; clauseIndexD--)
			{

				//printf("before resolution in +1 depth\n");
				//printf("numxsAtEnd[clauseIndexC]: %d\n", numxsAtEnd[clauseIndexC]);
				//printf("numxsAtEnd[clauseIndexD]: %d\n", numxsAtEnd[clauseIndexD]);


				resolution(numOfClauses+numberOfNewClauses, clauseIndexC, clauseIndexD,
										numOfZerosAtEnd2/(sizeof(unsigned int)*8),
										numOfZerosAtEnd2%(sizeof(unsigned int)*8));
				if (numxsAtEnd[numOfClauses+numberOfNewClauses] == -1) continue;

				//printf("after resolution in +1 depth\n");
				//printf("numOfZerosAtEnd2: %d\n", numOfZerosAtEnd2);
				//printf("numberOfNewClauses: %d\n", numberOfNewClauses);
				//printf("numxsAtEnd[numOfClauses+numberOfNewClauses]: %d\n", numxsAtEnd[numOfClauses+numberOfNewClauses]);

				numberOfNewClauses++;
				newClausesPerClause++;

				if (newClausesPerClause==howManyClausesAddMaximumPerClauses) break;
				if (numberOfNewClauses==addLongTailClauses) break;
			}
			if (newClausesPerClause==howManyClausesAddMaximumPerClauses) break;
			if (numberOfNewClauses==addLongTailClauses) break;
			if (numberOfNewClauses==addLongTailClauses) break;
			//+1 m?lys?g v?ge



		}
		numOfZerosAtEnd++;
		if (numOfZerosAtEnd == numOfVariables) break;
	}

	int i;
	for(i=numOfClauses; i<numOfClauses+numberOfNewClauses; i++)
	{
		int clauseIndex;
		for(clauseIndex=i-1; clauseIndex>=0; clauseIndex--)
		{
			if (numxsAtEnd[clauseIndex]<numxsAtEnd[clauseIndex+1])
			{
				unsigned int temp = numxsAtEnd[clauseIndex];
				numxsAtEnd[clauseIndex] = numxsAtEnd[clauseIndex+1];
				numxsAtEnd[clauseIndex+1] = temp;

				int indexA = clauseIndex * lentghOfBitArray * 2;
				int indexB = (clauseIndex+1) * lentghOfBitArray * 2;
				int relIndex;
				for(relIndex=0; relIndex<lentghOfBitArray*2; relIndex++)
				{
					temp = clauses[indexA+relIndex];
					clauses[indexA+relIndex] = clauses[indexB+relIndex];
					clauses[indexB+relIndex] = temp;
				}
			}
		}
	}

	numOfClauses+=numberOfNewClauses;
	createIndexClausesByNumxsAtEnd();
}


void CCCSolver(FILE* iofile)
{
	counter = malloc(sizeof(int)*lentghOfBitArray);
	int counterArrayIndex;
	for(counterArrayIndex=0; counterArrayIndex<lentghOfBitArray; counterArrayIndex++)
	{
		counter[counterArrayIndex] = 0;
	}

	int changed = 1;
	while(changed)
	{
		changed = 0;
		int maxNumx = -1;
		int clauseIndex = 0;
		if (doIndexing)
		{
			int numOfZerosAtEnd = countZeroBitsOnTheRightInBitArrayOldOne(counter);

			clauseIndex=indexClausesByNumxsAtEnd[numOfZerosAtEnd];
            fprintf(iofile,"z: %d %d\n", numOfZerosAtEnd, clauseIndex);
		}
		while(clauseIndex<numOfClauses)
		{
			int subsumed = 1;
			int intIndex = 0;
			int index = clauseIndex * lentghOfBitArray * 2;
			for(intIndex=0; intIndex<lentghOfBitArray; intIndex++)
			{
				if ((counter[intIndex] & clauses[index]) != (clauses[index+1] & clauses[index]))
				{
					subsumed = 0;
					break;
				}
				index+=2;
			}
			//printf("Subsumed: %d\n", subsumed);
			if (subsumed)
			{
				if (numxsAtEnd[clauseIndex]>maxNumx) maxNumx = numxsAtEnd[clauseIndex];
				// printf("s %u %u\n", clauseIndex, numxsAtEnd[clauseIndex]);
                if (doSorting) {
                    break;
                }
			}
			clauseIndex++;
		}
		if(maxNumx >= 0)
		{
			fprintf(iofile, "j: %d\n",maxNumx);
			int intIndex = maxNumx / (sizeof(int)*8);
			int bitIndex = maxNumx % (sizeof(int)*8);

			unsigned int oldCounter = counter[intIndex];
			//printf("Counter old = %d : %d\n", intIndex, oldCounter);

			counter[intIndex] += 1 << bitIndex;
			//printf("Counter new = %d : %u\n\n", intIndex, counter.array[intIndex]);

			// add carry
			while(oldCounter > counter[intIndex]) {
				//printf("add carry\n");
				//printf("num of clauses:%d\n",numOfClauses);
				//printf("i = %d\n", i);
				//printf("Counter old = %d : %u\n", intIndex, oldCounter);
				//printf("bitIndex = %d ; 1 << bitIndex = %d\n", bitIndex, 1 << bitIndex);
				//printf("Counter new = %d : %u\n", intIndex, counter.array[intIndex]);
				intIndex++;
				oldCounter = counter[intIndex];
				//printf("Counter old = %d : %u\n", intIndex, oldCounter);
				counter[intIndex]++; // carry added here
				//printf("Counter new = %d : %u\n\n", intIndex, counter[intIndex]);
			}

			if (counter[lentghOfBitArray-1] >= MAXVALUE) return;
			changed = 1;
		}

	}

	int i;
	for (i=0; i<lentghOfBitArray; i++) {
		counter[i] = ~counter[i];
	}
	counter[lentghOfBitArray-1] &= (MAXVALUE-1);
}

void printHelp() {
	printf("Count Clear Clause SAT Solver v2.0\n");
	printf("\tA SAT solver based on the CCC algorithm.\n");
	printf("\tDeveloped by Gabor Kusper, 2015.\n");
	printf("USAGE:\n");
	printf("\tcsfloc [-help] -input=<inputfile.cnf>\n");
	printf("\t\t<inputfile.cnf> is a file name, it is the SAT problem to be solved, "
			"it should be in DIMACS format.\n");
	printf("\t\tOUTPUT is written to standard output.\n");
	printf("OPTIONS:\n");
	printf("\t-help\tDisplays this help message.\n");
	printf("\t-dosort\tTurns on clause sorting.\n");
	printf("\t-donotsort\tTurns off clause sorting.\n");
	printf("\t-doindexing\tTurns on clause indexing, and also forces clause sorting to be switched on.\n");
	printf("\t-donotindexing\tTurns off clause indexing.\n");
	printf("\t-addLongTailClauses=N\tAllows to add long tail clauses, ");
	printf("max N clauses are allowed, if N is 0 then it switches off long tail clause adding. ");
	printf("If N is greater than 0 then it forces clause ordering and indexing.\n");
	printf("\t-addLongTailClausesPerClause=M\tAllows to add maximum M long tail clauses per each input clause, ");
	printf("if M is 0 then it switches off long tail clause adding, i.e., it sets N to be 0. ");
	printf("It has any effect if and only if long tail clause adding is switched on, ");
	printf("i.e., N and M are not 0.\n");
	printf("THE DEFAULT SETTINGS ARE:\n");
	printf("Clause indexing is turned on, clause sorting is turned on, ");
	printf("1000 long tail clauses are allowed, 100 per input clauses, i.e., N = 1000, and M = 100.\n");
	printf("EXAMPLE 1:\n");
	printf("\tcsfloc -input=hole6.cnf\n");
	printf("\tReads and solves the SAT problem represented by hole6.cnf. The solution is written to the standard output.\n");
	printf("EXAMPLE 2:\n");
	printf("\tcsfloc -input=uf50-01.cnf -dosort -doindex -addLongTailClauses=1000 -addLongTailClausesPerClause=100\n");
	printf("\tReads and solves the SAT problem represented by uf50-01.cnf. ");
	printf("Clause sorting is switched on. ");
	printf("Clause indexing is switched on. ");
	printf("Adding long tail clauses is switch on. Maximum 1000 new clauses are created, maximum 100 per input clauses. ");
	printf("The solution is written to the standard output.\n");
}

// read the "value" of a command line argument, where the format of the arguments is <name>=<value>
char* getCommandLineArgValue(char* arg) {
	char* s = strchr(arg, '=');

	if (!s) return NULL;

	// close the "name" of the argument, as a string
	*s = '\0';

	// return the "value" of the argument
	return s + 1;
}

// process all the command line argument
int processCommandLineArgs(int argc, char** argv) {
	int i=0;
	int numberOfSetMandatoryOptions=1;
	return numberOfSetMandatoryOptions == 1;
}

void runcsfloc(char* path, FILE* iofile) {

	long startTime = clock();
	//printf("phase 0\n");
	readDIMACScsfloc(path);
	//printf("phase 1\n");
    // printClauses();
	if (doSorting) {
		sortClausesByNumxsAtEnd();
	}
	//printf("phase 2\n");
    // printClauses();
	if (doIndexing) createIndexClausesByNumxsAtEnd();
	//printf("phase 3\n");
	if (addLongTailClauses>0) {
        addClausesByResolution();
        printf("Please don't do this\n");
    }


	CCCSolver(iofile);

	long endTime = clock();

    /*
	if (counter[lentghOfBitArray-1] >= MAXVALUE) printf("0\n");
	else
	{
		printf("1\n");
	}
     */



	free(numxsAtEnd);
	free(counter);
	free(clauses);
	free(indexClausesByNumxsAtEnd);


}