#ifndef READCNF_HEADER_INCLUDED

#include <stdio.h>
#include "satfront.h"

#define CNF_MAX_LITERALS 25
#define CNF_MAX_CLAUSES 100

/* Note that "constraint" refers to a "clause". */

/* Note: A variable is said to "appear" in a constraint when it has a non-zero
 * coefficient in that constraint.
 * We keep a sparse representation of these non-zero entries, indexable in
 * various ways.  The indices are often shown at the end of the comment (e.g.
 * [var]).
 */

extern int n;						/* Number of variables. */
extern int m;						/* Number of constraints. */
extern int *nYs;				/* Number of constraints in which each var appears [var]. */
extern int **Ys;				/* Index of the k-th constraint in which var appears [var][k]. */
extern int **Ysgns;			/* Sign of the k-th constraint in which var appears [var][k]. */
extern int *B;					/* Vector of bounds, one per constraint. [constraint] */
extern int *nXs;				/* Number of vars that appear in each constraint [constraint]. */
extern int **Xs;				/* Index of the k-th variable appearing in a constraint [constraint][k]. */
extern int **Xsgns;			/* Sign of the k-th variable appearing in a constraint [constraint][k]. */

	
	/* Used by solvers. */
extern int *X;					/* Current assignment to variables. [var]. */

	/* Used by SDF. */
extern int Nmax;				/* The length of the largest constraint. */
extern int *lencount;		/* Number of constraints of each length [constraint length]. */

	/* Prototypes. */
int readProblem(FILE *in, int maxLiterals, int maxClauses, int exactAlloc, int fileFormat, SATResults *results);
void freeProblem();
int verifySolution(int *solution);

#define READCNF_HEADER_INCLUDED
#endif