/* 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"

int n, m, Nmax;
int *nXs, **Xs, **Xsgns, *lencount;
int *nYs, **Ys, **Ysgns, *X;

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

#define CONFIRM_ALLOCATIONS 1

/*********************************************************/

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

	if (exactAlloc)
		retVal = readCNFExactly(in, maxLiterals);
	else
		retVal = readCNFQuickly(in, maxLiterals, maxClauses);

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

	return retVal;
}

int readCNFQuickly(FILE *in, int maxLiterals, int maxClauses)
{
	int N, M;
	int x, y, lit, s, nlits;
	int ch;

	if (maxLiterals == 0)
		maxLiterals = CNF_MAX_LITERALS;

	if (maxClauses == 0)
		maxClauses = CNF_MAX_CLAUSES;

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

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

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

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

	nYs = (int *) calloc(n, sizeof(int));
	checkAlloc(nYs, "Failed to allocate nYs.");
	Ys = (int **) malloc(n * sizeof(int *));
	checkAlloc(Ys, "Failed to allocate Ys.");
	Ysgns = (int **) malloc(n * sizeof(int *));
	checkAlloc(Ysgns, "Failed to allocate Ysgns.");
	for (x = 0; x < n; x++) 
	{
		Ys[x] = (int *) malloc(M * sizeof(int));
		checkAlloc(Ys[x], "Failed to allocate Ys[x].");
		Ysgns[x] = (int *) malloc(M * sizeof(int));
		checkAlloc(Ysgns[x], "Failed to allocate Ysgns[x].");
	}
	X = (int *) malloc(n * sizeof(int));
	checkAlloc(X, "Failed to allocate X.");

	/***** read cnf  *****/
	Nmax = 0;
	for (y = 0; y < m; y++) 
	{
		nlits = 0;
		for (fscanf(in, "%d", &lit); lit; fscanf(in, "%d", &lit)) 
		{
			if (nlits++ > maxLiterals) 
			{
				printf("Error: Number of literals exceeds built-in limit of %d (use -xm flag).\n", maxLiterals);
				exit(1);
			}

			x = abs(lit) - 1;
			s = (lit > 0) ? 1 : -1;
			Xs[y][nXs[y]] = x;
			Xsgns[y][nXs[y]] = s;
			nXs[y]++;
			Ys[x][nYs[x]] = y;
			Ysgns[x][nYs[x]] = s;
			nYs[x]++;

			if (nYs[x] > M) 
			{
				printf("Error: Number of clauses exceeds built-in limit of %d (use -xm flag).\n", M);
				exit(1);
			}
		}
		lencount[nXs[y]]++;
		if (nlits > Nmax) 
			Nmax = nlits;
	}

	return 1;
}


int readCNFExactly(FILE *in, int maxLiterals)
{
	int x, y, lit, s, nlits;
	int ch;

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

	fscanf(in, " cnf %d %d", &n, &m);
	
	/***** allocate cnf *****/
	nXs = (int *) calloc(m, sizeof(int));
	checkAlloc(nXs, "Failed to allocate nXs.");
	Xs = (int **) calloc(m, sizeof(int *));
	checkAlloc(Xs, "Failed to allocate Xs.");
	Xsgns = (int **) calloc(m, sizeof(int *));
	checkAlloc(Xsgns, "Failed to allocate Xsgns.");
	lencount = NULL;

	nYs = (int *) calloc(n, sizeof(int));
	checkAlloc(nYs, "Failed to allocate nYs.");
	Ys = (int **) calloc(n, sizeof(int *));
	checkAlloc(Ys, "Failed to allocate Ys.");
	Ysgns = (int **) calloc(n, sizeof(int *));
	checkAlloc(Ysgns, "Failed to allocate Ysgns.");
	X = (int *) malloc(n * sizeof(int));
	checkAlloc(X, "Failed to allocate X.");

	/***** read cnf  *****/
	Nmax = 0;
	for (y = 0; y < m; y++) 
	{
		nlits = 0;
		for (fscanf(in, "%d", &lit); lit; fscanf(in, "%d", &lit)) 
		{
			nlits++;
			x = abs(lit) - 1;
			s = (lit > 0) ? 1 : -1;
			Xs[y] = (int *) realloc(Xs[y], (nXs[y]+1) * sizeof(int));
			checkAlloc(Xs[y], "Failed to allocate Xs[y].");
			Xs[y][nXs[y]] = x;
			Xsgns[y] = (int *) realloc(Xsgns[y], (nXs[y]+1) * sizeof(int));
			checkAlloc(Xsgns[y], "Failed to allocate Xsgns[y].");
			Xsgns[y][nXs[y]] = s;
			nXs[y]++;
			Ys[x] = (int *) realloc(Ys[x], (nYs[x]+1) * sizeof(int));
			checkAlloc(Ys[x], "Failed to allocate Ys[x].");
			Ys[x][nYs[x]] = y;
			Ysgns[x] = (int *) realloc(Ysgns[x], (nYs[x]+1) * sizeof(int));
			checkAlloc(Ysgns[x], "Failed to allocate Ysgns[x].");
			Ysgns[x][nYs[x]] = s;
			nYs[x]++;
		}

		if (nlits > Nmax) {
			int t;

			lencount = realloc(lencount, (nlits + 1) * sizeof(int));
			checkAlloc(lencount, "Failed to allocate lencount.");
			for (t = Nmax; t <= nlits; t++)
				lencount[t] = 0;
			
			Nmax = nlits;
		}

		lencount[nXs[y]]++;
	}

	return 1;
}

void freeProblem()
{
	int x, y;

	for (x = 0; x < n; x++) {
		free(Ys[x]);
		free(Ysgns[x]);
	}
	for (y = 0; y < m; y++) {
		free(Xs[y]);
		free(Xsgns[y]);
	}
	free(nXs);
	free(Xs);
	free(Xsgns);
	free(lencount);
	free(nYs);
	free(Ys);
	free(Ysgns);
	free(X);
}

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

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] == Xsgns[y][i])
				goto clausesatisfied;
			i++;
		}

		return 0;

		clausesatisfied:
	}

	return 1;
}