rupOnly

marijnheule · May 22, 2023 · 2e5e29c · 2e5e29c
1 parent 633e4a9
commit 2e5e29c
Showing 1 changed file with 8 additions and 2 deletions.
diff --git a/drat-trim.c b/drat-trim.c
@@ -60,7 +60,7 @@ struct solver { FILE *inputFile, *proofFile, *lratFile, *traceFile, *activeFile;
       *processed, *assigned, count, *used, *max, COREcount, RATmode, RATcount, nActive, *lratTable,
       nLemmas, maxRAT, *preRAT, maxDependencies, nDependencies, bar, backforce, reduce,
       *dependencies, maxVar, maxSize, mode, verb, unitSize, unitStackSize, prep, *current, nRemoved, warning,
-      delProof, *setMap, *setTruth;
+      delProof, *setMap, *setTruth, rupOnly;
     char *coreStr, *lemmaStr;
     struct timeval start_time;
     long mem_used, time, nClauses, nStep, nOpt, nAlloc, *unitStack, *reason, lemmas, nResolve, *RATset,
@@ -656,6 +656,9 @@ int redundancyCheck (struct solver *S, int *clause, int size, int mark) {
 
   // Failed RUP check.  Now test RAT.
   // printf ("RUP check failed.  Starting RAT check.\n");
+  if (S->rupOnly) {
+      printf ("\rc RUP check failed\n");
+      return FAILED; }
   int reslit = clause[PIVOT];
   if (S->verb)
     printf ("\rc RUP checked failed; starting RAT check on pivot %d.\n", reslit);
@@ -1348,6 +1351,7 @@ void printHelp ( ) {
   printf ("  -p          run in plain mode (i.e., ignore deletion information)\n\n");
   printf ("  -R          turn off reduce mode\n\n");
   printf ("  -S          run in SAT check mode (forward checking)\n\n");
+  printf ("  -U          only allow RUP additions\n");
   printf ("and input and proof are specified as follows\n\n");
   printf ("  INPUT       input file in DIMACS format\n");
   printf ("  PROOF       proof file in DRAT format (stdin if no argument)\n\n");
@@ -1379,6 +1383,7 @@ int main (int argc, char** argv) {
   S.reduce     = 1;
   S.binMode    = 0;
   S.binOutput  = 0;
+  S.rupOnly    = 0;
   gettimeofday (&S.start_time, NULL);
 
   int i, tmp = 0;
@@ -1405,7 +1410,8 @@ int main (int argc, char** argv) {
       else if (argv[i][1] == 'p') S.delete     = 0;
       else if (argv[i][1] == 'R') S.reduce     = 0;
       else if (argv[i][1] == 'f') S.mode       = FORWARD_UNSAT;
-      else if (argv[i][1] == 'S') S.mode       = FORWARD_SAT; }
+      else if (argv[i][1] == 'S') S.mode       = FORWARD_SAT;
+      else if (argv[i][1] == 'U') S.rupOnly    = 1; }
     else {
       tmp++;
       if (tmp == 1) {