/* Copyright (C) 2000  Dale Schuurmans, Finnegan Southey                     */
/* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
* as published by the Free Software Foundation; either version 2
* of the License, or (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program; if not, write to the Free Software
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
* 
* See the accompanying file "gpl.txt" for details.
 */

/* This is the frontend for all FaleSAT solvers. */

#include <stdlib.h>
#include <stdio.h>
#include <math.h>
#include <time.h>
#include <limits.h>
#include <string.h>
#include <fcntl.h>
#include <sys/stat.h>
#include <errno.h>
#include <sys/time.h>
#include "readcnf.h"
#include "satfront.h"

#define REPEAT_PARAM_NAME "-rep"
#define MAX_LITERALS_PARAM_NAME "-ml"
#define MAX_CLAUSES_PARAM_NAME "-mc"
#define EXACT_ALLOC_PARAM_NAME "-xm"
#define COP_FILE_FORMAT_PARAM_NAME "-cop"
#define SHOW_HELP1_PARAM_NAME "-?"
#define SHOW_HELP2_PARAM_NAME "-help"
#define SHOW_VERSION_PARAM_NAME "-V"
#define FILE_PARAM_NAME "-f"
#define NOT_RANDOM_PARAM_NAME "-nr"
#define OUTPUT_BASE_NAME_PARAM_NAME "-o"
#define NO_DIRECTORY_OUTPUT_PARAM_NAME "-nd"
#define NO_FLUSH_PARAM_NAME "-nf"
#define NO_EXPECTATIONS_PARAM_NAME "-ne"
#define NO_SEQUENCE_OUTPUT_PARAM_NAME "-nso"
#define NO_PROBLEM_OUTPUT_PARAM_NAME "-npo"
#define NO_OVERALL_OUTPUT_PARAM_NAME "-noo"
#define COMPUTE_MOBILITY_PARAM_NAME "-cm"
#define LOG_UNSATS_PARAM_NAME "-lu"
#define LOG_ASSIGNS_PARAM_NAME "-la"
#define LOG_SOLNS_PARAM_NAME "-ls"
#define UNSAT_SKIP_PARAM_NAME "-us"

int main(int argc, char *argv[])
{
	SATParams *params;
	SATResults *results;
	int readFromFiles;
	int notRandom;
	int outputToDirectory;
	int flushOutput;
	int logUnsats;
	int unsatSkip;
	int logAssigns;
	int logSolns;
	int maxAssigns;
	int maxAssignRepeats;
	int showProblemOutput;
	int showSequenceOutput;
	int showOverallOutput;
	int computeExpectations;
	int computeMobility;
	int mobilityWindowLength = -1;
	int numRepeats, repeatCount;
	int argMatched;
	int arg, par;
	int fileFormat = FILE_FORMAT_CNF;
	int maxLiterals = 0;
	int maxClauses = 0;
	int exactAlloc = 0;
	int numFileNames = -1;
	char **fileNames = NULL;
	char *outputBaseName;
	char outputName[2000];
	char outputName2[2000];
	char shortName[2000];
	int prob;
	int percentiles[] = { 5, 25, 50, 75, 95 };
	int numPercentiles = 5;
	int perc;
	double percPoint;
	int *flipRepeats;
	int flipRepeatsSum;
	int flipRepeatsMin;
	int flipRepeatsMax;
	int flipRepeatsMed;
	double flipOverallSum;
	double *flipPercentiles;
	int reweightRepeatsSum;
	double reweightOverallSum;
	double timeDiff;
	double timeRepeatsSum;
	double timeOverallSum;
	int failRepeatsSum;
	double failOverallSum;
	int restRepeatsSum;
	double restOverallSum;
	double unsatRepeatsSum;
	double unsatOverallSum;
	double mobilityRepeatsSum;
	double mobilityOverallSum;
	double expectedFlips = 0;
	double expectedFlipsOverallSum;
	double minExpectedFlips = 0;
	int optimalFlips = 0;
	double optimalFlipsOverallSum;
	double optimalPercentile = 0;

	FILE *configOut = NULL;
	FILE *problemOut = NULL;
	FILE *sequenceOut = NULL;
	FILE *overallOut = NULL;
	FILE *unsatOut = NULL;
	FILE *solnOut = NULL;
	struct timeval startTime, endTime;

	params = getSATParams();
	readFromFiles = 0;
	notRandom = 0;
	outputBaseName = NULL;
	outputToDirectory = 1;
	flushOutput = 1;
	logUnsats = 0;
	unsatSkip = 0;
	logAssigns = 0;
	logSolns = 0;
	showProblemOutput = 1;
	showSequenceOutput = 1;
	showOverallOutput = 1;
	computeExpectations = 1;
	computeMobility = 1;
	numRepeats = 1;
	maxLiterals = 0;

	for (arg = 1; arg < argc; arg++)
	{
		if (strcmp(argv[arg], REPEAT_PARAM_NAME) == 0)
		{
			if (arg + 1 >= argc)
			{
				fprintf(stderr, "Integer arg expected after option: %s\n", REPEAT_PARAM_NAME); 
				showUsage(params);
				exit(EXIT_FAILURE);
			}
			else
			{
				if (sscanf(argv[arg + 1], "%d", &numRepeats) != 1)
				{
					fprintf(stderr, "Integer arg expected after option: %s\n", REPEAT_PARAM_NAME); 
					showUsage(params);
					exit(EXIT_FAILURE);
				}
				arg++;
			}
		}
		else if (strcmp(argv[arg], UNSAT_SKIP_PARAM_NAME) == 0)
		{
			if (arg + 1 >= argc)
			{
				fprintf(stderr, "Integer arg expected after option: %s\n",
						UNSAT_SKIP_PARAM_NAME); 
				showUsage(params);
				exit(EXIT_FAILURE);
			}
			else
			{
				if (sscanf(argv[arg + 1], "%d", &unsatSkip) != 1)
				{
					fprintf(stderr, "Integer arg expected after option: %s\n",
							UNSAT_SKIP_PARAM_NAME); 
					showUsage(params);
					exit(EXIT_FAILURE);
				}
				arg++;
			}
		}
		else if (strcmp(argv[arg], MAX_LITERALS_PARAM_NAME) == 0)
		{
			if (arg + 1 >= argc)
			{
				fprintf(stderr, "Integer arg expected after option: %s\n",
						MAX_LITERALS_PARAM_NAME); 
				showUsage(params);
				exit(EXIT_FAILURE);
			}
			else
			{
				if (sscanf(argv[arg + 1], "%d", &maxLiterals) != 1)
				{
					fprintf(stderr, "Integer arg expected after option: %s\n",
							MAX_LITERALS_PARAM_NAME); 
					showUsage(params);
					exit(EXIT_FAILURE);
				}
				arg++;
			}
		}		
		else if (strcmp(argv[arg], MAX_CLAUSES_PARAM_NAME) == 0)
		{
			if (arg + 1 >= argc)
			{
				fprintf(stderr, "Integer arg expected after option: %s\n",
						MAX_CLAUSES_PARAM_NAME); 
				showUsage(params);
				exit(EXIT_FAILURE);
			}
			else
			{
				if (sscanf(argv[arg + 1], "%d", &maxClauses) != 1)
				{
					fprintf(stderr, "Integer arg expected after option: %s\n",
							MAX_CLAUSES_PARAM_NAME); 
					showUsage(params);
					exit(EXIT_FAILURE);
				}
				arg++;
			}
		}
		else if (strcmp(argv[arg], COMPUTE_MOBILITY_PARAM_NAME) == 0)
		{
#if !USE_MOBILITY_TRACKING
			printf("You must enable the USE_MOBILITY_TRACKING option in satfront.h and recompile before using this option.\n");
			exit(EXIT_FAILURE);
#else

			if (arg + 1 >= argc)
			{
				fprintf(stderr, "Integer arg expected after option: %s\n", COMPUTE_MOBILITY_PARAM_NAME); 
				showUsage(params);
				exit(EXIT_FAILURE);
			}
			else
			{
				if (sscanf(argv[arg + 1], "%d", &mobilityWindowLength) != 1)
				{
					fprintf(stderr, "Integer arg expected after option: %s\n", COMPUTE_MOBILITY_PARAM_NAME); 
					showUsage(params);
					exit(EXIT_FAILURE);
				}
				computeMobility = 1;
				arg++;
			}
#endif
		}
		else if (strcmp(argv[arg], FILE_PARAM_NAME) == 0)
		{
			/* All remaining arguments are file names. */
			readFromFiles = 1;
			fileNames = argv + arg + 1;
			numFileNames = argc - arg - 1;
			break;
		}
		else if (strcmp(argv[arg], SHOW_VERSION_PARAM_NAME) == 0)
		{
			showVersion(stderr);
			exit(0);
		}

		else if (strcmp(argv[arg], SHOW_HELP1_PARAM_NAME) == 0)
		{
			showUsage(params);
			exit(0);
		}
		else if (strcmp(argv[arg], SHOW_HELP2_PARAM_NAME) == 0)
		{
			showUsage(params);
			exit(0);
		}
		else if (strcmp(argv[arg], EXACT_ALLOC_PARAM_NAME) == 0)
		{
			exactAlloc = 1;
		}
		else if (strcmp(argv[arg], COP_FILE_FORMAT_PARAM_NAME) == 0)
		{
			fileFormat = FILE_FORMAT_COP;
		}
		else if (strcmp(argv[arg], NOT_RANDOM_PARAM_NAME) == 0)
		{
			notRandom = 1;
		}
		else if (strcmp(argv[arg], NO_FLUSH_PARAM_NAME) == 0)
		{
			flushOutput = 0;
		}
		else if (strcmp(argv[arg], NO_DIRECTORY_OUTPUT_PARAM_NAME) == 0)
		{
			outputToDirectory = 0;
		}
		else if (strcmp(argv[arg], NO_PROBLEM_OUTPUT_PARAM_NAME) == 0)
		{
			showProblemOutput = 0;
		}
		else if (strcmp(argv[arg], NO_SEQUENCE_OUTPUT_PARAM_NAME) == 0)
		{
			showSequenceOutput = 0;
		}
		else if (strcmp(argv[arg], NO_OVERALL_OUTPUT_PARAM_NAME) == 0)
		{
			showOverallOutput = 0;
		}
		else if (strcmp(argv[arg], LOG_SOLNS_PARAM_NAME) == 0)
		{
#if USE_SOLNS_TRACKING
			logSolns = 1;
#else
			printf("You must enable the USE_SOLNS_TRACKING option in satfront.h and recompile before using this option.\n");
			exit(EXIT_FAILURE);
#endif
		}

		else if (strcmp(argv[arg], LOG_UNSATS_PARAM_NAME) == 0)
		{
#if USE_UNSAT_TRACKING
			logUnsats = 1;
#else
			printf("You must enable the USE_UNSAT_TRACKING option in satfront.h and recompile before using this option.\n");
			exit(EXIT_FAILURE);
#endif
		}
		else if (strcmp(argv[arg], LOG_ASSIGNS_PARAM_NAME) == 0)
		{
#if !USE_ASSIGNMENT_TRACKING
			printf("You must enable the USE_ASSIGNMENT_TRACKING option in satfront.h and recompile before using this option.\n");
			exit(EXIT_FAILURE);
#endif

			if (arg + 2 >= argc)
			{
				fprintf(stderr, "Two integer args expected after option: %s\n", LOG_ASSIGNS_PARAM_NAME); 
				showUsage(params);
				exit(EXIT_FAILURE);
			}
			else
			{
				logAssigns = 1;

				if (sscanf(argv[arg + 1], "%d", &maxAssigns) != 1)
				{
					fprintf(stderr, "Integer arg expected after option: %s\n", LOG_ASSIGNS_PARAM_NAME); 
					showUsage(params);
					exit(EXIT_FAILURE);
				}
				arg++;

				if (sscanf(argv[arg + 1], "%d", &maxAssignRepeats) != 1)
				{
					fprintf(stderr, "Second integer arg expected after option: %s\n", LOG_ASSIGNS_PARAM_NAME); 
					showUsage(params);
					exit(EXIT_FAILURE);
				}
				arg++;
			}
		}
		else if (strcmp(argv[arg], NO_EXPECTATIONS_PARAM_NAME) == 0)
		{
			computeExpectations = 0;
		}
		else if (strcmp(argv[arg], OUTPUT_BASE_NAME_PARAM_NAME) == 0)
		{
			if (arg + 1 >= argc)
			{
				fprintf(stderr, "Base name arg expected after option: %s\n", OUTPUT_BASE_NAME_PARAM_NAME); 
				showUsage(params);
				exit(EXIT_FAILURE);
			}
			else
			{
				outputBaseName = argv[arg + 1];
				arg++;
			}
		}
		else
		{
			/* Read int args. */
			par = 0;
			argMatched = 0;

			while (!argMatched && par < params->numIntParams)
			{
				if (strcmp(argv[arg], params->intParamNames[par]) == 0)
				{
					argMatched = 1;

					if (arg + 1 >= argc)
					{
						fprintf(stderr, "Integer arg expected after option: %s\n", params->intParamNames[par]); 
						showUsage(params);
						exit(EXIT_FAILURE);
					}
					else
					{
						if (sscanf(argv[arg + 1], "%d", params->intParams + par) != 1)
						{
							fprintf(stderr, "Integer arg expected after option: %s\n", params->intParamNames[par]); 
							showUsage(params);
							exit(EXIT_FAILURE);
						}
						arg++;
					}
				}

				par++;
			}

			/* Read double args. */
			par = 0;

			while (!argMatched && par < params->numDoubleParams)
			{
				if (strcmp(argv[arg], params->doubleParamNames[par]) == 0)
				{
					argMatched = 1;

					if (arg + 1 >= argc)
					{
						fprintf(stderr, "Double arg expected after option: %s\n", params->doubleParamNames[par]); 
						showUsage(params);
						exit(EXIT_FAILURE);
					}
					else
					{
						if (sscanf(argv[arg + 1], "%lg", params->doubleParams + par) != 1)
						{
							fprintf(stderr, "Double arg expected after option: %s\n", params->doubleParamNames[par]); 
							showUsage(params);
							exit(EXIT_FAILURE);
						}
						arg++;
					}
				}

				par++;
			}

			/* Read string args. */
			par = 0;

			while (!argMatched && par < params->numStringParams)
			{
				if (strcmp(argv[arg], params->stringParamNames[par]) == 0)
				{
					argMatched = 1;

					if (arg + 1 >= argc)
					{
						fprintf(stderr, "String arg expected after option: %s\n", params->stringParamNames[par]); 
						showUsage(params);
						exit(EXIT_FAILURE);
					}
					else
					{
						params->stringParams[par] = malloc(strlen(argv[arg + 1] + 1) * sizeof(char));
						strcpy(params->stringParams[par], argv[arg + 1]);
						arg++;
					}
				}

				par++;
			}


			if (!argMatched)
			{
				fprintf(stderr, "Unknown option: %s\n", argv[arg]);
				showUsage(params);
				exit(EXIT_FAILURE);
			}
		}
	}

	/* Seed PRNG. */
	if (!notRandom)
		srand(time(NULL));

	/* Prepare data tracking structures. */
	flipRepeats = malloc(numRepeats * sizeof(int));
	flipPercentiles = malloc(numPercentiles * sizeof(double));

	results = malloc(sizeof(SATResults));

	results->unsatFlipSkip = unsatSkip;
	if (logUnsats)
	{
		results->unsatFlipCounts = calloc(1000000, sizeof(int));
		results->unsatBufferLength = 1000000;
	}
	else
	{
		results->unsatFlipCounts = NULL;
		results->unsatBufferLength = 0;
	}

	results->numReweights = 0;
	results->mobilityWindow = NULL;
	results->mobilityWindowLength = mobilityWindowLength;
	results->sumMobility = 0;
	results->avgMobility = 0;
	results->currentWindowLength = 0;
	results->windowStart = 0;

	/* Set up read from stdin or files. */
	if (!readFromFiles)
	{
		numFileNames = 1;
		fileNames = malloc(sizeof(char*));
		fileNames[0] = "stdin";
	}

	/* Set up output base name. */
	if (outputBaseName != NULL)
	{
		if (outputToDirectory)
		{
			if (mkdir(outputBaseName, S_IRWXU) == -1 && errno != EEXIST)
			{
				fprintf(stderr, "Error creating output directory: %s\n", outputBaseName);
				showUsage(params);
				exit(EXIT_FAILURE);
			}
			strcpy(outputName, outputBaseName);
			strcat(outputName, "/");
		}
		else
		{
			if (outputBaseName == NULL)
				strcpy(outputName, "satres.");
			else
			{
				strcpy(outputName, outputBaseName);
				strcat(outputName, ".");
			}
		}
	}

	/* Write command line to file to record parameters. */
	if (outputBaseName != NULL)
	{
		char command[1000];

		strcpy(outputName2, outputName);
		strcat(outputName2, "cfg");

		configOut = fopen(outputName2, "w");
		if (configOut == NULL)
		{
			fprintf(stderr, "Error opening config output file: %s\n", outputName2);
			showUsage(params);
			exit(EXIT_FAILURE);
		}

		showVersion(configOut);
		fprintf(configOut, "\nSolver command line:\n");
		for (arg = 0; arg < argc; arg++)
			fprintf(configOut, "%s ", argv[arg]);
		fprintf(configOut, "\n\n");

		fclose(configOut);

		/* Try to dump some system information into the file as well. */
		sprintf(command, "echo Result from 'uname -a': >> %s", outputName2);
		system(command);
		sprintf(command, "uname -a >> %s", outputName2);
		system(command);
		sprintf(command, "echo >> %s", outputName2);
		system(command);
		sprintf(command, "echo Result from 'cat /proc/cpuinfo': >> %s", outputName2);
		system(command);
		sprintf(command, "cat /proc/cpuinfo >> %s", outputName2);
		system(command);
	}

	/* Open sequence output file. */

	if (showSequenceOutput)
	{
		if (outputBaseName == NULL)
		{
			sequenceOut = stdout;
		}
		else
		{
			strcpy(outputName2, outputName);
			strcat(outputName2, "seq");

			sequenceOut = fopen(outputName2, "w");
			if (sequenceOut == NULL)
			{
				fprintf(stderr, "Error opening sequence output file: %s\n", outputName2);
				showUsage(params);
				exit(EXIT_FAILURE);
			}
		}

		if (outputBaseName != NULL)
			fprintf(sequenceOut,
					"#Fails\tFlipAvg\tFlipMed\tFlipOpt\tFlipExp\tFlipSum\tTryAvg\tTrySum\tRewtAvg\tUnAvg\tMobAvg\tFlipMin\tFlipMax\tFlip%%5\tFlip%%25\tFlip%%50\tFlip%%75\tFlip%%95\tOpt%%\tTimeSum \tTimeAvg \tProblem\n");
	}

	/* Initialize overall counters. */
	reweightOverallSum = 0;
	flipOverallSum = 0;
	timeOverallSum = 0;
	failOverallSum = 0;
	restOverallSum = 0;
	unsatOverallSum = 0;
	mobilityOverallSum = 0;
	expectedFlipsOverallSum = 0;
	optimalFlipsOverallSum = 0;

	/* Execute sequence of problems. */

	for (prob = 0; prob < numFileNames; prob++)
	{
		FILE *in;

		/* Read problem. */
		if (readFromFiles)
		{
			char* lastSlash;

			in = fopen(fileNames[prob], "r");
			lastSlash = strrchr(fileNames[prob], '/');
			if (lastSlash == NULL)
				strcpy(shortName, fileNames[prob]);
			else
				strcpy(shortName, lastSlash + 1);

			params->problemFilename = fileNames[prob];
			params->shortFilename = shortName;
		}
		else
		{
			in = stdin;
			strcpy(shortName, "stdin");

			params->problemFilename = "stdin";
			params->shortFilename = shortName;
		}

		if (!in)
		{
			fprintf(stderr, "Error opening file: %s\n", fileNames[prob]);
			showUsage(params);
			exit(EXIT_FAILURE);
		}

		/* Allocate memory and read the problem. */
		readProblem(in, maxLiterals, maxClauses, exactAlloc, fileFormat, results);

		if (readFromFiles)
			fclose(in);

		/* Initialize repeats counters. */
		flipRepeatsSum = 0;
		reweightRepeatsSum = 0;
		timeRepeatsSum = 0;
		failRepeatsSum = 0;
		restRepeatsSum = 0;
		unsatRepeatsSum = 0;
		mobilityRepeatsSum = 0;

		/* Open problem output file. */
		if (showProblemOutput)
		{
			if (outputBaseName == NULL)
			{
				problemOut = stdout;
			}
			else
			{
				strcpy(outputName2, outputName);
				strcat(outputName2, shortName);
				strcat(outputName2, ".res");

				problemOut = fopen(outputName2, "w");
				if (problemOut == NULL)
				{
					fprintf(stderr, "Error opening problem output file: %s\n", outputName2);
					showUsage(params);
					exit(EXIT_FAILURE);
				}
			}

			/* Write problem output header. */
			fprintf(problemOut, "#Rep\tFail\tUnsat\tFlips\tTries\tRewts\tUnAvg\tMobAvg\tTime\n");
		}

		/* Open assignment output file. */
		if (logAssigns && outputBaseName != NULL)
		{
			strcpy(outputName2, outputName);
			strcat(outputName2, shortName);
			strcat(outputName2, ".ass");

			results->firstAssign = 1;
			results->firstRepeat = 1;
			results->maxAssigns = maxAssigns;
			results->maxAssignRepeats = maxAssignRepeats;
			results->assignCount = 0;
			results->repeatCount = 0;
			results->assignOut = fopen(outputName2, "w");
			if (results->assignOut == NULL)
			{
				fprintf(stderr, "Error opening assignment output file: %s\n", outputName2);
				showUsage(params);
				exit(EXIT_FAILURE);
			}

			fprintf(results->assignOut, "# %s\n", shortName);
			fprintf(results->assignOut, "r %d\n", results->maxAssignRepeats);
		}
		
			/* Open solution output file. */
		if (logSolns && outputBaseName != NULL)
		{
			results->solution = malloc(results->numVars * sizeof(int));
			results->copySolution = 1;

			strcpy(outputName2, outputName);
			strcat(outputName2, shortName);
			strcat(outputName2, ".sol");

			solnOut = fopen(outputName2, "w");
			if (solnOut == NULL)
			{
				fprintf(stderr, "Error opening solution output file: %s\n", outputName2);
				showUsage(params);
				exit(EXIT_FAILURE);
			}

			fprintf(solnOut, "# %s\n", shortName);
		}


			/* Run the pre-solve routine before actually solving. */

		preSolve(params);

		if (logAssigns && outputBaseName != NULL)
		{
			results->repeatCount = 0;
		}


			/* Repeatly solve problem */

		for (repeatCount = 0; repeatCount < numRepeats; repeatCount++)
		{
			gettimeofday(&startTime, NULL);

			results->unsatSum = 0;

				/* Run the actual solver. */
			runSolver(params, results);

			gettimeofday(&endTime, NULL);

				/* Log assignment history (if enabled). */
			if (logAssigns && outputBaseName != NULL && results->repeatCount < results->maxAssignRepeats)
			{
				fprintf(results->assignOut, "-1\n");
				results->firstAssign = 1;
				results->assignCount = 0;
				results->repeatCount++;
			}

				/* Log the solution history (if enabled). */
			if (logSolns && outputBaseName != NULL)
			{
				if (results->isSatisfied)
				{
						/* Dump solution to the file. */
					int x;

					#if USE_ORDERED_SOLN_FORMAT 
						fprintf(solnOut, "%d", results->solution[0]);
						for (x = 1; x < results->numVars; x++)
							fprintf(solnOut, " %d", results->solution[x] * (x+1));
					#else
						for (x = 1; x < results->numVars; x++)
							fprintf(solnOut, " %d", results->solution[x]);
						fprintf(solnOut, "%d", results->solution[0]);
					#endif
				}
				fprintf(solnOut, "\n");
			}


				/* Track repetition's stats. */
			timeDiff = (endTime.tv_sec - startTime.tv_sec) +
				(endTime.tv_usec - startTime.tv_usec) / 1000000.0;
			timeRepeatsSum  += timeDiff;
			flipRepeats[repeatCount] = results->numFlips;
			flipRepeatsSum += results->numFlips;
			reweightRepeatsSum += results->numReweights;
			restRepeatsSum += results->numRestarts;
			unsatRepeatsSum += (double)results->unsatSum / results->numFlips;
			mobilityRepeatsSum += results->avgMobility;
			if (!results->isSatisfied)
				failRepeatsSum++;

			if (showProblemOutput)
			{
				fprintf(problemOut, "%d\t%d\t%d\t%d\t%d\t%d\t%g\t%g\t%-9g\n", 
						repeatCount + 1, !results->isSatisfied, 
						results->numClauses - results->numSatisfied, results->numFlips, 
						results->numRestarts, results->numReweights, (double)results->unsatSum / results->numFlips, 
						results->avgMobility,
						timeDiff);

				if (flushOutput)
					fflush(problemOut);
			}
		}

		postSolve(params);

		freeProblem();

		/* Close problem output. */
		if (showProblemOutput)
		{
			if (outputBaseName != NULL)
				fclose(problemOut);
		}

		if (logAssigns && outputBaseName != NULL)
		{
			if (results->assignOut != NULL)
				fclose(results->assignOut);
		}


		if (logSolns && outputBaseName != NULL)
		{
			free(results->solution);
			fclose(solnOut);
		}

		/* Sort repeat results. */
		qsort(flipRepeats, numRepeats, sizeof(int), &compareInt);
		flipRepeatsMin = flipRepeats[0];
		flipRepeatsMax= flipRepeats[numRepeats - 1];

		if (numRepeats % 2 == 0)
		{
			flipRepeatsMed = (int)(flipRepeats[(int)floor(numRepeats / 2.0)] + flipRepeats[(int)ceil(numRepeats / 2.0)]) / 2.0;
		}
		else
		{
			flipRepeatsMed = flipRepeats[numRepeats / 2];
		}

		minExpectedFlips = 1e50;

		if (computeExpectations)
		{
			double cumFlips = 0;

			for (repeatCount = 0; repeatCount < numRepeats; repeatCount++)
			{
				cumFlips += flipRepeats[repeatCount];
				expectedFlips = ((double)flipRepeats[repeatCount] * numRepeats + cumFlips) / (repeatCount + 1) - flipRepeats[repeatCount];
				if (expectedFlips < 0)
				{
					printf("%g\n", expectedFlips);
					printf("%d %d %d\n", repeatCount, numRepeats,
							flipRepeats[repeatCount]);
					printf("cumFlips: %g\n", cumFlips);
					exit(EXIT_FAILURE);
				}

				if (expectedFlips < minExpectedFlips)
				{
					minExpectedFlips = expectedFlips;
					optimalFlips = flipRepeats[repeatCount];
					optimalPercentile = (repeatCount + 1.0) / numRepeats;
				}
			}

			expectedFlipsOverallSum += minExpectedFlips;
			optimalFlipsOverallSum += optimalFlips;
		}

		/* Output sequence results. */
		if (showSequenceOutput)
		{
			if (outputBaseName == NULL)
				fprintf(sequenceOut,
						"#Fails\tFlipAvg\tFlipMed\tFlipOpt\tFlipExp\tFlipSum\tTryAvg\tTrySum\tRewtAvg\tUnAvg\tMobAvg\tFlipMin\tFlipMax\tFlip%%5\tFlip%%25\tFlip%%50\tFlip%%75\tFlip%%95\tOpt%%\tTimeSum \tTimeAvg \tProblem\n");

			fprintf(sequenceOut, "%d\t%g\t%d\t%d\t%g\t%d\t%g\t%d\t%d\t%g\t%g\t%d\t%d", 
					failRepeatsSum, (double)flipRepeatsSum/numRepeats, flipRepeatsMed, 
					optimalFlips, minExpectedFlips, flipRepeatsSum,
					(double)restRepeatsSum/numRepeats, restRepeatsSum,
					reweightRepeatsSum/numRepeats,
					unsatRepeatsSum/numRepeats, 
					mobilityRepeatsSum/numRepeats, 
					flipRepeatsMin, flipRepeatsMax);
		}

		for (perc = 0; perc < numPercentiles; perc++)
		{
			percPoint= ((numRepeats-1) * percentiles[perc] / 100.0);

			flipPercentiles[perc] = flipRepeats[(int)ceil(percPoint)];

			if (showSequenceOutput)
				fprintf(sequenceOut, "\t%g", flipPercentiles[perc]);
		}

		if (showSequenceOutput)
		{
			fprintf(sequenceOut, "\t%g\t%g\t%g\t%s\n", optimalPercentile, timeRepeatsSum, timeRepeatsSum / numRepeats, shortName);

			if (flushOutput)
				fflush(sequenceOut);
		}

		flipOverallSum += flipRepeatsSum;
		restOverallSum += restRepeatsSum;
		reweightOverallSum += reweightRepeatsSum;
		timeOverallSum += timeRepeatsSum;
		failOverallSum += failRepeatsSum;
		unsatOverallSum += unsatRepeatsSum;
		mobilityOverallSum += mobilityRepeatsSum;

		if (results->mobilityWindow != NULL)
		{
			free(results->mobilityWindow);
			results->mobilityWindow = NULL;
		}
	}

	if (showSequenceOutput)
	{
		if (outputBaseName != NULL)
			fclose(sequenceOut);
	}

	/* Open overall output file. */

	if (showOverallOutput)
	{
		if (outputBaseName == NULL)
		{
			overallOut = stdout;
		}
		else
		{
			strcpy(outputName2, outputName);
			strcat(outputName2, "all");

			overallOut = fopen(outputName2, "w");
			if (overallOut == NULL)
			{
				fprintf(stderr, "Error opening overall output file: %s\n", outputName2);
				showUsage(params);
				exit(EXIT_FAILURE);
			}
		}

		fprintf(overallOut,
				"#FlpAvg\tFlipSum\tFlpOpt\tFlipExp\tTryAvg\tTrySum\tFailAvg\tFailSum\tRewtAvg\tUnAvg\tMobAvg\tTimeSum\tTimeAvg\tTimeExp\tFlipTim\n");
		fprintf(overallOut,
				"%g\t%g\t%g\t%g\t%g\t%g\t%g\t%g\t%g\t%g\t%g\t%g\t%g\t%g\t%g\n", 
				flipOverallSum / (numRepeats * numFileNames * 1.0), 
				flipOverallSum,
				optimalFlipsOverallSum / numFileNames,
				expectedFlipsOverallSum / numFileNames,
				restOverallSum / ((double)numRepeats * numFileNames), 
				restOverallSum,
				failOverallSum / ((double)numRepeats * numFileNames), 
				failOverallSum,
				reweightOverallSum / ((double)numRepeats * numFileNames), 
				unsatOverallSum / ((double)numRepeats * numFileNames), 
				mobilityOverallSum / ((double)numRepeats * numFileNames), 
				timeOverallSum, timeOverallSum / (numRepeats * numFileNames),
				timeOverallSum / flipOverallSum * expectedFlipsOverallSum / numFileNames,
				timeOverallSum / flipOverallSum);

		if (outputBaseName != NULL)
			fclose(overallOut);
	}


	if (logUnsats && outputBaseName != NULL)
	{
		int flip;
		strcpy(outputName2, outputName);
		strcat(outputName2, "depth");

		unsatOut = fopen(outputName2, "w");
		if (unsatOut == NULL)
		{
			fprintf(stderr, "Error opening overall output file: %s\n", outputName2);
			showUsage(params);
			exit(EXIT_FAILURE);
		}

		fprintf(unsatOut, "#UnSum\tUnAvg\n");
		flip = 0;
		while (flip < results->unsatBufferLength && results->unsatFlipCounts[flip] > 0)
		{
			fprintf(unsatOut, "%d\t%g\n", results->unsatFlipCounts[flip],
					(double)results->unsatFlipCounts[flip] / (numFileNames * numRepeats));
			flip++;
		}

		fclose(unsatOut);
	}

	freeParams(params);
	freeResults(results);

	free(flipRepeats);
	free(flipPercentiles);

	if (!readFromFiles)
		free(fileNames);

	return 0;
}

void showUsage(SATParams *params)
{
	int par;
	fprintf(stderr, "Usage: command [options] [-f <file list> ]\n");
	fprintf(stderr, "Universal options:\n");
	fprintf(stderr, "%-2s name   -   %s\n", "-o", "output to dir/files with specified name");
	fprintf(stderr, "%-6s #  -   %s\n", "-rep", "number of times to repeat each problem");
	fprintf(stderr, "%-6s #  -   %s\n", "-cm", "compute solution 'mobility'");
	fprintf(stderr, "%-6s #  -   %s\n", "-ml", "max literals per clause");
	fprintf(stderr, "%-6s    -   %s\n", "-xm", "use exact(minimal) memory allocation (slower)");
	fprintf(stderr, "%-6s    -   %s\n", "-cop", "problems are in COP format");
	fprintf(stderr, "%-6s    -   %s\n", "-nr", "use a fixed seed for the PRNG");
	fprintf(stderr, "%-6s    -   %s\n", "-npo", "do show problem output");
	fprintf(stderr, "%-6s    -   %s\n", "-nso", "do show sequence output");
	fprintf(stderr, "%-6s    -   %s\n", "-noo", "do show overall output");
	fprintf(stderr, "%-6s    -   %s\n", "-nd", "do not output to a new directory");
	fprintf(stderr, "%-6s    -   %s\n", "-nf", "do not flush output immediately");
	fprintf(stderr, "%-6s    -   %s\n", "-ne", "do not compute expectations");
	fprintf(stderr, "%-6s    -   %s\n", "-ls", "log all solutions found");
	fprintf(stderr, "%-6s    -   %s\n", "-lu", "log unsat clause counts per flip");
	fprintf(stderr, "%-6s #  -   %s\n", "-us", "skip # flips before starting to count unsat clauses");
	fprintf(stderr, "%-6s # #-   %s\n", "-la", "log assignments every flip up to max flips & restarts");
	fprintf(stderr, "%-6s    -   %s\n", "-V", "show version information");
	fprintf(stderr, "%-6s    -   %s\n", "-?", "show this help message");
	fprintf(stderr, "%-6s    -   %s\n", "-help", "show this help message");
	fprintf(stderr, "Solver specific options:\n");
	for (par = 0; par < params->numIntParams; par++)
		fprintf(stderr, "%-6s #  -   %s\n", params->intParamNames[par], params->intParamDescs[par]);
	for (par = 0; par < params->numDoubleParams; par++)
		fprintf(stderr, "%-6s #  -   %s\n", params->doubleParamNames[par], params->doubleParamDescs[par]);
	for (par = 0; par < params->numStringParams; par++)
		fprintf(stderr, "%-2s <str> -   %s\n", params->stringParamNames[par], params->stringParamDescs[par]);
}

void freeParams(SATParams *params)
{
	int par;

	if (params->numIntParams > 0)
	{
		free(params->intParamNames);
		free(params->intParamDescs);
		free(params->intParams);
	}

	if (params->numDoubleParams > 0)
	{
		free(params->doubleParamNames);
		free(params->doubleParamDescs);
		free(params->doubleParams);
	}

	if (params->numStringParams > 0)
	{
		free(params->stringParamNames);
		free(params->stringParamDescs);
		for (par = 0; par < params->numStringParams; par++)
			if (params->stringParams[par] != NULL)
				free(params->stringParams[par]);
		free(params->stringParams);
	}

	free(params);
}

void freeResults(SATResults *results)
{
	if (results->unsatFlipCounts != NULL)
		free(results->unsatFlipCounts);
	free(results);
}

int compareInt(const void *a, const void *b)
{
	if (*((int*)a) == (*(int*)b))
		return 0;
	if (*((int*)a) > (*(int*)b))
		return 1;
	return -1;
} 

void showVersion(FILE *outFile)
{
	fprintf(outFile, "Package Version: %s %s\n", FALESAT_VERSION_NAME, FALESAT_VERSION_NUMBER);
	fprintf(outFile, "Solver Version: %s\n", getSolverIdentity());
	fprintf(outFile, "Compile time options:\n");
	if (USE_UNSAT_TRACKING)
		fprintf(outFile, "\tUnsat tracking enabled.\n");
	else
		fprintf(outFile, "\tUnsat tracking disabled.\n");
	if (USE_MOBILITY_TRACKING)
		fprintf(outFile, "\tMobility tracking enabled.\n");
	else
		fprintf(outFile, "\tMobility tracking disabled.\n");
	if (USE_ASSIGNMENT_TRACKING)
		fprintf(outFile, "\tAssignment tracking enabled.\n");
	else
		fprintf(outFile, "\tAssignment tracking disabled.\n");
}