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