/* Copyright (C) 2000  Dale Schuurmans, Finnegan Southey                     */
/* This work is licensed under the Gnu General Public License (see gpl.txt). */

#include <stdlib.h>
#include <stdio.h>
#include <string.h>
#include "readcnf.h"
#include "satfront.h"

	/* Prototypes for function from DLMSAT. */
int ReadFile(char * fileName);
void Init();
void InitLink();
void ReadPara(char *fileName);
int Search(int argc, char *argv[]);
void freeStuff();

	/* Global variables for DLMSAT. */
SATResults *globResults;

	/* Global variables from DLMSAT. */
extern int clauseNum;						/* Number of clauses. */
extern u_int TH_ROUND;					/* Max restarts. */
extern u_int TH_FLIP_TIMES;			/* Max flips per restart. */
extern u_int totalFlipTime;			/* Flips executed in last round. */
extern int roundNum;						/* Number of rounds executed. */
extern int falseClauseNum;			/* Number of false clauses. */
extern char* paraFileName;			/* Parameter file name. */
extern int varNum;							/* Number of variables. */
extern int *x;									/* Variable assignments. */


	/* DLM has its own problem file reader so the readcnf.h functions are
	 * included here as bridges. */
int readProblem(FILE *in, int maxLiterals, int maxClauses, int exactAlloc, int fileFormat, SATResults *results)
{
	results->numClauses = clauseNum;
	results->numVars = varNum;
	return 1;
}

void preSolve(SATParams *params)
{
	if (strcmp(params->problemFilename, "stdin") == 0)
	{
		printf("Error: This solver cannot read from standard input.  Specify a filename using the -f option instead.\n");
		exit(1);
	}

	ReadFile(params->problemFilename);

	Init();

	InitLink();

	paraFileName = params->stringParams[0];
	if (paraFileName == NULL)
		paraFileName = "dlmparam";

	ReadPara(paraFileName);

	TH_FLIP_TIMES = params->intParams[0];
	if (TH_FLIP_TIMES == 0)
		TH_FLIP_TIMES = 100000;


	TH_ROUND = params->intParams[1];
	if (TH_ROUND > 0)
		TH_ROUND--;

}

/************************ DLM Bridge **********************/

void runSolver(SATParams *params, SATResults *inResults)
{
	int satisfied;
	char **fakeArgs;
	SATResults *results;

	results = inResults;
	globResults = inResults;

	#include "dlmparams/mobility1-dlm.c"

	fakeArgs = malloc(sizeof(char*) * 4);
	fakeArgs[1] = params->problemFilename;
	fakeArgs[3] = params->stringParams[1];
	if (fakeArgs[3] == NULL)
		fakeArgs[3] = "dlmout";

	satisfied = Search(4, fakeArgs);

	free(fakeArgs);

	if (satisfied)
		roundNum++;

	results->numFlips = (roundNum-1) * TH_FLIP_TIMES + totalFlipTime;
	results->numReweights = 0;
	results->numRestarts = roundNum;
	results->numSatisfied = clauseNum - falseClauseNum;
	results->isSatisfied = satisfied;

	#include "dlmparams/mobility3-dlm.c"
}

void postSolve(SATParams *params)
{
	freeStuff();
}

SATParams *getSATParams()
	{
	SATParams *params;

	params = malloc(sizeof(SATParams));
	params->numIntParams = 2;
	params->intParams = malloc(params->numIntParams * sizeof(int));
	params->intParamNames = malloc(params->numIntParams * sizeof(char*));
	params->intParamDescs = malloc(params->numIntParams * sizeof(char*));
	params->intParamNames[0] = "-mf";
	params->intParamDescs[0] = "max flips before restarting";
	params->intParams[0] = 0;
	params->intParamNames[1] = "-mr";
	params->intParamDescs[1] = "max restarts before aborting";
	params->intParams[1] = 0;
	
	params->numDoubleParams = 0;

	params->numStringParams = 2;
	params->stringParams = malloc(params->numStringParams * sizeof(char*));
	params->stringParamNames = malloc(params->numStringParams * sizeof(char*));
	params->stringParamDescs = malloc(params->numStringParams * sizeof(char*));
	params->stringParamNames[0] = "-pf";
	params->stringParamDescs[0] = "parameter filename";
	params->stringParams[0] = NULL;
	params->stringParamNames[1] = "-of";
	params->stringParamDescs[1] = "output filename";
	params->stringParams[1] = NULL;

	return params;
	}

char *getSolverIdentity()
	{
	return "$RCSfile: dlm2k.c,v $ $Revision: 1.19 $ $Date: 2001/11/14 05:49:12 $";
	}