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 (¤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);