/* Driver program for WALKSAT */
#include "../includes/globals.h"
#include "../WalkSat/WalkSat.h"
#include <sys/time.h>
#include<stdio.h>
#include<stdlib.h>

void displayResults(int result);
void printInputStats(void);

int main(int argc, char** argv)
{
	int i;
	int result,max_flips,max_tries ;
	int flipNum,retryNum;

	struct timeval initTv;
	struct timezone initTz;
	struct timeval finalTv;
	struct timezone finalTz;
	long timeElapsed;
	long timeMilli;
	long timeMicro;
	long timeSec;

	float ratio,prob;
	
	if(argc < 5){
		printf("[exectutable] [sentence file] [flip_probability] [maximum number of flips] [maximum number of retries]\n");
		exit(1);
	}
	
	readInputFile(argv[1]);
	prob = atof(argv[2]);
	max_flips = atoi(argv[3]);
	max_tries = atoi(argv[4]);

	fflush(stdin);
	fflush(stdout);
	//printf("%f %d %d\n",prob,max_flips,max_tries);
	gettimeofday(&initTv, &initTz);
	result = WalkSat(prob,max_flips,max_tries,&flipNum,&retryNum,NULL);  
	gettimeofday(&finalTv, &finalTz);

	timeElapsed = (finalTv.tv_usec - initTv.tv_usec) + (finalTv.tv_sec - initTv.tv_sec)*1000000;
	timeMilli = (timeElapsed)/1000;
	timeSec = (timeElapsed / 1000000);

	ratio = ((float)numberOfClauses/(float)numberOfLiterals);
	if(!result)
	    printf("# WALKSAT could not find a solution.\n");
	else
	    printf("# WALKSAT found a solution.\n");

	printf("# CLAUSES = %d \n",numberOfClauses);
	printf("# LITERALS = %d \n",numberOfLiterals);
	printf("# LITERALS PER CLAUSE= %d \n",maxLiteralsPerClause);
	if ( ratio < 4.2 )
	    printf("# LIT/CLAUSE RATIO LOW. POSSIBLY EASY PROBLEM \n");
	else if ( fabs(ratio - 4.33 ) < 0.13 )
	    printf("# LIT/CLAUSE RATIO AT BOUNDARY. POSSIBLY HARD PROBLEM \n");
	else 
	    printf("# CLAUSE/LITERAL RATIO HIGH. POSSIBLY UNSOLVABLE PROBLEM \n");
	printf("# FLIP PROBABILITY = %f \n",atof(argv[2]));
	printf("# MAX FLIPS = %d \n",atoi(argv[3]));
	printf("# MAX RETRIES = %d \n",atoi(argv[4]));
	printf("# NUMBER OF RETRIES = %d \n",retryNum);
	printf("# NUMBER OF FLIPS = %d\n",(retryNum-1)*max_flips + flipNum);
	printf("# TIME OF EXECUTION: %ld (in sec) %ld (in millisec) %ld (in microsec)\n",timeSec, timeMilli,timeElapsed);
	/*********** Print log *************/
	displayResults(result);
	return 0;
}

void printInputStats(void)
{
    int i,j;

    printf("\n#################################################\n");
    printf("Number of literals = %d\n",numberOfLiterals);
    printf("Number of clauses = %d\n",numberOfClauses);
    printf("Maximum number of literals per clause = %d\n",maxLiteralsPerClause);
    printf("Printing clauses .... \n");
    
    for( i = 0 ; i < numberOfClauses ; i++) {
	printf("Clause [#%d] : ",i+1);
	for ( j = 0 ; j < clauses[i].literalCount ; j++) {
	    printf("[%d] ",clauses[i].literals[j]);
	}
	printf("\n");
    }
    printf("\n#################################################\n");
}


void displayResults(int result)
{

	if ( !result ) {
	printf("Fail\n");
	return;
	}

	printf("Solution:\n\n( ");

    	int i;
    	for( i = 0 ; i < numberOfLiterals ; i++) 
		printf(" %d ",literals[i].value);
	printf(")\n");
}