/*
 * CFormula.cpp
 *
 *  Created on: Oct 1, 2016
 *      Author: Sina M.Baharlou
 */

#include "CFormula.hpp"

CFormula::CFormula():
nVars(0),
nClauses(0),
fStats{0,0,0},
fVars(NULL),
fPortions(NULL),
tPortion(0),
nLit(NULL),
evalArray(NULL),

evalClause(NULL),
varMap(NULL),

clCounter(0),

greedyFactor(DEFAULT_GREEDY_FACTOR),
arrayFiller(NULL),
nbSatisfiedClausesFill(0),
nbSatisfiedClausesSolve(0),
lastFillMethod(0),
lastHeuristic(0),
ite(0)
{

	this->fType.clear();
	this->fComments.clear();

	// -- Initializing distribution variables --

	rndReal=std::uniform_real_distribution<float>(0.0,1.0);
	rndMethod=std::uniform_int_distribution<int>(FIRST_FILL_METHOD,LAST_FILL_METHOD);
	rndHeuristic=std::uniform_int_distribution<int>(FIRST_H_METHOD,LAST_H_METHOD);

	// -- Init random engine --

	struct timespec ts;
	unsigned theTick = 0U;
	clock_gettime( CLOCK_REALTIME, &ts );
	theTick  = ts.tv_nsec / 1000000;
	theTick += ts.tv_sec * 1000;
	rndEngine.seed(theTick);
}




bool CFormula::initFormula(const char* filename)
{

	// -- Initialize variables --

	this->cFormula.empty();
	this->fComments.empty();
	this->fType.empty();
	this->fStats={0,0,0};
	this->clCounter=0;
	bool fReached=false;


	// -- Free previously allocated variables --

	if (this->fVars) free(this->fVars);
	if (this->fPortions) free(this->fPortions);
	if (this->nLit) free(this->nLit);
	if (this->evalArray) free(this->evalArray);
	if (this->arrayFiller) free(this->arrayFiller);
	if (this->varMap) free(this->varMap);
	if (this->evalClause) free(this->evalClause);

	// -- Open input file --

	ifstream input_file;
	input_file.open(filename);

	if (!input_file.is_open())
	{
		printf("STD Error: cannot open '%s'.",filename);
		return false;
	}


	// -- Parse the provided file --

	std::string line;
	while (std::getline(input_file, line))
	{
		// -- get the flag (can be 'c' or 'p') --
		char flag=line[0];
		std::vector<string> tokens;

		switch (flag)
		{

		case COMMENT_FLAG:	// -- Comment line has reached --

			// -- Add to comment string --
			this->fComments.append(&line[1]);
			this->fComments.append("\n");
			break;


		case PROBLEM_FLAG:	// -- Problem line has reached --

			// -- Tokenize current line --
			tokens.empty();
			tokens=tokenize(&line[1]," ");

			// -- Check if the syntax if correct in order to parse the parameters --
			if (tokens.size()<3)
			{
				printf("There is a syntax error in the problem definition.");
				return false;
			}

			// -- Assign the variables --
			this->fType=tokens[0];
			this->nVars=stoi(tokens[1])+1;		// -- starts from 1
			this->nClauses=stoi(tokens[2]);
			fReached=true;

			// -- allocate the arrays
			this->fVars=new bool[this->nVars];
			this->fPortions= new float[this->nVars];
			this->nLit=new int[this->nVars];
			this->evalArray=new int[this->nVars];
			this->evalClause=new bool[this->nClauses];
			this->varMap=new std::vector<int>[this->nVars];

			// -- initialize the arrays
			memset(this->fVars,0,this->nVars*sizeof(bool));
			memset(this->fPortions,0,this->nVars*sizeof(float));
			memset(this->nLit,0,this->nVars*sizeof(int));
			memset(this->evalArray,0,this->nVars*sizeof(int));
			memset(this->evalClause,0,this->nClauses*sizeof(bool));

			// -- Instantiate the arrayFiller class
			this->arrayFiller=new ArrayFiller(this->fVars,this->nVars);

			break;


		case END_FLAG: // -- End of the formula has reached --
			input_file.close();

			// -- Ppdate stats --
			this->tPortion=(float)this->fStats.nPosLits/this->fStats.nLits;
			for (unsigned int i=1;i<this->nVars;i++)
				this->fPortions[i]/=(float)this->nLit[i];

			// -- Init random filler --
			this->arrayFiller->setPortionRate(this->tPortion);
			this->arrayFiller->setPortionArray(this->fPortions);
			this->arrayFiller->fillArray(PORTION_EL_FILL);
			return true;
			break;

		default:	// -- Clause line has reached--
			if (!fReached)
				continue;
			this->cFormula.push_back(parseClause(&line[0]," "));
			break;
		}

	}

	return true;
}




bool CFormula::evalFormulaQ(unsigned int varIndex,int& clNum)
{

	bool fEval=true;
	clNum=0;

	// -- check through the modified clauses --
	for (unsigned int i=0;i<this->varMap[varIndex].size();i++)
	{
		// -- get the clause --
		int cIndex=this->varMap[varIndex].at(i);
		Clause cl=this->cFormula[cIndex];

		// -- for each literal
		for (unsigned int j=0;j<cl.size();j++)
		{

			Literal lit=cl[j];

			// -- get the index and sign
			bool neg=(lit<0);
			int index=abs(lit);
			// -- evaluate the literal
			bool litEval=neg^this->fVars[index];
			this->evalClause[cIndex]=litEval; // -- update clause truth list

			// -- if positive -> clause will be evaluated as positive
			if (litEval)
				break;

		}

	}


	// -- evaluate the whole formula --

	for (unsigned int i=0;i<this->cFormula.size();i++)
	{
		bool evalClause=this->evalClause[i];
		fEval&=evalClause;
		if (evalClause)clNum++;
	}
	return fEval;
}


bool CFormula::evalFormula(int& clNum)
{


	bool fEval=true;
	clNum=0;


	for (unsigned int i=0;i<this->cFormula.size();i++)
	{

		// -- get the clause --
		Clause cl=this->cFormula[i];
		bool clEval=false;

		// -- for each literal
		for (unsigned int j=0;j<cl.size();j++)
		{

			Literal lit=cl[j];

			// -- get the index and sign
			bool neg=(lit<0);
			int index=abs(lit);
			// -- evaluate the literal
			bool litEval=neg^this->fVars[index];

			this->evalClause[i]=litEval;

			// -- if positive -> clause will be evaluated as positive
			if (litEval)
			{
				clEval=true;
				clNum++;
				break;
			}
		}

		// -- and it with current evaluation of formula
		fEval&=clEval;

	}

	return fEval;
}



bool CFormula::startGSAT(int iterations,int maxTry,int fillMethod,int hMethod)
{
	float initGuessMean=0;	// -- initial guess average
	float negClauseMean=0;	// -- average number of negative clauses
	float elaborateMean=0; 	// -- averate number of elaboration
	bool fEval=false;
	int i;

	for (i=0;i<iterations;i++)
	{
		int initGuess=0;
		int clNum=0;
		fEval=false;

		// -- randomly select the filler method --
		FillMethod fMethod;
		if (fillMethod==-1)
			fMethod=getRandomMethod();
		else
			fMethod=(FillMethod)fillMethod;
		lastFillMethod=fMethod;
		ite++;
		// -- randomly select the heuristic method --
		HeuristicMethod heuristic;
		if (hMethod==-1)
			heuristic=getRandomHeuristic();
		else
			heuristic=(HeuristicMethod)hMethod;
		lastHeuristic=heuristic;
		
		this->arrayFiller->fillArray(fMethod);

		// -- evaluate the function
		fEval=this->evalFormula(clNum);
		initGuess=clNum;
		nbSatisfiedClausesFill=initGuess;
		initGuessMean+=initGuess;

		// -- return if already found the solution
		if (fEval)
			break;


		for (int j=0;j<maxTry;j++)
		{
			int choice=0;


			// -- select the choice with the given heuristics --

			switch (heuristic)
			{

			case FIRST_BEST:
				choice=this->getBestChoice(true);
				break;

			case RND_BEST:
				choice=this->getBestChoice();
				break;

			case RND_DIST:
				choice=this->getRndBest();
				break;

			case RND:
				choice=(int)(rndReal(rndEngine)*this->nVars);
				break;

			case RND_GREEDY:
				if (this->takeBestChoice())
					choice=this->getBestChoice();
				else
					choice=this->getRndBest();
				break;

			case WALK_SAT:
				choice=this->walkSatChoice();
				break;

			case GSAT_WSAT:
				if (this->takeGW())
					choice=this->getBestChoice();
				else
					choice=this->walkSatChoice();
				break;

			}


			toggle(this->fVars[choice]);
			fEval=this->evalFormulaQ(choice,clNum);//this->evalFormula(clNum);

			if (fEval)
				break;


		}


		negClauseMean+=this->nClauses-clNum;
		elaborateMean+=clNum-initGuess;
		nbSatisfiedClausesSolve=clNum;

		//printf("[iteration %d, fill :%d, heuristic :%d] - init Guess :%d - final Guess :%d - model found :%d\n",i,fMethod,heuristic,initGuess,clNum,fEval);

		if (fEval)
			break;
	}


	/*printf("Elaborate mean :%f\n",elaborateMean/(float)i);
	printf("Initial guess mean :%f\n",initGuessMean/(float)i);
	printf("Neg clause mean :%f\n",negClauseMean/(float)i);*/



	return fEval;

}


void CFormula::setGreedyFactor(float factor)
{
	this->greedyFactor=factor;
}

void CFormula::setGWFactor(float factor)
{
	this->gwFactor=factor;
}

std::vector<string> CFormula::tokenize(char*input,const char*split)
{
	char * token;
	std::vector<string> token_vec;

	token = strtok (input,split);
	while (token != NULL)
	{
		token_vec.push_back(string(token));
		token = strtok (NULL, " ");
	}
	return token_vec;
}

Clause CFormula::parseClause(char*input,const char*split)
{
	char * token;
	Clause cl;

	token = strtok (input,split);
	while (token != NULL)
	{
		Literal lit=stoi(token);
		if (lit!=0)
		{
			int index=abs(lit);
			// -- update the stats

			this->varMap[index].push_back(clCounter);

			if (lit>0)
			{
				this->fStats.nPosLits++;
				this->fPortions[index]+=1;
			}
			else this->fStats.nNegLits++;
			fStats.nLits++;
			this->nLit[index]++;
			// --

			cl.push_back(lit);
		}
		token = strtok (NULL, " ");
	}

	this->clCounter++;

	return cl;
}




FillMethod CFormula::getRandomMethod()
{
	return (FillMethod)rndMethod(rndEngine);
}


HeuristicMethod CFormula::getRandomHeuristic()
{
	return (HeuristicMethod)rndHeuristic(rndEngine);
}



bool CFormula::takeBestChoice()
{

	double random=rndReal(rndEngine);	// -- Get a double random number between 0 and 1

	// -- Check if GSAT should take a best action
	if (random<=this->greedyFactor)
		return true;
	return false;
}

bool CFormula::takeGW()
{

	double random=rndReal(rndEngine);	// -- Get a double random number between 0 and 1

	// -- Check if GSAT should take a best action
	if (random<=this->gwFactor)
		return true;
	return false;
}


void CFormula::evalMove(int&min,int&max)
{
	min=std::numeric_limits<int>::max();
	max=0;

	for (unsigned int i=1;i<this->nVars;i++)
	{
		int clNum=0;
		int temp=0;
		toggle(this->fVars[i]);

		this->evalFormulaQ(i,clNum);	//this->evalFormula(clNum);
		toggle(this->fVars[i]);
		this->evalFormulaQ(i,temp);

		this->evalArray[i]=clNum;
		if (clNum>max) max=clNum;
		if (clNum<min) min=clNum;

	}
}

std::vector<int> CFormula::evalUnsatClause(int clIndex,int&min,int&max)
{
	min=std::numeric_limits<int>::max();
	max=0;

	Clause cl=this->cFormula[clIndex];
	std::vector<int> evalArray;

	for (unsigned int i=0;i<cl.size();i++)
	{
		Literal lit=cl[i];
		int index=abs(lit);

		int clNum=0;
		int temp=0;

		// -- evaluate the positive clauses
		toggle(this->fVars[index]);
		this->evalFormulaQ(index,clNum);	//this->evalFormula(clNum);
		toggle(this->fVars[index]);
		this->evalFormulaQ(index,temp);
		// --

		evalArray.push_back(clNum);
		if (clNum>max) max=clNum;
		if (clNum<min) min=clNum;

	}

	return evalArray;
}

int CFormula::getBestChoice(bool retFirst)
{
	int min,max;
	this->evalMove(min,max);
	int bestCount=0;
	std::vector<int> bestArray;

	for (unsigned int i=1;i<this->nVars;i++)
	{
		if (this->evalArray[i]==max)
		{
			if (retFirst) return i;	// -- return immediately the first choice

			bestArray.push_back(i);
			bestCount++;
		}
	}

	if (bestCount==1)
		return bestArray[0];

	// -- randomly select the best choice
	int rndIndex=(int)(rndReal(rndEngine)*bestCount);
	return bestArray[rndIndex];

}


int CFormula::walkSatChoice(bool retFirst)
{

	// -- Randomly get one unsatisfied clause
	int clIndex=this->getUnsatClause(retFirst);

	int min,max;

	// -- List the best choices
	std::vector<int> evalArray=evalUnsatClause( clIndex,min,max);

	// -- select randomly from the best choices
	int bestCount=0;
	std::vector<int> bestArray;

	for (unsigned int i=0;i<evalArray.size();i++)
	{
		if (evalArray[i]==max)
		{
			if (retFirst) return i;	// -- return immediately the first choice

			bestArray.push_back(i);
			bestCount++;
		}
	}

	if (bestCount==1)
		return abs(this->cFormula[clIndex].at(bestArray[0]));

	// -- randomly select the best choice
	int rndIndex=(int)(rndReal(rndEngine)*bestCount);

	return abs(this->cFormula[clIndex].at(bestArray[rndIndex]));
}

int CFormula::getUnsatClause(bool retFirst)
{

	int clCount=0;
	std::vector<int> clArray;

	for (unsigned int i=0;i<this->nClauses;i++)
	{
		if (!this->evalClause[i])
		{
			if (retFirst) return i;	// -- return immediately the first choice

			clArray.push_back(i);
			clCount++;
		}
	}

	if (clCount==1)
		return clArray[0];

	// -- randomly select the best choice
	int rndIndex=(int)(rndReal(rndEngine)*clCount);
	return clArray[rndIndex];

}

int CFormula::getRndBest(bool exponential)
{
	int min,max;
	float cum=0;
	this->evalMove(min,max);
	float normalizer=0;

	// -- calculate the discrete probability distribution --
	float  probs[this->nVars];
	float rnd =rndReal(rndEngine);

	for (unsigned int i=1;i<this->nVars;i++)
	{

		probs[i]=(float)(this->evalArray[i]-min+DEFAULT_BIAS);

		if (exponential)probs[i]=exp(probs[i]);
		normalizer+=probs[i];
	}

	// -- sample from the distribution --
	for (unsigned int i=1;i<this->nVars;i++)
	{
		cum+=probs[i]/normalizer;

		if (cum>rnd)
			return i;

	}

	return 0;
}