1/************************************************************************************[drat-trim.c]2Copyright (c) 2014 Marijn Heule and Nathan Wetzler, The University of Texas at Austin.3Copyright (c) 2015-2024 Marijn Heule, Carnegie Mellon University4Last edit: April 21, 202456Permission is hereby granted, free of charge, to any person obtaining a copy of this software and7associated documentation files (the "Software"), to deal in the Software without restriction,8including without limitation the rights to use, copy, modify, merge, publish, distribute,9sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is10furnished to do so, subject to the following conditions:1112The above copyright notice and this permission notice shall be included in all copies or13substantial portions of the Software.1415THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT16NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND17NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,18DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT19OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.20**************************************************************************************************/2122#include <stdio.h>23#include <stdlib.h>24#include <assert.h>25#include <sys/time.h>2627//#define PARTIALPROOF2829#define TIMEOUT 4000030#define BIGINIT 100000031#define INIT 432#define END 033#define UNSAT 034#define SAT 135#define DERIVATION 236#define ID -137#define PIVOT -238#define MAXDEP -339#define EXTRA 4 // ID + PIVOT + MAXDEP + terminating 040#define INFOBITS 2 // could be 1 for SAT, must be 2 for QBF41#define DBIT 142#define ASSUMED 243#define MARK 344#define ERROR -145#define ACTIVE 14647#define FORWARD_SAT 1048#define FORWARD_UNSAT 2049#define BACKWARD_UNSAT 3050#define SUCCESS 4051#define FAILED 5052#define FIXPOINT 6053#define NOWARNING 7054#define HARDWARNING 805556#define COMPRESS5758struct solver { FILE *inputFile, *proofFile, *lratFile, *traceFile, *activeFile;59 int *DB, nVars, timeout, mask, delete, *falseStack, *falseA, *forced, binMode, optimize, binOutput,60 *processed, *assigned, count, *used, *max, COREcount, RATmode, RATcount, nActive, *lratTable,61 nLemmas, maxRAT, *preRAT, maxDependencies, nDependencies, bar, backforce, reduce,62 *dependencies, maxVar, maxSize, mode, verb, unitSize, unitStackSize, prep, *current, nRemoved, warning,63 delProof, *setMap, *setTruth, rupOnly;64 char *coreStr, *lemmaStr;65 struct timeval start_time;66 long mem_used, time, nClauses, nStep, nOpt, nAlloc, *unitStack, *reason, lemmas, nResolve, *RATset,67 nReads, nWrites, lratSize, lratAlloc, *lratLookup, **wlist, *optproof, *formula, *proof; };6869static inline void assign (struct solver* S, int lit) {70 S->falseA[-lit] = 1; *(S->assigned++) = -lit; }7172int compare (const void *a, const void *b) {73 return (*(int*)a - *(int*)b); }7475int abscompare (const void *a, const void *b) {76 return (abs(*(int*)a) - abs(*(int*)b)); }7778static inline void printClause (int* clause) {79 printf ("[%i] ", clause[ID]);80 while (*clause) printf ("%i ", *clause++); printf ("0\n"); }8182static inline void addWatchPtr (struct solver* S, int lit, long watch) {83 if (S->used[lit] + 1 == S->max[lit]) { S->max[lit] *= 1.5;84 S->wlist[lit] = (long *) realloc (S->wlist[lit], sizeof (long) * S->max[lit]);85 if (S->wlist[lit] == NULL) { printf("c MEMOUT: reallocation failed for watch list of %i\n", lit); exit (0); } }86 S->wlist[lit][ S->used[lit]++ ] = watch | S->mask;87 S->wlist[lit][ S->used[lit] ] = END; }8889static inline void addWatch (struct solver* S, int* clause, int index) {90 addWatchPtr (S, clause[index], ((long) (((clause) - S->DB)) << 1)); }9192static inline void removeWatch (struct solver* S, int* clause, int index) {93 int i, lit = clause[index];94 if ((S->used[lit] > INIT) && (S->max[lit] > 2 * S->used[lit])) {95 S->max[lit] = (3 * S->used[lit]) >> 1;96 S->wlist[lit] = (long *) realloc (S->wlist[lit], sizeof (long) * S->max[lit]);97 assert(S->wlist[lit] != NULL); }98 long *watch = S->wlist[lit];99 for (i = 0; i < S->used[lit]; i++) {100 int* _clause = S->DB + (*(watch++) >> 1);101 if (_clause == clause) {102 watch[-1] = S->wlist[lit][ --S->used[lit] ];103 S->wlist[lit][ S->used[lit] ] = END; return; } } }104105static inline void addUnit (struct solver* S, long index) {106// printf("c adding unit %i\n", S->DB[index]);107 if (S->unitSize >= S->unitStackSize) {108 S->unitStackSize = (S->unitStackSize * 3) >> 1;109 S->unitStack = (long*) realloc (S->unitStack, sizeof(long) * S->unitStackSize);110 if (S->unitStack == NULL) {111 printf ("c failed to reallocate unit stack\n"); exit (0); } }112 S->unitStack[S->unitSize++] = index; }113114static inline void removeUnit (struct solver* S, int lit) {115 int i, found = 0;116 for (i = 0; i < S->unitSize; i++) {117 if (found) S->unitStack[i - 1] = S->unitStack[i];118 if (S->DB[ S->unitStack[i] ] == lit) found = 1; }119 S->unitSize--; }120121static inline void unassignUnit (struct solver* S, int lit) {122 if (S->verb)123 printf ("\rc removing unit %i\n", lit);124 while (S->falseA[-lit]) {125 if (S->verb)126 printf ("\rc removing unit %i (%i)\n", S->forced[-1], lit);127 S->falseA[*(--S->forced)] = 0;128 S->reason[abs(*S->forced)] = 0; }129 S->processed = S->assigned = S->forced; }130131static inline void markWatch (struct solver* S, int* clause, int index, int offset) {132 long* watch = S->wlist[ clause[ index ] ];133 for (;;) {134 int *_clause = (S->DB + (*(watch++) >> 1) + (long) offset);135 if (_clause == clause) { watch[ID] |= ACTIVE; return; } } }136137static inline void addDependency (struct solver* S, int dep, int forced) {138 if (1 || S->traceFile || S->lratFile) { // temporary for MAXDEP139 if (S->nDependencies == S->maxDependencies) {140 S->maxDependencies = (S->maxDependencies * 3) >> 1;141// printf ("c dependencies increased to %i\n", S->maxDependencies);142 S->dependencies = realloc (S->dependencies, sizeof (int) * S->maxDependencies);143 if (S->dependencies == NULL) { printf ("c MEMOUT: dependencies reallocation failed\n"); exit (0); } }144// printf("c adding dep %i\n", (dep << 1) + forced);145 S->dependencies[S->nDependencies++] = (dep << 1) + forced; } }146147static inline void markClause (struct solver* S, int* clause, int index) {148 S->nResolve++;149 addDependency (S, clause[index - 1] >> 1, (S->assigned > S->forced));150151 if ((clause[index + ID] & ACTIVE) == 0) {152 S->nActive++;153 clause[index + ID] |= ACTIVE;154//#ifdef PARTIALPROOF155// if ((clause + index) > (S->DB + S->firstLemma)) // don't delete original clauses156//#endif157 if ((S->mode == BACKWARD_UNSAT) && clause[index + 1]) {158 S->optproof[S->nOpt++] = (((long) (clause - S->DB) + index) << INFOBITS) + 1; }159 if (clause[1 + index] == 0) return;160 markWatch (S, clause, index, -index);161 markWatch (S, clause, 1 + index, -index); }162 while (*clause) S->falseA[*(clause++)] = MARK; }163164void analyze (struct solver* S, int* clause, int index) { // Mark all clauses involved in conflict165 markClause (S, clause, index);166 while (S->assigned > S->falseStack) {167 int lit = *(--S->assigned);168 if (S->falseA[lit] == MARK) {169 if (S->reason[abs (lit)]) {170 markClause (S, S->DB + S->reason[abs (lit)], -1);171 if (S->assigned >= S->forced)172 S->reason[abs (lit)] = 0; } }173#ifndef PARTIALPROOF174 else if (S->falseA[lit] == ASSUMED && !S->RATmode && S->reduce && !S->lratFile) { // Remove unused literal175 S->nRemoved++;176 int *tmp = S->current;177 while (*tmp != lit) tmp++;178 while (*tmp) { tmp[0] = tmp[1]; tmp++; }179 tmp[-1] = 0; }180#endif181 if (S->assigned >= S->forced) S->reason[abs (lit)] = 0;182 S->falseA[lit] = (S->assigned < S->forced); }183184 S->processed = S->assigned = S->forced; }185186void noAnalyze (struct solver* S) {187 while (S->assigned > S->falseStack) {188 int lit = *(--S->assigned);189 if (S->assigned >= S->forced) S->reason[abs (lit)] = 0;190 S->falseA[lit] = (S->assigned < S->forced); }191192 S->processed = S->assigned = S->forced; }193194int propagate (struct solver* S, int init, int mark) { // Performs unit propagation (init not used?)195 int *start[2];196 int check = 0, mode = !S->prep;197 int i, lit, _lit = 0; long *watch, *_watch;198 start[0] = start[1] = S->processed;199 flip_check:;200 check ^= 1;201 while (start[check] < S->assigned) { // While unprocessed false literals202 lit = *(start[check]++); // Get first unprocessed literal203 if (lit == _lit) watch = _watch;204 else watch = S->wlist[ lit ]; // Obtain the first watch pointer205 while (*watch != END) { // While there are watched clauses (watched by lit)206 if ((*watch & mode) != check) {207 watch++; continue; }208 int *clause = S->DB + (*watch >> 1); // Get the clause from DB209 if (S->falseA[ -clause[0] ] ||210 S->falseA[ -clause[1] ]) {211 watch++; continue; }212 if (clause[0] == lit) clause[0] = clause[1]; // Ensure that the other watched literal is in front213 for (i = 2; clause[i]; ++i) // Scan the non-watched literals214 if (S->falseA[ clause[i] ] == 0) { // When clause[j] is not false, it is either true or unset215 clause[1] = clause[i]; clause[i] = lit; // Swap literals216 addWatchPtr (S, clause[1], *watch); // Add the watch to the list of clause[1]217 *watch = S->wlist[lit][ --S->used[lit] ]; // Remove pointer218 S->wlist[lit][ S->used[lit] ] = END;219 goto next_clause; } // Goto the next watched clause220 clause[1] = lit; watch++; // Set lit at clause[1] and set next watch221 if (!S->falseA[ clause[0] ]) { // If the other watched literal is falsified,222 assign (S, clause[0]); // A unit clause is found, and the reason is set223 S->reason[abs (clause[0])] = ((long) ((clause)-S->DB)) + 1;224 if (!check) {225 start[0]--; _lit = lit; _watch = watch;226 goto flip_check; } }227 else if (!mark) { noAnalyze (S); return UNSAT; }228 else { analyze (S, clause, 0); return UNSAT; } // Found a root level conflict -> UNSAT229 next_clause: ; } } // Set position for next clause230 if (check) goto flip_check;231 S->processed = S->assigned;232 return SAT; } // Finally, no conflict was found233234235// Propagate top level units236static inline int propagateUnits (struct solver* S, int init) {237 int i;238// printf("c propagateUnits %i\n", S->unitSize);239 while (S->forced > S->falseStack) {240 S->falseA[*(--S->forced)] = 0;241 S->reason[abs (*S->forced)] = 0; }242 S->forced = S->assigned = S->processed = S->falseStack;243 for (i = 0; i < S->unitSize; i++) {244 int lit = S->DB[ S->unitStack[i] ];245 S->reason[abs (lit)] = S->unitStack[i] + 1;246 assign (S, lit); }247248 if (propagate (S, init, 1) == UNSAT) { return UNSAT; }249 S->forced = S->processed;250 return SAT; }251252// Put falsified literals at the end and returns the size under the current253// assignment: negative size means satisfied, size = 0 means falsified254int sortSize (struct solver *S, int *lemma) {255 unsigned int size = 0, last = 0, sat = 1;256 while (lemma[last]) {257 int lit = lemma[last++];258 if (S->falseA[lit] == 0) {259 if (S->falseA[-lit]) sat = -1;260 lemma[last-1] = lemma[ size ];261 lemma[size++] = lit; } }262 return sat * size; }263264// print the core clauses to coreFile in DIMACS format265void printCore (struct solver *S) {266 int i, j;267 for (i = 0; i < S->nClauses; i++) {268 int *clause = S->DB + (S->formula[i] >> INFOBITS);269 if (clause[ID] & ACTIVE) S->COREcount++; }270 printf ("\rc %i of %li clauses in core \n", S->COREcount, S->nClauses);271272 if (S->coreStr) {273 FILE *coreFile = fopen (S->coreStr, "w");274 fprintf (coreFile, "p cnf %i %i\n", S->nVars, S->COREcount);275 for (i = 0; i < S->nClauses; i++) {276 int *clause = S->DB + (S->formula[i] >> INFOBITS);277 if (clause[ID] & ACTIVE) {278 while (*clause) fprintf (coreFile, "%i ", *clause++);279 fprintf (coreFile, "0\n"); } }280 fclose (coreFile); } }281282void write_lit (struct solver *S, FILE *output, int lit) { // change to long?283 unsigned int l = abs (lit) << 1;284 if (lit < 0) l++;285286 do {287 if (l <= 127) { fputc ((char) l, output); }288 else { fputc ((char) (128 + (l & 127)), output); }289 S->nWrites++;290 l = l >> 7; }291 while (l); }292293void printLRATline (struct solver *S, int time) {294 int *line = S->lratTable + S->lratLookup[time];295 if (S->binOutput) {296 fputc ('a', S->lratFile); S->nWrites++;297 while (*line) write_lit (S, S->lratFile, *line++);298 write_lit (S, S->lratFile, *line++);299 while (*line) write_lit (S, S->lratFile, *line++);300 write_lit (S, S->lratFile, *line++); }301 else {302 while (*line) fprintf (S->lratFile, "%i ", *line++);303 fprintf (S->lratFile, "%i ", *line++);304 while (*line) fprintf (S->lratFile, "%i ", *line++);305 fprintf (S->lratFile, "%i\n", *line++); } }306307// print the core lemmas to lemmaFile in DRAT format308void printProof (struct solver *S) {309 int step;310 printf ("\rc %i of %i lemmas in core using %lu resolution steps\n", S->nActive - S->COREcount + 1, S->nLemmas + 1, S->nResolve);311 printf ("\rc %d RAT lemmas in core; %i redundant literals in core lemmas\n", S->RATcount, S->nRemoved);312313 // NB: not yet working with forward checking314 if (S->mode == FORWARD_UNSAT) {315 printf ("\rc optimized proofs are not supported for forward checking\n");316 return; }317318 // replace S->proof by S->optproof319 if (S->mode == BACKWARD_UNSAT) {320 if (S->nOpt > S->nAlloc) {321 S->nAlloc = S->nOpt;322 S->proof = (long*) realloc (S->proof, sizeof (long) * S->nAlloc);323 if (S->proof == NULL) { printf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } }324 S->nStep = 0;325 S->nLemmas = 0;326 for (step = S->nOpt - 1; step >= 0; step--) {327 long ad = S->optproof[step];328 int *lemmas = S->DB + (ad >> INFOBITS);329 if ((ad & 1) == 0) S->nLemmas++;330// if (lemmas[ID] & ACTIVE) lemmas[ID] ^= ACTIVE; // only useful for checking multiple times?331 S->proof[S->nStep++] = S->optproof[step]; } } // why not reuse ad?332333 if (S->lemmaStr) {334 FILE *lemmaFile = fopen (S->lemmaStr, "w");335 for (step = 0; step < S->nStep; step++) {336 long ad = S->proof[step];337 int *lemmas = S->DB + (ad >> INFOBITS);338 if (!lemmas[1] && (ad & 1)) continue; // don't delete unit clauses339 if (S->binOutput) {340 S->nWrites++;341 if (ad & 1) fputc ('d', lemmaFile);342 else fputc ('a', lemmaFile); }343 else if (ad & 1) fprintf (lemmaFile, "d ");344 int reslit = lemmas[PIVOT];345 while (*lemmas) {346 int lit = *lemmas++;347 if (lit == reslit) {348 if (S->binOutput) write_lit (S, lemmaFile, lit);349 else fprintf (lemmaFile, "%i ", lit); } }350 lemmas = S->DB + (ad >> INFOBITS);351 while (*lemmas) {352 int lit = *lemmas++;353 if (lit != reslit) {354 if (S->binOutput) write_lit (S, lemmaFile, lit);355 else fprintf (lemmaFile, "%i ", lit); } }356 if (S->binOutput) write_lit (S, lemmaFile, 0);357 else fprintf (lemmaFile, "0\n"); }358 if (S->binOutput) { fputc ('a', lemmaFile); write_lit (S, lemmaFile, 0); }359 else fprintf (lemmaFile, "0\n");360 fclose (lemmaFile); }361362 if (S->lratFile) {363 int lastAdded = S->nClauses;364 int flag = 0;365 for (step = 0; step < S->nStep; step++) {366 long ad = S->proof[step];367 int *lemmas = S->DB + (ad >> INFOBITS);368 if ((ad & 1) == 0) {369 if (lastAdded == 0) {370 if (S->binOutput) {371 write_lit (S, S->lratFile, 0); }372 else {373 fprintf (S->lratFile, "0\n"); } }374 lastAdded = lemmas[ID] >> 1;375 printLRATline (S, lastAdded); }376 else if (lastAdded == S->nClauses) continue;377 else if (!lemmas[1] && (ad & 1)) continue; // don't delete unit clauses378 else if (ad & 1) {379 if (lastAdded != 0) {380 if (S->binOutput) {381 fputc ('d', S->lratFile); S->nWrites++; }382 else {383 fprintf (S->lratFile, "%i d ", lastAdded); } }384 lastAdded = 0;385 if (S->binOutput) {386 write_lit (S, S->lratFile, lemmas[ID] >> 1); }387 else {388 fprintf (S->lratFile, "%i ", lemmas[ID] >> 1); } } }389 if (lastAdded != S->nClauses) {390 if (S->binOutput) {391 write_lit (S, S->lratFile, 0); }392 else {393 fprintf(S->lratFile, "0\n"); } }394395 printLRATline (S, S->count);396397 fclose (S->lratFile);398 if (S->nWrites)399 printf ("c wrote optimized proof in LRAT format of %li bytes\n", S->nWrites); } }400401void printNoCore (struct solver *S) {402 if (S->lratFile) {403 if (S->binOutput) {404 fputc ('d', S->lratFile); S->nWrites++; }405 else {406 fprintf (S->lratFile, "%ld d ", S->nClauses); }407 int i;408 for (i = 0; i < S->nClauses; i++) {409 int *clause = S->DB + (S->formula[i] >> INFOBITS);410 if ((clause[ID] & ACTIVE) == 0) {411 if (S->binOutput) {412 write_lit (S, S->lratFile, clause[ID] >> 1); }413 else {414 fprintf (S->lratFile, "%i ", clause[ID] >> 1); } } }415 if (S->binOutput) {416 write_lit (S, S->lratFile, 0); }417 else {418 fprintf (S->lratFile, "0\n"); } } }419420// print the dependency graph to traceFile in TraceCheck+ format421// this procedure adds the active clauses at the end of the trace422void printTrace (struct solver *S) {423 if (S->traceFile) { int i;424 for (i = 0; i < S->nClauses; i++) {425 int *clause = S->DB + (S->formula[i] >> INFOBITS);426 if (clause[ID] & ACTIVE) {427 fprintf (S->traceFile, "%i ", i + 1);428 while (*clause) fprintf (S->traceFile, "%i ", *clause++);429 fprintf (S->traceFile, "0 0\n"); } }430 fclose (S->traceFile); } }431432void printActive (struct solver *S) {433 int i, j;434 if (S->activeFile) {435 for (i = -S->maxVar; i <= S->maxVar; i++)436 if (i != 0)437 for (j = 0; j < S->used[i]; j++) {438 int *clause = S->DB + (S->wlist[i][j] >> 1);439 if (*clause == i) {440 while (*clause)441 fprintf (S->activeFile, "%i ", *clause++);442 fprintf (S->activeFile, "0\n"); } } } }443444void postprocess (struct solver *S) {445 printNoCore (S); // print before proof optimization446 printActive (S);447 printCore (S);448 printTrace (S); // closes traceFile449 printProof (S); } // closes lratFile450451void lratAdd (struct solver *S, int elem) {452 if (S->lratSize == S->lratAlloc) {453 S->lratAlloc = S->lratAlloc * 3 >> 1;454 S->lratTable = (int *) realloc (S->lratTable, sizeof (int) * S->lratAlloc);455 if (S->lratTable == NULL) {456 printf ("c MEMOUT: failed to reallocate lrat table\n"); exit (0); } }457 S->lratTable[S->lratSize++] = elem; }458459void printDependenciesFile (struct solver *S, int* clause, int RATflag, int mode) {460 FILE *file = NULL;461 if (mode == 0) file = S->traceFile;462 if (mode == 1) file = S->lratFile;463464 if (file) {465 int i, j, k;466 int tmp = S->lratSize;467468 if (clause != NULL) {469 S->lratLookup[clause[ID] >> 1] = S->lratSize; }470 else { S->lratLookup[S->count] = S->lratSize; }471472 if (clause != NULL) {473 int size = 0;474 int *sortClause;475476 sortClause = (int *) malloc (sizeof(int) * S->maxSize);477 assert (sortClause != NULL);478 lratAdd (S, S->time >> 1); // NB: long to ing479 int reslit = clause[PIVOT];480 while (*clause) {481 if (*clause == reslit)482 lratAdd (S, reslit);483 sortClause[size++] = *clause++; }484 qsort (sortClause, size, sizeof (int), abscompare);485 for (i = 0; i < size; i++) {486 int lit = sortClause[i];487 if (lit != reslit)488 lratAdd (S, lit); }489 free (sortClause); }490 else { lratAdd (S, S->count); }491 lratAdd (S, 0);492493 int isRUP = 1;494 for (i = 0; i < S->nDependencies; i++)495 if (S->dependencies[i] < 0) { isRUP = 0; break; }496497 if (isRUP) {498 for (i = S->nDependencies - 1; i >= 0; i--)499 lratAdd (S, S->dependencies[i] >> 1);500 lratAdd (S, 0);501 goto printLine; }502503 // first print the preRAT units in order of becoming unit504 int size = 0;505 for (i = 0; i < S->nDependencies; i++) {506 if (S->dependencies[i] > 0) continue;507 for (j = i - 1; j >= 0 && S->dependencies[j] > 0; j--) {508 int flag = 0;509 int cls = S->dependencies[j];510 if (cls & 1) continue;511 for (k = 0; k < size; k++)512 if (S->preRAT[k] == cls) flag = 1;513 if (!flag) {514 S->preRAT[size++] = cls;515 lratAdd (S, cls >> 1); } } }516517 // print dependencies in order of becoming unit518 for (i = S->nDependencies - 1; i >= 0; i--) {519 int cls = S->dependencies[i];520 if ((mode == 0) && (cls < 0)) continue;521 if (mode == 0) {522 int flag = 0;523 for (j = 0; j < size; j++)524 if (S->preRAT[j] == cls) flag = 1;525 if (!flag) {526 S->preRAT[size++] = cls;527 lratAdd (S, cls >> 1); } }528 if ((mode == 1) && (cls & 1))529 lratAdd (S, cls >> 1); }530 lratAdd (S, 0);531532 printLine:;533 if (mode == 0) {534 for (i = tmp; i < S->lratSize; i++)535 fprintf (file, "%d ", S->lratTable[i]);536 S->lratSize = tmp;537 fprintf (file, "\n"); } } }538539void printDependencies (struct solver *S, int* clause, int RATflag) {540 if (clause != NULL) {541 int i;542 clause[MAXDEP] = 0;543 for (i = 0; i < S->nDependencies; i++) {544 if (S->dependencies[i] > clause[MAXDEP])545 clause[MAXDEP] = S->dependencies[i]; }546 assert (clause[MAXDEP] < clause[ID]); }547548 printDependenciesFile (S, clause, RATflag, 0);549 printDependenciesFile (S, clause, RATflag, 1); }550551int checkRAT (struct solver *S, int pivot, int mark) {552 int i, j, nRAT = 0;553554 // Loop over all literals to calculate resolution candidates555 for (i = -S->maxVar; i <= S->maxVar; i++) {556 if (i == 0) continue;557 // Loop over all watched clauses for literal558 for (j = 0; j < S->used[i]; j++) {559 int* watched = S->DB + (S->wlist[i][j] >> 1);560 int id = watched[ID] >> 1;561 int active = watched[ID] & ACTIVE;562 if (*watched == i) { // If watched literal is in first position563 while (*watched)564 if (*watched++ == -pivot) {565 if ((S->mode == BACKWARD_UNSAT) && !active) {566// printf ("\rc RAT check ignores unmarked clause : "); printClause (S->DB + (S->wlist[i][j] >> 1));567 continue; }568 if (nRAT == S->maxRAT) {569 S->maxRAT = (S->maxRAT * 3) >> 1;570 S->RATset = realloc (S->RATset, sizeof (long) * S->maxRAT);571 assert (S->RATset != NULL); }572 S->RATset[nRAT++] = S->wlist[i][j] >> 1;573 break; } } } }574575 // S->prep = 1;576 // Check all clauses in RATset for RUP577 int flag = 1;578 qsort (S->RATset, nRAT, sizeof (long), compare);579 S->nDependencies = 0;580 for (i = nRAT - 1; i >= 0; i--) {581 int* RATcls = (int*) (S->DB + S->RATset[i]);582 int id = RATcls[ID] >> 1;583 int blocked = 0;584 long int reason = 0;585 if (S->verb) {586 printf ("\rc RAT clause: "); printClause (RATcls); }587588 while (*RATcls) {589 int lit = *RATcls++;590 if (lit != -pivot && S->falseA[-lit])591 if (!blocked || reason > S->reason[abs (lit)])592 blocked = lit, reason = S->reason[abs (lit)]; }593594 if (blocked && reason) {595 analyze (S, S->DB + reason, -1);596 S->reason[abs (blocked)] = 0; }597598 if (!blocked) {599 RATcls = (int*) (S->DB + S->RATset[i]);600 while (*RATcls) {601 int lit = *RATcls++;602 if (lit != -pivot && !S->falseA[lit]) {603 assign (S, -lit); S->reason[abs (lit)] = 0; } }604 if (propagate (S, 0, mark) == SAT) { flag = 0; break; } }605 addDependency (S, -id, 1); }606607 if (flag == 0) {608 while (S->forced < S->assigned) {609 S->falseA[*(--S->assigned)] = 0;610 S->reason[abs (*S->assigned)] = 0; }611 if (S->verb) printf ("\rc RAT check on pivot %i failed\n", pivot);612 return FAILED; }613614 return SUCCESS; }615616int redundancyCheck (struct solver *S, int *clause, int size, int mark) {617 int i, indegree;618 int falsePivot = S->falseA[clause[PIVOT]];619 if (S->verb) { printf ("\rc checking lemma (%i, %i) ", size, clause[PIVOT]); printClause (clause); }620621 if (S->mode != FORWARD_UNSAT) {622 if ((clause[ID] & ACTIVE) == 0) return SUCCESS; } // redundant?623// clause[PIVOT] ^= ACTIVE; }624625 if (size < 0) {626 S->DB[ S->reason[abs (*clause)] - 2] |= 1;627 return SUCCESS; }628629 indegree = S->nResolve;630631 S->RATmode = 0;632 S->nDependencies = 0;633 for (i = 0; i < size; ++i) {634 if (S->falseA[-clause[i]]) { // should only occur in forward mode635 if (S->warning != NOWARNING) {636 printf ("\rc WARNING: found a tautological clause in proof: "); printClause (clause); }637 if (S->warning == HARDWARNING) exit (HARDWARNING);638 while (S->forced < S->assigned) {639 S->falseA[*(--S->assigned)] = 0;640 S->reason[abs (*S->assigned)] = 0; }641 return SUCCESS; }642 S->falseA[clause[i]] = ASSUMED;643 *(S->assigned++) = clause[i];644 S->reason[abs (clause[i])] = 0; }645646 S->current = clause;647 if (propagate (S, 0, mark) == UNSAT) {648 indegree = S->nResolve - indegree;649 if (indegree <= 2 && S->prep == 0) {650 S->prep = 1; if (S->verb) printf ("\rc [%li] preprocessing checking mode on\n", S->time); }651 if (indegree > 2 && S->prep == 1) {652 S->prep = 0; if (S->verb) printf ("\rc [%li] preprocessing checking mode off\n", S->time); }653 if (S->verb) printf ("\rc lemma has RUP\n");654 printDependencies (S, clause, 0);655 return SUCCESS; }656657 // Failed RUP check. Now test RAT.658 // printf ("RUP check failed. Starting RAT check.\n");659 if (S->rupOnly) {660 printf ("\rc RUP check failed\n");661 return FAILED; }662 int reslit = clause[PIVOT];663 if (S->verb)664 printf ("\rc RUP checked failed; starting RAT check on pivot %d.\n", reslit);665666 if (falsePivot) return FAILED;667668 int* savedForced = S->forced;669670 S->RATmode = 1;671 S->forced = S->assigned;672673 int failed = 0;674 if (checkRAT (S, reslit, mark) == FAILED) {675 failed = 1;676 if (S->warning != NOWARNING) {677 printf ("\rc WARNING: RAT check on proof pivot failed : "); printClause (clause); }678 if (S->warning == HARDWARNING) exit (HARDWARNING);679 for (i = 0; i < size; i++) {680 if (clause[i] == reslit) continue;681 if (checkRAT (S, clause[i], mark) == SUCCESS) {682 clause[PIVOT] = clause[i];683 failed = 0; break; } } }684685 if (failed == 0)686 printDependencies (S, clause, 1);687688 S->processed = S->forced = savedForced;689 while (S->forced < S->assigned) {690 S->falseA[*(--S->assigned)] = 0;691 S->reason[abs (*S->assigned)] = 0; }692693 if (failed) {694 printf ("c RAT check failed on all possible pivots\n");695 return FAILED; }696697698 if (mark) S->RATcount++;699 if (S->verb) printf ("\rc lemma has RAT on %i\n", clause[PIVOT]);700 return SUCCESS; }701702int init (struct solver *S) {703 S->forced = S->falseStack; // Points inside *falseStack at first decision (unforced literal)704 S->processed = S->falseStack; // Points inside *falseStack at first unprocessed literal705 S->assigned = S->falseStack; // Points inside *falseStack at last unprocessed literal706707 // initialize watch pointers on the original clauses708 S->RATmode = 0;709 S->nRemoved = 0;710 S->nOpt = 0;711 S->nResolve = 0;712 S->RATcount = 0;713 S->nActive = 0;714 S->COREcount = 0;715 S->unitSize = 0;716717 int i;718 for (i = 1; i <= S->maxVar; ++i) {719 S->reason [i] = 0;720 S->falseStack[i] = 0;721 S->falseA[i] = S->falseA[-i] = 0;722 S->used [i] = S->used [-i] = 0;723 S->wlist [i][0] = S->wlist [-i][0] = END; }724725 for (i = 0; i < S->nClauses; i++) {726 int *clause = S->DB + (S->formula[i] >> INFOBITS);727 if (clause[ID] & ACTIVE) clause[ID] ^= ACTIVE;728 if (clause[0] == 0) {729 printf ("\rc formula contains empty clause\n");730 if (S->coreStr) {731 FILE *coreFile = fopen (S->coreStr, "w");732 fprintf (coreFile, "p cnf 0 1\n 0\n");733 fclose (coreFile); }734 if (S->lemmaStr) {735 FILE *lemmaFile = fopen (S->lemmaStr, "w");736 fprintf (lemmaFile, "0\n");737 fclose (lemmaFile); }738 return UNSAT; }739 if (clause[1]) { addWatch (S, clause, 0); addWatch (S, clause, 1); }740 else if (S->falseA[clause[0]]) {741 printf ("\rc found complementary unit clauses: %i\n", clause[0]);742 if (S->coreStr) {743 FILE *coreFile = fopen (S->coreStr, "w");744 fprintf (coreFile, "p cnf %i 2\n%i 0\n%i 0\n", abs (clause[0]), clause[0], -clause[0]);745 fclose (coreFile); }746 if (S->lemmaStr) {747 FILE *lemmaFile = fopen (S->lemmaStr, "w");748 fprintf (lemmaFile, "0\n");749 fclose (lemmaFile); }750 if (S->lratFile) {751 int j;752 for (j = 0; j < i; j++) {753 int *_clause = S->DB + (S->formula[j] >> INFOBITS);754 if ((_clause[0] == -clause[0]) && !_clause[1]) break; }755 fprintf (S->lratFile, "%li 0 %i %i 0\n", S->nClauses + 1, j + 1, i + 1); }756 return UNSAT; }757 else if (!S->falseA[ -clause[0] ]) {758 addUnit (S, (long) (clause - S->DB));759 assign (S, clause[0]); } }760761 S->nDependencies = 0;762 S->time = S->count; // Alternative time init763 if (propagateUnits (S, 1) == UNSAT) {764 printf ("\rc UNSAT via unit propagation on the input instance\n");765 printDependencies (S, NULL, 0);766 postprocess (S); return UNSAT; }767 return SAT; }768769int verify (struct solver *S, int begin, int end) {770 int top_flag = 1;771 if (init (S) == UNSAT) return UNSAT;772773 if (S->mode == FORWARD_UNSAT) {774 if (begin == end)775 printf ("\rc start forward verification\n"); }776777 int step;778 int adds = 0;779 int active = S->nClauses;780 for (step = 0; step < S->nStep; step++) {781 if (step >= begin && step < end) continue;782 long ad = S->proof[step]; long d = ad & 1;783 int *lemmas = S->DB + (ad >> INFOBITS);784785 S->time = lemmas[ID];786 if (d) { active--; }787 else { active++; adds++; }788 if (S->mode == FORWARD_SAT && S->verb) printf ("\rc %i active clauses\n", active);789790 if (!lemmas[1]) { // found a unit791 int lit = lemmas[0];792 if (S->verb)793 printf ("\rc found unit in proof %i [%li]\n", lit, S->time);794 if (d) {795 if (S->mode == FORWARD_SAT) {796 removeUnit (S, lit); propagateUnits (S, 0); }797 else { // no need to remove units while checking UNSAT798 if (S->verb) { printf("c removing proof step: d "); printClause(lemmas); }799 S->proof[step] = 0; continue; } }800 else {801// printf ("c unit %i\n", lit);802// if (S->falseA[-lit]) S->reason[abs(lit)] = (lemmas - S->DB) + 1;803 if (S->mode == BACKWARD_UNSAT && S->falseA[-lit]) { S->proof[step] = 0; continue; }804 else { addUnit (S, (long) (lemmas - S->DB)); } } }805806 if (d && lemmas[1]) { // if delete and not unit807 if ((S->reason[abs (lemmas[0])] - 1) == (lemmas - S->DB)) { // what is this check?808 if (S->mode != FORWARD_SAT) { // ignore pseudo unit clause deletion809 if (S->warning != NOWARNING) {810 if (S->verb) { printf ("\rc WARNING: ignoring deletion instruction %li: ", (lemmas - S->DB)); printClause (lemmas); } }811 if (S->warning == HARDWARNING) exit (HARDWARNING);812 if (S->verb) { printf ("c ignoring deletion instruction %li: ", (lemmas - S->DB)); printClause (lemmas); }813// if (S->mode == BACKWARD_UNSAT) { // ignore pseudo unit clause deletion814 S->proof[step] = 0; }815 else { // if (S->mode == FORWARD_SAT) { // also for FORWARD_UNSAT?816 removeWatch (S, lemmas, 0), removeWatch (S, lemmas, 1);817 propagateUnits (S, 0); } }818 else {819 removeWatch (S, lemmas, 0), removeWatch (S, lemmas, 1); }820 if (S->mode == FORWARD_UNSAT ) continue; // Ignore deletion of top-level units821 if (S->mode == BACKWARD_UNSAT) continue; }822823 int size = sortSize (S, lemmas); // after removal of watches824825 if (d && S->mode == FORWARD_SAT) {826 if (size == -1) propagateUnits (S, 0); // necessary?827 if (redundancyCheck (S, lemmas, size, 1) == FAILED) {828 printf ("c failed at proof line %i (modulo deletion errors)\n", step + 1);829 return SAT; }830 continue; }831832 if (d == 0 && S->mode == FORWARD_UNSAT) {833 if (step > end) {834 if (size < 0) continue; // Fix of bus error: 10835 if (redundancyCheck (S, lemmas, size, 1) == FAILED) {836 printf ("c failed at proof line %i (modulo deletion errors)\n", step + 1);837 return SAT; }838839 size = sortSize (S, lemmas);840 S->nDependencies = 0; } }841842 if (lemmas[1])843 addWatch (S, lemmas, 0), addWatch (S, lemmas, 1);844845 if (size == 0) { printf ("\rc conflict claimed, but not detected\n"); return SAT; } // change to FAILED?846 if (size == 1) {847 if (S->verb) printf ("\rc found unit %i\n", lemmas[0]);848 assign (S, lemmas[0]); S->reason[abs (lemmas[0])] = ((long) ((lemmas)-S->DB)) + 1;849 if (propagate (S, 1, 1) == UNSAT) goto start_verification;850 S->forced = S->processed; } }851852 if (S->mode == FORWARD_SAT && active == 0) {853 postprocess (S); return UNSAT; }854855 if (S->mode == FORWARD_UNSAT) {856 if (begin == end) {857 postprocess (S);858 printf ("\rc VERIFIED derivation: all lemmas preserve satisfiability\n");859 if (S->warning != NOWARNING) {860 printf ("\rc WARNING: no empty clause detected, this is not a refutation\n"); }861 return DERIVATION; }862 return SAT; }863864 if (S->mode == BACKWARD_UNSAT) {865 if (S->backforce) {866 int s;867 for (s = 0; s < step; s++) {868 long ad = S->proof[s];869 int *clause = S->DB + (ad >> INFOBITS);870 if (sortSize(S, clause) >= 0) {871 if ( (ad & 1) && (clause[ID] & ACTIVE)) clause[ID] ^= ACTIVE;872 if (!(ad & 1)) clause[ID] |= ACTIVE; } } }873 if (!S->backforce) {874 printf ("\rc ERROR: no conflict\n");875 return SAT;876 } }877878 start_verification:;879 if (S->mode == FORWARD_UNSAT) {880 printDependencies (S, NULL, 0);881 postprocess (S); return UNSAT; }882883 if (!S->backforce)884 printDependencies (S, NULL, 0);885886 if (S->mode == FORWARD_SAT) {887 printf ("\rc ERROR: found empty clause during SAT check\n"); exit (0); }888 printf ("\rc detected empty clause; start verification via backward checking\n");889890 S->forced = S->processed;891 assert (S->mode == BACKWARD_UNSAT); // only reachable in BACKWARD_UNSAT mode892893 S->nOpt = 0;894895 int checked = 0, skipped = 0;896897 double max = (double) adds;898899 struct timeval backward_time;900 gettimeofday (&backward_time, NULL);901 for (; step >= 0; step--) {902 struct timeval current_time;903 gettimeofday (¤t_time, NULL);904 int seconds = (int) (current_time.tv_sec - S->start_time.tv_sec);905 if ((seconds > S->timeout) && (S->optimize == 0)) printf ("s TIMEOUT\n"), exit (0);906907 if (S->bar)908 if ((adds % 1000) == 0) {909 int f;910 long runtime = (current_time.tv_sec - backward_time.tv_sec ) * 1000000 +911 (current_time.tv_usec - backward_time.tv_usec);912 double time = (double) (runtime / 1000000.0);913 double fraction = (adds * 1.0) / max;914 printf("\rc %.2f%% [", 100.0 * (1.0 - fraction));915 for (f = 1; f <= 20; f++) {916 if ((1.0 - fraction) * 20.0 < 1.0 * f) printf(" ");917 else printf("="); }918 printf("] time remaining: %.2f seconds ", time / (1.0 - fraction) - time);919 if (step == 0) printf("\n");920 fflush (stdout); }921922 long ad = S->proof[step]; long d = ad & 1;923 int *clause = S->DB + (ad >> INFOBITS);924925926 if (ad == 0) continue; // Skip lemma that has been removed from proof927 if ( d == 0) {928 adds--;929 if (clause[1]) {930 removeWatch (S, clause, 0), removeWatch (S, clause, 1);931 if (S->reason[abs (clause[0])] == (clause + 1 - S->DB)) { // use this check also for units?932 unassignUnit (S, clause[0]); } }933 else unassignUnit (S, clause[0]); }934935 int size = sortSize (S, clause);936937 if (d) {938 if (S->verb) { printf ("\rc adding clause (%i) ", size); printClause (clause); }939 addWatch (S, clause, 0), addWatch (S, clause, 1); continue; }940941 S->time = clause[ID];942 if ((S->time & ACTIVE) == 0) {943 skipped++;944// if ((skipped % 100) == 0) printf("c skipped %i, checked %i\n", skipped, checked);945 continue; } // If not marked, continue946947 assert (size >= 1);948 int *_clause = clause + size;949 while (*_clause++) { S->nRemoved++; }950 clause[size] = 0;951952 if (S->verb) {953 printf ("\rc validating clause (%i, %i): ", clause[PIVOT], size); printClause (clause); }954955 if (redundancyCheck (S, clause, size, 1) == FAILED) {956 printf ("c failed at proof line %i (modulo deletion errors)\n", step + 1);957 return SAT; }958 checked++;959 S->optproof[S->nOpt++] = ad; }960961 postprocess (S);962 return UNSAT; }963964long matchClause (struct solver* S, long *clauselist, int listsize, int* input, int size) {965 int i, j;966 for (i = 0; i < listsize; ++i) {967 int *clause = S->DB + clauselist[i];968 for (j = 0; j <= size; j++)969 if (clause[j] != input[j]) goto match_next;970971 long result = clauselist[i];972 clauselist[i] = clauselist[--listsize];973 return result;974 match_next:; }975 return 0; }976977unsigned int getHash (int* input) {978 unsigned int sum = 0, prod = 1, xor = 0;979 while (*input) {980 prod *= *input; sum += *input; xor ^= *input; input++; }981 return (1023 * sum + prod ^ (31 * xor)) % BIGINIT; }982983int read_lit (struct solver *S, int *lit) {984 int l = 0, lc, shift = 0;985 do {986 lc = getc_unlocked (S->proofFile);987 S->nReads++;988 if ((shift == 0) && (lc == EOF)) return EOF;989 l |= (lc & 127) << shift;990 shift += 7; }991 while (lc > 127);992 if (l % 2) *lit = (l >> 1) * -1;993 else *lit = (l >> 1);994 return 1; }995996void deactivate (struct solver *S) {997 S->nActive = 0;998 int step;999 for (step = 0; step < S->nStep; step++) {1000 if ((S->proof[step] & 1) == 0) {1001 int *clause = S->DB + (S->proof[step] >> INFOBITS);1002 if (clause[ID] & ACTIVE) clause[ID] ^= ACTIVE; } }1003}10041005void shuffleProof (struct solver *S, int iteration) {1006 int i, step, _step;10071008 double base = 100;1009 for (i = 1; i < iteration; i++)1010 base *= 1.1;10111012 // randomly remove clause deletion steps1013 for (_step = 0, step = 0; step < S->nStep; step++) {1014 if (S->proof[step] & 1) {1015 int length = 0;1016 int *clause = S->DB + (S->proof[step] >> INFOBITS);1017 while (*clause) { length++; clause++; }1018 if ((rand() % 1000) < (base * iteration / length)) continue; }1019 S->proof[_step++] = S->proof[step]; }1020 S->nStep = _step;10211022 for (step = S->nStep - 1; step > 0; step--) {1023 long a = S->proof[step ];1024 if (a & DBIT) continue;1025 long b = S->proof[step-1];1026 if (b & DBIT) {1027 S->proof[step ] = b;1028 S->proof[step-1] = a; }1029 else {1030 int *c = S->DB + (a >> INFOBITS);1031 int *d = S->DB + (b >> INFOBITS);1032 int coinflip = 0;1033// int coinflip = rand () / (RAND_MAX >> 1);1034 if (c[MAXDEP] < d[MAXDEP] || (coinflip && (c[MAXDEP] < d[ID]))) {1035 int tmp = d[ID];1036 d[ID] = c[ID];1037 c[ID] = tmp;1038 S->proof[step ] = b;1039 S->proof[step-1] = a; } } }10401041 for (step = 0; step < S->nStep; step++) {1042 long ad = S->proof[step];1043 if (ad & 1) continue;1044 int *clause = S->DB + (ad >> INFOBITS);1045 int i, length = 0;1046 while (*clause) { length++; clause++; }1047 clause = S->DB + (ad >> INFOBITS);1048 for (i = 0; i < length - 1; i++) {1049 int j = i + rand() / (RAND_MAX / (length - i) + 1);1050 int t = clause[i]; clause[i] = clause[j]; clause[j] = t; } } }10511052int parse (struct solver* S) {1053 int tmp, active = 0, retvalue = SAT;1054 int del = 0, fileLine = 0;1055 int *buffer, bufferAlloc;10561057 S->nVars = 0;1058 S->nClauses = 0;1059 do { tmp = fscanf (S->inputFile, " cnf %i %li \n", &S->nVars, &S->nClauses); // Read the first line1060 if (tmp > 0 && tmp != EOF) break; tmp = fscanf (S->inputFile, "%*s\n"); } // In case a commment line was found1061 while (tmp != 2 && tmp != EOF); // Skip it and read next line1062 int nZeros = S->nClauses;10631064 if (!S->nVars && !S->nClauses) {1065 printf ("\rc ERROR: did not find p cnf line in input file\n"); exit (0); }10661067 printf ("\rc parsing input formula with %i variables and %li clauses\n", S->nVars, S->nClauses);10681069 bufferAlloc = INIT;1070 buffer = (int*) malloc (sizeof (int) * bufferAlloc);10711072 S->count = 1;1073 S->nStep = 0;1074 S->mem_used = 0; // The number of integers allocated in the DB10751076 long size;1077 long DBsize = S->mem_used + BIGINIT;1078 S->DB = (int*) malloc (DBsize * sizeof (int));1079 if (S->DB == NULL) { free (buffer); return ERROR; }10801081 S->maxVar = 0;1082 S->maxSize = 0;1083 S->nLemmas = 0;1084 S->nAlloc = BIGINIT;1085 S->formula = (long *) malloc (sizeof (long) * S->nClauses);1086 S->proof = (long *) malloc (sizeof (long) * S->nAlloc);1087 long **hashTable = (long**) malloc (sizeof (long*) * BIGINIT);1088 int *hashUsed = (int * ) malloc (sizeof (int ) * BIGINIT);1089 int *hashMax = (int * ) malloc (sizeof (int ) * BIGINIT);10901091 int i;1092 for (i = 0; i < BIGINIT; i++) {1093 hashUsed [i] = 0;1094 hashMax [i] = INIT;1095 hashTable[i] = (long*) malloc (sizeof (long) * hashMax[i]); }10961097 int fileSwitchFlag = 0;1098 long finalClause = 0;1099 size = 0;1100 while (1) {1101 int lit = 0; tmp = 0;1102 fileSwitchFlag = nZeros <= 0;11031104 if (size == 0) {1105 if (fileSwitchFlag) { // read for proof1106 if (S->binMode == 1) {1107 int res = getc_unlocked (S->proofFile);1108 if (res == EOF) break;1109 else if (res == 97) del = 0;1110 else if (res == 100) del = 1;1111 else {1112 if (S->warning != NOWARNING) {1113 printf ("\rc WARNING: wrong binary prefix, stop reading proof\n"); break; }1114 if (S->warning == HARDWARNING) exit (HARDWARNING); }1115 S->nReads++; }1116 else {1117 tmp = fscanf (S->proofFile, " d %i ", &lit);1118 if (tmp == EOF) break;1119 del = tmp > 0; } } }11201121 if (!lit) {1122 if (!fileSwitchFlag) tmp = fscanf (S->inputFile, " %i ", &lit); // Read a literal.1123 else {1124 if (S->binMode == 1) {1125 tmp = read_lit (S, &lit); }1126 else {1127 tmp = fscanf (S->proofFile, " %i ", &lit); } }1128 if (tmp == EOF && !fileSwitchFlag) {1129 if (S->warning != NOWARNING) {1130 printf ("\rc WARNING: early EOF of the input formula\n");1131 printf ("\rc WARNING: %i clauses less than expected\n", nZeros); }1132 if (S->warning == HARDWARNING) exit (HARDWARNING);1133 fileLine = 0;1134 fileSwitchFlag = 1; } }11351136 if (!tmp && !S->binMode) {1137 char ignore[1<<16];1138 if (!fileSwitchFlag) { if (fgets (ignore, sizeof (ignore), S->inputFile) == NULL) printf ("c\n"); }1139 else if (fgets (ignore, sizeof (ignore), S->proofFile) == NULL) printf ("c\n");1140 if (ignore[0] != 'c') continue;1141 for (i = 0; i < sizeof ignore; i++) { if (ignore[i] == '\n') break; }1142 if (i == sizeof ignore) {1143 printf ("c ERROR: comment longer than %zu characters: %s\n", sizeof ignore, ignore);1144 exit (HARDWARNING); }1145 if (S->verb) printf ("\rc WARNING: parsing mismatch assuming a comment\n");1146 continue; }11471148 if (abs (lit) > S->maxVar) S->maxVar = abs (lit);1149 if (tmp == EOF && fileSwitchFlag) break;1150 if (abs (lit) > S->nVars && !fileSwitchFlag) {1151 printf ("\rc illegal literal %i due to max var %i\n", lit, S->nVars); exit (0); }1152 if (!lit) {1153 fileLine++;1154 if (size > S->maxSize) S->maxSize = size;1155 int pivot = buffer[0];1156 buffer[size] = 0;1157 qsort (buffer, size, sizeof (int), compare);1158 int j = 0;1159 for (i = 0; i < size; ++i) {1160 if (buffer[i] == buffer[i+1]) {1161 if (S->warning != NOWARNING) {1162 printf ("\rc WARNING: detected and deleted duplicate literal %i at position %i of proof line %i\n", buffer[i+1], i+1, fileLine); }1163 if (S->warning == HARDWARNING) exit (HARDWARNING); }1164 else { buffer[j++] = buffer[i]; } }1165 buffer[j] = 0; size = j;11661167 if (size == 0 && !fileSwitchFlag) retvalue = UNSAT;1168 if (del && S->mode == BACKWARD_UNSAT && size <= 1) {1169 if (S->warning != NOWARNING) {1170 printf ("\rc WARNING: backward mode ignores deletion of (pseudo) unit clause ");1171 printClause (buffer); }1172 if (S->warning == HARDWARNING) exit (HARDWARNING);1173 del = 0; size = 0; continue; }1174 int rem = buffer[0];1175 buffer[size] = 0;1176 unsigned int hash = getHash (buffer);1177 if (del) {1178 if (S->delete) {1179 long match = 0;1180 match = matchClause (S, hashTable[hash], hashUsed[hash], buffer, size);1181 if (match == 0) {1182 if (S->warning != NOWARNING) {1183 printf ("\rc WARNING: deleted clause on proof line %i does not occur: ", fileLine); printClause (buffer); }1184 if (S->warning == HARDWARNING) exit (HARDWARNING);1185 goto end_delete; }1186 if (S->mode == FORWARD_SAT) S->DB[ match - 2 ] = rem;1187 hashUsed[hash]--;1188 active--;1189 if (S->nStep == S->nAlloc) { S->nAlloc = (S->nAlloc * 3) >> 1;1190 S->proof = (long*) realloc (S->proof, sizeof (long) * S->nAlloc);1191// printf ("c proof allocation increased to %li\n", S->nAlloc);1192 if (S->proof == NULL) { printf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } }1193 S->proof[S->nStep++] = (match << INFOBITS) + 1; }1194 end_delete:;1195 if (del) { del = 0; size = 0; continue; } }11961197 if (S->mem_used + size + EXTRA >= DBsize) { DBsize = (DBsize * 3) >> 1;1198 S->DB = (int *) realloc (S->DB, DBsize * sizeof (int));1199// printf("c database increased to %li\n", DBsize);1200 if (S->DB == NULL) { printf("c MEMOUT: reallocation of clause database failed\n"); exit (0); } }1201 int *clause = &S->DB[S->mem_used + EXTRA - 1];1202 if (size != 0) clause[PIVOT] = pivot;1203 clause[ID] = 2 * S->count; S->count++;1204 finalClause = S->mem_used + EXTRA - 1;1205 if (S->mode == FORWARD_SAT) if (nZeros > 0) clause[ID] |= ACTIVE;12061207 for (i = 0; i < size; ++i) { clause[ i ] = buffer[ i ]; } clause[ i ] = 0;1208 S->mem_used += size + EXTRA;12091210 hash = getHash (clause);1211 if (hashUsed[hash] == hashMax[hash]) { hashMax[hash] = (hashMax[hash] * 3) >> 1;1212 hashTable[hash] = (long *) realloc (hashTable[hash], sizeof (long*) * hashMax[hash]);1213 if (hashTable[hash] == NULL) { printf("c MEMOUT reallocation of hash table %i failed\n", hash); exit (0); } }1214 hashTable[ hash ][ hashUsed[hash]++ ] = (long) (clause - S->DB);12151216 active++;1217 if (nZeros > 0) { // if still parsing the formula1218 S->formula[S->nClauses - nZeros] = (((long) (clause - S->DB)) << INFOBITS); }1219 else {1220 if (S->nStep == S->nAlloc) { S->nAlloc = (S->nAlloc * 3) >> 1;1221 S->proof = (long*) realloc (S->proof, sizeof (long) * S->nAlloc);1222// printf ("c proof allocation increased to %li\n", S->nAlloc);1223 if (S->proof == NULL) { printf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } }1224 S->proof[S->nStep++] = (((long) (clause - S->DB)) << INFOBITS); }12251226 if (nZeros <= 0) S->nLemmas++;12271228 if (!nZeros) S->lemmas = (long) (clause - S->DB); // S->lemmas is no longer pointer1229 size = 0; del = 0; --nZeros; } // Reset buffer1230 else {1231 buffer[size++] = lit; // Add literal to buffer1232 if (size == bufferAlloc) { bufferAlloc = (bufferAlloc * 3) >> 1;1233 buffer = (int*) realloc (buffer, sizeof (int) * bufferAlloc);1234 if (buffer == NULL) {1235 printf ("c MEMOUT: failed to reallocate buffer\n"); exit (0); } } } }12361237 if (S->mode == FORWARD_SAT && active) {1238 if (S->warning != NOWARNING)1239 printf ("\rc WARNING: %i clauses active if proof succeeds\n", active);1240 if (S->warning == HARDWARNING) exit (HARDWARNING);1241 for (i = 0; i < BIGINIT; i++) {1242 int j;1243 for (j = 0; j < hashUsed[i]; j++) {1244 printf ("\rc ");1245 int *clause = S->DB + hashTable [i][j];1246 printClause (clause);1247 if (S->nStep == S->nAlloc) { S->nAlloc = (S->nAlloc * 3) >> 1;1248 S->proof = (long*) realloc (S->proof, sizeof (long) * S->nAlloc);1249// printf ("c proof allocation increased to %li\n", S->nAlloc);1250 if (S->proof == NULL) { printf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } }1251 S->proof[S->nStep++] = (((long) (clause - S->DB)) << INFOBITS) + 1; } } }12521253 S->DB = (int *) realloc (S->DB, S->mem_used * sizeof (int));1254 if (S->mem_used && S->DB == NULL) { printf("c MEMOUT: reallocation of DB failed\n"); exit (0); }12551256 for (i = 0; i < BIGINIT; i++) free (hashTable[i]);1257 free (hashTable);1258 free (hashUsed);1259 free (hashMax);1260 free (buffer);12611262 int *clause = &S->DB[finalClause];1263 if (clause) clause[ID] |= ACTIVE; // temporary12641265 printf ("\rc finished parsing");1266 if (S->nReads) printf (", read %li bytes from proof file", S->nReads);1267 printf ("\n");12681269 int n = S->maxVar;1270 S->falseStack = (int *) malloc (( n + 1) * sizeof (int )); // Stack of falsified literals -- this pointer is never changed1271 S->reason = (long *) malloc (( n + 1) * sizeof (long)); // Array of clauses1272 S->used = (int *) malloc ((2 * n + 1) * sizeof (int )); S->used += n; // Labels for variables, non-zero means false1273 S->max = (int *) malloc ((2 * n + 1) * sizeof (int )); S->max += n; // Labels for variables, non-zero means false1274 S->falseA = (int *) malloc ((2 * n + 1) * sizeof (int )); S->falseA += n; // Labels for variables, non-zero means false1275 S->setMap = (int *) malloc ((2 * n + 1) * sizeof (int )); S->setMap += n; // Labels for variables, non-zero means false1276 S->setTruth = (int *) malloc ((2 * n + 1) * sizeof (int )); S->setTruth += n; // Labels for variables, non-zero means false12771278 S->optproof = (long *) malloc (sizeof(long) * (2 * S->nLemmas + S->nClauses));12791280 S->maxRAT = INIT;1281 S->RATset = (long*) malloc (sizeof (long) * S->maxRAT);1282 for (i = 0; i < S->maxRAT; i++) S->RATset[i] = 0; // is this required?12831284 S->preRAT = (int*) malloc (sizeof (int) * n);12851286 S->lratAlloc = INIT;1287 S->lratSize = 0;1288 S->lratTable = (int *) malloc (sizeof(int ) * S->lratAlloc);1289 S->lratLookup = (long *) malloc (sizeof(long) * (S->count + 1));12901291 S->maxDependencies = INIT;1292 S->dependencies = (int*) malloc (sizeof (int) * S->maxDependencies);1293 for (i = 0; i < S->maxDependencies; i++) S->dependencies[i] = 0; // is this required?12941295 S->wlist = (long**) malloc (sizeof (long*) * (2*n+1)); S->wlist += n;12961297 for (i = 1; i <= n; ++i) { S->max [ i] = S->max [-i] = INIT;1298 S->setMap [ i] = S->setMap [-i] = 0;1299 S->setTruth[ i] = S->setTruth[-i] = 0;1300 S->wlist [ i] = (long*) malloc (sizeof (long) * S->max[ i]);1301 S->wlist [-i] = (long*) malloc (sizeof (long) * S->max[-i]); }13021303 S->unitStackSize = INIT;1304 S->unitStack = (long *) malloc (sizeof (long) * S->unitStackSize);13051306 return retvalue; }13071308void freeMemory (struct solver *S) {1309 free (S->DB);1310 free (S->falseStack);1311 free (S->reason);1312 free (S->proof);1313 free (S->formula);1314 int i;1315 for (i = 1; i <= S->maxVar; ++i) { free (S->wlist[i]); free (S->wlist[-i]); }1316 free (S->used - S->maxVar);1317 free (S->max - S->maxVar);1318 free (S->falseA - S->maxVar);1319 free (S->wlist - S->maxVar);1320 free (S->RATset);1321 free (S->dependencies);1322 return; }13231324int onlyDelete (struct solver* S, int begin, int end) {1325 int step;1326 for (step = begin; step < end; step++)1327 if ((S->proof[step] & 1) == 0) return 0;1328 return 1; }13291330void printHelp ( ) {1331 printf ("usage: drat-trim [INPUT] [<PROOF>] [<option> ...]\n\n");1332 printf ("where <option> is one of the following\n\n");1333 printf (" -h print this command line option summary\n");1334 printf (" -c CORE prints the unsatisfiable core to the file CORE (DIMACS format)\n");1335 printf (" -a ACTIVE prints the active clauses to the file ACTIVE (DIMACS format)\n");1336 printf (" -l LEMMAS prints the core lemmas to the file LEMMAS (DRAT format)\n");1337 printf (" -L LEMMAS prints the core lemmas to the file LEMMAS (LRAT format)\n");1338 printf (" -r TRACE resolution graph in the TRACE file (TRACECHECK format)\n\n");1339 printf (" -t <lim> time limit in seconds (default %i)\n", TIMEOUT);1340 printf (" -u default unit propatation (i.e., no core-first)\n");1341 printf (" -f forward mode for UNSAT\n");1342 printf (" -v more verbose output\n");1343 printf (" -b show progress bar\n");1344 printf (" -O optimize proof till fixpoint by repeating verification\n");1345 printf (" -C compress core lemmas (emit binary proof)\n");1346 printf (" -D delete proof file after parsing\n");1347 printf (" -I force ASCII proof parse mode\n");1348 printf (" -i force binary proof parse mode\n");1349 printf (" -w suppress warning messages\n");1350 printf (" -W exit after first warning\n");1351 printf (" -p run in plain mode (i.e., ignore deletion information)\n\n");1352 printf (" -R turn off reduce mode\n\n");1353 printf (" -S run in SAT check mode (forward checking)\n\n");1354 printf (" -U only allow RUP additions\n");1355 printf ("and input and proof are specified as follows\n\n");1356 printf (" INPUT input file in DIMACS format\n");1357 printf (" PROOF proof file in DRAT format (stdin if no argument)\n\n");1358 exit (0); }13591360int binChar (int c) {1361 // ASCII characters: 10 (LF), 13 (CR), 32 (' '), 45 ('-'), 48 ('0'), 57 ('9'), 99 ('c'), 100 ('d')1362 if ((c != 10) && (c != 13) && (c != 32) && (c != 45) && ((c < 48) || (c > 57)) && (c != 99) && (c != 100))1363 return 1;1364 return 0;1365}13661367int main (int argc, char** argv) {1368 struct solver S;13691370 S.inputFile = NULL;1371 S.proofFile = stdin;1372 S.coreStr = NULL;1373 S.activeFile = NULL;1374 S.lemmaStr = NULL;1375 S.lratFile = NULL;1376 S.traceFile = NULL;1377 S.timeout = TIMEOUT;1378 S.nReads = 0;1379 S.nWrites = 0;1380 S.mask = 0;1381 S.verb = 0;1382 S.delProof = 0;1383 S.backforce = 0;1384 S.optimize = 0;1385 S.warning = 0;1386 S.prep = 0;1387 S.bar = 0;1388 S.mode = BACKWARD_UNSAT;1389 S.delete = 1;1390 S.reduce = 1;1391 S.binMode = 0;1392 S.binOutput = 0;1393 S.rupOnly = 0;1394 gettimeofday (&S.start_time, NULL);13951396 int i, tmp = 0;1397 for (i = 1; i < argc; i++) {1398 if (argv[i][0] == '-') {1399 if (argv[i][1] == 'h') printHelp ();1400 else if (argv[i][1] == 'c') S.coreStr = argv[++i];1401 else if (argv[i][1] == 'a') S.activeFile = fopen (argv[++i], "w");1402 else if (argv[i][1] == 'l') S.lemmaStr = argv[++i];1403 else if (argv[i][1] == 'L') S.lratFile = fopen (argv[++i], "w");1404 else if (argv[i][1] == 'r') S.traceFile = fopen (argv[++i], "w");1405 else if (argv[i][1] == 't') S.timeout = atoi (argv[++i]);1406 else if (argv[i][1] == 'b') S.bar = 1;1407 else if (argv[i][1] == 'B') S.backforce = 1;1408 else if (argv[i][1] == 'O') S.optimize = 1;1409 else if (argv[i][1] == 'C') S.binOutput = 1;1410 else if (argv[i][1] == 'D') S.delProof = 1;1411 else if (argv[i][1] == 'i') S.binMode = 1;1412 else if (argv[i][1] == 'I') S.binMode = -1;1413 else if (argv[i][1] == 'u') S.mask = 1;1414 else if (argv[i][1] == 'v') S.verb = 1;1415 else if (argv[i][1] == 'w') S.warning = NOWARNING;1416 else if (argv[i][1] == 'W') S.warning = HARDWARNING;1417 else if (argv[i][1] == 'p') S.delete = 0;1418 else if (argv[i][1] == 'R') S.reduce = 0;1419 else if (argv[i][1] == 'f') S.mode = FORWARD_UNSAT;1420 else if (argv[i][1] == 'S') S.mode = FORWARD_SAT;1421 else if (argv[i][1] == 'U') S.rupOnly = 1; }1422 else {1423 tmp++;1424 if (tmp == 1) {1425 S.inputFile = fopen (argv[1], "r");1426 if (S.inputFile == NULL) {1427 printf ("\rc error opening \"%s\".\n", argv[i]); return ERROR; } }14281429 else if (tmp == 2) {1430 S.proofFile = fopen (argv[2], "r");1431 if (S.proofFile == NULL) {1432 printf ("\rc error opening \"%s\".\n", argv[i]); return ERROR; }14331434 int c, comment = 1;1435 if (S.binMode == 0) {1436 c = getc_unlocked (S.proofFile); // check the first character in the file1437 if (c == EOF) { S.binMode = 1; continue; }1438 if (binChar (c)) {1439 printf ("\rc turning on binary mode checking\n");1440 S.binMode = 1; }1441 if (c != 99) comment = 0; }1442 if (S.binMode == 0) {1443 c = getc_unlocked (S.proofFile); // check the second character in the file1444 if (c == EOF) { S.binMode = 1; continue; }1445 if (binChar (c)) {1446 printf ("\rc turning on binary mode checking\n");1447 S.binMode = 1; }1448 if (c != 32) comment = 0; }1449 if (S.binMode == 0) {1450 int j;1451 for (j = 0; j < 10; j++) {1452 c = getc_unlocked (S.proofFile);1453 if (c == EOF) break;1454 if (binChar (c) && (!comment || c < 65 || c > 122)) {1455 printf ("\rc turning on binary mode checking\n");1456 S.binMode = 1; break; } } }1457 fclose (S.proofFile);1458 if (S.binMode == -1) S.binMode = 0;1459 S.proofFile = fopen (argv[2], "r");1460 if (S.proofFile == NULL) {1461 printf ("\rc error opening \"%s\".\n", argv[i]); return ERROR; } } } }14621463 if (tmp == 1) printf ("\rc reading proof from stdin\n");1464 if (tmp == 0) printHelp ();14651466 int parseReturnValue = parse (&S);14671468 fclose (S.inputFile);1469 fclose (S.proofFile);14701471 if (S.mode == FORWARD_UNSAT) {1472 S.reduce = 0; }14731474 if (S.delProof && argv[2] != NULL) {1475 int ret = remove(argv[2]);1476 if (ret == 0) printf("c deleted proof %s\n", argv[2]); }14771478 int sts = ERROR;1479 if (parseReturnValue == ERROR) printf ("\rs MEMORY ALLOCATION ERROR\n");1480 else if (parseReturnValue == UNSAT) printf ("\rc trivial UNSAT\ns VERIFIED\n");1481 else if ((sts = verify (&S, -1, -1)) == UNSAT) printf ("\rs VERIFIED\n");1482 else if (sts == DERIVATION) printf ("\rs DERIVATION\n");1483 else printf ("\ns NOT VERIFIED\n") ;1484 struct timeval current_time;1485 gettimeofday (¤t_time, NULL);1486 long runtime = (current_time.tv_sec - S.start_time.tv_sec) * 1000000 +1487 (current_time.tv_usec - S.start_time.tv_usec);1488 printf ("\rc verification time: %.3f seconds\n", (double) (runtime / 1000000.0));14891490 if (S.optimize) {1491 printf("c proof optimization started (ignoring the timeout)\n");1492 int iteration = 1;1493 while (S.nRemoved && iteration < 10000) {1494 deactivate (&S);1495 shuffleProof (&S, iteration);1496 iteration++;1497 verify (&S, 0, 0); } }14981499 freeMemory (&S);1500 return (sts != UNSAT); // 0 on success, 1 on any failure1501}1502