/* 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 "satfront.h"
#include "readcnf.h"
#include "mbflip.h"

#define SBP_PARAM_INDEX 0
#define HOOS_PARAM_INDEX 1

int *lastime;
int steps, r;

/************************ WSAT - NOVELTY **********************/

void preSolve(SATParams *params)
{
	make = malloc(n * sizeof(int));
	brake = malloc(n * sizeof(int));                             
	sat = malloc(m * sizeof(int));
	yfalse = malloc(m * sizeof(int));
	wherefalse = malloc(m * sizeof(int));
	lastime = malloc(n * sizeof(int));
}


void runSolver(SATParams *params, SATResults *results)
{
	int t, x, y, i, j, xflip = -1, temp;
	int R;
	int T;
	int x2, diff2, diff, maxdiff, recent;
	double secondBestProb;
	int secondBestProbInt;
#ifdef NOVELTY_PLUS
	double hoosProb;
	int hoosProbInt;
#endif

#include "mobility1.c"

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

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

#ifdef NOVELTY_PLUS
	hoosProb = params->doubleParams[HOOS_PARAM_INDEX];
	if (hoosProb == 0)
		hoosProbInt = -1;
	else
		hoosProbInt = (int)RAND_MAX * hoosProb;
#endif

	secondBestProb = params->doubleParams[SBP_PARAM_INDEX];
	if (secondBestProb == 0)
		secondBestProbInt = -1;
	else
		secondBestProbInt = (int)RAND_MAX * secondBestProb;

	steps = 0;

	for (r = 0; r < R; r++) {  /***************************/

		for (x = 0; x < n; x++) {
			X[x] = (rand() > HALF_RAND_MAX) * 2 - 1;  
			lastime[x] = -1;
		}

		steps++;
		numvio = 0;
		for (y = 0; y < m; y++) {
			sat[y] = 0;
			for (i=0; i<nXs[y]; i++) 
				sat[y] += X[Xs[y][i]] == Xsgns[y][i];
			if (sat[y] <= 0) {
				yfalse[numvio] = y;
				wherefalse[y] = numvio;
				numvio++;
			}
		}
		for (x = 0; x < n; x++) {
			make[x] = brake[x] = 0;
			for (j = 0; j < nYs[x]; j++)
				if (sat[Ys[x][j]] == 0)
					make[x]++;
				else if (sat[Ys[x][j]] == 1 && X[x] == Ysgns[x][j])
					brake[x]++;
		}

		if (numvio == 0)
			goto finished;

		for (t = 0; t < T; t++) { /***************************/

#include "unsat1.c"
#include "mobility2.c"
#include "assigndump.c"

			y = yfalse[rand()%numvio];

#ifdef NOVELTY_PLUS
			/* Hoos fix for novelty. */
			if (rand() < hoosProbInt) {
				xflip = Xs[y][rand() / (RAND_MAX / nXs[y] + 1)];
			} else {
#else
			{
#endif
				maxdiff = diff2 = -m;
				xflip = x2 = 0;
				recent = -1;
				for (i = 0; i < nXs[y]; i++) {
					x = Xs[y][i];
					if (lastime[x] > recent) 
						recent = lastime[x];
					diff = make[x] - brake[x];
					if (diff > maxdiff ||
							(diff == maxdiff && lastime[x] < lastime[xflip])) {
						diff2 = maxdiff;
						maxdiff = diff;
						x2 = xflip;
						xflip = x;
					} else if (diff > diff2 ||
							(diff == diff2 && lastime[x] < lastime[x2])) {
						diff2 = diff;
						x2 = x;
					}
				}
				if (lastime[xflip] == recent && rand() < secondBestProbInt) 
					xflip = x2;
			}
			lastime[xflip] = t;
			X[xflip] = -X[xflip];
			steps++;

				/* The included code performs the make/break update. */
			#include "mbflipimpl.c"

			if (numvio == 0)
				goto finished;		/* Found solution so jump to label. */

		}                           /***************************/
	}                             /***************************/

	/* We only reach this point if we exited the above loop without finding a
	* solution. **/
	r--;

	/* We jump to this label when we find a solution. */
finished:

	results->numFlips = steps;
	results->numRestarts = r + 1;
	results->numSatisfied = m - numvio;
	results->isSatisfied = numvio == 0;
	#include "copysoln.c"

#include "mobility3.c"
}

void postSolve(SATParams *params)
{
	free(make);
	free(brake);
	free(yfalse);
	free(wherefalse);
	free(lastime);
	free(sat);
}

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;

#ifdef NOVELTY_PLUS
	params->numDoubleParams = 2;
#else
	params->numDoubleParams = 1;
#endif

	params->doubleParams = malloc(params->numDoubleParams * sizeof(double));
	params->doubleParamNames = malloc(params->numDoubleParams * sizeof(char*));
	params->doubleParamDescs = malloc(params->numDoubleParams * sizeof(char*));

	params->doubleParamNames[SBP_PARAM_INDEX] = "-sbp";
	params->doubleParamDescs[SBP_PARAM_INDEX] = "Prob. of picking second best (*0.5)";
	params->doubleParams[SBP_PARAM_INDEX] = 0.5;

#ifdef NOVELTY_PLUS
	params->doubleParamNames[HOOS_PARAM_INDEX] = "-hoos";
	params->doubleParamDescs[HOOS_PARAM_INDEX] = "Hoos fix prob for novelty (*0.01)";
	params->doubleParams[HOOS_PARAM_INDEX] = 0.01;
#endif


	params->numStringParams = 0;

	return params;
}

char *getSolverIdentity()
{
	return "$RCSfile: novel.c,v $ $Revision: 1.35 $ $Date: 2001/11/23 06:46:20 $";
}