Blob Blame Raw
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 <stdio.h>
 #include <stdlib.h>
 #include <assert.h>
+#include <stdarg.h>
+#include <stdbool.h>
 #include <sys/time.h>
 
 #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 (&current_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 (&current_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);