/* check resolution proof, mmap implementation, 64-bit pointers, some ints */ /* This should compile correctly for 32-bit or 64-bit architectures */ /* Note that usually an int return value of 0 means "no error", as in unix, * especially for functions that verify something. */ #include #include #include #include #include #include #include #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 INT32 int #define INT long #define UINT32 unsigned INT32 #define UINT unsigned INT /* Use INT_STRING and UINT_STRING for scanf-type format strings, not printf. */ #define INT_STRING " %ld" #define UINT_STRING " %lu" /* The default memory allocation is calculated from the two input files. * Command-line args 3 and 4 can override the defaults, but be careful. */ #define AVG_CNF_LINE 12 /* ONE-OF-A-KIND TYPES AND THEIR GLOBAL VARIABLES */ typedef struct MmapInfo { INT32* mmapArea; INT pfclauses; INT pfwords; INT cnfwords; INT pfHdrWords; off_t mmapOffset; size_t mmapLen; int pageSize; int pgwords_1; int hasMmap; int sz_off_t; int sz_size_t; int fd; } MmapInfo; MmapInfo sysMmap; typedef struct FmlaInfo { INT n; INT m; INT pfclauses; INT avg_pfline; INT pfwords; INT cnfwords; } FmlaInfo; FmlaInfo fmla; typedef struct ProofInfo { INT32* cnf; INT32* proof; INT32* proof0; UINT allocCnf; 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 UINT32 in ch[0 ... 3] */ UINT32 load32LittleEndian(unsigned char ch[4]); /** load32BigEndian() returns the BigEndian UINT32 in ch[0 ... 3] */ UINT32 load32BigEndian(unsigned char ch[4]); /* PROTOTYPES and SPECS */ void initMmap(FILE* fpProof); int verifyMmap(void); int initProof(void); int initProofNoMmap(UINT initLines, UINT avgLine); int initPfLineTbl(UINT 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); /** 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); void fatalErr(char msg[]); INT32* expandCnf(INT i, INT m); /** loadCnf() processes p-line, sets fmla fields, loads and records * labels of clauses, while checking carefully for errors. * Literals must be separated by white space, newlines not required * after literals begin. * Precondition: p.cnf[] has been allocated. * Sets p.startProof to location of next available item of p.cnf[]. * Does realloc to free excess space, setting p.allocCnf. */ int loadCnf(FILE* fp); /** processPfHdr() checks for valid header, sets p.endian, p.intBits, * checks that n, m in header agree with cnf file, and prints the * 256-byte header. */ int processPfHdr(char* pfHdr); int processPfHdrNoMmap(FILE* fp); /** loadProof() sets p.proof0 so that p.proof0[offset] accesses the int * that is logically 'offset' from beginning of proof including cnf. * I.e., p.proof0 = p.proof + 64 - p.startProof. * Sets p.endProof to location, relative to p.proof0, after the end * of the mmap-ed proof. * Return 0. */ int loadProof(void); /** loadProofNoMmap() reads fp into p.proof[] beginning at p.startProof. * 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. */ int loadProofNoMmap(FILE* fp); int loadAsciiProof(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[]); /* FUNCTIONS AND PROCEDURES */ int main(int argc, char* argv[]) { int argn = argc - 1; FILE* input_cnf_file; FILE* input_proof_file; int err; struct rlimit rlp[1]; /* If RLIMIT_STACK is too large, heap is too small. */ getrlimit(RLIMIT_STACK, rlp); rlp[0].rlim_cur = 20*1024*1024; setrlimit(RLIMIT_STACK, rlp); /* Avoid a huge corefile */ getrlimit(RLIMIT_CORE, rlp); if (rlp[0].rlim_cur > 10*1024*1024) { rlp[0].rlim_cur = 10*1024*1024; setrlimit(RLIMIT_CORE, rlp); } if (argn < 2 || argn > 4) { 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) { fatalErr("Cannot mmap stdin. Need real proof file."); prUsage(argv[0]); exit(- argn); } else { # ifdef __linux__ input_proof_file = cBigOpenR(argv[2]); # else input_proof_file = fopen(argv[2], "r"); # endif } if (input_cnf_file == NULL || input_proof_file == NULL) { fatalErr("failed to open an input file"); prUsage(argv[0]); exit(- argn); } if (argn >= 3) { fmla.pfclauses = (INT)atof(argv[3]) + 1; } else { fmla.pfclauses = 0; } if (argn >= 4) { fmla.cnfwords = (INT)atof(argv[4]); } else { fmla.cnfwords = 0; } initMmap(input_proof_file); /* sets fmla.pfwords, fmla.pfclauses and fmla.avg_pfline, et al. */ err = initPfLineTbl(fmla.pfclauses); if (err) { fatalErr("failed to init PfLineTbl"); exit(err); } //exit(0); err = loadCnf(input_cnf_file); if (err) { fatalErr("failed to load input_cnf_file"); exit(err); } err = processPfHdr((char*) sysMmap.mmapArea); if (err) { fatalErr("failed to process header of input_proof_file"); exit(err); } err = initResVerify(fmla.n); if (err) { fatalErr("failed to init ResVerify"); exit(err); } if (p.endian == 'A') err = loadAsciiProof(input_proof_file); else err = loadProof(); if (err) { fatalErr("failed to load input_proof_file"); exit(err); } err = checkProof(); return err; } /* MAP_NORESERVE is Linux extension. mmap not much use if limited to * available swap space, but at least it will compile, maybe. */ #ifndef MAP_NORESERVE #define MAP_NORESERVE 0 #endif void initMmap(FILE* fpProof) { void* mmapArea; size_t szInt32 = sizeof(INT32); int flags = (MAP_PRIVATE | MAP_NORESERVE); int flagsStd = MAP_PRIVATE; sysMmap.pageSize = getpagesize(); sysMmap.sz_off_t = sizeof(off_t); sysMmap.sz_size_t = sizeof(size_t); sysMmap.hasMmap = _POSIX_MAPPED_FILES; sysMmap.pgwords_1 = (sysMmap.pageSize / szInt32) - 1; sysMmap.fd = fileno(fpProof); fmla.pfwords = lseek(sysMmap.fd, 0, SEEK_END) / szInt32; lseek(sysMmap.fd, 0, SEEK_SET); // round up to multiple of pagesize sysMmap.pfwords = ( (fmla.pfwords + sysMmap.pgwords_1) & ~ sysMmap.pgwords_1 ); sysMmap.pfHdrWords = 256 / szInt32; sysMmap.mmapOffset = 0; sysMmap.mmapLen = sysMmap.pfwords * szInt32; printf("sysMmap %ld %lu %d %d %d %d %d %d\n", sysMmap.mmapOffset, sysMmap.mmapLen, sysMmap.pageSize, sysMmap.hasMmap, sysMmap.sz_size_t, sysMmap.sz_off_t, sysMmap.fd, MAP_NORESERVE); mmapArea = mmap(NULL, sysMmap.mmapLen, PROT_READ, flags, sysMmap.fd, sysMmap.mmapOffset); sysMmap.mmapArea = (INT32*) mmapArea; if (mmapArea == MAP_FAILED) { perror("initMmap"); fprintf(stdout, "initMmap MAP_FAILED errno = %d\n", errno); exit(errno); } if (0) verifyMmap(); if (fmla.pfclauses == 0) { /* Read backwards to last clause label */ INT32 len2 = sysMmap.mmapArea[fmla.pfwords - 1]; fmla.pfclauses = sysMmap.mmapArea[fmla.pfwords - len2 - 6] + 1; } fmla.avg_pfline = (INT)((fmla.pfwords - 1.0) / fmla.pfclauses) + 1; printf("fmla %lu %lu %lu sysMmap %lu\n", fmla.pfwords, fmla.cnfwords, fmla.pfclauses, sysMmap.pfwords); return; } int verifyMmap(void) { UINT i; UINT data0 = sysMmap.pfHdrWords; INT32 datum; printf("Trying to read from mmap data area.\n"); fflush(stdout); for (i = data0; i < fmla.pfwords; i++) { datum = sysMmap.mmapArea[i]; if (i < 12+data0 || fmla.pfwords - i <= 12) printf(" %d", datum); if (i == 12+data0) { printf("\n . . .\n"); fflush(stdout); } } printf("\n"); printf("Succeeded to read from all of mmap data area.\n"); fflush(stdout); return 0; } int initProof(void) { UINT mallocBytes, mmapBytes; UINT i; size_t szInt32 = sizeof(INT32); mmapBytes = (fmla.pfwords * szInt32); if (fmla.cnfwords == 0) { fmla.cnfwords = AVG_CNF_LINE * fmla.m + 1; } p.allocCnf = fmla.cnfwords; mallocBytes = (p.allocCnf * szInt32); printf("%lu = p.allocCnf, %lu = mallocBytes, %lu = mmapBytes\n", p.allocCnf, mallocBytes, mmapBytes); p.cnf = malloc(mallocBytes); p.proof = sysMmap.mmapArea; return (p.cnf == NULL || p.proof == NULL); } int initPfLineTbl(UINT initSize) { UINT callocBytes; pt.allocLines = initSize; callocBytes = pt.allocLines * sizeof(UINT); pt.pfLineStart = calloc(pt.allocLines, sizeof(UINT)); printf("%lu = pt.allocLines, %lu = callocBytes\n", pt.allocLines,callocBytes); pt.interval = 1; pt.numLines = 0; return (pt.pfLineStart == NULL); } int initProofNoMmap(UINT initLines, UINT avgLine) { UINT mallocBytes; p.allocCnf = initLines * avgLine; mallocBytes = (p.allocCnf * sizeof(INT32)); printf("%lu = p.allocCnf, %lu = mallocBytes\n", p.allocCnf,mallocBytes); p.proof = malloc(mallocBytes); return (p.proof == 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 { INT32* cnf = p.cnf; INT32* pf0 = p.proof0; UINT pfStart = p.startProof; INT32* pf; offset = pt.pfLineStart[label0]; pf = (offset >= pfStart ? pf0 : cnf); if (offset > 0 && pf[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) { INT32* cnf = p.cnf; INT32* pf0 = p.proof0; UINT pfStart = p.startProof; INT32* pf = (clause >= pfStart ? pf0 : cnf); 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) { INT32* cnf = p.cnf; INT32* pf0 = p.proof0; UINT pfStart = p.startProof; INT32* pf = (clause >= pfStart ? pf0 : cnf); 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; } 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) { INT32* cnf = p.cnf; INT32* pf0 = p.proof0; UINT pfStart = p.startProof; INT32* pf = (clause >= pfStart ? pf0 : cnf); 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) { INT32* cnf = p.cnf; INT32* pf0 = p.proof0; UINT pfStart = p.startProof; INT32* pf = (pfLineOffset >= pfStart ? pf0 : cnf); 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) { INT32* cnf = p.cnf; INT32* pf0 = p.proof0; UINT pfStart = p.startProof; INT32* pf = (pfLineOffset >= pfStart ? pf0 : cnf); 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 loadProof(void) { INT offset = p.startProof - (256 / sizeof(INT32)); printf("BEGIN loadProof\n"); p.proof0 = p.proof - offset; p.endProof = fmla.pfwords + offset; printf("END loadProof\n"); return 0; } int loadProofNoMmap(FILE* fp) { UINT32 i; unsigned char ch[4]; UINT offset; int fpRetn; UINT pfEnd = p.allocCnf; int endian = p.endian; printf("BEGIN loadProof\n"); offset = p.startProof; while (1) { fpRetn = fread(ch, sizeof(unsigned char), 4, fp); if (feof(fp) && fpRetn == 0) break; if (fpRetn != 4) { fatalErr("loadProof incomplete read"); exit(6); } if (offset >= pfEnd) { fatalErr("loadProof out of space"); return 6; } if (endian == 'L') i = load32LittleEndian(ch); else i = load32BigEndian(ch); p.proof[offset] = (INT32)i; offset ++; } p.endProof = offset; printf("END loadProof\n"); return 0; } int loadAsciiProof(FILE* fp) { long Lit[1]; INT lit; UINT offset; int fpRetn; UINT pfEnd = p.allocCnf; fatalErr("loadAsciiProof not available in this version"); exit(6); // could be converted to load into p.proof and not use mmap. printf("BEGIN loadAsciiProof\n"); offset = p.startProof; while (1) { fpRetn = fscanf(fp, INT_STRING, Lit); if (fpRetn == EOF) break; if (fpRetn != 1) { fatalErr("loadAsciiProof read error or bad lit"); exit(6); } if (offset >= pfEnd) { fatalErr("loadAsciiProof out of space"); return 6; } lit = Lit[0]; p.proof[offset] = lit; offset ++; } p.endProof = offset; printf("END loadAsciiProof\n"); return 0; } void fatalErr(char msg[]) { printf("FATAL: %s\n", msg); perror(msg); return; } void prUsage(char prog[]) { printf( "Usage: %s input_cnf_file|- input_proof_file [in_clauses [cnf_lits]]\n", prog); printf("\tUSE OF LAST TWO OPTIONAL ARGUMENTS IS NOT RECOMMENDED.\n"); printf("\tin_clauses includes both CNF and RES-proof.\n"); printf("\tin_clauses may be 0 if you want to specify cnf_lits.\n"); printf("\tin_clauses and cnf_lits may be over-estimates.\n"); printf("\tcnf_lits includes only CNF.\n"); printf("\tcnf_lits MUST INCLUDE 6 words per clause for res bookkeeping.\n"); printf("\t'-' denotes stdin. Output is on stdout.\n"); } INT32* expandCnf(INT i, INT m) { double expansion = 1.2 * (m+2.0) / (i+1.0); size_t newAlloc = p.allocCnf * expansion + 1; printf("expandCnf to %lu = newAlloc, %lu = newAllocBytes\n", newAlloc, newAlloc*sizeof(INT32)); p.cnf = (INT32*)realloc(p.cnf, newAlloc*sizeof(INT32)); if (p.cnf == NULL) { fatalErr("realloc in expandCnf failed"); exit(6); } p.allocCnf = newAlloc; return p.cnf; } int loadCnf(FILE* fp) { int nextCh, numf, cmtCnt, err; long N[1]; long M[1]; long Lit[1]; UINT offset, clauselen0; INT i, n, m, lit, len; INT32* pf; char* retn; char buf[4096]; printf( "BEGIN loading cnf file; up to 5 comments and p-line are echoed.\n"); cmtCnt = 0; 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; if (cmtCnt < 5) { printf("%s", buf); cmtCnt ++; } buf[0] = 0; retn = fgets(buf, 4096 - 1, fp); } printf("%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 >= fmla.pfclauses) { fatalErr("bad n (# vars) or m (# clauses) in cnf file"); return 4; } /* OK, we made it through the p-line. Now load m clauses. */ // err = initProofNoMmap(fmla.pfclauses, fmla.avg_pfline); err = initProof(); if (err) { fatalErr("failed to init Proof"); exit(err); } pf = p.cnf; pf[0] = 0; offset = 1; for (i = 1; i <= m; i ++) { if (offset + 6 > p.allocCnf) pf = expandCnf(i, m); 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 ++; if (clauselen0 + len + 1 >= p.allocCnf) pf = expandCnf(i, m); 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; p.cnf = (INT32*)realloc(p.cnf, offset*sizeof(INT32)); if (p.cnf == NULL) { fatalErr("realloc to smaller failed; memory corrupted?"); exit(6); } p.allocCnf = offset; /** Ensure no trailing white space or comments remain. * Error if another clause or garbage is found. */ nextCh = swallowJunk(fp); if (nextCh == '%' || nextCh == EOF) { printf("END loading cnf file.\n\n"); return 0; } else { fatalErr("Extra clauses or garbage at end of cnf file"); return 6; } } int processPfHdr(char* pfHdr) { char hdr[256 + 1]; int numf, i; long N[1], M[1]; for(i = 0; i < 256; i++) hdr[i] = pfHdr[i]; hdr[256] = 0; printf("256-byte header of input_proof_file:\n"); fwrite(hdr, sizeof(char), 256, stdout); printf("END of header\n"); /* Check the header against fileformat.txt. */ if (strncmp(hdr, "%RES", 4) != 0) { fatalErr("header does not begin %RES"); 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; } return 0; } int processPfHdrNoMmap(FILE* fp) { char hdr[256 + 1]; int numf; long N[1], M[1]; INT32 testint[1]; char* testch = (char*)testint; numf = fread(hdr, sizeof(char), 256, fp); if (numf < 0) return numf; else if (numf != 256) return -2; hdr[256] = 0; printf("256-byte header of input_proof_file:\n"); fwrite(hdr, sizeof(char), 256, stdout); printf("END of header\n"); /* Check the header against fileformat.txt. */ if (strncmp(hdr, "%RES", 4) != 0) { fatalErr("header does not begin %RES"); return 1; } p.endian = hdr[4]; if (p.endian != 'L' && p.endian != 'B' && p.endian != 'A') { fatalErr("format in header not known"); return 2; } testch[0] = 'L'; testch[1] = testch[2] = testch[3] = 0; if ((testint[0] == 'L' && p.endian == 'B') || (testint[0] != 'L' && p.endian == 'L')) { fatalErr("endian of mmap-ed file must match architecture"); return 3; } 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; } return 0; } int checkProof(void) { int err; INT32* cnf = p.cnf; INT32* pf0 = p.proof0; INT32* pf; UINT pfStart = p.startProof; UINT pfEnd = p.endProof; UINT label0, prevLabel, label1, label2; INT clashLit, len; UINT clauselen0, offset, prevOffset; printf("BEGIN proof check\n"); offset = p.startProof; len = -1; prevOffset = 0; prevLabel = fmla.m; while (1) { if (offset >= pfEnd) { break; } pf = (offset >= pfStart ? pf0 : cnf); 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) { printf("Label %lu smaller than previous label %lu\n", (unsigned long)label0, (unsigned long)prevLabel); printf("PROOF 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) printf("REFUTATION IS VALID\n"); printf("END proof check\n"); return 0; } void reportProofError(UINT offset, int err) { INT32* cnf = p.cnf; INT32* pf0 = p.proof0; UINT pfStart = p.startProof; INT32* pf = (offset >= pfStart ? pf0 : cnf); UINT label0 = pf[offset]; INT clashLit = pf[offset + 1]; UINT label1 = pf[offset + 2]; UINT label2 = pf[offset + 3]; UINT offset1 = findPfLine(label1); UINT offset2; printf("ERROR %d in ", err); if (clashLit != 0) { printf("Resolution operation with label %lu, clashLit %ld, ", (unsigned long)label0, (long)clashLit); printf("operands %lu, %lu\n", (unsigned long)label1, (unsigned long)label2); } else { printf("Copy operation with label %lu", (unsigned long)label0); printf("operand %lu\n", (unsigned long)label1); } if (err & 8) printf("Operand missing clashLit or -clashLit\n"); if (err & 4) printf("Operand label too large\n"); if (err & 2) printf("Extra literal in result\n"); if (err & 1) printf("Missing literal from result\n"); reportDerivedClause(offset, "Claimed"); if (offset1 == 0) printf("Operand1 deleted or never defined\n"); else reportDerivedClause(offset1, "Op1"); if (label2 != 0) { offset2 = findPfLine(label2); if (offset2 == 0) printf("Operand2 deleted or never defined\n"); else reportDerivedClause(offset2, "Op2"); } return; } void reportDerivedClause(UINT prevOffset, char desc[]) { UINT label0; INT len, i; INT32* cnf = p.cnf; INT32* pf0 = p.proof0; UINT pfStart = p.startProof; INT32* pf = (prevOffset >= pfStart ? pf0 : cnf); if (prevOffset == 0) { printf("%s: No clause derived yet.\n", desc); return; } label0 = pf[prevOffset]; len = pf[prevOffset + 4]; printf("%s: Clause has label %lu and %ld literals.\n", desc, (unsigned long)label0, (long)len); for (i = 1; i <= len; i ++) printf(" %ld", (long)pf[prevOffset + 4 + i]); printf("\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; } UINT32 load32LittleEndian(unsigned char ch[4]) { UINT32 ans; ans = 0; ans |= ch[0]; ans |= (ch[1] << 8); ans |= (ch[2] << 16); ans |= (ch[3] << 24); return ans; } UINT32 load32BigEndian(unsigned char ch[4]) { UINT32 ans; ans = 0; ans |= ch[3]; ans |= (ch[2] << 8); ans |= (ch[1] << 16); ans |= (ch[0] << 24); return ans; }