File format

c
c start with comments
c
c 
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0

• The file can start with comments, that is lines begining with the character c.
• Right after the comments, there is the line p cnf nbvar nbclauses indicating that the instance is in CNF format; nbvar is the exact number of variables appearing in the file; nbclauses is the exact number of clauses contained in the file.
• Then the clauses follow. Each clause is a sequence of distinct non-null numbers between -nbvar and nbvar ending with 0 on the same line; it cannot contain the opposite literals i and -i simultaneously. Positive numbers denote the corresponding variables. Negative numbers denote the negations of the corresponding variables.

网址：

http://www.satcompetition.org/2009/format-benchmarks2009.html

1. SAT solvers that are planning to participate in the Main track must be able to produce certificates for UNSAT instances in tracecheck or DRAT (Delete Resolution Asymmetric Tautologies) format which is backwards compatible with the DRUP format of SAT Competition 2013.

2007, 2009, and 2011.

Probably the most important disadvantage of the RUP approach is the computational costs to validate a given proof. In order to reduce this disadvantage, we propose to add clause deletion information to the proof. Clause deletion is one of the features that allow SAT solvers to have strong performance. By communicating this information to a RUP proof checker, one can significantly reduce the costs to validate a proof. We refer to our proposed format as DRUP (delete RUP). Details about the format are described below.

[1] E.Goldberg, Y.Novikov.
Verification of proofs of unsatisfiability for CNF formulas.
Design, Automation and Test in Europe. March 2003, pp. 886--891.

• The lastest version of our fast DRUP checker (drup-trim.c). It combines backward RUP checking with watch literals to realize efficient performance. Additionally, DRUP-check can exploit clause deletion information in the proof. The description below explains how to add this information to a RUP proof.
• A compact implementation of a RUP checker (rup-forward.c). This checker is slightly more than 100 lines of code. In contrast to drup-check, rup-forward does not support clause deletion information. Also, it implements forward checking which can be useful for debugging purposes.

1. Negate R_i = [L_{ij}] producing one or more unit clauses, [-L_{ij}].
   For example, the negation of [x, y, z] is [-x], [-y], [-z].
   (When i = r, there are no unit clauses produced.)
2. Add these unit clauses [-L_{ij}] and R_1 through R_{i-1} to F.
   (When i = r, there are no unit clauses to add.)
3. Perform unit-clause propagation.

DRAT-trim is a satisfiability proof checking and trimming utility designed to validate proofs for all known satisfiability solving and preprocessing techniques. DRAT-trim can also emit trimmed formulas, optimized proofs, and TraceCheck+ dependency graphs.

详细信息见网址：https://www.cs.utexas.edu/~marijn/drat-trim/

   1 /************************************************************************************[drat-trim.c]
   2 Copyright (c) 2014 Marijn Heule and Nathan Wetzler, The University of Texas at Austin.
   3 Copyright (c) 2015-2018 Marijn Heule, The University of Texas at Austin.
   4 Last edit, October 30, 2018
   5 
   6 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
   7 associated documentation files (the "Software"), to deal in the Software without restriction,
   8 including without limitation the rights to use, copy, modify, merge, publish, distribute,
   9 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
  10 furnished to do so, subject to the following conditions:
  11 
  12 The above copyright notice and this permission notice shall be included in all copies or
  13 substantial portions of the Software.
  14 
  15 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
  16 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  17 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
  18 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
  19 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  20 **************************************************************************************************/
  21 
  22 #include 
  23 #include 
  24 #include 
  25 #include 
  26 
  27 #define TIMEOUT     20000
  28 #define BIGINIT     1000000
  29 #define INIT        4
  30 #define END         0
  31 #define UNSAT       0
  32 #define SAT         1
  33 #define ID         -1
  34 #define PIVOT      -2
  35 #define MAXDEP       -3
  36 #define EXTRA       4        // ID + PIVOT + MAXDEP + terminating 0
  37 #define INFOBITS    2        // could be 1 for SAT, must be 2 for QBF
  38 #define DBIT        1
  39 #define ASSUMED     2
  40 #define MARK        3
  41 #define ERROR      -1
  42 #define ACTIVE      1
  43 
  44 #define FORWARD_SAT      10
  45 #define FORWARD_UNSAT    20
  46 #define BACKWARD_UNSAT   30
  47 #define SUCCESS          40
  48 #define FAILED           50
  49 #define FIXPOINT     60
  50 #define NOWARNING     70
  51 #define HARDWARNING     80
  52 
  53 #define COMPRESS
  54 
  55 struct solver { FILE *inputFile, *proofFile, *lratFile, *traceFile, *activeFile;
  56     int *DB, nVars, timeout, mask, delete, *falseStack, *falseA, *forced, binMode, optimize, binOutput,
  57       *processed, *assigned, count, *used, *max, COREcount, RATmode, RATcount, nActive, *lratTable,
  58       nLemmas, maxRAT, *RATset, *preRAT, maxDependencies, nDependencies, bar, backforce, reduce,
  59       *dependencies, maxVar, maxSize, mode, verb, unitSize, prep, *current, nRemoved, warning,
  60       delProof, *setMap, *setTruth;
  61     char *coreStr, *lemmaStr;
  62     struct timeval start_time;
  63     long mem_used, time, nClauses, nStep, nOpt, nAlloc, *unitStack, *reason, lemmas, nResolve,
  64          nReads, nWrites, lratSize, lratAlloc, *lratLookup, **wlist, *optproof, *formula, *proof;  };
  65 
  66 static inline void assign (struct solver* S, int lit) {
  67   S->falseA[-lit] = 1; *(S->assigned++) = -lit; }
  68 
  69 int compare (const void *a, const void *b) {
  70   return (*(int*)a - *(int*)b); }
  71 
  72 int abscompare (const void *a, const void *b) {
  73   return (abs(*(int*)a) - abs(*(int*)b)); }
  74 
  75 static inline void printClause (int* clause) {
  76   printf ("[%i] ", clause[ID]);
  77   while (*clause) printf ("%i ", *clause++); printf ("0\n"); }
  78 
  79 static inline void addWatchPtr (struct solver* S, int lit, long watch) {
  80   if (S->used[lit] + 1 == S->max[lit]) { S->max[lit] *= 1.5;
  81     S->wlist[lit] = (long *) realloc (S->wlist[lit], sizeof (long) * S->max[lit]);
  82 //    if (S->max[lit] > 1000) printf("c watchlist %i increased to %i\n", lit, S->max[lit]);
  83     if (S->wlist[lit] == NULL) { printf("c MEMOUT: reallocation failed for watch list of %i\n", lit); exit (0); } }
  84   S->wlist[lit][ S->used[lit]++ ] = watch | S->mask;
  85   S->wlist[lit][ S->used[lit]   ] = END; }
  86 
  87 static inline void addWatch (struct solver* S, int* clause, int index) {
  88   addWatchPtr (S, clause[index], ((long) (((clause) - S->DB)) << 1)); }
  89 
  90 static inline void removeWatch (struct solver* S, int* clause, int index) {
  91   int i, lit = clause[index];
  92   if ((S->used[lit] > INIT) && (S->max[lit] > 2 * S->used[lit])) {
  93     S->max[lit] = (3 * S->used[lit]) >> 1;
  94     S->wlist[lit] = (long *) realloc (S->wlist[lit], sizeof (long) * S->max[lit]);
  95     assert(S->wlist[lit] != NULL); }
  96   long *watch = S->wlist[lit];
  97   for (i = 0; i < S->used[lit]; i++) {
  98     int* _clause = S->DB + (*(watch++) >> 1);
  99     if (_clause == clause) {
 100       watch[-1] = S->wlist[lit][ --S->used[lit] ];
 101       S->wlist[lit][ S->used[lit] ] = END; return; } } }
 102 
 103 static inline void addUnit (struct solver* S, long index) {
 104   S->unitStack[S->unitSize++] = index; }
 105 
 106 static inline void removeUnit (struct solver* S, int lit) {
 107   int i, found = 0;
 108   for (i = 0; i < S->unitSize; i++) {
 109     if (found) S->unitStack[i - 1] = S->unitStack[i];
 110     if (S->DB[ S->unitStack[i] ] == lit) found = 1; }
 111   S->unitSize--; }
 112 
 113 static inline void unassignUnit (struct solver* S, int lit) {
 114   if (S->verb)
 115     printf ("\rc removing unit %i\n", lit);
 116   while (S->falseA[-lit]) {
 117     if (S->verb)
 118       printf ("\rc removing unit %i (%i)\n", S->forced[-1], lit);
 119     S->falseA[*(--S->forced)] = 0;
 120     S->reason[abs(*S->forced)] = 0; }
 121   S->processed = S->assigned = S->forced; }
 122 
 123 static inline void markWatch (struct solver* S, int* clause, int index, int offset) {
 124   long* watch = S->wlist[ clause[ index ] ];
 125   for (;;) {
 126     int *_clause = (S->DB + (*(watch++) >> 1) + (long) offset);
 127     if (_clause == clause) { watch[ID] |= ACTIVE; return; } } }
 128 
 129 static inline void addDependency (struct solver* S, int dep, int forced) {
 130   if (1 || S->traceFile || S->lratFile) { // temporary for MAXDEP
 131     if (S->nDependencies == S->maxDependencies) {
 132       S->maxDependencies = (S->maxDependencies * 3) >> 1;
 133 //      printf ("c dependencies increased to %i\n", S->maxDependencies);
 134       S->dependencies = realloc (S->dependencies, sizeof (int) * S->maxDependencies);
 135       if (S->dependencies == NULL) { printf ("c MEMOUT: dependencies reallocation failed\n"); exit (0); } }
 136 //    printf("c adding dep %i\n", (dep << 1) + forced);
 137     S->dependencies[S->nDependencies++] = (dep << 1) + forced; } }
 138 
 139 static inline void markClause (struct solver* S, int* clause, int index) {
 140   S->nResolve++;
 141   addDependency (S, clause[index - 1] >> 1, (S->assigned > S->forced));
 142 
 143   if ((clause[index + ID] & ACTIVE) == 0) {
 144     S->nActive++;
 145     clause[index + ID] |= ACTIVE;
 146     if ((S->mode == BACKWARD_UNSAT) && clause[index + 1]) {
 147       S->optproof[S->nOpt++] = (((long) (clause - S->DB) + index) << INFOBITS) + 1; }
 148     if (clause[1 + index] == 0) return;
 149     markWatch (S, clause,     index, -index);
 150     markWatch (S, clause, 1 + index, -index); }
 151   while (*clause) S->falseA[*(clause++)] = MARK; }
 152 
 153 void analyze (struct solver* S, int* clause, int index) {     // Mark all clauses involved in conflict
 154   markClause (S, clause, index);
 155   while (S->assigned > S->falseStack) {
 156     int lit = *(--S->assigned);
 157     if (S->falseA[lit] == MARK) {
 158       if (S->reason[abs (lit)]) {
 159         markClause (S, S->DB + S->reason[abs (lit)], -1);
 160         if (S->assigned >= S->forced)
 161           S->reason[abs (lit)] = 0; } }
 162     else if (S->falseA[lit] == ASSUMED && !S->RATmode && S->reduce && !S->lratFile) { // Remove unused literal
 163       S->nRemoved++;
 164       int *tmp = S->current;
 165       while (*tmp != lit) tmp++;
 166       while (*tmp) { tmp[0] = tmp[1]; tmp++; }
 167       tmp[-1] = 0; }
 168     if (S->assigned >= S->forced) S->reason[abs (lit)] = 0;
 169     S->falseA[lit] = (S->assigned < S->forced); }
 170 
 171   S->processed = S->assigned = S->forced; }
 172 
 173 void noAnalyze (struct solver* S) {
 174   while (S->assigned > S->falseStack) {
 175     int lit = *(--S->assigned);
 176     if (S->assigned >= S->forced) S->reason[abs (lit)] = 0;
 177     S->falseA[lit] = (S->assigned < S->forced); }
 178 
 179   S->processed = S->assigned = S->forced; }
 180 
 181 int propagate (struct solver* S, int init, int mark) { // Performs unit propagation (init not used?)
 182   int *start[2];
 183   int check = 0, mode = !S->prep;
 184   int i, lit, _lit = 0; long *watch, *_watch;
 185   start[0] = start[1] = S->processed;
 186   flip_check:;
 187   check ^= 1;
 188   while (start[check] < S->assigned) {                 // While unprocessed false literals
 189     lit = *(start[check]++);                           // Get first unprocessed literal
 190     if (lit == _lit) watch = _watch;
 191     else watch = S->wlist[ lit ];                      // Obtain the first watch pointer
 192     while (*watch != END) {                            // While there are watched clauses (watched by lit)
 193      if ((*watch & mode) != check) {
 194         watch++; continue; }
 195      int *clause = S->DB + (*watch >> 1);           // Get the clause from DB
 196      if (S->falseA[ -clause[0] ] ||
 197          S->falseA[ -clause[1] ]) {
 198        watch++; continue; }
 199      if (clause[0] == lit) clause[0] = clause[1];      // Ensure that the other watched literal is in front
 200       for (i = 2; clause[i]; ++i)                      // Scan the non-watched literals
 201         if (S->falseA[ clause[i] ] == 0) {             // When clause[j] is not false, it is either true or unset
 202           clause[1] = clause[i]; clause[i] = lit;      // Swap literals
 203           addWatchPtr (S, clause[1], *watch);          // Add the watch to the list of clause[1]
 204           *watch = S->wlist[lit][ --S->used[lit] ];    // Remove pointer
 205           S->wlist[lit][ S->used[lit] ] = END;
 206           goto next_clause; }                          // Goto the next watched clause
 207       clause[1] = lit; watch++;                        // Set lit at clause[1] and set next watch
 208       if (!S->falseA[  clause[0] ]) {                  // If the other watched literal is falsified,
 209         assign (S, clause[0]);                         // A unit clause is found, and the reason is set
 210         S->reason[abs (clause[0])] = ((long) ((clause)-S->DB)) + 1;
 211         if (!check) {
 212           start[0]--; _lit = lit; _watch = watch;
 213           goto flip_check; } }
 214       else if (!mark) { noAnalyze (S); return UNSAT; }
 215       else { analyze (S, clause, 0); return UNSAT; }   // Found a root level conflict -> UNSAT
 216       next_clause: ; } }                               // Set position for next clause
 217   if (check) goto flip_check;
 218   S->processed = S->assigned;
 219   return SAT; }                                           // Finally, no conflict was found
 220 
 221 
 222 // Propagate top level units
 223 static inline int propagateUnits (struct solver* S, int init) {
 224   int i;
 225 //  printf("c propagateUnits %i\n", S->unitSize);
 226   while (S->forced > S->falseStack) {
 227     S->falseA[*(--S->forced)] = 0;
 228     S->reason[abs (*S->forced)] = 0; }
 229   S->forced = S->assigned = S->processed = S->falseStack;
 230   for (i = 0; i < S->unitSize; i++) {
 231     int lit = S->DB[ S->unitStack[i] ];
 232     S->reason[abs (lit)] = S->unitStack[i] + 1;
 233     assign (S, lit); }
 234 
 235   if (propagate (S, init, 1) == UNSAT) { return UNSAT; }
 236   S->forced = S->processed;
 237   return SAT; }
 238 
 239 // Put falsified literals at the end and returns the size under the current
 240 // assignment: negative size means satisfied, size = 0 means falsified
 241 int sortSize (struct solver *S, int *lemma) {
 242   unsigned int size = 0, last = 0, sat = 1;
 243   while (lemma[last]) {
 244     int lit = lemma[last++];
 245     if (S->falseA[lit] == 0) {
 246       if (S->falseA[-lit]) sat = -1;
 247       lemma[last-1] = lemma[ size ];
 248       lemma[size++] = lit; } }
 249   return sat * size; }
 250 
 251 // print the core clauses to coreFile in DIMACS format
 252 void printCore (struct solver *S) {
 253   int i, j;
 254   for (i = 0; i < S->nClauses; i++) {
 255     int *clause = S->DB + (S->formula[i] >> INFOBITS);
 256     if (clause[ID] & ACTIVE) S->COREcount++; }
 257   printf ("\rc %i of %li clauses in core                            \n", S->COREcount, S->nClauses);
 258 
 259   if (S->coreStr) {
 260     FILE *coreFile = fopen (S->coreStr, "w");
 261     fprintf (coreFile, "p cnf %i %i\n", S->nVars, S->COREcount);
 262     for (i = 0; i < S->nClauses; i++) {
 263       int *clause = S->DB + (S->formula[i] >> INFOBITS);
 264       if (clause[ID] & ACTIVE) {
 265         while (*clause) fprintf (coreFile, "%i ", *clause++);
 266         fprintf (coreFile, "0\n"); } }
 267     fclose (coreFile); } }
 268 
 269 void write_lit (struct solver *S, FILE *output, int lit) { // change to long?
 270   unsigned int l = abs (lit) << 1;
 271   if (lit < 0) l++;
 272 
 273   do {
 274     if (l <= 127) { fputc ((char)                 l, output); }
 275     else          { fputc ((char) (128 + (l & 127)), output); }
 276     S->nWrites++;
 277     l = l >> 7; }
 278   while (l); }
 279 
 280 void printLRATline (struct solver *S, int time) {
 281   int *line = S->lratTable + S->lratLookup[time];
 282   if (S->binOutput) {
 283     fputc ('a', S->lratFile); S->nWrites++;
 284     while (*line) write_lit (S, S->lratFile, *line++);
 285     write_lit (S, S->lratFile, *line++);
 286     while (*line) write_lit (S, S->lratFile, *line++);
 287     write_lit (S, S->lratFile, *line++); }
 288   else {
 289     while (*line) fprintf (S->lratFile, "%i ", *line++);
 290     fprintf (S->lratFile, "%i ", *line++);
 291     while (*line) fprintf (S->lratFile, "%i ", *line++);
 292     fprintf (S->lratFile, "%i\n", *line++); } }
 293 
 294 // print the core lemmas to lemmaFile in DRAT format
 295 void printProof (struct solver *S) {
 296   int step;
 297   printf ("\rc %i of %i lemmas in core using %lu resolution steps\n", S->nActive - S->COREcount + 1, S->nLemmas + 1, S->nResolve);
 298   printf ("\rc %d RAT lemmas in core; %i redundant literals in core lemmas\n", S->RATcount, S->nRemoved);
 299 
 300   // NB: not yet working with forward checking
 301   if (S->mode == FORWARD_UNSAT) {
 302     printf ("\rc optimized proofs are not supported for forward checking\n");
 303     return; }
 304 
 305   // replace S->proof by S->optproof
 306   if (S->mode == BACKWARD_UNSAT) {
 307     if (S->nOpt > S->nAlloc) {
 308       S->nAlloc = S->nOpt;
 309       S->proof = (long*) realloc (S->proof, sizeof (long) * S->nAlloc);
 310       if (S->proof == NULL) { printf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } }
 311     S->nStep   = 0;
 312     S->nLemmas = 0;
 313     for (step = S->nOpt - 1; step >= 0; step--) {
 314       long ad = S->optproof[step];
 315       int *lemmas = S->DB + (ad >> INFOBITS);
 316       if ((ad & 1) == 0) S->nLemmas++;
 317 //      if (lemmas[ID] & ACTIVE) lemmas[ID] ^= ACTIVE; // only useful for checking multiple times?
 318       S->proof[S->nStep++] = S->optproof[step]; } }  // why not reuse ad?
 319 
 320   if (S->lemmaStr) {
 321     FILE *lemmaFile = fopen (S->lemmaStr, "w");
 322     for (step = 0; step < S->nStep; step++) {
 323       long ad = S->proof[step];
 324       int *lemmas = S->DB + (ad >> INFOBITS);
 325       if (!lemmas[1] && (ad & 1)) continue; // don't delete unit clauses
 326       if (S->binOutput) {
 327         S->nWrites++;
 328         if (ad & 1) fputc ('d', lemmaFile);
 329         else        fputc ('a', lemmaFile); }
 330       else if (ad & 1) fprintf (lemmaFile, "d ");
 331       int reslit = lemmas[PIVOT];
 332       while (*lemmas) {
 333         int lit = *lemmas++;
 334         if (lit == reslit) {
 335           if (S->binOutput) write_lit (S, lemmaFile, lit);
 336           else fprintf (lemmaFile, "%i ", lit); } }
 337       lemmas = S->DB + (ad >> INFOBITS);
 338       while (*lemmas) {
 339         int lit = *lemmas++;
 340         if (lit != reslit) {
 341           if (S->binOutput) write_lit (S, lemmaFile, lit);
 342           else fprintf (lemmaFile, "%i ", lit); } }
 343       if (S->binOutput) write_lit (S, lemmaFile, 0);
 344       else fprintf (lemmaFile, "0\n"); }
 345     if (S->binOutput) { fputc ('a', lemmaFile); write_lit (S, lemmaFile, 0); }
 346     else fprintf (lemmaFile, "0\n");
 347     fclose (lemmaFile); }
 348 
 349   if (S->lratFile) {
 350     int lastAdded = S->nClauses;
 351     int flag = 0;
 352     for (step = 0; step < S->nStep; step++) {
 353       long ad = S->proof[step];
 354       int *lemmas = S->DB + (ad >> INFOBITS);
 355       if ((ad & 1) == 0) {
 356         if (lastAdded == 0) {
 357           if (S->binOutput) {
 358             write_lit (S, S->lratFile, 0); }
 359           else {
 360             fprintf (S->lratFile, "0\n"); } }
 361         lastAdded = lemmas[ID] >> 1;
 362         printLRATline (S, lastAdded); }
 363       else if (lastAdded == S->nClauses) continue;
 364       else if (!lemmas[1] && (ad & 1)) continue; // don't delete unit clauses
 365       else if (ad & 1) {
 366         if (lastAdded != 0) {
 367           if (S->binOutput) {
 368             fputc ('d', S->lratFile); S->nWrites++; }
 369           else {
 370             fprintf (S->lratFile, "%i d ", lastAdded); } }
 371         lastAdded = 0;
 372         if (S->binOutput) {
 373           write_lit (S, S->lratFile, lemmas[ID] >> 1); }
 374         else {
 375           fprintf (S->lratFile, "%i ", lemmas[ID] >> 1); } } }
 376     if (lastAdded != S->nClauses) {
 377       if (S->binOutput) {
 378         write_lit (S, S->lratFile, 0); }
 379       else {
 380         fprintf(S->lratFile, "0\n"); } }
 381 
 382     printLRATline (S, S->count);
 383 
 384     fclose (S->lratFile);
 385     if (S->nWrites)
 386       printf ("c wrote optimized proof in LRAT format of %li bytes\n", S->nWrites); } }
 387 
 388 void printNoCore (struct solver *S) {
 389   if (S->lratFile) {
 390     if (S->binOutput) {
 391       fputc ('d', S->lratFile); S->nWrites++; }
 392     else {
 393       fprintf (S->lratFile, "%ld d ", S->nClauses); }
 394     int i;
 395     for (i = 0; i < S->nClauses; i++) {
 396       int *clause = S->DB + (S->formula[i] >> INFOBITS);
 397       if ((clause[ID] & ACTIVE) == 0) {
 398         if (S->binOutput) {
 399           write_lit (S, S->lratFile, clause[ID] >> 1); }
 400         else {
 401           fprintf (S->lratFile, "%i ", clause[ID] >> 1); } } }
 402     if (S->binOutput) {
 403       write_lit (S, S->lratFile, 0); }
 404     else {
 405       fprintf (S->lratFile, "0\n"); } } }
 406 
 407 // print the dependency graph to traceFile in TraceCheck+ format
 408 // this procedure adds the active clauses at the end of the trace
 409 void printTrace (struct solver *S) {
 410   if (S->traceFile) { int i;
 411     for (i = 0; i < S->nClauses; i++) {
 412       int *clause = S->DB + (S->formula[i] >> INFOBITS);
 413       if (clause[ID] & ACTIVE) {
 414         fprintf (S->traceFile, "%i ", i + 1);
 415         while (*clause) fprintf (S->traceFile, "%i ", *clause++);
 416         fprintf (S->traceFile, "0 0\n"); } }
 417     fclose (S->traceFile); } }
 418 
 419 void printActive (struct solver *S) {
 420   int i, j;
 421   if (S->activeFile) {
 422     for (i = -S->maxVar; i <= S->maxVar; i++)
 423       if (i != 0)
 424         for (j = 0; j < S->used[i]; j++) {
 425           int *clause = S->DB + (S->wlist[i][j] >> 1);
 426           if (*clause == i) {
 427             while (*clause)
 428               fprintf (S->activeFile, "%i ", *clause++);
 429             fprintf (S->activeFile, "0\n"); } } } }
 430 
 431 void postprocess (struct solver *S) {
 432   printNoCore (S);   // print before proof optimization
 433   printActive (S);
 434   printCore   (S);
 435   printTrace  (S);   // closes traceFile
 436   printProof  (S); } // closes lratFile
 437 
 438 void lratAdd (struct solver *S, int elem) {
 439   if (S->lratSize == S->lratAlloc) {
 440     S->lratAlloc = S->lratAlloc * 3 >> 1;
 441     S->lratTable = (int *) realloc (S->lratTable, sizeof (int) * S->lratAlloc); }
 442   S->lratTable[S->lratSize++] = elem; }
 443 
 444 void printDependenciesFile (struct solver *S, int* clause, int RATflag, int mode) {
 445   FILE *file = NULL;
 446   if (mode == 0) file = S->traceFile;
 447   if (mode == 1) file = S->lratFile;
 448 
 449   if (file) {
 450     int i, j, k;
 451     int tmp = S->lratSize;
 452 
 453     if (clause != NULL) {
 454            S->lratLookup[clause[ID] >> 1] = S->lratSize; }
 455     else { S->lratLookup[S->count] = S->lratSize;   }
 456 
 457     if (clause != NULL) {
 458       int size = 0;
 459       int *sortClause;
 460       sortClause = (int *) malloc (sizeof(int) * S->maxSize);
 461       lratAdd (S, S->time >> 1); // NB: long to ing
 462       int reslit = clause[PIVOT];
 463       while (*clause) {
 464         if (*clause == reslit)
 465           lratAdd (S, reslit);
 466         sortClause[size++] = *clause++; }
 467       qsort (sortClause, size, sizeof (int), abscompare);
 468       for (i = 0; i < size; i++) {
 469         int lit = sortClause[i];
 470         if (lit != reslit)
 471           lratAdd (S, lit); } }
 472     else { lratAdd (S, S->count); }
 473     lratAdd (S, 0);
 474 
 475     int isRUP = 1;
 476     for (i = 0; i < S->nDependencies; i++)
 477       if (S->dependencies[i] < 0) { isRUP = 0; break; }
 478 
 479     if (isRUP) {
 480       for (i = S->nDependencies - 1; i >= 0; i--)
 481         lratAdd (S, S->dependencies[i] >> 1);
 482       lratAdd (S, 0);
 483       goto printLine; }
 484 
 485     // first print the preRAT units in order of becoming unit
 486     int size = 0;
 487     for (i = 0; i < S->nDependencies; i++) {
 488       if (S->dependencies[i] > 0) continue;
 489       for (j = i - 1; j >= 0 && S->dependencies[j] > 0; j--) {
 490         int flag = 0;
 491         int cls  = S->dependencies[j];
 492         if (cls & 1) continue;
 493         for (k = 0; k < size; k++)
 494           if (S->preRAT[k] == cls) flag = 1;
 495         if (!flag) {
 496           S->preRAT[size++] = cls;
 497           lratAdd (S, cls >> 1); } } }
 498 
 499     // print dependencies in order of becoming unit
 500     for (i = S->nDependencies - 1; i >= 0; i--) {
 501       int cls = S->dependencies[i];
 502       if ((mode == 0) && (cls < 0)) continue;
 503       if (mode == 0) {
 504         int flag = 0;
 505         for (j = 0; j < size; j++)
 506           if (S->preRAT[j] == cls) flag = 1;
 507         if (!flag) {
 508           S->preRAT[size++] = cls;
 509           lratAdd (S, cls >> 1); } }
 510       if ((mode == 1) && (cls & 1))
 511         lratAdd (S, cls >> 1); }
 512       lratAdd (S, 0);
 513 
 514     printLine:;
 515     if (mode == 0) {
 516       for (i = tmp; i < S->lratSize; i++)
 517         fprintf (file, "%d ", S->lratTable[i]);
 518       S->lratSize = tmp;
 519       fprintf (file, "\n"); } } }
 520 
 521 void printDependencies (struct solver *S, int* clause, int RATflag) {
 522   if (clause != NULL) {
 523     int i;
 524     clause[MAXDEP] = 0;
 525     for (i = 0; i < S->nDependencies; i++) {
 526 //      printf ("%i ", S->dependencies[i]);
 527       if (S->dependencies[i] > clause[MAXDEP])
 528         clause[MAXDEP] = S->dependencies[i]; }
 529 //    printf("\n%i :", clause[MAXDEP]);
 530 //    printClause(clause);
 531     assert (clause[MAXDEP] < clause[ID]);
 532   }
 533 
 534   printDependenciesFile (S, clause, RATflag, 0);
 535   printDependenciesFile (S, clause, RATflag, 1); }
 536 
 537 int checkRAT (struct solver *S, int pivot, int mark) {
 538   int i, j, nRAT = 0;
 539 
 540   // Loop over all literals to calculate resolution candidates
 541   for (i = -S->maxVar; i <= S->maxVar; i++) {
 542     if (i == 0) continue;
 543     // Loop over all watched clauses for literal
 544     for (j = 0; j < S->used[i]; j++) {
 545       int* watched = S->DB + (S->wlist[i][j] >> 1);
 546       int id = watched[ID] >> 1;
 547       int active = watched[ID] & ACTIVE;
 548       if (*watched == i) { // If watched literal is in first position
 549     while (*watched)
 550           if (*watched++ == -pivot) {
 551             if ((S->mode == BACKWARD_UNSAT) && !active) {
 552 //              printf ("\rc RAT check ignores unmarked clause : "); printClause (S->DB + (S->wlist[i][j] >> 1));
 553               continue; }
 554         if (nRAT == S->maxRAT) {
 555           S->maxRAT = (S->maxRAT * 3) >> 1;
 556           S->RATset = realloc (S->RATset, sizeof (int) * S->maxRAT);
 557               assert (S->RATset != NULL); }
 558         S->RATset[nRAT++] = S->wlist[i][j] >> 1;
 559             break; } } } }
 560 
 561   // S->prep = 1;
 562   // Check all clauses in RATset for RUP
 563   int flag = 1;
 564   qsort (S->RATset, nRAT, sizeof (int), compare);
 565   S->nDependencies = 0;
 566   for (i = nRAT - 1; i >= 0; i--) {
 567     int* RATcls = S->DB + S->RATset[i];
 568     int id = RATcls[ID] >> 1;
 569     int blocked = 0;
 570     long int reason  = 0;
 571     if (S->verb) {
 572       printf ("\rc RAT clause: "); printClause (RATcls); }
 573 
 574     while (*RATcls) {
 575       int lit = *RATcls++;
 576       if (lit != -pivot && S->falseA[-lit])
 577         if (!blocked || reason > S->reason[abs (lit)])
 578           blocked = lit, reason = S->reason[abs (lit)]; }
 579 
 580     if (blocked && reason) {
 581       analyze (S, S->DB + reason, -1);
 582       S->reason[abs (blocked)] = 0; }
 583 
 584     if (!blocked) {
 585       RATcls = S->DB + S->RATset[i];
 586       while (*RATcls) {
 587         int lit = *RATcls++;
 588         if (lit != -pivot && !S->falseA[lit]) {
 589           assign (S, -lit); S->reason[abs (lit)] = 0; } }
 590       if (propagate (S, 0, mark) == SAT) { flag  = 0; break; } }
 591     addDependency (S, -id, 1); }
 592 
 593   if (flag == 0) {
 594     while (S->forced < S->assigned) {
 595       S->falseA[*(--S->assigned)] = 0;
 596       S->reason[abs (*S->assigned)] = 0; }
 597     if (S->verb) printf ("\rc RAT check on pivot %i failed\n", pivot);
 598     return FAILED; }
 599 
 600   return SUCCESS; }
 601 
 602 int setUCP (struct solver *S, int *cnf, int *trail) {
 603   int touched = 0, satisfied = 1;
 604   int *clause = cnf;
 605 
 606   while (*clause) {
 607     int *literals = clause;
 608     int unit = 0, sat = 0, und = 0;
 609     int i;
 610     while (*literals) {
 611       int lit = *literals++;
 612       if (S->setTruth[ lit ] == 1) { sat = 1; }
 613       if (S->setTruth[ lit ] == 0) { und++; unit = lit; } }
 614     clause = literals + 1;
 615     if (!sat && und == 1) {
 616       sat = 1;
 617       touched = 1;
 618       *trail++ = unit;
 619       *trail   = 0;
 620       if (S->verb) printf("c found unit %i\n", unit);
 621       S->setTruth[ unit] =  1;
 622       S->setTruth[-unit] = -1; }
 623     satisfied &= sat;
 624     if (!sat && !und) return FAILED; }
 625 
 626   *trail = 0;
 627   if (satisfied) return SUCCESS;
 628   if ( touched ) return setUCP (S, cnf, trail);
 629   return FIXPOINT; }
 630 
 631 /*
 632 int setDLL (struct solver *S, int *cnf, int *trail) {
 633   int res = setUCP (S, cnf, trail);
 634   if (res == SUCCESS) return SUCCESS;
 635   if (res == FAILED ) return FAILED;
 636   while (*trail) trail++;
 637 
 638   int decision = 1;
 639   while (S->setTruth[decision]) decision++;
 640 
 641   *trail++ = decision;
 642   *trail   = 0;
 643   S->setTruth[ decision] =  1;
 644   S->setTruth[-decision] = -1;
 645 
 646   if (S->verb) printf("c branch on %i\n", decision);
 647   if (setDLL (S, cnf, trail) == SUCCESS) return SUCCESS;
 648 
 649   while (*trail) trail++;
 650   while (*trail != decision) {
 651     S->setTruth[ *trail] = 0;
 652     S->setTruth[-*trail] = 0;
 653     trail--; }
 654 
 655   *trail++ = -decision;
 656   *trail = 0;
 657   S->setTruth[ decision] = -1;
 658   S->setTruth[-decision] =  1;
 659 
 660   if (S->verb) printf("c branch on %i\n", -decision);
 661   return setDLL (S, cnf, trail); }
 662 
 663 int setRedundancyCheck (struct solver *S, int *clause, int size, int uni) {
 664   int i, j, blocked, nSPR = 0;
 665   long int reason;
 666 
 667   int *trail = (int*) malloc (sizeof(int) * (size + 1));
 668 
 669   if (S->verb) printf("c starting SPR check\n");
 670 
 671   for (i = 1; i <= size; i++) {
 672     trail            [i - 1]  =  0;
 673     S->setMap[ clause[i - 1]] =  i;
 674     S->setMap[-clause[i - 1]] = -i; }
 675 
 676   // Loop over all literals to calculate resolution candidates
 677   for (i = -S->maxVar; i <= S->maxVar; i++) {
 678     if (i == 0) continue;
 679     // Loop over all watched clauses for literal
 680     for (j = 0; j < S->used[i]; j++) {
 681       int* watchedClause = S->DB + (S->wlist[i][j] >> 1);
 682       if (*watchedClause == i) { // If watched literal is in first position
 683         int flag = 0;
 684         blocked = 0;
 685         reason = 0;
 686         while (*watchedClause) {
 687           int lit = *watchedClause++;
 688           if (S->setMap[lit] < 0) flag = 1;
 689           else if (!S->setMap[lit] && S->falseA[-lit]) {
 690             if (blocked == 0 || reason > S->reason[ abs(lit) ])
 691               blocked = lit, reason = S->reason[ abs(lit) ]; } }
 692 
 693        if (blocked != 0 && reason != 0 && flag == 1) {
 694          analyze (S, S->DB + reason, -1); S->reason[abs(blocked)] = 0; }
 695 
 696        // If resolution candidate, add to list
 697        if (blocked == 0 && flag == 1) {
 698          if (nSPR == S->maxRAT) {
 699            S->maxRAT = (S->maxRAT * 3) >> 1;
 700            S->RATset = realloc(S->RATset, sizeof(int) * S->maxRAT); }
 701          S->RATset[nSPR++] = S->wlist[i][j] >> 1; } } } }
 702 
 703   // Check all candidates for RUP
 704   int cnfSize = size + 2; // first clause + terminating zero
 705   int filtered = 0;
 706   for (i = 0; i < nSPR; i++) {
 707     int inSet = 1;
 708     int* candidate = S->DB + S->resolutionCandidates[i];
 709     if (S->verb) {
 710       printf("c candidate: "); printLiterals (candidate); }
 711     while (*candidate) { int lit = *candidate++;
 712       if (S->setMap[lit]) inSet++;
 713       if (!S->setMap[lit] && !S->falseA[lit]) {
 714         ASSIGN(-lit); S->reason[abs(lit)] = 0; } }
 715     if (propagate (S, 0) == SAT) {
 716       if (S->verb) printf(" FAILED\n");
 717       cnfSize += inSet;
 718       S->processed = S->forced;
 719       while (S->forced < S->assigned) S->falseA[*(--S->assigned)] = 0;
 720       S->resolutionCandidates[filtered++] = S->resolutionCandidates[i]; }
 721     else {
 722       if (S->verb) printf(" SUCCESS\n"); } }
 723 
 724   int *cnf = (int*) malloc (sizeof(int) * cnfSize);
 725   int *tmp = cnf;
 726   for (i = 1; i <= size; i++) *tmp++ = i;
 727   *tmp++ = 0;
 728   numCandidates = filtered;
 729   for (i = 0; i < numCandidates; i++) {
 730     int* candidate = S->DB + S->resolutionCandidates[i];
 731     while (*candidate) {
 732       int lit = *candidate++;
 733       if (S->setMap[lit]) *tmp++ = S->setMap[lit]; }
 734     *tmp++ = 0; }
 735   *tmp++ = 0;
 736 
 737   if (S->verb) {
 738     tmp = cnf;
 739     printf("c printing CNF:\n");
 740     while (*tmp) {
 741       int *clause = tmp;
 742       printf("c ");
 743       while (*clause) printf("%i ", *clause++);
 744       printf("\n");
 745       tmp = clause + 1; } }
 746 
 747   int res = setDLL (S, cnf, trail);
 748   if (S->verb) {
 749     if (res == SUCCESS) printf("c SUCCESS\n");
 750     if (res == FAILED ) printf("c FAILED\n"); }
 751 
 752   for (i = 1; i <= size; i++) {
 753     S->setMap[ clause[i - 1]] = 0;
 754     S->setMap[-clause[i - 1]] = 0;
 755     S->setTruth[  i ]         = 0;
 756     S->setTruth[ -i ]         = 0; }
 757 
 758   free(trail);
 759   free( cnf );
 760   return res; }
 761 */
 762 
 763 int redundancyCheck (struct solver *S, int *clause, int size, int mark) {
 764   int i, indegree;
 765   int falsePivot = S->falseA[clause[PIVOT]];
 766   if (S->verb) { printf ("\rc checking lemma (%i, %i) ", size, clause[PIVOT]); printClause (clause); }
 767 
 768   if (S->mode != FORWARD_UNSAT) {
 769     if ((clause[ID] & ACTIVE) == 0) return SUCCESS; }  // redundant?
 770 //    clause[PIVOT] ^= ACTIVE; }
 771 
 772   if (size < 0) {
 773     S->DB[ S->reason[abs (*clause)] - 2] |= 1;
 774     return SUCCESS; }
 775 
 776   indegree = S->nResolve;
 777 
 778   S->RATmode = 0;
 779   S->nDependencies = 0;
 780   for (i = 0; i < size; ++i) {
 781     if (S->falseA[-clause[i]]) { // should only occur in forward mode
 782       if (S->warning != NOWARNING) {
 783         printf ("\rc WARNING: found a tautological clause in proof: "); printClause (clause); }
 784       if (S->warning == HARDWARNING) exit (HARDWARNING);
 785       while (S->forced < S->assigned) {
 786         S->falseA[*(--S->assigned)] = 0;
 787         S->reason[abs (*S->assigned)] = 0; }
 788       return SUCCESS; }
 789     S->falseA[clause[i]] = ASSUMED;
 790     *(S->assigned++) = clause[i];
 791     S->reason[abs (clause[i])] = 0; }
 792 
 793   S->current = clause;
 794   if (propagate (S, 0, mark) == UNSAT) {
 795     indegree = S->nResolve - indegree;
 796     if (indegree <= 2 && S->prep == 0) {
 797       S->prep = 1; if (S->verb) printf ("\rc [%li] preprocessing checking mode on\n", S->time); }
 798     if (indegree  > 2 && S->prep == 1) {
 799       S->prep = 0; if (S->verb) printf ("\rc [%li] preprocessing checking mode off\n", S->time); }
 800     if (S->verb) printf ("\rc lemma has RUP\n");
 801     printDependencies (S, clause, 0);
 802     return SUCCESS; }
 803 
 804   // Failed RUP check.  Now test RAT.
 805   // printf ("RUP check failed.  Starting RAT check.\n");
 806   int reslit = clause[PIVOT];
 807   if (S->verb)
 808     printf ("\rc RUP checked failed; starting RAT check on pivot %d.\n", reslit);
 809 
 810   if (falsePivot) return FAILED;
 811 
 812   int* savedForced = S->forced;
 813 
 814   S->RATmode = 1;
 815   S->forced = S->assigned;
 816 
 817   int failed = 0;
 818   if (checkRAT (S, reslit, mark) == FAILED) {
 819     failed = 1;
 820     if (S->warning != NOWARNING) {
 821       printf ("\rc WARNING: RAT check on proof pivot failed : "); printClause (clause); }
 822     if (S->warning == HARDWARNING) exit (HARDWARNING);
 823     for (i = 0; i < size; i++) {
 824       if (clause[i] == reslit) continue;
 825       if (checkRAT (S, clause[i], mark) == SUCCESS) {
 826         clause[PIVOT] = clause[i];
 827         failed = 0; break; } } }
 828 
 829   if (failed == 0)
 830     printDependencies (S, clause, 1);
 831 
 832   S->processed = S->forced = savedForced;
 833   while (S->forced < S->assigned) {
 834     S->falseA[*(--S->assigned)] = 0;
 835     S->reason[abs (*S->assigned)] = 0; }
 836 
 837   if (failed) {
 838     printf ("c RAT check failed on all possible pivots\n");
 839     return FAILED; }
 840 
 841 
 842   if (mark) S->RATcount++;
 843   if (S->verb) printf ("\rc lemma has RAT on %i\n", clause[PIVOT]);
 844   return SUCCESS; }
 845 
 846 int init (struct solver *S) {
 847   S->forced     = S->falseStack; // Points inside *falseStack at first decision (unforced literal)
 848   S->processed  = S->falseStack; // Points inside *falseStack at first unprocessed literal
 849   S->assigned   = S->falseStack; // Points inside *falseStack at last unprocessed literal
 850 
 851   // initialize watch pointers on the original clauses
 852   S->RATmode    = 0;
 853   S->nRemoved   = 0;
 854   S->nOpt       = 0;
 855   S->nResolve   = 0;
 856   S->RATcount   = 0;
 857   S->nActive    = 0;
 858   S->COREcount  = 0;
 859   S->unitSize   = 0;
 860 
 861   int i;
 862   for (i = 1; i <= S->maxVar; ++i) {
 863     S->reason    [i]                   = 0;
 864     S->falseStack[i]                   = 0;
 865     S->falseA[i]    = S->falseA[-i]    = 0;
 866     S->used  [i]    = S->used  [-i]    = 0;
 867     S->wlist [i][0] = S->wlist [-i][0] = END; }
 868 
 869   for (i = 0; i < S->nClauses; i++) {
 870     int *clause = S->DB + (S->formula[i] >> INFOBITS);
 871     if (clause[ID] & ACTIVE) clause[ID] ^= ACTIVE;
 872     if (clause[0] == 0) {
 873       printf ("\rc formula contains empty clause\n");
 874       if (S->coreStr) {
 875         FILE *coreFile = fopen (S->coreStr, "w");
 876         fprintf (coreFile, "p cnf 0 1\n 0\n");
 877         fclose (coreFile); }
 878       if (S->lemmaStr) {
 879         FILE *lemmaFile = fopen (S->lemmaStr, "w");
 880         fprintf (lemmaFile, "0\n");
 881         fclose (lemmaFile); }
 882       return UNSAT; }
 883     if (clause[1]) { addWatch (S, clause, 0); addWatch (S, clause, 1); }
 884     else if (S->falseA[clause[0]]) {
 885       printf ("\rc found complementary unit clauses\n");
 886       if (S->coreStr) {
 887         FILE *coreFile = fopen (S->coreStr, "w");
 888         fprintf (coreFile, "p cnf %i 2\n%i 0\n%i 0\n", abs (clause[0]), clause[0], -clause[0]);
 889         fclose (coreFile); }
 890       if (S->lemmaStr) {
 891         FILE *lemmaFile = fopen (S->lemmaStr, "w");
 892         fprintf (lemmaFile, "0\n");
 893         fclose (lemmaFile); }
 894       if (S->lratFile) {
 895         int j;
 896         for (j = 0; j < i; j++) {
 897           int *_clause = S->DB + (S->formula[j] >> INFOBITS);
 898           if ((_clause[0] == -clause[0]) && !_clause[1]) break; }
 899         fprintf (S->lratFile, "%li 0 %i %i 0\n", S->nClauses + 1, j + 1, i + 1); }
 900       return UNSAT; }
 901     else if (!S->falseA[ -clause[0] ]) {
 902       addUnit (S, (long) (clause - S->DB));
 903       assign (S, clause[0]); } }
 904 
 905   S->nDependencies = 0;
 906   S->time = S->count; // Alternative time init
 907   if (propagateUnits (S, 1) == UNSAT) {
 908     printf ("\rc UNSAT via unit propagation on the input instance\n");
 909     printDependencies (S, NULL, 0);
 910     postprocess (S); return UNSAT; }
 911   return SAT; }
 912 
 913 int verify (struct solver *S, int begin, int end) {
 914   int top_flag = 1;
 915   if (init (S) == UNSAT) return UNSAT;
 916 
 917   if (S->mode == FORWARD_UNSAT) {
 918     if (begin == end)
 919       printf ("\rc start forward verification\n"); }
 920 
 921   int step;
 922   int adds = 0;
 923   int active = S->nClauses;
 924   for (step = 0; step < S->nStep; step++) {
 925     if (step >= begin && step < end) continue;
 926     long ad = S->proof[step]; long d = ad & 1;
 927     int *lemmas = S->DB + (ad >> INFOBITS);
 928 
 929     S->time = lemmas[ID];
 930     if (d) { active--; }
 931     else   { active++; adds++; }
 932     if (S->mode == FORWARD_SAT && S->verb) printf ("\rc %i active clauses\n", active);
 933 
 934     if (!lemmas[1]) { // found a unit
 935       int lit = lemmas[0];
 936       if (S->verb)
 937         printf ("\rc found unit in proof %i [%li]\n", lit, S->time);
 938       if (d) {
 939         if (S->mode == FORWARD_SAT) {
 940           removeUnit (S, lit); propagateUnits (S, 0); }
 941         else { // no need to remove units while checking UNSAT
 942           if (S->verb) { printf("c removing proof step: d "); printClause(lemmas); }
 943           S->proof[step] = 0; continue; } }
 944       else {
 945         if (S->mode == BACKWARD_UNSAT && S->falseA[-lit]) { S->proof[step] = 0; continue; }
 946         else { addUnit (S, (long) (lemmas - S->DB)); } } }
 947 
 948     if (d && lemmas[1]) { // if delete and not unit
 949       if ((S->reason[abs (lemmas[0])] - 1) == (lemmas - S->DB)) { // what is this check?
 950         if (S->mode != FORWARD_SAT) { // ignore pseudo unit clause deletion
 951           if (S->verb) { printf ("c ignoring deletion intruction %li: ", (lemmas - S->DB)); printClause (lemmas); }
 952 //        if (S->mode == BACKWARD_UNSAT) { // ignore pseudo unit clause deletion
 953           S->proof[step] = 0; }
 954         else { // if (S->mode == FORWARD_SAT) { // also for FORWARD_UNSAT?
 955           removeWatch (S, lemmas, 0), removeWatch (S, lemmas, 1);
 956           propagateUnits (S, 0); } }
 957       else {
 958         removeWatch (S, lemmas, 0), removeWatch (S, lemmas, 1); }
 959       if (S->mode == FORWARD_UNSAT ) continue;   // Ignore deletion of top-level units
 960       if (S->mode == BACKWARD_UNSAT) continue; }
 961 
 962     int size = sortSize (S, lemmas); // after removal of watches
 963 
 964     if (d && S->mode == FORWARD_SAT) {
 965       if (size == -1) propagateUnits (S, 0);  // necessary?
 966       if (redundancyCheck (S, lemmas, size, 1) == FAILED)  {
 967         printf ("c failed at proof line %i (modulo deletion errors)\n", step + 1);
 968         return SAT; }
 969       continue; }
 970 
 971     if (d == 0 && S->mode == FORWARD_UNSAT) {
 972       if (step > end) {
 973         if (size < 0) continue; // Fix of bus error: 10
 974         if (redundancyCheck (S, lemmas, size, 1) == FAILED) {
 975           printf ("c failed at proof line %i (modulo deletion errors)\n", step + 1);
 976           return SAT; }
 977 
 978         size = sortSize (S, lemmas);
 979         S->nDependencies = 0; } }
 980 
 981     if (lemmas[1])
 982       addWatch (S, lemmas, 0), addWatch (S, lemmas, 1);
 983 
 984     if (size == 0) { printf ("\rc conflict claimed, but not detected\n"); return SAT; }  // change to FAILED?
 985     if (size == 1) {
 986       if (S->verb) printf ("\rc found unit %i\n", lemmas[0]);
 987       assign (S, lemmas[0]); S->reason[abs (lemmas[0])] = ((long) ((lemmas)-S->DB)) + 1;
 988       if (propagate (S, 1, 1) == UNSAT) goto start_verification;
 989       S->forced = S->processed; } }
 990 
 991   if (S->mode == FORWARD_SAT && active == 0) {
 992     postprocess (S); return UNSAT; }
 993 
 994   if (S->mode == FORWARD_UNSAT) {
 995     if (begin == end) {
 996       postprocess (S);
 997       printf ("\rc ERROR: all lemmas verified, but no conflict\n"); }
 998     return SAT; }
 999 
1000   if (S->mode == BACKWARD_UNSAT) {
1001     if (S->backforce) {
1002       int s;
1003       for (s = 0; s < step; s++) {
1004         long ad = S->proof[s];
1005         int *clause = S->DB + (ad >> INFOBITS);
1006         if (sortSize(S, clause) >= 0) {
1007           if ( (ad & 1) && (clause[ID] & 1)) clause[ID] ^= ACTIVE;
1008           if (!(ad & 1))                     clause[ID] |= ACTIVE; } } }
1009     if (!S->backforce) {
1010       printf ("\rc ERROR: no conflict\n");
1011       return SAT; } }
1012 
1013   start_verification:;
1014   if (S->mode == FORWARD_UNSAT) {
1015     printDependencies (S, NULL, 0);
1016     postprocess (S); return UNSAT; }
1017 
1018   if (!S->backforce)
1019     printDependencies (S, NULL, 0);
1020 
1021   if (S->mode == FORWARD_SAT) {
1022     printf ("\rc ERROR: found empty clause during SAT check\n"); exit (0); }
1023   printf ("\rc detected empty clause; start verification via backward checking\n");
1024 
1025   S->forced = S->processed;
1026   assert (S->mode == BACKWARD_UNSAT); // only reachable in BACKWARD_UNSAT mode
1027 
1028   S->nOpt = 0;
1029 
1030   int checked = 0, skipped = 0;
1031 
1032   double max = (double) adds;
1033 
1034   struct timeval backward_time;
1035   gettimeofday (&backward_time, NULL);
1036   for (; step >= 0; step--) {
1037     struct timeval current_time;
1038     gettimeofday (&current_time, NULL);
1039     int seconds = (int) (current_time.tv_sec - S->start_time.tv_sec);
1040     if ((seconds > S->timeout) && (S->optimize == 0)) printf ("s TIMEOUT\n"), exit (0);
1041 
1042     if (S->bar)
1043       if ((adds % 1000) == 0) {
1044         int f;
1045         long runtime = (current_time.tv_sec  - backward_time.tv_sec ) * 1000000 +
1046                        (current_time.tv_usec - backward_time.tv_usec);
1047         double time = (double) (runtime / 1000000.0);
1048         double fraction = (adds * 1.0) / max;
1049         printf("\rc %.2f%% [", 100.0 * (1.0 - fraction));
1050         for (f = 1; f <= 20; f++) {
1051           if ((1.0 - fraction) * 20.0 < 1.0 * f) printf(" ");
1052           else printf("="); }
1053         printf("] time remaining: %.2f seconds ", time / (1.0 - fraction) - time);
1054         if (step == 0) printf("\n");
1055         fflush (stdout); }
1056 
1057     long ad = S->proof[step]; long d = ad & 1;
1058     int *clause = S->DB + (ad >> INFOBITS);
1059 
1060 
1061     if (ad == 0) continue; // Skip lemma that has been removed from proof
1062     if ( d == 0) {
1063       adds--;
1064       if (clause[1]) {
1065         removeWatch (S, clause, 0), removeWatch (S, clause, 1);
1066         if (S->reason[abs (clause[0])] == (clause + 1 - S->DB)) {  // use this check also for units?
1067           unassignUnit (S, clause[0]); } }
1068       else unassignUnit (S, clause[0]); }
1069 
1070     int size = sortSize (S, clause);
1071 
1072     if (d) {
1073       if (S->verb) { printf ("\rc adding clause (%i) ", size); printClause (clause); }
1074       addWatch (S, clause, 0), addWatch (S, clause, 1); continue; }
1075 
1076     S->time = clause[ID];
1077     if ((S->time & ACTIVE) == 0) {
1078       skipped++;
1079 //      if ((skipped % 100) == 0) printf("c skipped %i, checked %i\n", skipped, checked);
1080       continue; } // If not marked, continue
1081 
1082     assert (size >= 1);
1083     int *_clause = clause + size;
1084     while (*_clause++) { S->nRemoved++; }
1085     clause[size] = 0;
1086 
1087     if (S->verb) {
1088       printf ("\rc validating clause (%i, %i):  ", clause[PIVOT], size); printClause (clause); }
1089 /*
1090     int i;
1091     if (size > 1 && (top_flag == 1)) {
1092       int last = clause[size - 1];
1093       int pivot = clause[PIVOT];
1094       for (i = 0; i < size; i++) {
1095         int tmp = clause[i];
1096         clause[i] = last;
1097         clause[size - 1] = 0;
1098         if (tmp == pivot) clause[PIVOT] = clause[0];
1099         if (redundancyCheck (S, clause, size - 1, 0) != FAILED) {
1100           top_flag = 0;
1101           size = size - 1; break; }
1102         else {
1103           clause[i] = tmp;
1104           clause[size - 1] = last; }
1105         clause[PIVOT] = pivot; } }
1106 */
1107     if (redundancyCheck (S, clause, size, 1) == FAILED) {
1108       printf ("c failed at proof line %i (modulo deletion errors)\n", step + 1);
1109       return SAT; }
1110     checked++;
1111     S->optproof[S->nOpt++] = ad; }
1112 
1113   postprocess (S);
1114   return UNSAT; }
1115 
1116 long matchClause (struct solver* S, long *clauselist, int listsize, int* input, int size) {
1117   int i, j;
1118   for (i = 0; i < listsize; ++i) {
1119     int *clause = S->DB + clauselist[i];
1120     for (j = 0; j <= size; j++)
1121       if (clause[j] != input[j]) goto match_next;
1122 
1123     long result = clauselist[i];
1124     clauselist[i] = clauselist[--listsize];
1125     return result;
1126     match_next:; }
1127   return 0; }
1128 
1129 unsigned int getHash (int* input) {
1130   unsigned int sum = 0, prod = 1, xor = 0;
1131   while (*input) {
1132     prod *= *input; sum += *input; xor ^= *input; input++; }
1133   return (1023 * sum + prod ^ (31 * xor)) % BIGINIT; }
1134 
1135 int read_lit (struct solver *S, int *lit) {
1136   int l = 0, lc, shift = 0;
1137   do {
1138     lc = getc_unlocked (S->proofFile);
1139     S->nReads++;
1140     if ((shift == 0) && (lc == EOF)) return EOF;
1141     l |= (lc & 127) << shift;
1142     shift += 7; }
1143   while (lc > 127);
1144   if (l % 2) *lit = (l >> 1) * -1;
1145   else       *lit = (l >> 1);
1146   return 1; }
1147 
1148 void deactivate (struct solver *S) {
1149   S->nActive = 0;
1150   int step;
1151   for (step = 0; step < S->nStep; step++) {
1152     if ((S->proof[step] & 1) == 0) {
1153       int *clause = S->DB + (S->proof[step] >> INFOBITS);
1154       if (clause[ID] & ACTIVE) clause[ID] ^= ACTIVE; } }
1155 }
1156 
1157 void shuffleProof (struct solver *S, int iteration) {
1158   int i, step, _step;
1159 
1160   double base = 100;
1161   for (i = 1; i < iteration; i++)
1162     base *= 1.1;
1163 
1164   // randomly remove clause deletion steps
1165   for (_step = 0, step = 0; step < S->nStep; step++) {
1166     if (S->proof[step] & 1) {
1167       int length = 0;
1168       int *clause = S->DB + (S->proof[step] >> INFOBITS);
1169       while (*clause) { length++; clause++; }
1170       if ((rand() % 1000) < (base * iteration / length)) continue; }
1171     S->proof[_step++] = S->proof[step]; }
1172   S->nStep = _step;
1173 
1174   for (step = S->nStep - 1; step > 0; step--) {
1175     long a = S->proof[step  ];
1176     if (a & DBIT) continue;
1177     long b = S->proof[step-1];
1178     if (b & DBIT) {
1179       S->proof[step  ] = b;
1180       S->proof[step-1] = a; }
1181     else {
1182       int *c = S->DB + (a >> INFOBITS);
1183       int *d = S->DB + (b >> INFOBITS);
1184       int coinflip = 0;
1185 //      int coinflip = rand () / (RAND_MAX >> 1);
1186       if (c[MAXDEP] < d[MAXDEP] || (coinflip && (c[MAXDEP] < d[ID]))) {
1187         int tmp = d[ID];
1188         d[ID] = c[ID];
1189         c[ID] = tmp;
1190         S->proof[step  ] = b;
1191         S->proof[step-1] = a; } } }
1192 
1193   for (step = 0; step < S->nStep; step++) {
1194     long ad = S->proof[step];
1195     if (ad & 1) continue;
1196     int *clause = S->DB + (ad >> INFOBITS);
1197     int i, length = 0;
1198     while (*clause) { length++; clause++; }
1199     clause = S->DB + (ad >> INFOBITS);
1200     for (i = 0; i < length - 1; i++) {
1201       int j = i + rand() / (RAND_MAX / (length - i) + 1);
1202       int t = clause[i]; clause[i] = clause[j]; clause[j] = t; } } }
1203 
1204 int parse (struct solver* S) {
1205   int tmp, active = 0, retvalue = SAT;
1206   int del = 0, fileLine = 0;
1207   int *buffer, bufferAlloc;
1208 
1209   S->nVars    = 0;
1210   S->nClauses = 0;
1211   do { tmp = fscanf (S->inputFile, " cnf %i %li \n", &S->nVars, &S->nClauses); // Read the first line
1212     if (tmp > 0 && tmp != EOF) break; tmp = fscanf (S->inputFile, "%*s\n"); }  // In case a commment line was found
1213   while (tmp != 2 && tmp != EOF);                                              // Skip it and read next line
1214   int nZeros = S->nClauses;
1215 
1216   if (!S->nVars && !S->nClauses) {
1217     printf ("\rc ERROR: did not find p cnf line in input file\n"); exit (0); }
1218 
1219   printf ("\rc parsing input formula with %i variables and %li clauses\n", S->nVars, S->nClauses);
1220 
1221   bufferAlloc = INIT;
1222   buffer = (int*) malloc (sizeof (int) * bufferAlloc);
1223 
1224   S->count    = 1;
1225   S->nStep    = 0;
1226   S->mem_used = 0;                  // The number of integers allocated in the DB
1227 
1228   long size;
1229   long DBsize = S->mem_used + BIGINIT;
1230   S->DB = (int*) malloc (DBsize * sizeof (int));
1231   if (S->DB == NULL) { free (buffer); return ERROR; }
1232 
1233   S->maxVar  = 0;
1234   S->maxSize = 0;
1235   S->nLemmas = 0;
1236   S->nAlloc  = BIGINIT;
1237   S->formula = (long *) malloc (sizeof (long) * S->nClauses);
1238   S->proof   = (long *) malloc (sizeof (long) * S->nAlloc);
1239   long **hashTable = (long**) malloc (sizeof (long*) * BIGINIT);
1240   int   *hashUsed  = (int * ) malloc (sizeof (int  ) * BIGINIT);
1241   int   *hashMax   = (int * ) malloc (sizeof (int  ) * BIGINIT);
1242 
1243   int i;
1244   for (i = 0; i < BIGINIT; i++) {
1245     hashUsed [i] = 0;
1246     hashMax  [i] = INIT;
1247     hashTable[i] = (long*) malloc (sizeof (long) * hashMax[i]); }
1248 
1249   int fileSwitchFlag = 0;
1250   size = 0;
1251   while (1) {
1252     int lit = 0; tmp = 0;
1253     fileSwitchFlag = nZeros <= 0;
1254 
1255     if (size == 0) {
1256       if (fileSwitchFlag) { // read for proof
1257         if (S->binMode) {
1258           int res = getc_unlocked (S->proofFile);
1259           if      (res == EOF) break;
1260           else if (res ==  97) del = 0;
1261           else if (res == 100) del = 1;
1262           else { printf ("\rc ERROR: wrong binary prefix\n"); exit (0); }
1263           S->nReads++; }
1264         else {
1265           tmp = fscanf (S->proofFile, " d  %i ", &lit);
1266           if (tmp == EOF) break;
1267           del = tmp > 0; } } }
1268 
1269     if (!lit) {
1270       if (!fileSwitchFlag) tmp = fscanf (S->inputFile, " %i ", &lit);  // Read a literal.
1271       else {
1272         if (S->binMode) {
1273           tmp = read_lit (S, &lit); }
1274         else {
1275           tmp = fscanf (S->proofFile, " %i ", &lit); } }
1276       if (tmp == EOF && !fileSwitchFlag) {
1277         if (S->warning != NOWARNING) {
1278           printf ("\rc WARNING: early EOF of the input formula\n");
1279           printf ("\rc WARNING: %i clauses less than expected\n", nZeros); }
1280         if (S->warning == HARDWARNING) exit (HARDWARNING);
1281         fileLine = 0;
1282         fileSwitchFlag = 1; } }
1283 
1284     if (tmp == 0) {
1285       char ignore[1024];
1286       if (!fileSwitchFlag) { if (fgets (ignore, sizeof (ignore), S->inputFile) == NULL) printf ("c\n"); }
1287       else if (fgets (ignore, sizeof (ignore), S->proofFile) == NULL) printf ("c\n");
1288       for (i = 0; i < 1024; i++) { if (ignore[i] == '\n') break; }
1289       if (i == 1024) {
1290         printf ("c ERROR: comment longer than 1024 characters: %s\n", ignore);
1291         exit (HARDWARNING); }
1292       if (S->verb) printf ("\rc WARNING: parsing mismatch assuming a comment\n");
1293       continue; }
1294 
1295     if (abs (lit) > S->maxVar) S->maxVar = abs (lit);
1296     if (tmp == EOF && fileSwitchFlag) break;
1297     if (abs (lit) > S->nVars && !fileSwitchFlag) {
1298       printf ("\rc illegal literal %i due to max var %i\n", lit, S->nVars); exit (0); }
1299     if (!lit) {
1300       fileLine++;
1301       if (size > S->maxSize) S->maxSize = size;
1302       int pivot = buffer[0];
1303       buffer[size] = 0;
1304       qsort (buffer, size, sizeof (int), compare);
1305       int j = 0;
1306       for (i = 0; i < size; ++i) {
1307         if (buffer[i] == buffer[i+1]) {
1308           if (S->warning != NOWARNING) {
1309             printf ("\rc WARNING: detected and deleted duplicate literal %i at position %i of line %i\n", buffer[i+1], i+1, fileLine); }
1310           if (S->warning == HARDWARNING) exit (HARDWARNING); }
1311         else { buffer[j++] = buffer[i]; } }
1312       buffer[j] = 0; size = j;
1313 
1314       if (size == 0 && !fileSwitchFlag) retvalue = UNSAT;
1315       if (del && S->mode == BACKWARD_UNSAT && size <= 1)  {
1316         if (S->warning != NOWARNING) {
1317           printf ("\rc WARNING: backward mode ignores deletion of (pseudo) unit clause ");
1318           printClause (buffer); }
1319         if (S->warning == HARDWARNING) exit (HARDWARNING);
1320         del = 0; size = 0; continue; }
1321       int rem = buffer[0];
1322       buffer[size] = 0;
1323       unsigned int hash = getHash (buffer);
1324       if (del) {
1325         if (S->delete) {
1326           long match = 0;
1327             match = matchClause (S, hashTable[hash], hashUsed[hash], buffer, size);
1328             if (match == 0) {
1329               if (S->warning != NOWARNING) {
1330                 printf ("\rc WARNING: deleted clause on line %i does not occur: ", fileLine); printClause (buffer); }
1331               if (S->warning == HARDWARNING) exit (HARDWARNING);
1332               goto end_delete; }
1333             if (S->mode == FORWARD_SAT) S->DB[ match - 2 ] = rem;
1334             hashUsed[hash]--;
1335             active--;
1336             if (S->nStep == S->nAlloc) { S->nAlloc = (S->nAlloc * 3) >> 1;
1337               S->proof = (long*) realloc (S->proof, sizeof (long) * S->nAlloc);
1338 //              printf ("c proof allocation increased to %li\n", S->nAlloc);
1339               if (S->proof == NULL) { printf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } }
1340             S->proof[S->nStep++] = (match << INFOBITS) + 1; }
1341         end_delete:;
1342         if (del) { del = 0; size = 0; continue; } }
1343 
1344       if (S->mem_used + size + EXTRA > DBsize) { DBsize = (DBsize * 3) >> 1;
1345     S->DB = (int *) realloc (S->DB, DBsize * sizeof (int));
1346 //        printf("c database increased to %li\n", DBsize);
1347         if (S->DB == NULL) { printf("c MEMOUT: reallocation of clause database failed\n"); exit (0); } }
1348       int *clause = &S->DB[S->mem_used + EXTRA - 1];
1349       if (size != 0) clause[PIVOT] = pivot;
1350       clause[ID] = 2 * S->count; S->count++;
1351       if (S->mode == FORWARD_SAT) if (nZeros > 0) clause[ID] |= ACTIVE;
1352 
1353       for (i = 0; i < size; ++i) { clause[ i ] = buffer[ i ]; } clause[ i ] = 0;
1354       S->mem_used += size + EXTRA;
1355 
1356       hash = getHash (clause);
1357       if (hashUsed[hash] == hashMax[hash]) { hashMax[hash] = (hashMax[hash] * 3) >> 1;
1358         hashTable[hash] = (long *) realloc (hashTable[hash], sizeof (long*) * hashMax[hash]);
1359         if (hashTable[hash] == NULL) { printf("c MEMOUT reallocation of hash table %i failed\n", hash); exit (0); } }
1360       hashTable[ hash ][ hashUsed[hash]++ ] = (long) (clause - S->DB);
1361 
1362       active++;
1363       if (nZeros > 0) { // if still parsing the formula
1364         S->formula[S->nClauses - nZeros] = (((long) (clause - S->DB)) << INFOBITS); }
1365       else {
1366         if (S->nStep == S->nAlloc) { S->nAlloc = (S->nAlloc * 3) >> 1;
1367           S->proof = (long*) realloc (S->proof, sizeof (long) * S->nAlloc);
1368 //        printf ("c proof allocation increased to %li\n", S->nAlloc);
1369         if (S->proof == NULL) { printf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } }
1370         S->proof[S->nStep++] = (((long) (clause - S->DB)) << INFOBITS); }
1371 
1372       if (nZeros <= 0) S->nLemmas++;
1373 
1374       if (!nZeros) S->lemmas   = (long) (clause - S->DB); // S->lemmas is no longer pointer
1375       size = 0; del = 0; --nZeros; }                      // Reset buffer
1376    else {
1377      buffer[size++] = lit;                                // Add literal to buffer
1378      if (size == bufferAlloc) { bufferAlloc = (bufferAlloc * 3) >> 1;
1379        buffer = (int*) realloc (buffer, sizeof (int) * bufferAlloc); } } }
1380 
1381   if (S->mode == FORWARD_SAT && active) {
1382     if (S->warning != NOWARNING)
1383       printf ("\rc WARNING: %i clauses active if proof succeeds\n", active);
1384     if (S->warning == HARDWARNING) exit (HARDWARNING);
1385     for (i = 0; i < BIGINIT; i++) {
1386       int j;
1387       for (j = 0; j < hashUsed[i]; j++) {
1388         printf ("\rc ");
1389         int *clause = S->DB + hashTable [i][j];
1390         printClause (clause);
1391         if (S->nStep == S->nAlloc) { S->nAlloc = (S->nAlloc * 3) >> 1;
1392           S->proof = (long*) realloc (S->proof, sizeof (long) * S->nAlloc);
1393 //          printf ("c proof allocation increased to %li\n", S->nAlloc);
1394           if (S->proof == NULL) { printf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } }
1395         S->proof[S->nStep++] = (((int) (clause - S->DB)) << INFOBITS) + 1; } } }
1396 
1397   S->DB = (int *) realloc (S->DB, S->mem_used * sizeof (int));
1398 
1399   for (i = 0; i < BIGINIT; i++) free (hashTable[i]);
1400   free (hashTable);
1401   free (hashUsed);
1402   free (hashMax);
1403   free (buffer);
1404 
1405   printf ("\rc finished parsing");
1406   if (S->nReads) printf (", read %li bytes from proof file", S->nReads);
1407   printf ("\n");
1408 
1409   int n = S->maxVar;
1410   S->falseStack = (int  *) malloc ((    n + 1) * sizeof (int )); // Stack of falsified literals -- this pointer is never changed
1411   S->reason     = (long *) malloc ((    n + 1) * sizeof (long)); // Array of clauses
1412   S->used       = (int  *) malloc ((2 * n + 1) * sizeof (int )); S->used     += n; // Labels for variables, non-zero means false
1413   S->max        = (int  *) malloc ((2 * n + 1) * sizeof (int )); S->max      += n; // Labels for variables, non-zero means false
1414   S->falseA     = (int  *) malloc ((2 * n + 1) * sizeof (int )); S->falseA   += n; // Labels for variables, non-zero means false
1415   S->setMap     = (int  *) malloc ((2 * n + 1) * sizeof (int )); S->setMap   += n; // Labels for variables, non-zero means false
1416   S->setTruth   = (int  *) malloc ((2 * n + 1) * sizeof (int )); S->setTruth += n; // Labels for variables, non-zero means false
1417 
1418   S->optproof   = (long *) malloc (sizeof(long) * (2 * S->nLemmas + S->nClauses));
1419 
1420   S->maxRAT = INIT;
1421   S->RATset = (int*) malloc (sizeof (int) * S->maxRAT);
1422   for (i = 0; i < S->maxRAT; i++) S->RATset[i] = 0; // is this required?
1423 
1424   S->preRAT = (int*) malloc (sizeof (int) * n);
1425 
1426   S->lratAlloc  = INIT;
1427   S->lratSize   = 0;
1428   S->lratTable  = (int  *) malloc (sizeof(int ) * S->lratAlloc);
1429   S->lratLookup = (long *) malloc (sizeof(long) * (S->count + 1));
1430 
1431   S->maxDependencies = INIT;
1432   S->dependencies = (int*) malloc (sizeof (int) * S->maxDependencies);
1433   for (i = 0; i < S->maxDependencies; i++) S->dependencies[i] = 0;  // is this required?
1434 
1435   S->wlist = (long**) malloc (sizeof (long*) * (2*n+1)); S->wlist += n;
1436 
1437   for (i = 1; i <= n; ++i) { S->max     [ i] = S->max     [-i] = INIT;
1438                              S->setMap  [ i] = S->setMap  [-i] =    0;
1439                              S->setTruth[ i] = S->setTruth[-i] =    0;
1440                              S->wlist   [ i] = (long*) malloc (sizeof (long) * S->max[ i]);
1441                              S->wlist   [-i] = (long*) malloc (sizeof (long) * S->max[-i]); }
1442 
1443   S->unitStack = (long *) malloc (sizeof (long) * n);
1444 
1445   return retvalue; }
1446 
1447 void freeMemory (struct solver *S) {
1448   int i;
1449 //  printf("c database size %li; ", S->mem_used);
1450 //  int sum = 0;
1451 //  for (i = 1; i <= S->maxVar; i++)
1452 //    sum += S->max[i] + S->max[-i];
1453 //  printf(" watch pointers size %i.\n", sum);
1454 
1455   free (S->DB);
1456   free (S->falseStack);
1457   free (S->reason);
1458   free (S->proof);
1459   free (S->formula);
1460   for (i = 1; i <= S->maxVar; ++i) { free (S->wlist[i]); free (S->wlist[-i]); }
1461   free (S->used   - S->maxVar);
1462   free (S->max    - S->maxVar);
1463   free (S->falseA - S->maxVar);
1464   free (S->wlist  - S->maxVar);
1465   free (S->RATset);
1466   free (S->dependencies);
1467   return; }
1468 
1469 int onlyDelete (struct solver* S, int begin, int end) {
1470   int step;
1471   for (step = begin; step < end; step++)
1472     if ((S->proof[step] & 1) == 0) return 0;
1473   return 1; }
1474 
1475 void printHelp ( ) {
1476   printf ("usage: drat-trim [INPUT] [] [ ...]\n\n");
1477   printf ("where  is one of the following\n\n");
1478   printf ("  -h          print this command line option summary\n");
1479   printf ("  -c CORE     prints the unsatisfiable core to the file CORE (DIMACS format)\n");
1480   printf ("  -a ACTIVE   prints the active clauses to the file ACTIVE (DIMACS format)\n");
1481   printf ("  -l LEMMAS   prints the core lemmas to the file LEMMAS (DRAT format)\n");
1482   printf ("  -L LEMMAS   prints the core lemmas to the file LEMMAS (LRAT format)\n");
1483   printf ("  -r TRACE    resolution graph in the TRACE file (TRACECHECK format)\n\n");
1484   printf ("  -t     time limit in seconds (default %i)\n", TIMEOUT);
1485   printf ("  -u          default unit propatation (i.e., no core-first)\n");
1486   printf ("  -f          forward mode for UNSAT\n");
1487   printf ("  -v          more verbose output\n");
1488   printf ("  -b          show progress bar\n");
1489   printf ("  -O          optimize proof till fixpoint by repeating verification\n");
1490   printf ("  -C          compress core lemmas (emit binary proof)\n");
1491   printf ("  -D          delete proof file after parsing\n");
1492   printf ("  -i          force binary proof parse mode\n");
1493   printf ("  -w          suppress warning messages\n");
1494   printf ("  -W          exit after first warning\n");
1495   printf ("  -p          run in plain mode (i.e., ignore deletion information)\n\n");
1496   printf ("  -R          turn off reduce mode\n\n");
1497   printf ("  -S          run in SAT check mode (forward checking)\n\n");
1498   printf ("and input and proof are specified as follows\n\n");
1499   printf ("  INPUT       input file in DIMACS format\n");
1500   printf ("  PROOF       proof file in DRAT format (stdin if no argument)\n\n");
1501   exit (0); }
1502 
1503 int main (int argc, char** argv) {
1504   struct solver S;
1505 
1506   S.inputFile  = NULL;
1507   S.proofFile  = stdin;
1508   S.coreStr    = NULL;
1509   S.activeFile = NULL;
1510   S.lemmaStr   = NULL;
1511   S.lratFile   = NULL;
1512   S.traceFile  = NULL;
1513   S.timeout    = TIMEOUT;
1514   S.nReads     = 0;
1515   S.nWrites    = 0;
1516   S.mask       = 0;
1517   S.verb       = 0;
1518   S.delProof   = 0;
1519   S.backforce  = 0;
1520   S.optimize   = 0;
1521   S.warning    = 0;
1522   S.prep       = 0;
1523   S.bar        = 0;
1524   S.mode       = BACKWARD_UNSAT;
1525   S.delete     = 1;
1526   S.reduce     = 1;
1527   S.binMode    = 0;
1528   S.binOutput  = 0;
1529   gettimeofday (&S.start_time, NULL);
1530 
1531   int i, tmp = 0;
1532   for (i = 1; i < argc; i++) {
1533     if        (argv[i][0] == '-') {
1534       if      (argv[i][1] == 'h') printHelp ();
1535       else if (argv[i][1] == 'c') S.coreStr    = argv[++i];
1536       else if (argv[i][1] == 'a') S.activeFile = fopen (argv[++i], "w");
1537       else if (argv[i][1] == 'l') S.lemmaStr   = argv[++i];
1538       else if (argv[i][1] == 'L') S.lratFile   = fopen (argv[++i], "w");
1539       else if (argv[i][1] == 'r') S.traceFile  = fopen (argv[++i], "w");
1540       else if (argv[i][1] == 't') S.timeout    = atoi (argv[++i]);
1541       else if (argv[i][1] == 'b') S.bar        = 1;
1542       else if (argv[i][1] == 'B') S.backforce  = 1;
1543       else if (argv[i][1] == 'O') S.optimize   = 1;
1544       else if (argv[i][1] == 'C') S.binOutput  = 1;
1545       else if (argv[i][1] == 'D') S.delProof   = 1;
1546       else if (argv[i][1] == 'i') S.binMode    = 1;
1547       else if (argv[i][1] == 'u') S.mask       = 1;
1548       else if (argv[i][1] == 'v') S.verb       = 1;
1549       else if (argv[i][1] == 'w') S.warning    = NOWARNING;
1550       else if (argv[i][1] == 'W') S.warning    = HARDWARNING;
1551       else if (argv[i][1] == 'p') S.delete     = 0;
1552       else if (argv[i][1] == 'R') S.reduce     = 0;
1553       else if (argv[i][1] == 'f') S.mode       = FORWARD_UNSAT;
1554       else if (argv[i][1] == 'S') S.mode       = FORWARD_SAT; }
1555     else {
1556       tmp++;
1557       if (tmp == 1) {
1558         S.inputFile = fopen (argv[1], "r");
1559         if (S.inputFile == NULL) {
1560           printf ("\rc error opening \"%s\".\n", argv[i]); return ERROR; } }
1561 
1562       else if (tmp == 2) {
1563         S.proofFile = fopen (argv[2], "r");
1564         if (S.proofFile == NULL) {
1565           printf ("\rc error opening \"%s\".\n", argv[i]); return ERROR; }
1566 
1567        int c, comment = 1;
1568        if (S.binMode == 0) {
1569           c = getc_unlocked (S.proofFile); // check the first character in the file
1570           if (c == EOF) { S.binMode = 1; continue; }
1571           if ((c != 13) && (c != 32) && (c != 45) && ((c < 48) || (c > 57)) && (c != 99) && (c != 100)) {
1572              printf ("\rc turning on binary mode checking\n");
1573              S.binMode = 1; }
1574           if (c != 99) comment = 0; }
1575         if (S.binMode == 0) {
1576           c = getc_unlocked (S.proofFile); // check the second character in the file
1577           if (c == EOF) { S.binMode = 1; continue; }
1578           if ((c != 13) && (c != 32) && (c != 45) && ((c < 48) || (c > 57)) && (c != 99) && (c != 100)) {
1579              printf ("\rc turning on binary mode checking\n");
1580              S.binMode = 1; }
1581           if (c != 32) comment = 0; }
1582         if (S.binMode == 0) {
1583           int j;
1584           for (j = 0; j < 10; j++) {
1585             c = getc_unlocked (S.proofFile);
1586             if (c == EOF) break;
1587             if ((c != 100) && (c != 10) && (c != 13) && (c != 32) && (c != 45) && ((c < 48) || (c > 57)) && (comment && ((c < 65) || (c > 122))))  {
1588               printf ("\rc turning on binary mode checking\n");
1589               S.binMode = 1; break; } } }
1590         fclose (S.proofFile);
1591         S.proofFile = fopen (argv[2], "r");
1592         if (S.proofFile == NULL) {
1593           printf ("\rc error opening \"%s\".\n", argv[i]); return ERROR; } } } }
1594 
1595   if (tmp == 1) printf ("\rc reading proof from stdin\n");
1596   if (tmp == 0) printHelp ();
1597 
1598   int parseReturnValue = parse (&S);
1599 
1600   fclose (S.inputFile);
1601   fclose (S.proofFile);
1602 
1603   if (S.mode == FORWARD_UNSAT) {
1604     S.reduce = 0; }
1605 
1606   if (S.delProof && argv[2] != NULL) {
1607     int ret = remove(argv[2]);
1608     if (ret == 0) printf("c deleted proof %s\n", argv[2]); }
1609 
1610   int sts = ERROR;
1611   if       (parseReturnValue == ERROR)          printf ("\rs MEMORY ALLOCATION ERROR\n");
1612   else if  (parseReturnValue == UNSAT)          printf ("\rc trivial UNSAT\ns VERIFIED\n");
1613   else if  ((sts = verify (&S, -1, -1)) == UNSAT) printf ("\rs VERIFIED\n");
1614   else printf ("\ns NOT VERIFIED\n")  ;
1615   struct timeval current_time;
1616   gettimeofday (&current_time, NULL);
1617   long runtime = (current_time.tv_sec  - S.start_time.tv_sec) * 1000000 +
1618                  (current_time.tv_usec - S.start_time.tv_usec);
1619   printf ("\rc verification time: %.3f seconds\n", (double) (runtime / 1000000.0));
1620 
1621   if (S.optimize) {
1622     printf("c proof optimization started (ignoring the timeout)\n");
1623     int iteration = 1;
1624     while (S.nRemoved && iteration < 10000) {
1625       deactivate (&S);
1626       shuffleProof (&S, iteration);
1627       iteration++;
1628       verify (&S, 0, 0); } }
1629 
1630   freeMemory (&S);
1631   return (sts != UNSAT); // 0 on success, 1 on any failure
1632 }