#ifndef COP_HEADER_INCLUDED

#include "satfront.h"

#define CNF_MAX_LITERALS 100
#define CNF_MAX_CLAUSES  500

/* 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 *A;					/* Vector of values for the objective function (x.a). [var] */
extern int *nCs;				/* Number of constraints in which each var appears [var]. */
extern int **Cs;				/* Index of the k-th constraint in which var appears [var][k]. */
extern int **Ccoefs;		/* Coefficient 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 **Xcoefs;		/* Coefficient of the k-th variable appearing in a constraint [constraint][k]. */

extern int MaxCoef;			/* Largest magnitude of any coefficient. */
extern int MinB;				/* Smallest bounding value that appears in any constraint. */
extern int MaxB;				/* Largest bounding value that appears in any constraint. */

	/* Used for memory allocation. */
extern int N;						/* Max number of variables a constraint can use. */
extern int M;						/* Max number of constraints in which a var can appear. */


	/* Used by solvers. */
extern int *X;					/* Current assignment to variables. [var]. */
extern int steps;				/* Number of primal steps taken. */
extern int dsteps;			/* Number of dual steps taken. */
extern int r;						/* Counter for restart loop. */

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