/* Expand resolution proof from trace, simple implementation.  */

/* Note that usually an int return value of 0 means "no error", as in unix,
 * especially for functions that verify something.
 */

#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include <unistd.h>

#ifdef __linux__
#	include "cbigopen.h"
#endif

/* The convention used is that n is the maximum propositional variable
 * that might appear, and m is the number of input cnf clauses.
 * Program variables whose order of magnitude are n or m should be
 * type INT.
 * Program variables related to indexes for p.proof or pt.pfLineStart
 * or whose order of magnitude are the proof length should be
 * type UINT.
 * Casts between INT and UINT require great care to avoid unexpected
 * arithmetical results.  A straight cast does not change any bits, though.
 */

#define	INT	long
#define	UINT	unsigned INT

/* Use INT_STRING and UINT_STRING for scanf-type format strings and
 * ASCII proof output, not informational fprintf.
 */
#define	INT_STRING	" %ld"
#define	UINT_STRING	" %lu"

#define	MAX_PF_LINES (40*1024*1024)
#define	AVG_PF_LINE 16

/* ONE-OF-A-KIND TYPES AND THEIR GLOBAL VARIABLES */

typedef	struct	FmlaInfo {
	INT	n;
	INT	m;
	}
	FmlaInfo;

FmlaInfo	fmla;

typedef	struct	ProofInfo {
	INT*	proof;
	UINT	allocProof;
	UINT	startProof;
	UINT	endProof;
	int	endian;
	int	intBits;
	}
	ProofInfo;

ProofInfo	p;

typedef struct PfLineTbl {
	INT	interval;
	UINT	numLines;
	UINT	allocLines;
	UINT*	pfLineStart;
	}
	PfLineTbl;

PfLineTbl	pt;

typedef	struct	ResVerify {
	INT	top;
	INT*	usedStack;
	unsigned char*	resDtlAbs;
	unsigned char*	resDtl;
	}
	ResVerify;

ResVerify	rv;




/* PROTOTYPES and SPECS FOR LITTLE TECHNICAL SUBROUTINES */

/** fpeek() returns next char in file fp without consuming it;
 *  Returns EOF if at end-of-file.
 */
int	fpeek(FILE* fp);

/** swallowLine() consumes chars from fp through first '\n' and returns 0.
 *  It is an error for '\n' to be missing.
 */
int	swallowLine(FILE* fp);

/** swallowJunk() consumes white space and/or embedded comment lines
 *  and returns the next (unread) char in fp file, or EOF if there is none.
 */
int	swallowJunk(FILE* fp);

/** load32LittleEndian() returns the LittleEndian UINT in ch[0 ... 3] */
UINT	load32LittleEndian(unsigned char ch[4]);

/** load32BigEndian() returns the BigEndian UINT in ch[0 ... 3] */
UINT	load32BigEndian(unsigned char ch[4]);

void	store32LittleEndian(UINT i, unsigned char ch[4]);

void	store32BigEndian(UINT i, unsigned char ch[4]);





/* PROTOTYPES and SPECS */

int	initProof(INT initLines, INT avgLine);

int	initPfLineTbl(INT initSize);

void	recordPfLine(UINT label, UINT offset);

void	deletePfLine(UINT label1);

/** findPfLine(label0) returns the offset such that pfLine that starts at
  * p.proof[offset] has label label0.
  * An offset of 0 denotes an undefined or deleted clause,
  * because there is no pfLine at 0.
  * Exit on error.
  * Precondition: label0 > 0.
  */
UINT	findPfLine(UINT label0);

int	initResVerify(INT n);

/** resetResVerify() resets resDtl[lit] to 0 for all lits in usedStack
 *  and empties usedStack.
 */
void	resetResVerify(void);

/** loadOp() sets the 1-bit of resDtl[lit] for each lit in the clause that is
 *  different from clashLit.
 *  Push on usedStack if resDtl[lit] was 0.
 */
void	loadOp(UINT clause, INT clashLit);

/** loadResult() sets the 2-bit of resDtl[lit] for each lit in the clause.
 *  Push on usedStack if resDtl[lit] was 0.
 */
void	loadResult(UINT clause);

/** buildResult() stores clause represented in usedStack.
 *  Exit if p.proof[] runs out of space.
 */
void	buildResult(UINT clause);

/** dtlResVerify() returns 0 if symmetric difference in usedStack is empty;
 *  returns 1 if some lit in an operand is missing from the result;
 *  returns 2 if if some lit in result is missing from operand(s).
 *  Precondition: loadOp() and loadResult have been invoked.
 */
int	dtlResVerify(void);

int	confirmLit(UINT clause, INT clashLit);

/** resVerify() returns 0 if the resolution op at pfLineOffset is valid;
  * returns nonzero if resolution op is invalid; errors might be or-ed.
  * return 1: lit in op missing in result.
  * return 2: lit in result missing in op.
  * return 4: operand label >= this op's label or operand was deleted or
  *           never defined.
  * return 8: missing clashLit or -clashLit in an op.
  * Exit on error in data structures.
  */
int	resVerify(UINT pfLineOffset);

/** copyVerify() returns 0 if the copy op at pfLineOffset is valid;
  * returns nonzero if op is invalid.
  * return 1: lit in op missing in result.
  * return 2: lit in result missing in op.
  * return 4: operand label >= this op's label or operand was deleted or
  *           never defined.
  * Exit on error in data structures.
  */
int	copyVerify(UINT pfLineOffset);

/** resBuild() returns 0, builds and stores the resolvent clause,
  * if the resolution op at pfLineOffset is valid;
  * returns nonzero if resolution op is invalid; errors might be or-ed.
  * return 4: operand label >= this op's label or operand was deleted or
  *           never defined.
  * return 8: missing clashLit or -clashLit in an op.
  * Exit on error in data structures.
  */
int	resBuild(UINT pfLineOffset);

/** copyBuild() returns 0, builds and stores the copy clause,
  * if the copy op at pfLineOffset is valid;
  * returns nonzero if op is invalid.
  * return 4: operand label >= this op's label or operand was deleted or
  *           never defined.
  * Exit on error in data structures.
  */
int	copyBuild(UINT pfLineOffset);

void	fatalErr(char msg[]);

/** loadCnf() processes p-line, sets fmla fields, loads and records
 *  labels of clauses, while checking carefully for errors.
 *  It is careful not to consume possible proof file following the cnf
 *  portion.
 *  Literals must be separated by white space, newlines not required
 *  after literals begin.
 *  Precondition: p.proof[] has been allocated.
 *  Sets p.startProof to location of next available item of p.proof[].
 */
int	loadCnf(FILE* fp);

/** processPfHdr() checks for valid proof-trace header,
 *  sets p.endian, p.intBits, checks that n, m in header agree with cnf file,
 *  prints the 256-byte header, and writes the corresponding proof header.
 */
int	processPfHdr(FILE* fp);

/** loadTrace() reads fp (a trace) into p.proof[] beginning at p.startProof.
 *  It performs resolution and copy operations as they appear, and
 *  writes the proof operations on stdout.
 *  Precondition: 256-byte header has been read already and p.proof[] has
 *  been allocated enough space.
 *  Update p.endProof to location of next available item of p.proof[];
 *  i.e., last item is at p.proof[p.endProof - 1].
 *  Return 0 if successful, nonzero on error, such as out-of-space..
 *  Exit on read error or write error.
 */
int	loadTrace(FILE* fp);

int	loadAsciiTrace(FILE* fp);

void	reportDerivedClause(UINT prevOffset, char desc[]);

/** checkProof() prints whether proof has error or is valid;
 *  returns 0 on valid proof, which might NOT end with the empty clause.
 */
int	checkProof(void);

/** reportProofError() prints detailed info about the error in the
  * proof operation at offset.
  * Precondition: labels that should be positive at offset,offset+2,offset+3
  * are positive.
  */
void	reportProofError(UINT offset, int err);

void	reportDerivedClause(UINT prevOffset, char desc[]);

void	prUsage(char prog[]);

void	writeClause(UINT clause0, int endian, INT* pf);

void	writeAsciiClause(UINT clause0, INT* pf);

void	badLabelExit(UINT prevLabel, UINT label0, INT clashLit, UINT label1,
			UINT label2);





/* FUNCTIONS AND PROCEDURES */

int	main(int argc, char* argv[])
	{
	int	argn = argc - 1;
	FILE*	input_cnf_file;
	FILE*	input_trace_file;
	int	err;

	if (argn != 2)
		{
		prUsage(argv[0]);
		exit(- argn);
		}

	if (argv[1][0] == '-' && argv[1][1] == 0)
		input_cnf_file = stdin;
	else
		input_cnf_file = fopen(argv[1], "r");


	if (argv[2][0] == '-' && argv[2][1] == 0)
		input_trace_file = stdin;
	else
		{
#		ifdef __linux__
			input_trace_file = cBigOpenR(argv[2]);
#		else
			input_trace_file = fopen(argv[2], "r");
#		endif
		}

	if (input_cnf_file == NULL || input_trace_file == NULL)
		{
		fatalErr("failed to open an input file");
		prUsage(argv[0]);
		exit(- argn);
		}

	err = initPfLineTbl(MAX_PF_LINES);
	if (err)
		{
		fatalErr("failed to init PfLineTbl");
		exit(9);
		}

	err = initProof(MAX_PF_LINES, AVG_PF_LINE);
	if (err)
		{
		fatalErr("failed to init Proof");
		exit(9);
		}

	err = loadCnf(input_cnf_file);
	if (err)
		{
		fatalErr("failed to load input_cnf_file");
		exit(9);
		}

	err = processPfHdr(input_trace_file);
	if (err)
		{
		fatalErr("failed to process header of input_trace_file");
		exit(9);
		}

	err = initResVerify(fmla.n);
	if (err)
		{
		fatalErr("failed to init ResVerify");
		exit(9);
		}

	if (p.endian == 'A')
		err = loadAsciiTrace(input_trace_file);
	else
		err = loadTrace(input_trace_file);
	if (err)
		{
		fatalErr("failed to load input_trace_file");
		exit(9);
		}

	err = fclose(stdout);
	if (err)
		{
		fatalErr("fclose failed on stdout; proof may be incomplete");
		exit(9);
		}


	return err;
	}

int	initProof(INT initLines, INT avgLine)
	{
	p.allocProof = initLines * avgLine;
	p.proof = malloc(p.allocProof * sizeof(INT));
	return (p.proof == NULL);
	}

int	initPfLineTbl(INT initSize)
	{
	pt.allocLines = initSize;
	pt.pfLineStart = calloc(pt.allocLines, sizeof(UINT));
	pt.interval = 1;
	pt.numLines = 0;
	return (pt.pfLineStart == NULL);
	}


void	recordPfLine(UINT label, UINT offset)
	{
	UINT	nextLabel;

	if (label >= pt.allocLines)
		{
		fatalErr("label exceeded allocLines");
		exit(1);
		}

	pt.numLines = label;
	pt.pfLineStart[pt.numLines] = offset;
	}

void	deletePfLine(UINT label1)
	{
	/* NOTE: This simple method of deleting depends on every
	 * label being indexed -- i.e., pt.interval = 1.
	 * Currently there is no way to mark an operation or input clause
	 * in p.proof[] as being deleted.
	 * Possibly setting op1 = 0 in resolution or copy can be used,
	 * but this requires going through the code carefully.
	 */
	if (label1 >= pt.allocLines)
		{
		fatalErr("label exceeded allocLines");
		exit(1);
		}

	pt.pfLineStart[label1] = 0;
	return;
	}

UINT	findPfLine(UINT label0)
	{
	UINT	offset;

	if (label0 > pt.numLines)
		{
		fatalErr("label exceeds numLines");
		exit(3);
		}
	else
		{
		offset = pt.pfLineStart[label0];
		if (offset > 0 && p.proof[offset] != label0)
			{
			fatalErr("pfLineStart table error");
			exit(3);
			}
		}
	return offset;
	}


int	initResVerify(INT n)
	{
	rv.usedStack = calloc(n, sizeof(INT));
	rv.resDtlAbs = calloc(2 * n + 1, sizeof(unsigned char));
	rv.resDtl = rv.resDtlAbs + n;
	rv.top = 0;
	if (rv.usedStack == NULL || rv.resDtlAbs == NULL)
		return 1;
	else
		return 0;
	}

void	resetResVerify(void)
	{
	INT	lit;
	INT	t;

	t = rv.top;
	while (t > 0)
		{
		t --;
		lit = rv.usedStack[t];
		rv.resDtl[lit] = 0;
		}
	rv.top = 0;
	return;
	}

void	loadOp(UINT clause, INT clashLit)
	{
	INT*	pf = p.proof;
	INT	len = pf[clause];
	UINT	i;
	INT	lit;
	unsigned  dtl;

	for (i = clause + 1; i <= clause + len; i ++)
		{
		lit = pf[i];
		if (lit == clashLit)
			continue;

		dtl = rv.resDtl[lit];
		if (dtl == 0)
			{
			rv.usedStack[rv.top] = lit;
			rv.top ++;
			}
		if ((dtl & 1) == 0)
			{
			rv.resDtl[lit] = dtl | 1;
			}
		}
	return;
	}


void	loadResult(UINT clause)
	{
	INT*	pf = p.proof;
	INT	len = pf[clause];
	UINT	i;
	INT	lit;
	unsigned  dtl;

	for (i = clause + 1; i <= clause + len; i ++)
		{
		lit = pf[i];
		dtl = rv.resDtl[lit];
		if (dtl == 0)
			{
			rv.usedStack[rv.top] = lit;
			rv.top ++;
			}
		if ((dtl & 2) == 0)
			{
			rv.resDtl[lit] = dtl | 2;
			}
		}
	return;
	}


void	buildResult(UINT clause)
	{
	INT	t = rv.top;
	INT	len = t;
	INT*	pf = p.proof;
	UINT	newEnd = clause + len + 2;
	UINT	i;
	INT	lit;

	if (newEnd > p.allocProof)
		{
		fatalErr("buildResult out of space");
		exit(11);
		}

	pf[clause] = len;
	for (i = clause + 1; i <= clause + len; i ++)
		{
		t --;
		lit = rv.usedStack[t];
		pf[i] = lit;
		}
	pf[clause + len + 1] = len;
	p.endProof = newEnd;
	return;
	}

int	dtlResVerify(void)
	{
	INT	t = rv.top;
	INT	lit;
	int	ans;

	ans = 0;
	while (t > 0)
		{
		t --;
		lit = rv.usedStack[t];
		if (rv.resDtl[lit] != 3)
			{
			ans = rv.resDtl[lit];
			break;
			}
		}
	return ans;
	}

int	confirmLit(UINT clause, INT lit1)
	{
	INT*	pf = p.proof;
	INT	len = pf[clause];
	UINT	i;
	INT	lit;

	for (i = clause + 1; i <= clause + len; i ++)
		{
		lit = pf[i];
		if (lit == lit1)
			return 0;

		}
	return 8;
	}


int	resVerify(UINT pfLineOffset)
	{
	INT*	pf = p.proof;
	UINT	label0 = pf[pfLineOffset];
	INT	clashLit = pf[pfLineOffset + 1];
	UINT	label1 = pf[pfLineOffset + 2];
	UINT	label2 = pf[pfLineOffset + 3];
	UINT	clause0 = pfLineOffset + 4;
	UINT	offset1 = findPfLine(label1);
	UINT	offset2 = findPfLine(label2);
	UINT	clause1 = offset1 + 4;
	UINT	clause2 = offset2 + 4;
	int	ans, ans1, ans2;

	if (clashLit == 0 || clashLit > fmla.n || clashLit < -fmla.n)
		{
		fatalErr("bad clashLit for resolution op");
		exit(4);
		}
	if (label1 == 0 || label2 == 0)
		{
		fatalErr("bad operand label for resolution op");
		exit(4);
		}

	if (label1 >= label0 || label2 >= label0)
		{
		ans = 4;
		return ans;
		}

	if (offset1 == 0 || offset2 == 0)
		{
		ans = 4;
		return ans;
		}

	ans1 = confirmLit(clause1, -clashLit);
	ans2 = confirmLit(clause2, clashLit);
	loadOp(clause1, -clashLit);
	loadOp(clause2, clashLit);
	loadResult(clause0);
	ans = dtlResVerify();
	if (ans1 || ans2)
		ans = ans | 8;
	resetResVerify();

	return ans;
	}



int	copyVerify(UINT pfLineOffset)
	{
	INT*	pf = p.proof;
	UINT	label0 = pf[pfLineOffset];
	INT	clashLit = pf[pfLineOffset + 1];
	UINT	label1 = pf[pfLineOffset + 2];
	UINT	label2 = pf[pfLineOffset + 3];
	UINT	clause0 = pfLineOffset + 4;
	UINT	offset1 = findPfLine(label1);
	UINT	clause1 = offset1 + 4;
	int	ans;

	if (clashLit != 0)
		{
		fatalErr("nonzero clashLit for copy op");
		exit(5);
		}
	if (label1 == 0 || label2 != 0)
		{
		fatalErr("bad operand label for copy op");
		exit(5);
		}

	if (label1 >= label0)
		{
		ans = 4;
		return ans;
		}

	if (offset1 == 0)
		{
		ans = 4;
		return ans;
		}

	loadOp(clause1, 0);
	loadResult(clause0);
	ans = dtlResVerify();
	resetResVerify();

	return ans;
	}


int	resBuild(UINT pfLineOffset)
	{
	INT*	pf = p.proof;
	UINT	label0 = pf[pfLineOffset];
	INT	clashLit = pf[pfLineOffset + 1];
	UINT	label1 = pf[pfLineOffset + 2];
	UINT	label2 = pf[pfLineOffset + 3];
	UINT	clause0 = pfLineOffset + 4;
	UINT	offset1 = findPfLine(label1);
	UINT	offset2 = findPfLine(label2);
	UINT	clause1 = offset1 + 4;
	UINT	clause2 = offset2 + 4;
	int	ans, ans1, ans2;

	if (clashLit == 0 || clashLit > fmla.n || clashLit < -fmla.n)
		{
		fatalErr("bad clashLit for resolution op");
		exit(4);
		}
	if (label1 == 0 || label2 == 0)
		{
		fatalErr("bad operand label for resolution op");
		exit(4);
		}

	if (label1 >= label0 || label2 >= label0)
		{
		ans = 4;
		return ans;
		}

	if (offset1 == 0 || offset2 == 0)
		{
		ans = 4;
		return ans;
		}

	ans1 = confirmLit(clause1, -clashLit);
	ans2 = confirmLit(clause2, clashLit);
	loadOp(clause1, -clashLit);
	loadOp(clause2, clashLit);
	buildResult(clause0);
	ans = 0;
	if (ans1 || ans2)
		ans = ans | 8;
	resetResVerify();

	return ans;
	}



int	copyBuild(UINT pfLineOffset)
	{
	INT*	pf = p.proof;
	UINT	label0 = pf[pfLineOffset];
	INT	clashLit = pf[pfLineOffset + 1];
	UINT	label1 = pf[pfLineOffset + 2];
	UINT	label2 = pf[pfLineOffset + 3];
	UINT	clause0 = pfLineOffset + 4;
	UINT	offset1 = findPfLine(label1);
	UINT	clause1 = offset1 + 4;
	int	ans;

	if (clashLit != 0)
		{
		fatalErr("nonzero clashLit for copy op");
		exit(5);
		}
	if (label1 == 0 || label2 != 0)
		{
		fatalErr("bad operand label for copy op");
		exit(5);
		}

	if (label1 >= label0)
		{
		ans = 4;
		return ans;
		}

	if (offset1 == 0)
		{
		ans = 4;
		return ans;
		}

	loadOp(clause1, 0);
	loadResult(clause0);
	buildResult(clause0);
	ans = 0;
	resetResVerify();

	return ans;
	}

void	writeClause(UINT clause0, int endian, INT* pf)
	{
	unsigned char ch[4];
	INT	len = pf[clause0];
	int	outRetn;
	UINT	i;

	for (i = clause0; i < clause0 + len + 2; i ++)
		{
		if (endian == 'L')
			store32LittleEndian(pf[i], ch);
		else
			store32BigEndian(pf[i], ch);
		outRetn = fwrite(ch, sizeof(unsigned char), 4, stdout);
		if (outRetn != 4)
			{
			fatalErr("writeClause incomplete write");
			exit(7);
			}
		}
	return;
	}

void	writeAsciiClause(UINT clause0, INT* pf)
	{
	INT	len = pf[clause0];
	int	outRetn, k;
	UINT	i;
	char	s0[4] = "";
	char	s1[4] = "\n\t";
	char*	sfx;

	/* For human readability, the literals are indented by tab
	 * and printed at most 8 per line.
	 */
	outRetn = fprintf(stdout, INT_STRING "%s", len, s1);
	if (outRetn < 0)
		{
		fatalErr("writeAsciiClause write error");
		exit(7);
		}
	k = 0;
	for (i = clause0 + 1; i <= clause0 + len; i ++)
		{
		k ++;
		if (i < clause0 + len && k >= 8)
			{
			k = 0;
			sfx = s1;
			}
		else
			sfx = s0;
		outRetn = fprintf(stdout, INT_STRING "%s",
				pf[i], sfx);
		if (outRetn < 0)
			{
			fatalErr("writeAsciiClause write error");
			exit(7);
			}
		}
	outRetn = fprintf(stdout, "\n" INT_STRING , len);
	if (outRetn < 0)
		{
		fatalErr("writeAsciiClause write error");
		exit(7);
		}
	return;
	}


int	loadTrace(FILE* fp)
	{
	UINT	label0, label1, label2, prevLabel;
	unsigned char trace_ch[16];
	UINT	offset, clause0;
	int	fpRetn, outRetn, err;
	INT*	pf = p.proof;
	UINT	pfEnd = p.allocProof;
	int	endian = p.endian;
	INT	len, clashLit;

	fprintf(stderr, "BEGIN loadTrace\n");
	offset = p.startProof;
	prevLabel = fmla.m;
	while (1)
		{
		fpRetn = fread(trace_ch, sizeof(unsigned char), 16, fp);
		if (feof(fp) && fpRetn == 0)
			break;

		if (fpRetn != 16)
			{
			fatalErr("loadTrace incomplete read");
			exit(6);
			}
		if (offset + 4 > pfEnd)
			{
			fatalErr("loadTrace out of space");
			return 6;
			}

		outRetn = fwrite(trace_ch, sizeof(unsigned char), 16, stdout);
		if (outRetn != 16)
			{
			fatalErr("loadTrace incomplete write");
			exit(6);
			}

		if (endian == 'L')
			{
			label0 = load32LittleEndian(trace_ch);
			clashLit = load32LittleEndian(trace_ch + 4);
			label1 = load32LittleEndian(trace_ch + 8);
			label2 = load32LittleEndian(trace_ch + 12);
			}
		else
			{
			label0 = load32BigEndian(trace_ch);
			clashLit = load32BigEndian(trace_ch + 4);
			label1 = load32BigEndian(trace_ch + 8);
			label2 = load32BigEndian(trace_ch + 12);
			}
		pf[offset] = (INT)label0;
		pf[offset + 1] = clashLit;
		pf[offset + 2] = (INT)label1;
		pf[offset + 3] = (INT)label2;
		if (label0 == 0)
			{
			offset += 4;
			continue;
			}

		badLabelExit(prevLabel, label0, clashLit,
				label1, label2);

		clause0 = offset + 4;
		if (clashLit == 0)
			{
			err = copyBuild(offset);
			}
		else
			{
			err = resBuild(offset);
			}
		if (err)
			{
			reportProofError(offset, err);
			return err;
			}

		len = pf[clause0];
		writeClause(clause0, endian, pf);
		if (len == 0)
			fprintf(stderr,
				"PROOF TRACE REPRESENTS VALID REFUTATION\n");
		recordPfLine(label0, offset);
		prevLabel = label0;
		offset += 4 + len + 2;
		}

	p.endProof = offset;
	fprintf(stderr, "END loadTrace\n");
	return 0;
	}

int	loadAsciiTrace(FILE* fp)
	{
	UINT	label0, label1, label2, prevLabel;
	INT	Lit[4];
	UINT	offset, clause0;
	int	fpRetn, outRetn, err;
	INT*	pf = p.proof;
	UINT	pfEnd = p.allocProof;
	INT	len, clashLit;

	fprintf(stderr, "BEGIN loadAsciiTrace\n");
	offset = p.startProof;
	prevLabel = fmla.m;
	while (1)
		{
		fpRetn = fscanf(fp,
				INT_STRING INT_STRING INT_STRING INT_STRING ,
				Lit, Lit + 1, Lit + 2, Lit + 3);
		if (fpRetn == EOF)
			break;

		if (fpRetn != 4)
			{
			fatalErr("loadAsciiTrace read error or bad lit");
			exit(6);
			}
		if (offset + 4 > pfEnd)
			{
			fatalErr("loadAsciiTrace out of space");
			return 6;
			}

		outRetn = fprintf(stdout,
			UINT_STRING INT_STRING UINT_STRING UINT_STRING ,
			Lit[0], Lit[1], Lit[2], Lit[3]);
		if (outRetn < 0)
			{
			fatalErr("loadAsciiTrace write error");
			exit(6);
			}

		label0 = Lit[0];
		clashLit = Lit[1];
		label1 = Lit[2];
		label2 = Lit[3];
		pf[offset] = (INT)label0;
		pf[offset + 1] = clashLit;
		pf[offset + 2] = (INT)label1;
		pf[offset + 3] = (INT)label2;
		if (label0 == 0)
			{
			fprintf(stdout, "\n");
			offset += 4;
			continue;
			}

		badLabelExit(prevLabel, label0, clashLit,
				label1, label2);

		clause0 = offset + 4;
		if (clashLit == 0)
			{
			err = copyBuild(offset);
			}
		else
			{
			err = resBuild(offset);
			}
		if (err)
			{
			fprintf(stdout, "\n");
			reportProofError(offset, err);
			return err;
			}

		len = pf[clause0];
		writeAsciiClause(clause0, pf);
		fprintf(stdout, "\n");
		if (len == 0)
			fprintf(stderr,
				"PROOF TRACE REPRESENTS VALID REFUTATION\n");
		recordPfLine(label0, offset);
		prevLabel = label0;
		offset += 4 + len + 2;
		}

	p.endProof = offset;
	fprintf(stderr, "END loadAsciiTrace\n");
	return 0;
	}

void	badLabelExit(UINT prevLabel, UINT label0, INT clashLit, UINT label1,
			UINT label2)
	{
	if (label0 <= prevLabel)
		{
		fprintf(stderr,
		"Label %lu smaller than previous label %lu\n",
			(unsigned long)label0,
			(unsigned long)prevLabel);
		fprintf(stderr, "PROOF TRACE IS INVALID.\n");
		exit(8);
		}

	if (label1 >= label0 || label1 == 0)
		{
		fprintf(stderr,
		"Bad op1 label %lu in trace-line %lu\n",
			(unsigned long)label1,
			(unsigned long)label0);
		fprintf(stderr, "PROOF TRACE IS INVALID.\n");
		exit(8);
		}

	if (clashLit != 0 && (label2 >= label0 || label2 == 0))
		{
		fprintf(stderr,
		"Bad op2 label %lu in trace-line %lu\n",
			(unsigned long)label2,
			(unsigned long)label0);
		fprintf(stderr, "PROOF TRACE IS INVALID.\n");
		exit(8);
		}
	return;
	}
void	fatalErr(char msg[])
	{
	fprintf(stderr, "FATAL: %s\n", msg);
	return;
	}

void	prUsage(char prog[])
	{
	fprintf(stderr, "Usage: %s  input_cnf_file  input_trace_file\n", prog);
	fprintf(stderr, "\t'-' denotes stdin.\n");
	fprintf(stderr, "\tProof output is on stdout.  "
		"Use '>' to redirect to a file.\n");
	fprintf(stderr, "\tInformational output is on stderr.\n");
	}

int	loadCnf(FILE* fp)
	{
	int	nextCh, numf;
	long	N[1];
	long	M[1];
	long	Lit[1];
	UINT	offset, clauselen0;
	INT	i, n, m, lit, len;
	INT*	pf;
	char*	retn;
	char	buf[4096];

	fprintf(stderr, "BEGIN loading cnf file; lines through p-line are echoed.\n");

	buf[0] = 0;
	retn = fgets(buf, 4096 - 1, fp);
	while (1)
		{
		if (retn != buf)
			return 1;

		if (buf[0] == 'p')
			break;

		if (buf[0] != 'c')
			return 2;

		fprintf(stderr, "%s", buf);
		buf[0] = 0;
		retn = fgets(buf, 4096 - 1, fp);
		}

	fprintf(stderr, "%s", buf);
	numf = sscanf(buf, " p cnf" INT_STRING INT_STRING , N, M);
	if (numf != 2)
		{
		fatalErr("bad p-line in cnf file");
		return 3;
		}

	fmla.n = n = N[0];
	fmla.m = m = M[0];
	if (n <= 0 || m < 0 || m >= MAX_PF_LINES)
		{
		fatalErr("bad n (# vars) or m (# clauses) in cnf file");
		return 4;
		}

	/* OK, we made it through the p-line. Now load m clauses. */
	pf = p.proof;
	pf[0] = 0;
	offset = 1;
	for (i = 1; i <= m; i ++)
	    {
	    pf[offset] = i;
	    pf[offset + 1] = 0;
	    pf[offset + 2] = 0;
	    pf[offset + 3] = 0;
	    clauselen0 = offset + 4;
	    len = 0;

	    /** Read and load lits for i-th clause of cnf file, setting len.
	     *  Return without exiting loop if error is found.
	     */
	    while (1)
		{
		/* skip white space, including '\n', and embedded comments. */
		nextCh = swallowJunk(fp);
		if (nextCh == '%' || nextCh == EOF)
			{
			fatalErr("unexpected end of cnf file");
			return nextCh;
			}

		numf = fscanf(fp, INT_STRING , Lit);
		if (numf != 1)
			{
			fatalErr("failed to read lit or 0 in cnf file");
			return 5;
			}
		lit = Lit[0];
		if (lit == 0)
			break;

		if (lit > n || lit < - n)
			{
			fatalErr("lit out of range in cnf file");
			return 5;
			}
		len ++;
		pf[clauselen0 + len] = lit;
		}
	    /* Complete the bookkeeping for i-th clause of cnf file. */
	    pf[clauselen0 + len + 1] = len;
	    pf[clauselen0] = len;
	    recordPfLine(i, offset);
	    offset = clauselen0 + len + 2;
	    }

	p.endProof = p.startProof = offset;

	/** Ensure no trailing white space or comments remain.
	  * Error if another clause or garbage is found.
	  */
	nextCh = swallowJunk(fp);
	if (nextCh == '%' || nextCh == EOF)
		{
		fprintf(stderr, "END loading cnf file.\n\n");
		return 0;
		}
	else
		{
		fatalErr("Extra clauses or garbage at end of cnf file");
		return 6;
		}
	}


int	processPfHdr(FILE* fp)
	{
	char	hdr[256 + 1];
	int	numf, outRetn;
	long	N[1], M[1];

	numf = fread(hdr, sizeof(char), 256, fp);
	if (numf < 0)
		return numf;
	else if (numf != 256)
		return -2;

	hdr[256] = 0;
	fprintf(stderr, "256-byte header of input_trace_file:\n");
	fwrite(hdr, sizeof(char), 256, stderr);
	fprintf(stderr, "END of header\n");
	/* Check the header against fileformat.txt. */
	if (strncmp(hdr, "%RPT", 4) != 0)
		{
		fatalErr("header does not begin %RPT");
		return 1;
		}

	p.endian = hdr[4];
	if (p.endian != 'L' && p.endian != 'B' && p.endian != 'A')
		{
		fatalErr("format in header not known");
		return 2;
		}

	if (strncmp(hdr + 5, "   ", 3) == 0)
		{
		p.intBits = 32;
		}
	else if (strncmp(hdr + 5, "32 ", 3) == 0)
		{
		p.intBits = 32;
		}
	else if (strncmp(hdr + 5, "64 ", 3) == 0)
		{
		p.intBits = 64;
		fatalErr("This program does not support 64-bit formats");
		return 3;
		}
	else
		{
		p.intBits = 32;
		fatalErr("format in header not known");
		return 2;
		}

	N[0] = M[0] = 0;
	sscanf(hdr + 8, INT_STRING INT_STRING , N, M);
	if (N[0] != fmla.n || M[0] != fmla.m)
		{
		fatalErr("n or m in header disagrees with cnf file");
		return 4;
		}

	hdr[1] = 'R'; hdr[2] = 'E'; hdr[3] = 'S';
	if (hdr[5] == ' ')
		{
		hdr[5] = '3'; hdr[6] = '2'; hdr[7] = ' ';
		}
	outRetn = fwrite(hdr, sizeof(char), 256, stdout);
	if (outRetn != 256)
		{
		fatalErr("processPfHeader incomplete write");
		return 6;
		}

	return 0;
	}



int	checkProof(void)
	{
	int	err;
	INT*	pf = p.proof;
	UINT	pfEnd = p.endProof;
	UINT	label0, prevLabel, label1, label2;
	INT	clashLit, len;
	UINT	clauselen0, offset, prevOffset;

	fprintf(stderr, "BEGIN proof check\n");
	offset = p.startProof;
	prevOffset = 0;
	prevLabel = fmla.m;
	while (1)
		{
		if (offset >= pfEnd)
			{
			break;
			}

		label0 = pf[offset];
		clashLit = pf[offset + 1];
		label1 = pf[offset + 2];
		label2 = pf[offset + 3];
		if (label0 == 0 && label1 == 0)
			{
			reportDerivedClause(prevOffset, "Output Request");
			offset += 4;
			continue;
			}

		if (label0 == 0)
			{
			deletePfLine(label1);
			offset += 4;
			continue;
			}

		if (label0 <= prevLabel)
			{
			fprintf(stderr, "Label %lu smaller than previous label %lu\n",
				(unsigned long)label0,
				(unsigned long)prevLabel);
			fprintf(stderr, "PROOF TRACE IS INVALID.\n");
			return 8;
			}

		clauselen0 = offset + 4;
		len = pf[clauselen0];
		if (clashLit != 0)
			{
			err = resVerify(offset);
			}
		else
			{
			err = copyVerify(offset);
			}
		if (err)
			{
			reportProofError(offset, err);
			return err;
			}

		recordPfLine(label0, offset);
		prevOffset = offset;
		prevLabel = label0;
		if (len == 0)
			{
			break;
			}

		offset = clauselen0 + len + 2;
		}

	reportDerivedClause(prevOffset, "Final");
	if (len == 0 && prevOffset > 0)
		fprintf(stderr, "PROOF TRACE REPRESENTS VALID REFUTATION\n");
	fprintf(stderr, "END proof check\n");
	return 0;
	}

void	reportProofError(UINT offset, int err)
	{
	UINT	label0 = p.proof[offset];
	INT	clashLit = p.proof[offset + 1];
	UINT	label1 = p.proof[offset + 2];
	UINT	label2 = p.proof[offset + 3];
	UINT	offset1, offset2;

	fprintf(stderr, "ERROR %d in ", err);
	if (clashLit != 0)
		{
		fprintf(stderr, "Resolution operation with label %lu, clashLit %ld, ",
			(unsigned long)label0, (long)clashLit);
		fprintf(stderr, "operands %lu, %lu\n",
			(unsigned long)label1, (unsigned long)label2);
		}
	else
		{
		fprintf(stderr, "Copy operation with label %lu",
			(unsigned long)label0);
		fprintf(stderr, "operand %lu\n",
			(unsigned long)label1);
		}
	if (err & 8)
		fprintf(stderr, "Operand missing clashLit or -clashLit\n");
	if (err & 4)
		fprintf(stderr, "Operand label too large\n");

	offset1 = findPfLine(label1);
	if (offset1 == 0)
		fprintf(stderr, "Operand1 deleted or never defined\n");
	else
		reportDerivedClause(offset1, "Op1");

	if (label2 != 0)
		{
		offset2 = findPfLine(label2);
		if (offset2 == 0)
			fprintf(stderr, "Operand2 deleted or never defined\n");
		else
			reportDerivedClause(offset2, "Op2");
		}
	return;
	}

void	reportDerivedClause(UINT prevOffset, char desc[])
	{
	UINT	label0;
	INT	len, i;

	if (prevOffset == 0)
		{
		fprintf(stderr, "%s: No clause derived yet.\n", desc);
		return;
		}

	label0 = p.proof[prevOffset];
	len = p.proof[prevOffset + 4];
	fprintf(stderr, "%s: Clause has label %lu and %ld literals.\n", desc,
		(unsigned long)label0, (long)len);
	for (i = 1; i <= len; i ++)
		fprintf(stderr, " %ld", (long)p.proof[prevOffset + 4 + i]);
	fprintf(stderr, "\n");
	return;
	}




/* LITTLE TECHNICAL SUBROUTINES */

int	swallowLine(FILE* fp)
	{
	int	err = fscanf(fp, "%*[^\n]\n");
	return err;
	}

int	swallowJunk(FILE* fp)
	{
	int	err, nextCh;

	while (1)
		{
		/* skip white space, including '\n'. */
		fscanf(fp, " ");
		/* Check for embedded comment or other non-literal text. */
		nextCh = fpeek(fp);
		if (nextCh != 'c')
			break;

		/* consume through '\n'.  EOF is an error here. */
		err = fscanf(fp, "%*[^\n]\n");
		if (err)
			{
			fatalErr("failed reading embedded comment");
			return err;
			}
		}
	return nextCh;
	}

int	fpeek(FILE* fp)
	{
	int ch = getc(fp);

	if (ch != EOF) ungetc(ch, fp);
	return ch;
	}


UINT	load32LittleEndian(unsigned char ch[4])
	{
	UINT	ans;
	ans = 0;
	ans |= ch[0];
	ans |= (ch[1] << 8);
	ans |= (ch[2] << 16);
	ans |= (ch[3] << 24);
	return ans;
	}

UINT	load32BigEndian(unsigned char ch[4])
	{
	UINT	ans;
	ans = 0;
	ans |= ch[3];
	ans |= (ch[2] << 8);
	ans |= (ch[1] << 16);
	ans |= (ch[0] << 24);
	return ans;
	}


void	store32LittleEndian(UINT i, unsigned char ch[4])
	{
	UINT	ans;
	ans = i;          ch[0] = ans & 0xff;
	ans = (ans >> 8); ch[1] = ans & 0xff;
	ans = (ans >> 8); ch[2] = ans & 0xff;
	ans = (ans >> 8); ch[3] = ans & 0xff;
	return;
	}

void	store32BigEndian(UINT i, unsigned char ch[4])
	{
	UINT	ans;
	ans = i;          ch[3] = ans & 0xff;
	ans = (ans >> 8); ch[2] = ans & 0xff;
	ans = (ans >> 8); ch[1] = ans & 0xff;
	ans = (ans >> 8); ch[0] = ans & 0xff;
	return;
	}