#ifndef SATFRONT_HEADER_INCLUDED

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

#define FALESAT_VERSION_NAME "ESG-SAT"
#define FALESAT_VERSION_NUMBER "1.4.0"

	/* Set this value to 1 to enable the unsatisfied clause tracking. */
#define USE_UNSAT_TRACKING 0
	/* Set this value to 1 to enable mobility tracking. */
#define USE_MOBILITY_TRACKING 0
	/* Set this value to 1 to enable the "-la" flag for logging assignments. */
#define USE_ASSIGNMENT_TRACKING 0
	/* Set this value to 1 to enable the "-ls" flag for logging solutions. */
#define USE_SOLNS_TRACKING 0
	/* Set this value to 1 to output solutions by literal instead implicit order. */
	/* E.g. When 0, a solution looks like: -1 1 1 -1 -1 1
	 *      When 1, a solution looks like: -1 2 3 -4 -5 6
	 * The latter format is used by some software packages. */
#define USE_ORDERED_SOLN_FORMAT 0

	/* Set this value to 1 to enable a double-check for correct solutions. */
#define CHECK_SOLUTIONS 0

	/* Used in several solvers for 50/50 chance decisions. */
#define HALF_RAND_MAX (RAND_MAX / 2)

	/* Some flags used internally to differentiate file types. */
#define FILE_FORMAT_CNF 0
#define FILE_FORMAT_COP 1

typedef struct
	{
	char *problemFilename;			/* The filename of the problem. */
	char *shortFilename;				/* the filename of the problem without path. */
	int numIntParams;						/* Number of int valued params. */
	char **intParamNames;				/* Names of int valued params. */
	char **intParamDescs;				/* Descriptions of int-valued params. */
	int *intParams;							/* Values of int-valued params. */
	int numDoubleParams;				/* Number of double valued params. */
	char **doubleParamNames;		/* Names of double-valued params. */
	char **doubleParamDescs;		/* Descriptions of double-valued params. */
	double *doubleParams;				/* Values of double-valued params. */
	int numStringParams;				/* Number of string valued params. */
	char **stringParamNames;		/* Names of string-valued params. */
	char **stringParamDescs;		/* Descriptions of string-valued params. */
	char **stringParams;				/* Strings of double-valued params. */
	} SATParams; 

typedef struct
	{
	int numVars;								/* Number of variables. */
	int numClauses;							/* Number of clauses. */
	int numFlips;								/* Number of flips before termination. */
	int numReweights;						/* Number of weight adjustments before termination. */
	int numRestarts;						/* Number of restarts before termination. */
	int isSatisfied;						/* Flag for problem satisfied at termination. */
	int numSatisfied;						/* Number of satisfied clauses at termination. */
	int unsatSum;								/* Sum of unsat clauses over run. */
	int unsatBufferLength;			/* Number of unsat observations tracked. */
	int *unsatFlipCounts;				/* Unsat observations. */
	int unsatFlipSkip;					/* Flips to skip before starting to track unsats. */
	int *mobilityWindow;				/* Array of mob assignments. */
	int currentWindowLength;		/* Number of mob assignments tracked so far. */
	int windowStart;						/* Position in mob window that is the start. */
	int mobilityWindowLength;		/* Mobility autocorrelation length. */
	int sumMobility;						/* Current mobility sum for run. */
	double avgMobility;					/* Average mobility of the run. */
	FILE *assignOut;						/* File for storing assignments. */
	int firstAssign;						/* Flag for first assignment of run. */
	int firstRepeat;						/* Flag for first repeat of run. */
	int maxAssigns;							/* Maximum number of assigns to store. */
	int assignCount;						/* Number of assigns stored. */
	int maxAssignRepeats;				/* Maximum number of repeats to track assignments. */
	int repeatCount;						/* Number of repeats passed. */
	int copySolution;						/* Flag for whether solutions should be copied. */
	int *solution;							/* An array to store the solution (if any). */
	} SATResults;


int main(int argc, char *argv[]);
void showUsage(SATParams *params);
void freeParams(SATParams *params);
void freeResults(SATResults *results);
int compareInt(const void *a, const void *b);
void showVersion(FILE *outFile);

	/* These functions must be implemented by the backend. */
SATParams *getSATParams();
void preSolve(SATParams *params);
void runSolver(SATParams *params, SATResults *results);
void postSolve(SATParams *params);
char *getSolverIdentity();

#define SATFRONT_HEADER_INCLUDED
#endif