lingeling/code/lglmain.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
  17 static LGL * lgl4sigh;
  18 static int catchedsig, verbose, ignmissingheader, ignaddcls;
  19
  20 static int * targets, sztargets, ntargets, multiple;
  21
  22 static void (*sig_int_handler)(int);
  23 static void (*sig_segv_handler)(int);
  24 static void (*sig_abrt_handler)(int);
  25 static void (*sig_term_handler)(int);
  26 static void (*sig_bus_handler)(int);
  27 static void (*sig_alrm_handler)(int);
  28
  29 static void resetsighandlers (void) {
  30   (void) signal (SIGINT, sig_int_handler);
  31   (void) signal (SIGSEGV, sig_segv_handler);
  32   (void) signal (SIGABRT, sig_abrt_handler);
  33   (void) signal (SIGTERM, sig_term_handler);
  34   (void) signal (SIGBUS, sig_bus_handler);
  35 }
  36
  37 static void caughtsigmsg (int sig) {
  38   if (verbose < 0) return;
  39   printf ("c\nc CAUGHT SIGNAL %d", sig);
  40   switch (sig) {
  41     case SIGINT: printf (" SIGINT"); break;
  42     case SIGSEGV: printf (" SIGSEGV"); break;
  43     case SIGABRT: printf (" SIGABRT"); break;
  44     case SIGTERM: printf (" SIGTERM"); break;
  45     case SIGBUS: printf (" SIGBUS"); break;
  46     case SIGALRM: printf (" SIGALRM"); break;
  47     default: break;
  48   }
  49   printf ("\nc\n");
  50   fflush (stdout);
  51 }
  52
  53 static void catchsig (int sig) {
  54   if (!catchedsig) {
  55     catchedsig = 1;
  56     caughtsigmsg (sig);
  57     fputs ("c s UNKNOWN\n", stdout);
  58     fflush (stdout);
  59     if (verbose >= 0) {
  60       lglflushtimers (lgl4sigh);
  61       lglstats (lgl4sigh);
  62       caughtsigmsg (sig);
  63     }
  64   }
  65   resetsighandlers ();
  66   if (!getenv ("LGLNABORT")) raise (sig); else exit (1);
  67 }
  68
  69 static void setsighandlers (void) {
  70   sig_int_handler = signal (SIGINT, catchsig);
  71   sig_segv_handler = signal (SIGSEGV, catchsig);
  72   sig_abrt_handler = signal (SIGABRT, catchsig);
  73   sig_term_handler = signal (SIGTERM, catchsig);
  74   sig_bus_handler = signal (SIGBUS, catchsig);
  75 }
  76
  77 static int timelimit = -1, caughtalarm = 0;
  78
  79 static void catchalrm (int sig) {
  80   assert (sig == SIGALRM);
  81   if (!caughtalarm) {
  82     caughtalarm = 1;
  83     caughtsigmsg (sig);
  84     if (timelimit >= 0) {
  85       printf ("c time limit of %d reached after %.1f seconds\nc\n",
  86               timelimit, lglsec (lgl4sigh));
  87       fflush (stdout);
  88     }
  89   }
  90 }
  91
  92 static int checkalarm (void * ptr) {
  93   assert (ptr == (void*) &caughtalarm);
  94   return caughtalarm;
  95 }
  96
  97 static int next (FILE * in, int *linenoptr) {
  98   int res = getc (in);
  99   if (res == '\n') *linenoptr += 1;
 100   return res;
 101 }
 102
 103 static char isoptchartab[256];
 104 static int isoptchartabinitialized;
 105
 106 static int isoptchar (unsigned char uch) {
 107   int i;
 108   if (!isoptchartabinitialized) {
 109     for (i = 'a'; i <= 'z'; i++) isoptchartab[i] = 1;
 110     for (i = 'A'; i <= 'Z'; i++) isoptchartab[i] = 1;
 111     for (i = '0'; i <= '9'; i++) isoptchartab[i] = 1;
 112     isoptchartab['-'] = isoptchartab['_'] = 1;
 113     isoptchartabinitialized = 1;
 114   }
 115   return isoptchartab[uch];
 116 }
 117
 118 typedef struct Opt { char * name; int size, count; } Opt;
 119
 120 static void pushoptch (Opt * opt, int ch) {
 121   if (opt->count + 1 >= opt->size)
 122    opt->name = realloc (opt->name, opt->size = opt->size ? 2*opt->size : 2);
 123
 124   opt->name[opt->count++] = ch;
 125   opt->name[opt->count] = 0;
 126 }
 127
 128 static const char * parse (LGL * lgl, FILE * in, int * lp) {
 129   int ch, prev, m, n, v, c, l, lit, sign, val, embedded = 0, header;
 130   Opt opt;
 131   memset (&opt, 0, sizeof opt);
 132 SKIP:
 133   ch = next (in, lp);
 134   if (ch == ' ' || ch == '\t' || ch == '\n' || ch == '\r') goto SKIP;
 135   if (ch == 'c') {
 136     ch  = next (in, lp);
 137     while (ch != '\n') {
 138       if (ch == EOF) return "end of file in comment";
 139       prev = ch;
 140       ch = next (in, lp);
 141       if (prev != '-') continue;
 142       if (ch != '-') continue;
 143       assert (!opt.count);
 144       ch = next (in, lp);
 145       while (isoptchar (ch)) {
 146         assert (ch != '\n');
 147         pushoptch (&opt, ch);
 148         ch = next (in, lp);
 149       }
 150       opt.count = 0;
 151       if (ch != '=') continue;
 152       ch = next (in, lp);
 153       if (ch == '-') sign = -1, ch = next (in, lp); else sign = 1;
 154       if (!isdigit (ch)) continue;
 155       val = ch - '0';
 156       while (isdigit (ch = next (in, lp)))
 157         val = 10 * val + (ch - '0');
 158
 159       if (!lglhasopt (lgl, opt.name)) {
 160         fprintf (stderr,
 161                  "*** lingeling warning: "
 162                  "parsed invalid embedded option '--%s'\n",
 163                  opt.name);
 164         continue;
 165       }
 166
 167       val *= sign;
 168
 169       if (!embedded++ && verbose >= 0)
 170         printf ("c\nc embedded options:\nc\n");
 171       if (!strcmp (opt.name, "verbose")) verbose = val;
 172       if (verbose >= 0) printf ("c --%s=%d\n", opt.name, val);
 173       lglsetopt (lgl, opt.name, val);
 174     }
 175     goto SKIP;
 176   }
 177   free (opt.name);
 178   if (verbose >= 0) {
 179      if (embedded) printf ("c\n"); else printf ("c no embedded options\n");
 180      fflush (stdout);
 181   }
 182   header = m = n = v = l = c = 0;
 183   if (ignmissingheader) {
 184     if (ch == 'p')  {
 185       if (verbose >= 0) printf ("will not read header");
 186       while ((ch = next (in, lp)) != '\n' && ch != EOF)
 187         ;
 188     } else if (verbose >= 0) printf ("c skipping missing header\n");
 189     goto BODY2;
 190   }
 191   if (ch != 'p') return "missing 'p ...' header";
 192   if (next (in, lp) != ' ') return "invalid header: expected ' ' after 'p'";
 193   while ((ch = next (in, lp)) == ' ')
 194     ;
 195   if (ch != 'c') return "invalid header: expected 'c' after ' '";
 196   if (next (in, lp) != 'n') return "invalid header: expected 'n' after 'c'";
 197   if (next (in, lp) != 'f') return "invalid header: expected 'f' after 'n'";
 198   if (next (in, lp) != ' ') return "invalid header: expected ' ' after 'f'";
 199   while ((ch = next (in, lp)) == ' ')
 200     ;
 201   if (!isdigit (ch)) return "invalid header: expected digit after 'p cnf '";
 202   m = ch - '0';
 203   while (isdigit (ch = next (in, lp)))
 204     m = 10 * m + (ch - '0');
 205   if (ch != ' ') return "invalid header: expected ' ' after 'p cnf <m>'";
 206   while ((ch = next (in, lp)) == ' ')
 207     ;
 208   if (!isdigit (ch))
 209     return "invalid header: expected digit after 'p cnf <m> '";
 210   n = ch - '0';
 211   while (isdigit (ch = next (in, lp)))
 212     n = 10 * n + (ch - '0');
 213   while (ch == ' ')
 214     ch = next (in, lp);
 215   if (ch != '\n') return "invalid header: expected new line after header";
 216   if (verbose >= 0)
 217     printf ("c found 'p cnf %d %d' header\n", m, n), fflush (stdout);
 218   header = 1;
 219 BODY:
 220   ch = next (in, lp);
 221 BODY2:
 222   if (ch == ' ' || ch == '\t' || ch == '\n' || ch == '\r') goto BODY;
 223   if (ch == 'c') {
 224     while ((ch = next (in, lp)) != '\n')
 225       if (ch == EOF) return "end of file in comment";
 226     goto BODY;
 227   }
 228   if (ch == EOF) {
 229     if (header && c + 1 == n) return "clause missing";
 230     if (header && c < n) return "clauses missing";
 231 DONE:
 232     if (verbose >= 0) {
 233       printf ("c read %d variables, %d clauses, %d literals in %.2f seconds\n",
 234               v, c, l, lglsec (lgl));
 235       fflush (stdout);
 236     }
 237     return 0;
 238   }
 239   if (ch == '-') {
 240     ch = next (in, lp);
 241     if (ch == '0') return "expected positive digit after '-'";
 242     sign = -1;
 243   } else sign = 1;
 244   if (!isdigit (ch)) return "expected digit";
 245   if (header && c == n) return "too many clauses";
 246   lit = ch - '0';
 247   while (isdigit (ch = next (in, lp)))
 248     lit = 10 * lit + (ch - '0');
 249   if (header && lit > m) return "maxium variable index exceeded";
 250   if (lit > v) v = lit;
 251   if (lit) l++;
 252   else c++;
 253   lit *= sign;
 254   lgladd (lgl, lit);
 255   if (!lit && ignaddcls && c == n) goto DONE;
 256   goto BODY;
 257 }
 258
 259 typedef struct OBuf { char line[81]; int pos; } OBuf;
 260
 261 static void flushobuf (OBuf * obuf, int simponly, FILE * file) {
 262   assert (0 < obuf->pos);
 263   assert (obuf->pos < 81);
 264   obuf->line[obuf->pos++] = '\n';
 265   assert (obuf->pos < 81);
 266   obuf->line[obuf->pos++] = 0;
 267   if (simponly) fputs ("c ", file);
 268   fputc ('v', file);
 269   fputs (obuf->line, file);
 270   obuf->pos = 0;
 271 }
 272
 273 static void print2obuf (OBuf * obuf, int i, int simponly, FILE * file) {
 274   char str[20];
 275   int len;
 276   sprintf (str, " %d", i);
 277   len = strlen (str);
 278   assert (len > 1);
 279   if (obuf->pos + len > 79) flushobuf (obuf, simponly, file);
 280   strcpy (obuf->line + obuf->pos, str);
 281   obuf->pos += len;
 282   assert (obuf->pos <= 79);
 283 }
 284
 285 static FILE * writefile (const char * name, int * clptr) {
 286   int len = strlen (name);
 287   char * tmp;
 288   FILE * res;
 289   if (len >= 3 && !strcmp (name + len - 3, ".gz")) {
 290     tmp = malloc (len + 20);
 291     unlink (name);
 292     sprintf (tmp, "gzip -c > %s", name);
 293     res = popen (tmp, "w");
 294     if (res) *clptr = 2;
 295     free (tmp);
 296   } else {
 297     res = fopen (name, "w");
 298     if (res) *clptr = 1;
 299   }
 300   if (!res) fprintf (stderr, "*** lingeling error: can not write %s\n", name);
 301   return res;
 302 }
 303
 304 static void closefile (FILE * file, int type) {
 305   if (type == 1) fclose (file);
 306   if (type == 2) pclose (file);
 307 }
 308
 309 static void lgltravcounter (void * voidptr, int lit) {
 310   int * cntptr = voidptr;
 311   if (!lit) *cntptr += 1;
 312 }
 313
 314 static void lglpushtarget (int target) {
 315   if (ntargets == sztargets)
 316     targets = realloc (targets, sizeof *targets *
 317                (sztargets = sztargets ? 2*sztargets : 1));
 318   targets[ntargets++] = target;
 319 }
 320
 321 static int lglmonotifiy (void * lgl, int target, int val) {
 322   printf ("t %d %d after %.3f seconds\n", target, val, lglsec (lgl));
 323   fflush (stdout);
 324   return 1;
 325 }
 326
 327 static int primes[] = {
 328   200000033, 200000039, 200000051, 200000069, 200000081,
 329 };
 330
 331 static int nprimes = sizeof primes / sizeof *primes;
 332
 333 int main (int argc, char ** argv) {
 334   int res, i, j, clin, clout, val, len, lineno, simponly, count, target;
 335   const char * iname, * oname, * pname, * match, * p, * err, * thanks;
 336   int maxvar, lit, nopts, simplevel;
 337   FILE * in, * out, * pfile;
 338   char * tmp;
 339   LGL * lgl;
 340   OBuf obuf;
 341   lineno = 1;
 342   in = out = 0;
 343   res = clin = clout = simponly = simplevel = 0;
 344   iname = oname = pname = thanks = 0;
 345   lgl4sigh = lgl = lglinit ();
 346   setsighandlers ();
 347   for (i = 1; i < argc; i++) {
 348     if (!strcmp (argv[i], "-h") || !strcmp (argv[i], "--help")) {
 349       printf ("usage: lingeling [<option> ...][<file>[.gz]]\n");
 350       printf ("\n");
 351       printf ("where <option> is one of the following:\n");
 352       printf ("\n");
 353       printf ("-q               be quiet (same as '--verbose=-1')\n");
 354       printf ("-s               only simplify and print to output file\n");
 355       printf ("-O<L>            set simplification level to <L>\n");
 356       printf ("-o <output>      set output file (default 'stdout')\n");
 357       printf ("-p <options>     read options from file\n");
 358       printf ("\n");
 359       printf ("-t <seconds>     set time limit\n");
 360       printf ("\n");
 361       printf ("-a <assumption>  use multiple assumptions\n");
 362       printf ("-m <objective>   use multiple objectives\n");
 363       printf ("\n");
 364       printf ("-h|--help        print command line option summary\n");
 365       printf ("-f|--force       force reading even without header\n");
 366       printf ("-i|--ignore      ignore additional clauses\n");
 367       printf ("-r|--ranges      print value ranges of options\n");
 368       printf ("-d|--defaults    print default values of options\n");
 369       printf ("-P|--pcs         print (full) PCS file\n");
 370       printf ("--pcs-mixed      print mixed PCS file\n");
 371       printf ("--pcs-reduced    print reduced PCS file\n");
 372       printf ("-e|--embedded    ditto but in an embedded format print\n");
 373       printf ("-n|--no-witness   do not print solution (see '--witness')\n");
 374       printf ("\n");
 375       printf ("--thanks=<whom>  alternative way of specifying the seed\n");
 376       printf ("                 (inspired by Vampire)\n");
 377       printf ("\n");
 378       printf (
 379 "The following options can also be used in the form '--<name>=<int>',\n"
 380 "just '--<name>' for increment and '--no-<name>' for zero.  They\n"
 381 "can be embedded into the CNF file, set through the API or capitalized\n"
 382 "with prefix 'LGL' instead of '--' through environment variables.\n"
 383 "Their default values are displayed in square brackets.\n");
 384       printf ("\n");
 385       lglusage (lgl);
 386       goto DONE;
 387     } else if (!strcmp (argv[i], "-s")) simponly = 1;
 388     else if (argv[i][0] == '-' && argv[i][1] == 'O') {
 389       if (simplevel > 0) {
 390         fprintf (stderr, "*** lingeling error: multiple '-O..' options\n");
 391         res = 1;
 392         goto DONE;
 393       }
 394       if ((simplevel = atoi (argv[i] + 2)) <= 0) {
 395         fprintf (stderr,
 396            "*** lingeling error: invalid '%s' option\n", argv[i]);
 397         res = 1;
 398         goto DONE;
 399       }
 400     } else if (!strcmp (argv[i], "-q")) lglsetopt (lgl, "verbose", -1);
 401     else if (!strcmp (argv[i], "-o")) {
 402       if (++i == argc) {
 403         fprintf (stderr, "*** lingeling error: argument to '-o' missing\n");
 404         res = 1;
 405         goto DONE;
 406       }
 407       if (oname) {
 408         fprintf (stderr,
 409                  "*** lingeling error: "
 410                  "multiple output files '%s' and '%s'\n",
 411                  oname, argv[i]);
 412         res = 1;
 413         goto DONE;
 414       }
 415       oname = argv[i];
 416     } else if (!strcmp (argv[i], "-p")) {
 417       if (++i == argc) {
 418         fprintf (stderr, "*** lingeling error: argument to '-p' missing\n");
 419         res = 1;
 420         goto DONE;
 421       }
 422       if (pname) {
 423         fprintf (stderr,
 424                  "*** lingeling error: "
 425                  "multiple option files '%s' and '%s'\n",
 426                  pname, argv[i]);
 427         res = 1;
 428         goto DONE;
 429       }
 430       pname = argv[i];
 431     } else if (!strcmp (argv[i], "-t")) {
 432       if (++i == argc) {
 433         fprintf (stderr, "*** lingeling error: argument to '-t' missing\n");
 434         res = 1;
 435         goto DONE;
 436       }
 437       if (timelimit >= 0) {
 438         fprintf (stderr, "*** lingeling error: timit limit set twice\n");
 439         res = 1;
 440         goto DONE;
 441       }
 442       for (p = argv[i]; *p && isdigit (*p); p++)
 443         ;
 444       if (p == argv[i] || *p || (timelimit = atoi (argv[i])) < 0) {
 445         fprintf (stderr,
 446           "*** lingeling error: invalid time limit '-t %s'\n", argv[i]);
 447         res = 1;
 448         goto DONE;
 449       }
 450     } else if (!strcmp (argv[i], "-a")) {
 451       if (++i == argc) {
 452         fprintf (stderr, "*** lingeling error: argument to '-a' missing\n");
 453         res = 1;
 454         goto DONE;
 455       }
 456       if (multiple) {
 457         assert (ntargets > 0);
 458         fprintf (stderr, "*** lingeling error: unexpectd '-a' after '-m'\n");
 459         res = 1;
 460         goto DONE;
 461       }
 462       target = atoi (argv[i]);
 463       if (!target) {
 464         fprintf (stderr,
 465           "*** lingeling error: invalid literal in '-a %d'\n", target);
 466         res = 1;
 467         goto DONE;
 468       }
 469       lglpushtarget (target);
 470     } else if (!strcmp (argv[i], "-m")) {
 471       if (++i == argc) {
 472         fprintf (stderr, "*** lingeling error: argument to '-m' missing\n");
 473         res = 1;
 474         goto DONE;
 475       }
 476       if (!multiple && ntargets > 0) {
 477         fprintf (stderr, "*** lingeling error: unexpectd '-m' after '-a'\n");
 478         res = 1;
 479         goto DONE;
 480       }
 481       target = atoi (argv[i]);
 482       if (!target) {
 483         fprintf (stderr,
 484           "*** lingeling error: invalid literal in '-m %d'\n", target);
 485         res = 1;
 486         goto DONE;
 487       }
 488       lglpushtarget (target);
 489       multiple = 1;
 490     } else if (!strcmp (argv[i], "-d") || !strcmp (argv[i], "--defaults")) {
 491       lglopts (lgl, "", 0);
 492       goto DONE;
 493     } else if (!strcmp (argv[i], "-e") || !strcmp (argv[i], "--embedded")) {
 494       lglopts (lgl, "c ", 1);
 495       goto DONE;
 496     } else if (!strcmp (argv[i], "-r") || !strcmp (argv[i], "--ranges")) {
 497       lglrgopts (lgl);
 498       goto DONE;
 499     } else if (!strcmp (argv[i], "-P") || !strcmp (argv[i], "--pcs")) {
 500       printf ("# generated by 'lingeling --pcs'\n");
 501       printf ("# version %s\n", lglversion ());
 502       lglpcs (lgl, 0);
 503       goto DONE;
 504     } else if (!strcmp (argv[i], "--pcs-mixed")) {
 505       printf ("# generated by 'lingeling --pcs-mixed'\n");
 506       printf ("# version %s\n", lglversion ());
 507       lglpcs (lgl, 1);
 508       goto DONE;
 509     } else if (!strcmp (argv[i], "--pcs-reduced")) {
 510       printf ("# generated by 'lingeling --pcs-reduced'\n");
 511       printf ("# version %s\n", lglversion ());
 512       lglpcs (lgl, -1);
 513       goto DONE;
 514     } else if (!strcmp (argv[i], "-f") || !strcmp (argv[i], "--force")) {
 515       ignmissingheader = 1;
 516     } else if (!strcmp (argv[i], "-i") || !strcmp (argv[i], "--ignore")) {
 517       ignaddcls = 1;
 518     } else if (!strcmp (argv[i], "-n") || !strcmp (argv[i], "no-witness")) {
 519       lglsetopt (lgl, "witness", 0);
 520     } else if (argv[i][0] == '-') {
 521       if (argv[i][1] == '-') {
 522         match = strchr (argv[i] + 2, '=');
 523         if (match) {
 524           p = match + 1;
 525           if (*p == '-') p++;   // TODO for what is this useful again?
 526           len = p - argv[i];
 527           if (!strncmp (argv[i], "--write-api-trace=", len)) {
 528             // TODO not handled yet ...
 529             continue;
 530           } else if (!strncmp (argv[i], "--thanks=", len)) {
 531             thanks = match + 1;
 532             continue;
 533           } else if (!isdigit (*p)) {
 534 ERR:
 535             fprintf (stderr,
 536               "*** lingeling error: invalid command line option '%s'\n",
 537               argv[i]);
 538             res = 1;
 539             goto DONE;
 540           }
 541           while (*++p) if (!isdigit (*p)) goto ERR;
 542           len = match - argv[i] - 2;
 543           tmp = malloc (len + 1);
 544           j = 0;
 545           for (p = argv[i] + 2; *p != '='; p++) tmp[j++] = *p;
 546           tmp[j] = 0;
 547           val = atoi (match + 1);
 548         } else if (!strncmp (argv[i], "--no-", 5)) {
 549           tmp = strdup (argv[i] + 5);
 550           val = 0;
 551         } else {
 552           tmp = strdup (argv[i] + 2);
 553           val = lglgetopt (lgl, tmp) + 1;
 554         }
 555         if (!lglhasopt (lgl, tmp)) { free (tmp); goto ERR; }
 556         lglsetopt (lgl, tmp, val);
 557         free (tmp);
 558       } else {
 559         if (argv[i][2]) goto ERR;
 560         if (!lglhasopt (lgl, argv[i] + 1)) goto ERR;
 561         val = lglgetopt (lgl, argv[i] + 1) + 1;
 562         lglsetopt (lgl, argv[i] + 1, val);
 563       }
 564     } else if (iname) {
 565       fprintf (stderr, "*** lingeling error: can not read '%s' and '%s'\n",
 566                iname, argv[i]);
 567       res = 1;
 568       goto DONE;
 569     } else iname = argv[i];
 570   }
 571   verbose = lglgetopt (lgl, "verbose");
 572   if (verbose >= 0) {
 573     lglbnr ("Lingeling SAT Solver", "c ", stdout);
 574     if (simponly) printf ("c simplifying only\n");
 575     if (oname) printf ("c output file %s\n", oname);
 576     if (simponly || oname) fflush (stdout);
 577     lglsetopt (lgl, "trep", 1);
 578   }
 579   if (thanks) {
 580     unsigned seed = 0, i = 0, ch;
 581     int iseed;
 582     for (p = thanks; (ch = *p); p++) {
 583       seed += primes[i++] * ch;
 584       if (i == nprimes) i = 0;
 585     }
 586     if (seed >= (unsigned) INT_MAX) seed >>= 1;
 587     assert (seed <= (unsigned) INT_MAX);
 588     iseed = (int) seed;
 589     assert (iseed >= 0);
 590     if (verbose)
 591       printf ("c will have to thank %s (--seed=%d)\nc\n",
 592         thanks, iseed);
 593     lglsetopt (lgl, "seed", iseed);
 594   }
 595   if (verbose >= 2) {
 596    printf ("c\nc options after command line parsing:\nc\n");
 597    lglopts (lgl, "c ", 0);
 598    printf ("c\n");
 599    lglsizes (lgl);
 600    printf ("c\n");
 601   }
 602   if (iname) {
 603     len = strlen (iname);
 604     if (len >= 3 && !strcmp (iname + len - 3, ".gz")) {
 605       if (verbose >= 1) printf ("c piping '%s' through 'gunzip'\n", iname);
 606       tmp = malloc (len + 20);
 607       sprintf (tmp, "gunzip -c %s", iname);
 608       in = popen (tmp, "r");
 609       if (in) clin = 2;
 610       free (tmp);
 611     } else if (len >= 5 && !strcmp (iname + len - 5, ".lzma")) {
 612       if (verbose >= 1) printf ("c piping '%s' through 'lzcat'\n", iname);
 613       tmp = malloc (len + 20);
 614       sprintf (tmp, "lzcat %s", iname);
 615       in = popen (tmp, "r");
 616       if (in) clin = 2;
 617       free (tmp);
 618     } else if (len >= 4 && !strcmp (iname + len - 4, ".bz2")) {
 619       if (verbose >= 1) printf ("c piping '%s' through 'bzcat'\n", iname);
 620       tmp = malloc (len + 20);
 621       sprintf (tmp, "bzcat %s", iname);
 622       in = popen (tmp, "r");
 623       if (in) clin = 2;
 624       free (tmp);
 625     } else if (len >= 3 && !strcmp (iname + len - 3, ".7z")) {
 626       if (verbose >= 1) printf ("c piping '%s' through '7z'\n", iname);
 627       tmp = malloc (len + 40);
 628       sprintf (tmp, "7z x -so %s 2>/dev/null", iname);
 629       in = popen (tmp, "r");
 630       if (in) clin = 2;
 631       free (tmp);
 632     } else {
 633       in = fopen (iname, "r");
 634       if (in) clin = 1;
 635     }
 636     if (!in) {
 637       fprintf (stderr,
 638          "*** lingeling error: can not read input file %s\n", iname);
 639       res = 1;
 640       goto DONE;
 641     }
 642   } else iname = "<stdin>", in = stdin;
 643   if (pname) {
 644     pfile = fopen (pname, "r");
 645     if (!pfile) {
 646       fprintf (stderr,
 647         "*** lingeling error: can not read option file %s\n", pname);
 648       res = 1;
 649       goto DONE;
 650     }
 651     if (verbose >= 0) {
 652       printf ("c reading options file %s\n", pname);
 653       fflush (stdout);
 654     }
 655     nopts = lglreadopts (lgl, pfile);
 656     if (verbose >= 0)
 657       printf ("c read and set %d options\nc\n", nopts), fflush (stdout);
 658     fclose (pfile);
 659   }
 660   if (verbose >= 0) printf ("c reading input file %s\n", iname);
 661   fflush (stdout);
 662   if ((err = parse (lgl, in, &lineno))) {
 663     fprintf (stderr, "%s:%d: %s\n", iname, lineno, err);
 664     res = 1;
 665     goto DONE;
 666   }
 667   closefile (in, clin);
 668   clin = 0;
 669   if (verbose >= 1) {
 670     printf ("c\n");
 671     if (verbose >= 2) printf ("c final options:\nc\n");
 672     lglopts (lgl, "c ", 0);
 673   }
 674   if (timelimit >= 0) {
 675     if (verbose >= 0) {
 676       printf ("c\nc setting time limit of %d seconds\n", timelimit);
 677       fflush (stdout);
 678     }
 679     lglseterm (lgl, checkalarm, &caughtalarm);
 680     sig_alrm_handler = signal (SIGALRM, catchalrm);
 681     alarm (timelimit);
 682   }
 683   if (multiple) lglpushtarget (0), ntargets--;
 684   else for (i = 0; i < ntargets; i++) lglassume (lgl, targets[i]);
 685   if (multiple) res = lglmosat (lgl, lgl, lglmonotifiy, targets);
 686   else {
 687     if (simplevel > 0) {
 688       if (verbose >= 1) {
 689         printf ("c simplifying with simplification level %d\n", simplevel);
 690         fflush (stdout);
 691       }
 692       res = lglsimp (lgl, simplevel);
 693       if (verbose >= 1) {
 694         printf ("c simplifying result %d after %.2f seconds\n",
 695           res, lglsec (lgl));
 696         fflush (stdout);
 697       }
 698     } else res = 0;
 699     res = lglsat (lgl);
 700   }
 701   if (timelimit >= 0) {
 702     caughtalarm = 0;
 703     (void) signal (SIGALRM, sig_alrm_handler);
 704   }
 705   if (oname) {
 706     double start = lglsec (lgl), delta;
 707     if (!strcmp (oname, "-")) out = stdout, oname = "<stdout>", clout = 0;
 708     else if (!(out = writefile (oname, &clout))) { res = 1; goto DONE; }
 709     if (verbose >= 0) {
 710       count = 0;
 711       lglctrav (lgl, &count, lgltravcounter);
 712       printf ("c\nc writing 'p cnf %d %d' to '%s'\n",
 713               lglmaxvar (lgl), count, oname);
 714       fflush (stdout);
 715     }
 716     lglprint (lgl, out);
 717     closefile (out, clout);
 718     if (verbose >= 0) {
 719       delta = lglsec (lgl) - start; if (delta < 0) delta = 0;
 720       printf ("c collected garbage and wrote '%s' in %.1f seconds\n",
 721               oname, delta);
 722       printf ("c\n"), fflush (stdout);
 723     }
 724   }
 725   if (!simponly || verbose >= 0) {
 726     if (simponly) fputs ("c ", stdout);
 727     if (res == 10) fputs ("s SATISFIABLE\n", stdout);
 728     else if (res == 20) fputs ("s UNSATISFIABLE\n", stdout);
 729     else fputs ("c s UNKNOWN\n", stdout);
 730     if (thanks) printf ("c\nc Thanks to %s!\nc\n", thanks);
 731     fflush (stdout);
 732     if (res == 10 && lglgetopt (lgl, "witness")) {
 733       obuf.pos = 0;
 734       maxvar = lglmaxvar (lgl);
 735       for (i = 1; i <= maxvar; i++) {
 736         lit = (lglderef (lgl, i) > 0) ? i : -i;
 737         print2obuf (&obuf, lit, simponly, stdout);
 738       }
 739       print2obuf (&obuf, 0, simponly, stdout);
 740       if (obuf.pos > 0) flushobuf (&obuf, simponly, stdout);
 741       fflush (stdout);
 742     }
 743   }
 744   if (verbose >= 0) fputs ("c\n", stdout), lglstats (lgl);
 745 DONE:
 746   closefile (in, clin);
 747   resetsighandlers ();
 748   lgl4sigh = 0;
 749   lglrelease (lgl);
 750   free (targets);
 751   return res;
 752 }