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