diff -urpN a/drat-trim.c b/drat-trim.c --- a/drat-trim.c.orig 2019-07-12 14:19:29.096507625 -0600 +++ b/drat-trim.c 2019-07-12 14:22:37.372487837 -0600 @@ -22,6 +22,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR #include #include #include +#include +#include #include #define TIMEOUT 40000 @@ -52,6 +54,17 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR #define COMPRESS +static bool silentMode; + +static int qprintf(const char * format, ...) { + va_list arglist; + if (silentMode) return 0; + va_start(arglist, format); + int result = vprintf(format, arglist); + va_end(arglist); + return result; +} + struct solver { FILE *inputFile, *proofFile, *lratFile, *traceFile, *activeFile; int *DB, nVars, timeout, mask, delete, *falseStack, *falseA, *forced, binMode, optimize, binOutput, *processed, *assigned, count, *used, *max, COREcount, RATmode, RATcount, nActive, *lratTable, @@ -73,14 +86,14 @@ int abscompare (const void *a, const voi return (abs(*(int*)a) - abs(*(int*)b)); } static inline void printClause (int* clause) { - printf ("[%i] ", clause[ID]); - while (*clause) printf ("%i ", *clause++); printf ("0\n"); } + qprintf ("[%i] ", clause[ID]); + while (*clause) qprintf ("%i ", *clause++); qprintf ("0\n"); } static inline void addWatchPtr (struct solver* S, int lit, long watch) { if (S->used[lit] + 1 == S->max[lit]) { S->max[lit] *= 1.5; S->wlist[lit] = (long *) realloc (S->wlist[lit], sizeof (long) * S->max[lit]); // if (S->max[lit] > 1000) printf("c watchlist %i increased to %i\n", lit, S->max[lit]); - if (S->wlist[lit] == NULL) { printf("c MEMOUT: reallocation failed for watch list of %i\n", lit); exit (0); } } + if (S->wlist[lit] == NULL) { qprintf("c MEMOUT: reallocation failed for watch list of %i\n", lit); exit (0); } } S->wlist[lit][ S->used[lit]++ ] = watch | S->mask; S->wlist[lit][ S->used[lit] ] = END; } @@ -112,10 +125,10 @@ static inline void removeUnit (struct so static inline void unassignUnit (struct solver* S, int lit) { if (S->verb) - printf ("\rc removing unit %i\n", lit); + qprintf ("\rc removing unit %i\n", lit); while (S->falseA[-lit]) { if (S->verb) - printf ("\rc removing unit %i (%i)\n", S->forced[-1], lit); + qprintf ("\rc removing unit %i (%i)\n", S->forced[-1], lit); S->falseA[*(--S->forced)] = 0; S->reason[abs(*S->forced)] = 0; } S->processed = S->assigned = S->forced; } @@ -132,7 +145,7 @@ static inline void addDependency (struct S->maxDependencies = (S->maxDependencies * 3) >> 1; // printf ("c dependencies increased to %i\n", S->maxDependencies); S->dependencies = realloc (S->dependencies, sizeof (int) * S->maxDependencies); - if (S->dependencies == NULL) { printf ("c MEMOUT: dependencies reallocation failed\n"); exit (0); } } + if (S->dependencies == NULL) { qprintf ("c MEMOUT: dependencies reallocation failed\n"); exit (0); } } // printf("c adding dep %i\n", (dep << 1) + forced); S->dependencies[S->nDependencies++] = (dep << 1) + forced; } } @@ -254,7 +267,7 @@ void printCore (struct solver *S) { for (i = 0; i < S->nClauses; i++) { int *clause = S->DB + (S->formula[i] >> INFOBITS); if (clause[ID] & ACTIVE) S->COREcount++; } - printf ("\rc %i of %li clauses in core \n", S->COREcount, S->nClauses); + qprintf ("\rc %i of %li clauses in core \n", S->COREcount, S->nClauses); if (S->coreStr) { FILE *coreFile = fopen (S->coreStr, "w"); @@ -294,12 +307,12 @@ void printLRATline (struct solver *S, in // print the core lemmas to lemmaFile in DRAT format void printProof (struct solver *S) { int step; - printf ("\rc %i of %i lemmas in core using %lu resolution steps\n", S->nActive - S->COREcount + 1, S->nLemmas + 1, S->nResolve); - printf ("\rc %d RAT lemmas in core; %i redundant literals in core lemmas\n", S->RATcount, S->nRemoved); + qprintf ("\rc %i of %i lemmas in core using %lu resolution steps\n", S->nActive - S->COREcount + 1, S->nLemmas + 1, S->nResolve); + qprintf ("\rc %d RAT lemmas in core; %i redundant literals in core lemmas\n", S->RATcount, S->nRemoved); // NB: not yet working with forward checking if (S->mode == FORWARD_UNSAT) { - printf ("\rc optimized proofs are not supported for forward checking\n"); + qprintf ("\rc optimized proofs are not supported for forward checking\n"); return; } // replace S->proof by S->optproof @@ -307,7 +320,7 @@ void printProof (struct solver *S) { if (S->nOpt > S->nAlloc) { S->nAlloc = S->nOpt; S->proof = (long*) realloc (S->proof, sizeof (long) * S->nAlloc); - if (S->proof == NULL) { printf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } } + if (S->proof == NULL) { qprintf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } } S->nStep = 0; S->nLemmas = 0; for (step = S->nOpt - 1; step >= 0; step--) { @@ -383,7 +396,7 @@ void printProof (struct solver *S) { fclose (S->lratFile); if (S->nWrites) - printf ("c wrote optimized proof in LRAT format of %li bytes\n", S->nWrites); } } + qprintf ("c wrote optimized proof in LRAT format of %li bytes\n", S->nWrites); } } void printNoCore (struct solver *S) { if (S->lratFile) { @@ -572,7 +585,7 @@ int checkRAT (struct solver *S, int pivo int blocked = 0; long int reason = 0; if (S->verb) { - printf ("\rc RAT clause: "); printClause (RATcls); } + qprintf ("\rc RAT clause: "); printClause (RATcls); } while (*RATcls) { int lit = *RATcls++; @@ -597,7 +610,7 @@ int checkRAT (struct solver *S, int pivo while (S->forced < S->assigned) { S->falseA[*(--S->assigned)] = 0; S->reason[abs (*S->assigned)] = 0; } - if (S->verb) printf ("\rc RAT check on pivot %i failed\n", pivot); + if (S->verb) qprintf ("\rc RAT check on pivot %i failed\n", pivot); return FAILED; } return SUCCESS; } @@ -620,7 +633,7 @@ int setUCP (struct solver *S, int *cnf, touched = 1; *trail++ = unit; *trail = 0; - if (S->verb) printf("c found unit %i\n", unit); + if (S->verb) qprintf("c found unit %i\n", unit); S->setTruth[ unit] = 1; S->setTruth[-unit] = -1; } satisfied &= sat; @@ -766,7 +779,7 @@ int setRedundancyCheck (struct solver *S int redundancyCheck (struct solver *S, int *clause, int size, int mark) { int i, indegree; int falsePivot = S->falseA[clause[PIVOT]]; - if (S->verb) { printf ("\rc checking lemma (%i, %i) ", size, clause[PIVOT]); printClause (clause); } + if (S->verb) { qprintf ("\rc checking lemma (%i, %i) ", size, clause[PIVOT]); printClause (clause); } if (S->mode != FORWARD_UNSAT) { if ((clause[ID] & ACTIVE) == 0) return SUCCESS; } // redundant? @@ -783,7 +796,7 @@ int redundancyCheck (struct solver *S, i for (i = 0; i < size; ++i) { if (S->falseA[-clause[i]]) { // should only occur in forward mode if (S->warning != NOWARNING) { - printf ("\rc WARNING: found a tautological clause in proof: "); printClause (clause); } + qprintf ("\rc WARNING: found a tautological clause in proof: "); printClause (clause); } if (S->warning == HARDWARNING) exit (HARDWARNING); while (S->forced < S->assigned) { S->falseA[*(--S->assigned)] = 0; @@ -797,10 +810,10 @@ int redundancyCheck (struct solver *S, i if (propagate (S, 0, mark) == UNSAT) { indegree = S->nResolve - indegree; if (indegree <= 2 && S->prep == 0) { - S->prep = 1; if (S->verb) printf ("\rc [%li] preprocessing checking mode on\n", S->time); } + S->prep = 1; if (S->verb) qprintf ("\rc [%li] preprocessing checking mode on\n", S->time); } if (indegree > 2 && S->prep == 1) { - S->prep = 0; if (S->verb) printf ("\rc [%li] preprocessing checking mode off\n", S->time); } - if (S->verb) printf ("\rc lemma has RUP\n"); + S->prep = 0; if (S->verb) qprintf ("\rc [%li] preprocessing checking mode off\n", S->time); } + if (S->verb) qprintf ("\rc lemma has RUP\n"); printDependencies (S, clause, 0); return SUCCESS; } @@ -808,7 +821,7 @@ int redundancyCheck (struct solver *S, i // printf ("RUP check failed. Starting RAT check.\n"); int reslit = clause[PIVOT]; if (S->verb) - printf ("\rc RUP checked failed; starting RAT check on pivot %d.\n", reslit); + qprintf ("\rc RUP checked failed; starting RAT check on pivot %d.\n", reslit); if (falsePivot) return FAILED; @@ -821,7 +834,7 @@ int redundancyCheck (struct solver *S, i if (checkRAT (S, reslit, mark) == FAILED) { failed = 1; if (S->warning != NOWARNING) { - printf ("\rc WARNING: RAT check on proof pivot failed : "); printClause (clause); } + qprintf ("\rc WARNING: RAT check on proof pivot failed : "); printClause (clause); } if (S->warning == HARDWARNING) exit (HARDWARNING); for (i = 0; i < size; i++) { if (clause[i] == reslit) continue; @@ -838,12 +851,12 @@ int redundancyCheck (struct solver *S, i S->reason[abs (*S->assigned)] = 0; } if (failed) { - printf ("c RAT check failed on all possible pivots\n"); + qprintf ("c RAT check failed on all possible pivots\n"); return FAILED; } if (mark) S->RATcount++; - if (S->verb) printf ("\rc lemma has RAT on %i\n", clause[PIVOT]); + if (S->verb) qprintf ("\rc lemma has RAT on %i\n", clause[PIVOT]); return SUCCESS; } int init (struct solver *S) { @@ -873,7 +886,7 @@ int init (struct solver *S) { int *clause = S->DB + (S->formula[i] >> INFOBITS); if (clause[ID] & ACTIVE) clause[ID] ^= ACTIVE; if (clause[0] == 0) { - printf ("\rc formula contains empty clause\n"); + qprintf ("\rc formula contains empty clause\n"); if (S->coreStr) { FILE *coreFile = fopen (S->coreStr, "w"); fprintf (coreFile, "p cnf 0 1\n 0\n"); @@ -885,7 +898,7 @@ int init (struct solver *S) { return UNSAT; } if (clause[1]) { addWatch (S, clause, 0); addWatch (S, clause, 1); } else if (S->falseA[clause[0]]) { - printf ("\rc found complementary unit clauses\n"); + qprintf ("\rc found complementary unit clauses\n"); if (S->coreStr) { FILE *coreFile = fopen (S->coreStr, "w"); fprintf (coreFile, "p cnf %i 2\n%i 0\n%i 0\n", abs (clause[0]), clause[0], -clause[0]); @@ -908,7 +921,7 @@ int init (struct solver *S) { S->nDependencies = 0; S->time = S->count; // Alternative time init if (propagateUnits (S, 1) == UNSAT) { - printf ("\rc UNSAT via unit propagation on the input instance\n"); + qprintf ("\rc UNSAT via unit propagation on the input instance\n"); printDependencies (S, NULL, 0); postprocess (S); return UNSAT; } return SAT; } @@ -919,7 +932,7 @@ int verify (struct solver *S, int begin, if (S->mode == FORWARD_UNSAT) { if (begin == end) - printf ("\rc start forward verification\n"); } + qprintf ("\rc start forward verification\n"); } int step; int adds = 0; @@ -932,17 +945,17 @@ int verify (struct solver *S, int begin, S->time = lemmas[ID]; if (d) { active--; } else { active++; adds++; } - if (S->mode == FORWARD_SAT && S->verb) printf ("\rc %i active clauses\n", active); + if (S->mode == FORWARD_SAT && S->verb) qprintf ("\rc %i active clauses\n", active); if (!lemmas[1]) { // found a unit int lit = lemmas[0]; if (S->verb) - printf ("\rc found unit in proof %i [%li]\n", lit, S->time); + qprintf ("\rc found unit in proof %i [%li]\n", lit, S->time); if (d) { if (S->mode == FORWARD_SAT) { removeUnit (S, lit); propagateUnits (S, 0); } else { // no need to remove units while checking UNSAT - if (S->verb) { printf("c removing proof step: d "); printClause(lemmas); } + if (S->verb) { qprintf("c removing proof step: d "); printClause(lemmas); } S->proof[step] = 0; continue; } } else { if (S->mode == BACKWARD_UNSAT && S->falseA[-lit]) { S->proof[step] = 0; continue; } @@ -951,7 +964,7 @@ int verify (struct solver *S, int begin, if (d && lemmas[1]) { // if delete and not unit if ((S->reason[abs (lemmas[0])] - 1) == (lemmas - S->DB)) { // what is this check? if (S->mode != FORWARD_SAT) { // ignore pseudo unit clause deletion - if (S->verb) { printf ("c ignoring deletion intruction %li: ", (lemmas - S->DB)); printClause (lemmas); } + if (S->verb) { qprintf ("c ignoring deletion intruction %li: ", (lemmas - S->DB)); printClause (lemmas); } // if (S->mode == BACKWARD_UNSAT) { // ignore pseudo unit clause deletion S->proof[step] = 0; } else { // if (S->mode == FORWARD_SAT) { // also for FORWARD_UNSAT? @@ -967,7 +980,7 @@ int verify (struct solver *S, int begin, if (d && S->mode == FORWARD_SAT) { if (size == -1) propagateUnits (S, 0); // necessary? if (redundancyCheck (S, lemmas, size, 1) == FAILED) { - printf ("c failed at proof line %i (modulo deletion errors)\n", step + 1); + qprintf ("c failed at proof line %i (modulo deletion errors)\n", step + 1); return SAT; } continue; } @@ -975,7 +988,7 @@ int verify (struct solver *S, int begin, if (step > end) { if (size < 0) continue; // Fix of bus error: 10 if (redundancyCheck (S, lemmas, size, 1) == FAILED) { - printf ("c failed at proof line %i (modulo deletion errors)\n", step + 1); + qprintf ("c failed at proof line %i (modulo deletion errors)\n", step + 1); return SAT; } size = sortSize (S, lemmas); @@ -984,9 +997,9 @@ int verify (struct solver *S, int begin, if (lemmas[1]) addWatch (S, lemmas, 0), addWatch (S, lemmas, 1); - if (size == 0) { printf ("\rc conflict claimed, but not detected\n"); return SAT; } // change to FAILED? + if (size == 0) { qprintf ("\rc conflict claimed, but not detected\n"); return SAT; } // change to FAILED? if (size == 1) { - if (S->verb) printf ("\rc found unit %i\n", lemmas[0]); + if (S->verb) qprintf ("\rc found unit %i\n", lemmas[0]); assign (S, lemmas[0]); S->reason[abs (lemmas[0])] = ((long) ((lemmas)-S->DB)) + 1; if (propagate (S, 1, 1) == UNSAT) goto start_verification; S->forced = S->processed; } } @@ -997,7 +1010,7 @@ int verify (struct solver *S, int begin, if (S->mode == FORWARD_UNSAT) { if (begin == end) { postprocess (S); - printf ("\rc ERROR: all lemmas verified, but no conflict\n"); } + qprintf ("\rc ERROR: all lemmas verified, but no conflict\n"); } return SAT; } if (S->mode == BACKWARD_UNSAT) { @@ -1010,7 +1023,7 @@ int verify (struct solver *S, int begin, if ( (ad & 1) && (clause[ID] & 1)) clause[ID] ^= ACTIVE; if (!(ad & 1)) clause[ID] |= ACTIVE; } } } if (!S->backforce) { - printf ("\rc ERROR: no conflict\n"); + qprintf ("\rc ERROR: no conflict\n"); return SAT; } } start_verification:; @@ -1022,8 +1035,8 @@ int verify (struct solver *S, int begin, printDependencies (S, NULL, 0); if (S->mode == FORWARD_SAT) { - printf ("\rc ERROR: found empty clause during SAT check\n"); exit (0); } - printf ("\rc detected empty clause; start verification via backward checking\n"); + qprintf ("\rc ERROR: found empty clause during SAT check\n"); exit (0); } + qprintf ("\rc detected empty clause; start verification via backward checking\n"); S->forced = S->processed; assert (S->mode == BACKWARD_UNSAT); // only reachable in BACKWARD_UNSAT mode @@ -1040,7 +1053,7 @@ int verify (struct solver *S, int begin, struct timeval current_time; gettimeofday (¤t_time, NULL); int seconds = (int) (current_time.tv_sec - S->start_time.tv_sec); - if ((seconds > S->timeout) && (S->optimize == 0)) printf ("s TIMEOUT\n"), exit (0); + if ((seconds > S->timeout) && (S->optimize == 0)) qprintf ("s TIMEOUT\n"), exit (0); if (S->bar) if ((adds % 1000) == 0) { @@ -1049,12 +1062,12 @@ int verify (struct solver *S, int begin, (current_time.tv_usec - backward_time.tv_usec); double time = (double) (runtime / 1000000.0); double fraction = (adds * 1.0) / max; - printf("\rc %.2f%% [", 100.0 * (1.0 - fraction)); + qprintf("\rc %.2f%% [", 100.0 * (1.0 - fraction)); for (f = 1; f <= 20; f++) { - if ((1.0 - fraction) * 20.0 < 1.0 * f) printf(" "); - else printf("="); } - printf("] time remaining: %.2f seconds ", time / (1.0 - fraction) - time); - if (step == 0) printf("\n"); + if ((1.0 - fraction) * 20.0 < 1.0 * f) qprintf(" "); + else qprintf("="); } + qprintf("] time remaining: %.2f seconds ", time / (1.0 - fraction) - time); + if (step == 0) qprintf("\n"); fflush (stdout); } long ad = S->proof[step]; long d = ad & 1; @@ -1073,7 +1086,7 @@ int verify (struct solver *S, int begin, int size = sortSize (S, clause); if (d) { - if (S->verb) { printf ("\rc adding clause (%i) ", size); printClause (clause); } + if (S->verb) { qprintf ("\rc adding clause (%i) ", size); printClause (clause); } addWatch (S, clause, 0), addWatch (S, clause, 1); continue; } S->time = clause[ID]; @@ -1088,7 +1101,7 @@ int verify (struct solver *S, int begin, clause[size] = 0; if (S->verb) { - printf ("\rc validating clause (%i, %i): ", clause[PIVOT], size); printClause (clause); } + qprintf ("\rc validating clause (%i, %i): ", clause[PIVOT], size); printClause (clause); } /* int i; if (size > 1 && (top_flag == 1)) { @@ -1108,7 +1121,7 @@ int verify (struct solver *S, int begin, clause[PIVOT] = pivot; } } */ if (redundancyCheck (S, clause, size, 1) == FAILED) { - printf ("c failed at proof line %i (modulo deletion errors)\n", step + 1); + qprintf ("c failed at proof line %i (modulo deletion errors)\n", step + 1); return SAT; } checked++; S->optproof[S->nOpt++] = ad; } @@ -1217,9 +1230,9 @@ int parse (struct solver* S) { int nZeros = S->nClauses; if (!S->nVars && !S->nClauses) { - printf ("\rc ERROR: did not find p cnf line in input file\n"); exit (0); } + qprintf ("\rc ERROR: did not find p cnf line in input file\n"); exit (0); } - printf ("\rc parsing input formula with %i variables and %li clauses\n", S->nVars, S->nClauses); + qprintf ("\rc parsing input formula with %i variables and %li clauses\n", S->nVars, S->nClauses); bufferAlloc = INIT; buffer = (int*) malloc (sizeof (int) * bufferAlloc); @@ -1264,7 +1277,7 @@ int parse (struct solver* S) { else if (res == 100) del = 1; else { if (S->warning != NOWARNING) { - printf ("\rc WARNING: wrong binary prefix, stop reading proof\n"); break; } + qprintf ("\rc WARNING: wrong binary prefix, stop reading proof\n"); break; } if (S->warning == HARDWARNING) exit (HARDWARNING); } S->nReads++; } else { @@ -1281,27 +1294,27 @@ int parse (struct solver* S) { tmp = fscanf (S->proofFile, " %i ", &lit); } } if (tmp == EOF && !fileSwitchFlag) { if (S->warning != NOWARNING) { - printf ("\rc WARNING: early EOF of the input formula\n"); - printf ("\rc WARNING: %i clauses less than expected\n", nZeros); } + qprintf ("\rc WARNING: early EOF of the input formula\n"); + qprintf ("\rc WARNING: %i clauses less than expected\n", nZeros); } if (S->warning == HARDWARNING) exit (HARDWARNING); fileLine = 0; fileSwitchFlag = 1; } } if (tmp == 0) { char ignore[1024]; - if (!fileSwitchFlag) { if (fgets (ignore, sizeof (ignore), S->inputFile) == NULL) printf ("c\n"); } - else if (fgets (ignore, sizeof (ignore), S->proofFile) == NULL) printf ("c\n"); + if (!fileSwitchFlag) { if (fgets (ignore, sizeof (ignore), S->inputFile) == NULL) qprintf ("c\n"); } + else if (fgets (ignore, sizeof (ignore), S->proofFile) == NULL) qprintf ("c\n"); for (i = 0; i < 1024; i++) { if (ignore[i] == '\n') break; } if (i == 1024) { - printf ("c ERROR: comment longer than 1024 characters: %s\n", ignore); + qprintf ("c ERROR: comment longer than 1024 characters: %s\n", ignore); exit (HARDWARNING); } - if (S->verb) printf ("\rc WARNING: parsing mismatch assuming a comment\n"); + if (S->verb) qprintf ("\rc WARNING: parsing mismatch assuming a comment\n"); continue; } if (abs (lit) > S->maxVar) S->maxVar = abs (lit); if (tmp == EOF && fileSwitchFlag) break; if (abs (lit) > S->nVars && !fileSwitchFlag) { - printf ("\rc illegal literal %i due to max var %i\n", lit, S->nVars); exit (0); } + qprintf ("\rc illegal literal %i due to max var %i\n", lit, S->nVars); exit (0); } if (!lit) { fileLine++; if (size > S->maxSize) S->maxSize = size; @@ -1312,7 +1325,7 @@ int parse (struct solver* S) { for (i = 0; i < size; ++i) { if (buffer[i] == buffer[i+1]) { if (S->warning != NOWARNING) { - printf ("\rc WARNING: detected and deleted duplicate literal %i at position %i of line %i\n", buffer[i+1], i+1, fileLine); } + qprintf ("\rc WARNING: detected and deleted duplicate literal %i at position %i of line %i\n", buffer[i+1], i+1, fileLine); } if (S->warning == HARDWARNING) exit (HARDWARNING); } else { buffer[j++] = buffer[i]; } } buffer[j] = 0; size = j; @@ -1320,7 +1333,7 @@ int parse (struct solver* S) { if (size == 0 && !fileSwitchFlag) retvalue = UNSAT; if (del && S->mode == BACKWARD_UNSAT && size <= 1) { if (S->warning != NOWARNING) { - printf ("\rc WARNING: backward mode ignores deletion of (pseudo) unit clause "); + qprintf ("\rc WARNING: backward mode ignores deletion of (pseudo) unit clause "); printClause (buffer); } if (S->warning == HARDWARNING) exit (HARDWARNING); del = 0; size = 0; continue; } @@ -1333,7 +1346,7 @@ int parse (struct solver* S) { match = matchClause (S, hashTable[hash], hashUsed[hash], buffer, size); if (match == 0) { if (S->warning != NOWARNING) { - printf ("\rc WARNING: deleted clause on line %i does not occur: ", fileLine); printClause (buffer); } + qprintf ("\rc WARNING: deleted clause on line %i does not occur: ", fileLine); printClause (buffer); } if (S->warning == HARDWARNING) exit (HARDWARNING); goto end_delete; } if (S->mode == FORWARD_SAT) S->DB[ match - 2 ] = rem; @@ -1342,7 +1355,7 @@ int parse (struct solver* S) { if (S->nStep == S->nAlloc) { S->nAlloc = (S->nAlloc * 3) >> 1; S->proof = (long*) realloc (S->proof, sizeof (long) * S->nAlloc); // printf ("c proof allocation increased to %li\n", S->nAlloc); - if (S->proof == NULL) { printf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } } + if (S->proof == NULL) { qprintf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } } S->proof[S->nStep++] = (match << INFOBITS) + 1; } end_delete:; if (del) { del = 0; size = 0; continue; } } @@ -1350,7 +1363,7 @@ int parse (struct solver* S) { if (S->mem_used + size + EXTRA > DBsize) { DBsize = (DBsize * 3) >> 1; S->DB = (int *) realloc (S->DB, DBsize * sizeof (int)); // printf("c database increased to %li\n", DBsize); - if (S->DB == NULL) { printf("c MEMOUT: reallocation of clause database failed\n"); exit (0); } } + if (S->DB == NULL) { qprintf("c MEMOUT: reallocation of clause database failed\n"); exit (0); } } int *clause = &S->DB[S->mem_used + EXTRA - 1]; if (size != 0) clause[PIVOT] = pivot; clause[ID] = 2 * S->count; S->count++; @@ -1362,7 +1375,7 @@ int parse (struct solver* S) { hash = getHash (clause); if (hashUsed[hash] == hashMax[hash]) { hashMax[hash] = (hashMax[hash] * 3) >> 1; hashTable[hash] = (long *) realloc (hashTable[hash], sizeof (long*) * hashMax[hash]); - if (hashTable[hash] == NULL) { printf("c MEMOUT reallocation of hash table %i failed\n", hash); exit (0); } } + if (hashTable[hash] == NULL) { qprintf("c MEMOUT reallocation of hash table %i failed\n", hash); exit (0); } } hashTable[ hash ][ hashUsed[hash]++ ] = (long) (clause - S->DB); active++; @@ -1372,7 +1385,7 @@ int parse (struct solver* S) { if (S->nStep == S->nAlloc) { S->nAlloc = (S->nAlloc * 3) >> 1; S->proof = (long*) realloc (S->proof, sizeof (long) * S->nAlloc); // printf ("c proof allocation increased to %li\n", S->nAlloc); - if (S->proof == NULL) { printf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } } + if (S->proof == NULL) { qprintf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } } S->proof[S->nStep++] = (((long) (clause - S->DB)) << INFOBITS); } if (nZeros <= 0) S->nLemmas++; @@ -1386,18 +1399,18 @@ int parse (struct solver* S) { if (S->mode == FORWARD_SAT && active) { if (S->warning != NOWARNING) - printf ("\rc WARNING: %i clauses active if proof succeeds\n", active); + qprintf ("\rc WARNING: %i clauses active if proof succeeds\n", active); if (S->warning == HARDWARNING) exit (HARDWARNING); for (i = 0; i < BIGINIT; i++) { int j; for (j = 0; j < hashUsed[i]; j++) { - printf ("\rc "); + qprintf ("\rc "); int *clause = S->DB + hashTable [i][j]; printClause (clause); if (S->nStep == S->nAlloc) { S->nAlloc = (S->nAlloc * 3) >> 1; S->proof = (long*) realloc (S->proof, sizeof (long) * S->nAlloc); // printf ("c proof allocation increased to %li\n", S->nAlloc); - if (S->proof == NULL) { printf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } } + if (S->proof == NULL) { qprintf("c MEMOUT: reallocation of proof list failed\n"); exit (0); } } S->proof[S->nStep++] = (((int) (clause - S->DB)) << INFOBITS) + 1; } } } S->DB = (int *) realloc (S->DB, S->mem_used * sizeof (int)); @@ -1408,9 +1421,9 @@ int parse (struct solver* S) { free (hashMax); free (buffer); - printf ("\rc finished parsing"); - if (S->nReads) printf (", read %li bytes from proof file", S->nReads); - printf ("\n"); + qprintf ("\rc finished parsing"); + if (S->nReads) qprintf (", read %li bytes from proof file", S->nReads); + qprintf ("\n"); int n = S->maxVar; S->falseStack = (int *) malloc (( n + 1) * sizeof (int )); // Stack of falsified literals -- this pointer is never changed @@ -1491,6 +1504,7 @@ void printHelp ( ) { printf (" -u default unit propatation (i.e., no core-first)\n"); printf (" -f forward mode for UNSAT\n"); printf (" -v more verbose output\n"); + printf (" -q suppress all output\n"); printf (" -b show progress bar\n"); printf (" -O optimize proof till fixpoint by repeating verification\n"); printf (" -C compress core lemmas (emit binary proof)\n"); @@ -1534,10 +1548,11 @@ int run_drat_trim (int argc, const char* S.binOutput = 0; gettimeofday (&S.start_time, NULL); - int i, tmp = 0; + int i, proof = -1, tmp = 0; for (i = 1; i < argc; i++) { if (argv[i][0] == '-') { if (argv[i][1] == 'h') printHelp (); + else if (argv[i][1] == 'q') silentMode = 1; else if (argv[i][1] == 'c') S.coreStr = argv[++i]; else if (argv[i][1] == 'a') S.activeFile = fopen (argv[++i], "w"); else if (argv[i][1] == 'l') S.lemmaStr = argv[++i]; @@ -1561,28 +1576,29 @@ int run_drat_trim (int argc, const char* else { tmp++; if (tmp == 1) { - S.inputFile = fopen (argv[1], "r"); + S.inputFile = fopen (argv[i], "r"); if (S.inputFile == NULL) { - printf ("\rc error opening \"%s\".\n", argv[i]); return ERROR; } } + qprintf ("\rc error opening \"%s\".\n", argv[i]); return ERROR; } } else if (tmp == 2) { - S.proofFile = fopen (argv[2], "r"); + proof = i; + S.proofFile = fopen (argv[i], "r"); if (S.proofFile == NULL) { - printf ("\rc error opening \"%s\".\n", argv[i]); return ERROR; } + qprintf ("\rc error opening \"%s\".\n", argv[i]); return ERROR; } int c, comment = 1; if (S.binMode == 0) { c = getc_unlocked (S.proofFile); // check the first character in the file if (c == EOF) { S.binMode = 1; continue; } if ((c != 13) && (c != 32) && (c != 45) && ((c < 48) || (c > 57)) && (c != 99) && (c != 100)) { - printf ("\rc turning on binary mode checking\n"); + qprintf ("\rc turning on binary mode checking\n"); S.binMode = 1; } if (c != 99) comment = 0; } if (S.binMode == 0) { c = getc_unlocked (S.proofFile); // check the second character in the file if (c == EOF) { S.binMode = 1; continue; } if ((c != 13) && (c != 32) && (c != 45) && ((c < 48) || (c > 57)) && (c != 99) && (c != 100)) { - printf ("\rc turning on binary mode checking\n"); + qprintf ("\rc turning on binary mode checking\n"); S.binMode = 1; } if (c != 32) comment = 0; } if (S.binMode == 0) { @@ -1591,14 +1607,14 @@ int run_drat_trim (int argc, const char* c = getc_unlocked (S.proofFile); if (c == EOF) break; if ((c != 100) && (c != 10) && (c != 13) && (c != 32) && (c != 45) && ((c < 48) || (c > 57)) && (comment && ((c < 65) || (c > 122)))) { - printf ("\rc turning on binary mode checking\n"); + qprintf ("\rc turning on binary mode checking\n"); S.binMode = 1; break; } } } fclose (S.proofFile); - S.proofFile = fopen (argv[2], "r"); + S.proofFile = fopen (argv[i], "r"); if (S.proofFile == NULL) { - printf ("\rc error opening \"%s\".\n", argv[i]); return ERROR; } } } } + qprintf ("\rc error opening \"%s\".\n", argv[i]); return ERROR; } } } } - if (tmp == 1) printf ("\rc reading proof from stdin\n"); + if (tmp == 1) qprintf ("\rc reading proof from stdin\n"); if (tmp == 0) printHelp (); int parseReturnValue = parse (&S); @@ -1609,23 +1625,23 @@ int run_drat_trim (int argc, const char* if (S.mode == FORWARD_UNSAT) { S.reduce = 0; } - if (S.delProof && argv[2] != NULL) { - int ret = remove(argv[2]); - if (ret == 0) printf("c deleted proof %s\n", argv[2]); } + if (S.delProof && proof >= 0 && argv[proof] != NULL) { + int ret = remove(argv[proof]); + if (ret == 0) qprintf("c deleted proof %s\n", argv[proof]); } int sts = ERROR; - if (parseReturnValue == ERROR) printf ("\rs MEMORY ALLOCATION ERROR\n"); - else if (parseReturnValue == UNSAT) printf ("\rc trivial UNSAT\ns VERIFIED\n"); - else if ((sts = verify (&S, -1, -1)) == UNSAT) printf ("\rs VERIFIED\n"); - else printf ("\ns NOT VERIFIED\n") ; + if (parseReturnValue == ERROR) qprintf ("\rs MEMORY ALLOCATION ERROR\n"); + else if (parseReturnValue == UNSAT) qprintf ("\rc trivial UNSAT\ns VERIFIED\n"); + else if ((sts = verify (&S, -1, -1)) == UNSAT) qprintf ("\rs VERIFIED\n"); + else qprintf ("\ns NOT VERIFIED\n") ; struct timeval current_time; gettimeofday (¤t_time, NULL); long runtime = (current_time.tv_sec - S.start_time.tv_sec) * 1000000 + (current_time.tv_usec - S.start_time.tv_usec); - printf ("\rc verification time: %.3f seconds\n", (double) (runtime / 1000000.0)); + qprintf ("\rc verification time: %.3f seconds\n", (double) (runtime / 1000000.0)); if (S.optimize) { - printf("c proof optimization started (ignoring the timeout)\n"); + qprintf("c proof optimization started (ignoring the timeout)\n"); int iteration = 1; while (S.nRemoved && iteration < 10000) { deactivate (&S);