lingeling/code/lglincremental.c

   1 /*-------------------------------------------------------------------------*/
   2 /* Copyright 2010-2014 Armin Biere Johannes Kepler University Linz Austria */
   3 /*-------------------------------------------------------------------------*/
   4
   5 #include "lglib.h"
   6
   7 #include <assert.h>
   8 #include <ctype.h>
   9 #include <limits.h>
  10 #include <signal.h>
  11 #include <stdarg.h>
  12 #include <stdio.h>
  13 #include <stdlib.h>
  14 #include <string.h>
  15 #include <unistd.h>
  16 #include "solver_interface.h"
  17
  18 static LGL * lgl4sigh;
  19 static int catchedsig, verbose, ignmissingheader, ignaddcls;
  20
  21 static void (*sig_int_handler)(int);
  22 static void (*sig_segv_handler)(int);
  23 static void (*sig_abrt_handler)(int);
  24 static void (*sig_term_handler)(int);
  25 static void (*sig_bus_handler)(int);
  26 static void (*sig_alrm_handler)(int);
  27
  28 static void resetsighandlers (void) {
  29   (void) signal (SIGINT, sig_int_handler);
  30   (void) signal (SIGSEGV, sig_segv_handler);
  31   (void) signal (SIGABRT, sig_abrt_handler);
  32   (void) signal (SIGTERM, sig_term_handler);
  33   (void) signal (SIGBUS, sig_bus_handler);
  34 }
  35
  36 static inline double cpuTime(void) {
  37   struct rusage ru;
  38   getrusage(RUSAGE_SELF, &ru);
  39   return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000;
  40 }
  41
  42 static void caughtsigmsg (int sig) {
  43   if (verbose < 0) return;
  44   printf ("c\nc CAUGHT SIGNAL %d", sig);
  45   switch (sig) {
  46     case SIGINT: printf (" SIGINT"); break;
  47     case SIGSEGV: printf (" SIGSEGV"); break;
  48     case SIGABRT: printf (" SIGABRT"); break;
  49     case SIGTERM: printf (" SIGTERM"); break;
  50     case SIGBUS: printf (" SIGBUS"); break;
  51     case SIGALRM: printf (" SIGALRM"); break;
  52     default: break;
  53   }
  54   printf ("\nc\n");
  55   fflush (stdout);
  56 }
  57
  58 static void catchsig (int sig) {
  59   if (!catchedsig) {
  60     catchedsig = 1;
  61     caughtsigmsg (sig);
  62     fputs ("c s UNKNOWN\n", stdout);
  63     fflush (stdout);
  64     if (verbose >= 0) {
  65       lglflushtimers (lgl4sigh);
  66       lglstats (lgl4sigh);
  67       caughtsigmsg (sig);
  68     }
  69   }
  70   resetsighandlers ();
  71   if (!getenv ("LGLNABORT")) raise (sig); else exit (1);
  72 }
  73
  74 static void setsighandlers (void) {
  75   sig_int_handler = signal (SIGINT, catchsig);
  76   sig_segv_handler = signal (SIGSEGV, catchsig);
  77   sig_abrt_handler = signal (SIGABRT, catchsig);
  78   sig_term_handler = signal (SIGTERM, catchsig);
  79   sig_bus_handler = signal (SIGBUS, catchsig);
  80 }
  81
  82 static int timelimit = -1, caughtalarm = 0;
  83
  84 static void catchalrm (int sig) {
  85   assert (sig == SIGALRM);
  86   if (!caughtalarm) {
  87     caughtalarm = 1;
  88     caughtsigmsg (sig);
  89     if (timelimit >= 0) {
  90       printf ("c time limit of %d reached after %.1f seconds\nc\n",
  91               timelimit, lglsec (lgl4sigh));
  92       fflush (stdout);
  93     }
  94   }
  95 }
  96
  97 static int checkalarm (void * ptr) {
  98   assert (ptr == (void*) &caughtalarm);
  99   return caughtalarm;
 100 }
 101
 102 static int primes[] = {
 103   200000033, 200000039, 200000051, 200000069, 200000081,
 104 };
 105
 106 static int nprimes = sizeof primes / sizeof *primes;
 107
 108
 109
 110 int *buffer;
 111 int length;
 112 int offset;
 113
 114 int *outbuffer;
 115 int outoffset;
 116
 117 int getInt() {
 118   if (offset>=length) {
 119     ssize_t ptr;
 120     offset = 0;
 121     do {
 122       ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE);
 123       if (ptr == -1)
 124         exit(-1);
 125     } while(ptr==0);
 126     ssize_t bytestoread=(4-(ptr & 3)) & 3;
 127     while(bytestoread != 0) {
 128       ssize_t p=read(0, &((char *)buffer)[ptr], bytestoread);
 129       if (p == -1)
 130         exit(-1);
 131       bytestoread -= p;
 132       ptr += p;
 133     }
 134     length = ptr / 4;
 135     offset = 0;
 136   }
 137
 138   return buffer[offset++];
 139 }
 140
 141 void flushInts() {
 142   ssize_t bytestowrite=sizeof(int)*outoffset;
 143   ssize_t byteswritten=0;
 144   do {
 145     ssize_t n=write(IS_OUT_FD, &((char *)outbuffer)[byteswritten], bytestowrite);
 146     if (n == -1) {
 147       fprintf(stderr, "Write failure\n");
 148       exit(-1);
 149     }
 150     bytestowrite -= n;
 151     byteswritten += n;
 152   } while(bytestowrite != 0);
 153   outoffset = 0;
 154 }
 155
 156 void putInt(int value) {
 157   if (outoffset>=IS_BUFFERSIZE) {
 158     flushInts();
 159   }
 160   outbuffer[outoffset++]=value;
 161 }
 162
 163 #define bool int
 164 #define false 0
 165 #define true 1
 166
 167 void readClauses(LGL *solver) {
 168   bool haveClause = false;
 169   while(true) {
 170     int lit=getInt();
 171     if (lit!=0) {
 172       haveClause = true;
 173       lgladd(solver, lit);
 174     } else {
 175       if (haveClause) {
 176         lgladd(solver, 0);
 177         haveClause = false;
 178       } else {
 179         //done with clauses
 180         return;
 181       }
 182     }
 183   }
 184 }
 185
 186 void processCommands(LGL *solver) {
 187   while(true) {
 188     int command=getInt();
 189     switch(command) {
 190     case IS_FREEZE: {
 191       int var=getInt();
 192       lglfreeze(solver, var);
 193       break;
 194     }
 195     case IS_RUNSOLVER: {
 196       int ret = lglsat(solver);
 197       if (ret == 10) {
 198         putInt(IS_SAT);
 199         int numvars=lglmaxvar(solver);
 200         putInt(numvars);
 201         for(int i=1;i<=numvars;i++) {
 202           putInt(lglderef(solver, i) > 0);
 203         }
 204       } else if (ret == 20) {
 205         putInt(IS_UNSAT);
 206       } else {
 207         putInt(IS_INDETER);
 208       }
 209       flushInts();
 210       return;
 211     }
 212     default:
 213       fprintf(stderr, "Unreconized command\n");
 214       exit(-1);
 215     }
 216   }
 217 }
 218
 219 void processSAT(LGL *solver) {
 220   buffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE);
 221   offset=0;
 222   length=0;
 223   outbuffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE);
 224   outoffset=0;
 225
 226   while(true) {
 227     double initial_time = cpuTime();
 228     readClauses(solver);
 229     double parse_time = cpuTime();
 230     processCommands(solver);
 231     double finish_time = cpuTime();
 232     printf("Parse time: %12.2f s Solve time:%12.2f s\n", parse_time-initial_time, finish_time-parse_time);
 233   }
 234 }
 235
 236
 237
 238 int main (int argc, char ** argv) {
 239   int res, i, j, val, len, lineno, simponly;
 240   const char * pname, * match, * p, * thanks;
 241   int nopts, simplevel;
 242   FILE * pfile;
 243   char * tmp;
 244   LGL * lgl;
 245   lineno = 1;
 246   res = simponly = simplevel = 0;
 247   pname = thanks = 0;
 248   lgl4sigh = lgl = lglinit ();
 249   setsighandlers ();
 250   for (i = 1; i < argc; i++) {
 251     if (!strcmp (argv[i], "-h") || !strcmp (argv[i], "--help")) {
 252       printf ("usage: lingeling [<option> ...][<file>[.gz]]\n");
 253       printf ("\n");
 254       printf ("where <option> is one of the following:\n");
 255       printf ("\n");
 256       printf ("-q               be quiet (same as '--verbose=-1')\n");
 257       printf ("-s               only simplify and print to output file\n");
 258       printf ("-O<L>            set simplification level to <L>\n");
 259       printf ("-p <options>     read options from file\n");
 260       printf ("\n");
 261       printf ("-t <seconds>     set time limit\n");
 262       printf ("\n");
 263       printf ("\n");
 264       printf ("-h|--help        print command line option summary\n");
 265       printf ("-f|--force       force reading even without header\n");
 266       printf ("-i|--ignore      ignore additional clauses\n");
 267       printf ("-r|--ranges      print value ranges of options\n");
 268       printf ("-d|--defaults    print default values of options\n");
 269       printf ("-P|--pcs         print (full) PCS file\n");
 270       printf ("--pcs-mixed      print mixed PCS file\n");
 271       printf ("--pcs-reduced    print reduced PCS file\n");
 272       printf ("-e|--embedded    ditto but in an embedded format print\n");
 273       printf ("-n|--no-witness   do not print solution (see '--witness')\n");
 274       printf ("\n");
 275       printf ("--thanks=<whom>  alternative way of specifying the seed\n");
 276       printf ("                 (inspired by Vampire)\n");
 277       printf ("\n");
 278       printf (
 279 "The following options can also be used in the form '--<name>=<int>',\n"
 280 "just '--<name>' for increment and '--no-<name>' for zero.  They\n"
 281 "can be embedded into the CNF file, set through the API or capitalized\n"
 282 "with prefix 'LGL' instead of '--' through environment variables.\n"
 283 "Their default values are displayed in square brackets.\n");
 284       printf ("\n");
 285       lglusage (lgl);
 286       goto DONE;
 287     } else if (!strcmp (argv[i], "-s")) simponly = 1;
 288     else if (argv[i][0] == '-' && argv[i][1] == 'O') {
 289       if (simplevel > 0) {
 290         fprintf (stderr, "*** lingeling error: multiple '-O..' options\n");
 291         res = 1;
 292         goto DONE;
 293       }
 294       if ((simplevel = atoi (argv[i] + 2)) <= 0) {
 295         fprintf (stderr,
 296            "*** lingeling error: invalid '%s' option\n", argv[i]);
 297         res = 1;
 298         goto DONE;
 299       }
 300     } else if (!strcmp (argv[i], "-q")) lglsetopt (lgl, "verbose", -1);
 301     else if (!strcmp (argv[i], "-p")) {
 302       if (++i == argc) {
 303         fprintf (stderr, "*** lingeling error: argument to '-p' missing\n");
 304         res = 1;
 305         goto DONE;
 306       }
 307       if (pname) {
 308         fprintf (stderr,
 309                  "*** lingeling error: "
 310                  "multiple option files '%s' and '%s'\n",
 311                  pname, argv[i]);
 312         res = 1;
 313         goto DONE;
 314       }
 315       pname = argv[i];
 316     } else if (!strcmp (argv[i], "-t")) {
 317       if (++i == argc) {
 318         fprintf (stderr, "*** lingeling error: argument to '-t' missing\n");
 319         res = 1;
 320         goto DONE;
 321       }
 322       if (timelimit >= 0) {
 323         fprintf (stderr, "*** lingeling error: timit limit set twice\n");
 324         res = 1;
 325         goto DONE;
 326       }
 327       for (p = argv[i]; *p && isdigit (*p); p++)
 328         ;
 329       if (p == argv[i] || *p || (timelimit = atoi (argv[i])) < 0) {
 330         fprintf (stderr,
 331           "*** lingeling error: invalid time limit '-t %s'\n", argv[i]);
 332         res = 1;
 333         goto DONE;
 334       }
 335     } else if (!strcmp (argv[i], "-d") || !strcmp (argv[i], "--defaults")) {
 336       lglopts (lgl, "", 0);
 337       goto DONE;
 338     } else if (!strcmp (argv[i], "-e") || !strcmp (argv[i], "--embedded")) {
 339       lglopts (lgl, "c ", 1);
 340       goto DONE;
 341     } else if (!strcmp (argv[i], "-r") || !strcmp (argv[i], "--ranges")) {
 342       lglrgopts (lgl);
 343       goto DONE;
 344     } else if (!strcmp (argv[i], "-P") || !strcmp (argv[i], "--pcs")) {
 345       printf ("# generated by 'lingeling --pcs'\n");
 346       printf ("# version %s\n", lglversion ());
 347       lglpcs (lgl, 0);
 348       goto DONE;
 349     } else if (!strcmp (argv[i], "--pcs-mixed")) {
 350       printf ("# generated by 'lingeling --pcs-mixed'\n");
 351       printf ("# version %s\n", lglversion ());
 352       lglpcs (lgl, 1);
 353       goto DONE;
 354     } else if (!strcmp (argv[i], "--pcs-reduced")) {
 355       printf ("# generated by 'lingeling --pcs-reduced'\n");
 356       printf ("# version %s\n", lglversion ());
 357       lglpcs (lgl, -1);
 358       goto DONE;
 359     } else if (!strcmp (argv[i], "-f") || !strcmp (argv[i], "--force")) {
 360       ignmissingheader = 1;
 361     } else if (!strcmp (argv[i], "-i") || !strcmp (argv[i], "--ignore")) {
 362       ignaddcls = 1;
 363     } else if (!strcmp (argv[i], "-n") || !strcmp (argv[i], "no-witness")) {
 364       lglsetopt (lgl, "witness", 0);
 365     } else if (argv[i][0] == '-') {
 366       if (argv[i][1] == '-') {
 367         match = strchr (argv[i] + 2, '=');
 368         if (match) {
 369           p = match + 1;
 370           if (*p == '-') p++;   // TODO for what is this useful again?
 371           len = p - argv[i];
 372           if (!strncmp (argv[i], "--write-api-trace=", len)) {
 373             // TODO not handled yet ...
 374             continue;
 375           } else if (!strncmp (argv[i], "--thanks=", len)) {
 376             thanks = match + 1;
 377             continue;
 378           } else if (!isdigit (*p)) {
 379 ERR:
 380             fprintf (stderr,
 381               "*** lingeling error: invalid command line option '%s'\n",
 382               argv[i]);
 383             res = 1;
 384             goto DONE;
 385           }
 386           while (*++p) if (!isdigit (*p)) goto ERR;
 387           len = match - argv[i] - 2;
 388           tmp = malloc (len + 1);
 389           j = 0;
 390           for (p = argv[i] + 2; *p != '='; p++) tmp[j++] = *p;
 391           tmp[j] = 0;
 392           val = atoi (match + 1);
 393         } else if (!strncmp (argv[i], "--no-", 5)) {
 394           tmp = strdup (argv[i] + 5);
 395           val = 0;
 396         } else {
 397           tmp = strdup (argv[i] + 2);
 398           val = lglgetopt (lgl, tmp) + 1;
 399         }
 400         if (!lglhasopt (lgl, tmp)) { free (tmp); goto ERR; }
 401         lglsetopt (lgl, tmp, val);
 402         free (tmp);
 403       } else {
 404         if (argv[i][2]) goto ERR;
 405         if (!lglhasopt (lgl, argv[i] + 1)) goto ERR;
 406         val = lglgetopt (lgl, argv[i] + 1) + 1;
 407         lglsetopt (lgl, argv[i] + 1, val);
 408       }
 409     }
 410   }
 411   verbose = lglgetopt (lgl, "verbose");
 412   if (verbose >= 0) {
 413     lglbnr ("Lingeling SAT Solver", "c ", stdout);
 414     if (simponly) printf ("c simplifying only\n");
 415     if (simponly) fflush (stdout);
 416     lglsetopt (lgl, "trep", 1);
 417   }
 418   if (thanks) {
 419     unsigned seed = 0, i = 0, ch;
 420     int iseed;
 421     for (p = thanks; (ch = *p); p++) {
 422       seed += primes[i++] * ch;
 423       if (i == nprimes) i = 0;
 424     }
 425     if (seed >= (unsigned) INT_MAX) seed >>= 1;
 426     assert (seed <= (unsigned) INT_MAX);
 427     iseed = (int) seed;
 428     assert (iseed >= 0);
 429     if (verbose)
 430       printf ("c will have to thank %s (--seed=%d)\nc\n",
 431         thanks, iseed);
 432     lglsetopt (lgl, "seed", iseed);
 433   }
 434   if (verbose >= 2) {
 435    printf ("c\nc options after command line parsing:\nc\n");
 436    lglopts (lgl, "c ", 0);
 437    printf ("c\n");
 438    lglsizes (lgl);
 439    printf ("c\n");
 440   }
 441
 442   if (pname) {
 443     pfile = fopen (pname, "r");
 444     if (!pfile) {
 445       fprintf (stderr,
 446         "*** lingeling error: can not read option file %s\n", pname);
 447       res = 1;
 448       goto DONE;
 449     }
 450     if (verbose >= 0) {
 451       printf ("c reading options file %s\n", pname);
 452       fflush (stdout);
 453     }
 454     nopts = lglreadopts (lgl, pfile);
 455     if (verbose >= 0)
 456       printf ("c read and set %d options\nc\n", nopts), fflush (stdout);
 457     fclose (pfile);
 458   }
 459
 460   fflush (stdout);
 461
 462   if (verbose >= 1) {
 463     printf ("c\n");
 464     if (verbose >= 2) printf ("c final options:\nc\n");
 465     lglopts (lgl, "c ", 0);
 466   }
 467   if (timelimit >= 0) {
 468     if (verbose >= 0) {
 469       printf ("c\nc setting time limit of %d seconds\n", timelimit);
 470       fflush (stdout);
 471     }
 472     lglseterm (lgl, checkalarm, &caughtalarm);
 473     sig_alrm_handler = signal (SIGALRM, catchalrm);
 474     alarm (timelimit);
 475   }
 476
 477   processSAT(lgl);
 478
 479   if (timelimit >= 0) {
 480     caughtalarm = 0;
 481     (void) signal (SIGALRM, sig_alrm_handler);
 482   }
 483   if (verbose >= 0) fputs ("c\n", stdout), lglstats (lgl);
 484 DONE:
 485   resetsighandlers ();
 486   lgl4sigh = 0;
 487   lglrelease (lgl);
 488   return 0;
 489 }