/* 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 "readcnf.h"

int n, m, M, N, Nmax;
int *nXs, **Xs, **Xsgns, *lencount;
int *nYs, **Ys, **Ysgns, *assign;

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

	if (maxLiterals == 0)
		maxLiterals = CNF_MAX_LITERALS;

	/***** 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 = (m < 500) ? m : 500;

	/***** allocate cnf *****/
	nXs = (int *) calloc(m, sizeof(int));
	Xs = (int **) calloc(m, sizeof(int *));
	for (y = 0; y < m; y++) 
		Xs[y] = (int *) calloc(maxLiterals, sizeof(int));
	Xsgns = (int **) calloc(m, sizeof(int *));
	for (y = 0; y < m; y++) 
		Xsgns[y] = (int *) calloc(maxLiterals, sizeof(int));
	lencount = (int *) calloc(maxLiterals+1, sizeof(int));

	nYs = (int *) calloc(n+1, sizeof(int));
	Ys = (int **) calloc(n+1, sizeof(int *));
	for (x = 1; x <= n; x++) 
		Ys[x] = (int *) calloc(M, sizeof(int));
	Ysgns = (int **) calloc(n+1, sizeof(int *));
	for (x = 1; x <= n; x++) 
		Ysgns[x] = (int *) calloc(M, sizeof(int));
	assign = (int *) calloc(n+1, sizeof(int));

	/***** 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: nlits exceeds maxLiterals=%d\n", maxLiterals);
				exit(1);
				}

			x = abs(lit);
			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: nYs exceeds M=%d\n", M);
				exit(1);
				}
			}
		lencount[nXs[y]]++;
		if (nlits > Nmax) 
			Nmax = nlits;
		}

	return 1;
	}

void freeCNF()
	{
	int x, y;

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