/* Heuristically solve a Constrained Optimization Problem (COP) */

#include <stdlib.h>
#include <stdio.h>
#include <float.h>
#include <limits.h>
#include "satfront.h"
#include "cop.h"

	/* See cop.h for descriptions of these variables. */
int n, m, N, M;
int *X, *nCs, **Cs, **Ccoefs;
int *B, *nXs, **Xs, **Xcoefs;
int MaxCoef, MaxB, MinB;
int steps, dsteps, r;

int compare();
int readCOPExactly(FILE *in);
int readCOPQuickly(FILE *in, int maxLiterals, int maxClauses);
int readCNFExactly(FILE *in);
int readCNFQuickly(FILE *in, int maxLiterals, int maxClauses);
void checkAlloc(void *ptr, char *msg);

#define CONFIRM_ALLOCATIONS 0

/*********************************************************/
int readProblem(FILE *in, int maxLiterals, int maxClauses, int exactAlloc, int fileFormat, SATResults *results)
{
	int retVal;

	if (fileFormat == FILE_FORMAT_COP)
		if (exactAlloc)
			retVal =  readCOPExactly(in);
		else
			retVal =  readCOPQuickly(in, maxLiterals, maxClauses);
	else
		if (exactAlloc)
			retVal =  readCNFExactly(in);
		else
			retVal =  readCNFQuickly(in, maxLiterals, maxClauses);

	results->numClauses = m;
	results->numVars = n;

	return retVal;
}

int readCOPQuickly(FILE *in, int maxLiterals, int maxClauses)
{
	int x, j, c, var, coef;

	while (getc(in) != '(');
	fscanf(in, "%d %d", &n, &m);
	while (getc(in) != ')');

	while (getc(in) != '(');
	fscanf(in, "%d %d", &N, &M);
	while (getc(in) != ')');

	if (maxLiterals == 0)
		maxLiterals = CNF_MAX_LITERALS;

	if (maxClauses == 0)
		maxClauses = CNF_MAX_CLAUSES;

	if (!N) 
		N = (n < maxLiterals) ? n : maxLiterals;
	if (!M) 
		M = (m < maxClauses) ? m : maxClauses;

	/***** allocate COP *****/
	X = (int *) malloc(n * sizeof(int));
	checkAlloc(X, "Failed to allocate X.");
	nCs = (int *) calloc(n, sizeof(int));
	checkAlloc(nCs, "Failed to allocate nCs.");
	Cs = (int **) malloc(n * sizeof(int *));
	checkAlloc(Cs, "Failed to allocate Cs.");
	Ccoefs = (int **) malloc(n * sizeof(int *));
	checkAlloc(Ccoefs, "Failed to allocate Ccoefs.");
	for (x = 0; x < n; x++) 
	{
		Cs[x] = (int *) malloc(M * sizeof(int));
		checkAlloc(Cs[x], "Failed to allocate Cs[x].");
		Ccoefs[x] = (int *) malloc(M * sizeof(int));
		checkAlloc(Ccoefs[x], "Failed to allocate Ccoefs[x].");
	}

	B = (int *) malloc(m * sizeof(int));
	checkAlloc(B, "Failed to allocate B.");
	nXs = (int *) calloc(m, sizeof(int));
	checkAlloc(nXs, "Failed to allocate nXs.");
	Xs = (int **) malloc(m * sizeof(int *));
	checkAlloc(Xs, "Failed to allocate Xs.");
	Xcoefs = (int **) malloc(m * sizeof(int *));
	checkAlloc(Xcoefs, "Failed to allocate Xcoefs.");
	for (c = 0; c < m; c++) 
	{
		Xs[c] = (int *) malloc(N * sizeof(int));
		checkAlloc(Xs[c], "Failed to allocate Xs[c].");
		Xcoefs[c] = (int *) malloc(N * sizeof(int));
		checkAlloc(Xcoefs[c], "Failed to allocate Xcoefs[c].");
	}

	/***** read COP *****/
		/* Read values for objective function (A). */
		/* Since this is a zero vector for SAT, we simply throw it away. */
	while (getc(in) != '(');
	while (getc(in) != ')');

	MaxCoef = 0;
	MaxB = INT_MIN;		/* Was default 0, this should be more general. */
	MinB = INT_MAX;		/* Was default N, this should be more general. */

		/* Read in constraints. */
	for (c = 0; c < m; c++) {
		while (getc(in) != '(');
			/* Read bounding value for constraint (Cij.Xi <= Bj)
			 * and the number of variables that appear in the constraint. */
		fscanf(in, "%d %d", B+c, nXs+c);
		if (nXs[c] > N) {
			printf("Error: #vars exceeds max vars=%d\n", N);
			exit(EXIT_FAILURE);
		}
			/* Keep track of max and min bounding values. */
		if (B[c] > MaxB) 
			MaxB = B[c];
		else if (B[c] < MinB) 
			MinB = B[c];

			/* For each var in the current constraint... */
		for (j = 0; j < nXs[c]; j++) {
			while (getc(in) != '(');
				/* Read the variable and coefficient (i and Cij). */
			fscanf(in, "%d %d", &var, &coef);
			if (var >= n || var < 0) {
				printf("Error: illegal variable number=%d out of range\n", var);
				exit(EXIT_FAILURE);
			}
				
				/* Track highest magnitude coefficient. */
			if (abs(coef) > MaxCoef) 
				MaxCoef = abs(coef);

				/* Store the index of the j-th variable appearing in constraint c. */
			Xs[c][j] = var;
				/* Store the coefficient of the j-th var appearing in constraint c. */
			Xcoefs[c][j] = coef;
				/* Store the index of the nCs[var]-th constraint in which var appears. */
			Cs[var][nCs[var]] = c;
				/* Store the coefficient of the nCs[var]-th constraint in which var appears. */
			Ccoefs[var][nCs[var]] = coef;
				/* Increment the counter for the number of constraints in which var appears. */
			nCs[var]++;
			if (nCs[var] > M) {
				printf("Error: #constraints exceeds max constraints=%d\n", M);
				exit(EXIT_FAILURE);
			}
			while (getc(in) != ')');
		}
		while (getc(in) != ')');
	}

	return 1;
}

int readCOPExactly(FILE *in)
{
	int j, c, var, coef;

	while (getc(in) != '(');
	fscanf(in, "%d %d", &n, &m);
	while (getc(in) != ')');

	while (getc(in) != '(');
	fscanf(in, "%d %d", &N, &M);
	while (getc(in) != ')');
	
	/***** allocate COP *****/
	X = (int *) malloc(n * sizeof(int));
	checkAlloc(X, "Failed to allocate X.");
	nCs = (int *) calloc(n, sizeof(int));
	checkAlloc(nCs, "Failed to allocate nCs.");
	Cs = (int **) calloc(n, sizeof(int *));
	checkAlloc(Cs, "Failed to allocate Cs.");
	Ccoefs = (int **) calloc(n, sizeof(int *));
	checkAlloc(Ccoefs, "Failed to allocate Ccoefs.");

	B = (int *) malloc(m * sizeof(int));
	checkAlloc(B, "Failed to allocate B.");
	nXs = (int *) calloc(m, sizeof(int));
	checkAlloc(nXs, "Failed to allocate nXs.");
	Xs = (int **) calloc(m, sizeof(int *));
	checkAlloc(Xs, "Failed to allocate Xs.");
	Xcoefs = (int **) calloc(m, sizeof(int *));

	/***** read COP *****/
		/* Read values for objective function (A). */
		/* Since this is a zero vector for SAT, we simply throw it away. */
	while (getc(in) != '(');
	while (getc(in) != ')');

	MaxCoef = 0;
	MaxB = INT_MIN;		/* Was default 0, this should be more general. */
	MinB = INT_MAX;		/* Was default N, this should be more general. */

		/* Read in constraints. */
	for (c = 0; c < m; c++) {
		while (getc(in) != '(');
			/* Read bounding value for constraint (Cij.Xi <= Bj)
			 * and the number of variables that appear in the constraint. */
		fscanf(in, "%d %d", B+c, nXs+c);
			/* Keep track of max and min bounding values. */
		if (B[c] > MaxB) 
			MaxB = B[c];
		else if (B[c] < MinB) 
			MinB = B[c];

			/* Allocate memory for the current constraint. */
		Xs[c] = (int *) malloc(nXs[c] * sizeof(int));
		checkAlloc(Xs[c], "Failed to allocate Xs[c].");
		Xcoefs[c] = (int *) malloc(nXs[c] * sizeof(int));
		checkAlloc(Xcoefs[c], "Failed to allocate Xcoefs[c].");

			/* For each var in the current constraint... */
		for (j = 0; j < nXs[c]; j++) {
			while (getc(in) != '(');
				/* Read the variable and coefficient (i and Cij). */
			fscanf(in, "%d %d", &var, &coef);
			if (var >= n || var < 0) {
				printf("Error: illegal variable number=%d out of range\n", var);
				exit(EXIT_FAILURE);
			}
				
				/* Track highest magnitude coefficient. */
			if (abs(coef) > MaxCoef) 
				MaxCoef = abs(coef);

				/* Store the index of the j-th variable appearing in constraint c. */
			Xs[c][j] = var;
				/* Store the coefficient of the j-th var appearing in constraint c. */
			Xcoefs[c][j] = coef;

				/* Reallocate space for Cs[var] and Ccoefs[var]. */
			Cs[var] = (int *) realloc(Cs[var], (nCs[var]+1) * sizeof(int));
			checkAlloc(Cs[var], "Failed to allocate Cs[var].");
			Ccoefs[var] = (int *) realloc(Ccoefs[var], (nCs[var]+1) * sizeof(int));
			checkAlloc(Ccoefs[var], "Failed to allocate Ccoefs[var].");
			
				/* Store the index of the nCs[var]-th constraint in which var appears. */
			Cs[var][nCs[var]] = c;
				/* Store the coefficient of the nCs[var]-th constraint in which var appears. */
			Ccoefs[var][nCs[var]] = coef;

				/* Increment the counter for the number of constraints in which var appears. */
			nCs[var]++;
			while (getc(in) != ')');
		}
		while (getc(in) != ')');
	}

	return 1;
}


/*********************************************************/
int readCNFExactly(FILE *in)
{
	int x, y, lit, s;
	char ch;

	ch = fgetc(in);
	while (ch == 'c' || ch == '#')
	{
		while (fgetc(in) != '\n');
		ch = fgetc(in);
	}

	fscanf(in, " cnf %d %d", &n, &m);

		/***** allocate COP *****/
	X = (int *) malloc(n * sizeof(int));
	checkAlloc(X, "Failed to allocate X.");
	nCs = (int *) calloc(n, sizeof(int));
	checkAlloc(nCs, "Failed to allocate nCs.");
	Cs = (int **) calloc(n, sizeof(int *));
	checkAlloc(Cs, "Failed to allocate Cs.");
	Ccoefs = (int **) calloc(n, sizeof(int *));
	checkAlloc(Ccoefs, "Failed to allocate Ccoefs.");

	B = (int *) malloc(m * sizeof(int));
	checkAlloc(B, "Failed to allocate B.");
	nXs = (int *) calloc(m, sizeof(int));
	checkAlloc(nXs, "Failed to allocate nXs.");
	Xs = (int **) calloc(m, sizeof(int *));
	checkAlloc(Xs, "Failed to allocate Xs.");
	Xcoefs = (int **) calloc(m, sizeof(int *));
	checkAlloc(Xcoefs, "Failed to allocate Xcoefs.");


	/***** read cnf *****/
	for (y = 0; y < m; y++) {
		for (fscanf(in, "%d", &lit); lit; fscanf(in, "%d", &lit)) {
			if (lit < 0) {
				x = -lit - 1;
				s = 1;
			}
			else {
				x = lit - 1;
				s = -1;
			}

			Xs[y] = (int *) realloc(Xs[y], (nXs[y]+1) * sizeof(int));
			checkAlloc(Xs[y], "Failed to allocate Xs[y].");
			Xcoefs[y] = (int *) realloc(Xcoefs[y], (nXs[y]+1) * sizeof(int));
			checkAlloc(Xcoefs[y], "Failed to allocate Xcoefs[y].");
			Xs[y][nXs[y]] = x;
			Xcoefs[y][nXs[y]] = s;
			nXs[y]++;

			Cs[x] = (int *) realloc(Cs[x], (nCs[x]+1) * sizeof(int));
			checkAlloc(Cs[x], "Failed to allocate Cs[x].");
			Ccoefs[x] = (int *) realloc(Ccoefs[x], (nCs[x]+1) * sizeof(int));
			checkAlloc(Ccoefs[x], "Failed to allocate Ccoefs[x].");
			Cs[x][nCs[x]] = y;
			Ccoefs[x][nCs[x]] = s;
			nCs[x]++;
		}
		B[y] = nXs[y]-2;
	}

	return 1;
}

/*********************************************************/
int readCNFQuickly(FILE *in, int maxLiterals, int maxClauses)
{
	int x, y, lit, s;
	char ch;

	ch = fgetc(in);
	while (ch == 'c' || ch == '#')
	{
		while (fgetc(in) != '\n');
		ch = fgetc(in);
	}

	fscanf(in, " cnf %d %d", &n, &m);

	if (maxLiterals == 0)
		maxLiterals = CNF_MAX_LITERALS;

	if (maxClauses == 0)
		maxClauses = CNF_MAX_CLAUSES;

	N = (n < maxLiterals) ? n : maxLiterals;
	M = (m < maxClauses) ? m : maxClauses;

		/***** allocate COP *****/
	X = (int *) malloc(n * sizeof(int));
	checkAlloc(X, "Failed to allocate X.");
	nCs = (int *) calloc(n, sizeof(int));
	checkAlloc(nCs, "Failed to allocate nCs.");
	Cs = (int **) malloc(n * sizeof(int *));
	checkAlloc(Cs, "Failed to allocate Cs.");
	Ccoefs = (int **) malloc(n * sizeof(int *));
	checkAlloc(Ccoefs, "Failed to allocate Ccoefs.");
	for (x = 0; x < n; x++) 
	{
		Cs[x] = (int *) malloc(M * sizeof(int));
		checkAlloc(Cs[x], "Failed to allocate Cs[x].");
		Ccoefs[x] = (int *) malloc(M * sizeof(int));
		checkAlloc(Ccoefs[x], "Failed to allocate Ccoefs[x].");
	}

	nXs = (int *) calloc(m, sizeof(int));
	checkAlloc(nXs, "Failed to allocate nXs.");
	Xs = (int **) malloc(m * sizeof(int *));
	checkAlloc(Xs, "Failed to allocate Xs.");
	Xcoefs = (int **) malloc(m * sizeof(int *));
	checkAlloc(Xcoefs, "Failed to allocate Xcoefs.");
	for (y = 0; y < m; y++) {
		Xs[y] = (int *) malloc(N * sizeof(int));
		checkAlloc(Xs[y], "Failed to allocate Xs[y].");
		Xcoefs[y] = (int *) malloc(N * sizeof(int));
		checkAlloc(Xcoefs[y], "Failed to allocate Xcoefs[y].");
	}
	B = (int *) malloc(m * sizeof(int));
	checkAlloc(B, "Failed to allocate B.");


	/***** read cnf *****/
	for (y = 0; y < m; y++) {
		for (fscanf(in, "%d", &lit); lit; fscanf(in, "%d", &lit)) {
			if (lit < 0) {
				x = -lit - 1;
				s = 1;
			}
			else {
				x = lit - 1;
				s = -1;
			}
			if (nXs[y] == N) {
				printf("Error: Maximum number of literals per constraint exceeded: %d\n", nXs[y]);
				exit(EXIT_FAILURE);
			}

			Xs[y][nXs[y]] = x;
			Xcoefs[y][nXs[y]] = s;
			nXs[y]++;

			if (nCs[x] == M) {
				printf("Error: Maximum number of constraints per variable exceeded: %d\n", nCs[x]);
				exit(EXIT_FAILURE);
			}
			Cs[x][nCs[x]] = y;
			Ccoefs[x][nCs[x]] = s;
			nCs[x]++;
		}
		B[y] = nXs[y]-2;
	}

	return 1;
}

/*********************************************************/
void checkAlloc(void *ptr, char *msg)
{
	#if CONFIRM_ALLOCATIONS
		if (ptr == NULL)
		{
			fprintf(stderr, "%s\n", msg);
			exit(EXIT_FAILURE);
		}
	#endif
}


/*********************************************************/
void freeProblem()
{
	int x, c;

	free(X);
	free(B);
	free(nXs);
	free(nCs);
	for (x = 0; x < n; x++) {
		free(Cs[x]);
		free(Ccoefs[x]);
	}
	free(Cs);
	free(Ccoefs);
	for (c = 0; c < m; c++) {
		free(Xs[c]);
		free(Xcoefs[c]);
	}
	free(Xs);
	free(Xcoefs);
}

/*********************************************************/
int compare(const void *i, const void *j)
{
	if ( *((int *)i) < *((int *)j) ) 
		return -1;
	else if ( *((int *)i) == *((int *)j) )
		return 0;
	else 
		return 1;
}

/*********************************************************/
int verifySolution(int *solution)
{
	int x, i, y;

	for (y = 0; y < m; y++)
	{
		i = 0;
		while (i < nXs[y])
		{
			x = Xs[y][i];
			if (solution[x] != Xcoefs[y][i])
				goto clausesatisfied;
			i++;
		}

		return 0;

		clausesatisfied:
	}

	return 1;
}