backends/precosat/precomain.cc

   1 /***************************************************************************
   2 Copyright (c) 2009, Armin Biere, Johannes Kepler University.
   3
   4 Permission is hereby granted, free of charge, to any person obtaining a copy
   5 of this software and associated documentation files (the "Software"), to
   6 deal in the Software without restriction, including without limitation the
   7 rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
   8 sell copies of the Software, and to permit persons to whom the Software is
   9 furnished to do so, subject to the following conditions:
  10
  11 The above copyright notice and this permission notice shall be included in
  12 all copies or substantial portions of the Software.
  13
  14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
  15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
  16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
  17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
  18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
  19 FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
  20 IN THE SOFTWARE.
  21 ****************************************************************************/
  22
  23 #include "precosat.hh"
  24 #include "precobnr.hh"
  25
  26 extern "C" {
  27 #include <signal.h>
  28 #include <stdio.h>
  29 #include <string.h>
  30 #include <ctype.h>
  31 };
  32
  33 using namespace PrecoSat;
  34
  35 static Solver * solverptr;
  36 static bool catchedsig;
  37 static int verbose, quiet;
  38
  39 static void (*sig_int_handler)(int);
  40 static void (*sig_segv_handler)(int);
  41 static void (*sig_abrt_handler)(int);
  42 static void (*sig_term_handler)(int);
  43
  44 static bool hasgzsuffix (const char * str)
  45   { return strlen (str) >= 3 && !strcmp (str + strlen (str) - 3, ".gz"); }
  46
  47 static void
  48 resetsighandlers (void) {
  49   (void) signal (SIGINT, sig_int_handler);
  50   (void) signal (SIGSEGV, sig_segv_handler);
  51   (void) signal (SIGABRT, sig_abrt_handler);
  52   (void) signal (SIGTERM, sig_term_handler);
  53 }
  54
  55 static void caughtsigmsg (int sig) {
  56   if (verbose) printf ("c\n");
  57   if (!quiet) printf ("c *** CAUGHT SIGNAL %d ***\n", sig);
  58   if (verbose) printf ("c\n");
  59   fflush (stdout);
  60 }
  61
  62 static void catchsig (int sig) {
  63   if (!catchedsig) {
  64     catchedsig = true;
  65     caughtsigmsg (sig);
  66     if (verbose) solverptr->prstats (), caughtsigmsg (sig);
  67   }
  68
  69   resetsighandlers ();
  70   raise (sig);
  71 }
  72
  73 static void
  74 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 }
  80
  81 static const char * usage =
  82 "usage: precosat [-h|-v|-n][-l <lim>][--[no-]<opt>[=<val>]] [<dimacs>]\n"
  83 "\n"
  84 "  -h             this command line summary\n"
  85 "  -v             increase verbosity\n"
  86 "  -q             be quiet and only set exit code\n"
  87 "  -n             do not print witness\n"
  88 "  -N             do not print witness nor result line\n"
  89 "  -l <lim>       set decision limit\n"
  90 "  -p             print CNF after first simplification \n"
  91 "  -s             simplify and print (same as '-N -p -l 0')\n"
  92 "  -e             satelite only style preprocessing\n"
  93 "  -k             blocked clause only style preprocessing\n"
  94 "  -o <file>      set output file for '-p' respectively '-s'\n"
  95 "  <dimacs>       dimacs input file (default stdin)\n"
  96 "\n"
  97 "  --<opt>        set internal option <opt> to 1\n"
  98 "  --no-<opt>     set internal option <opt> to 0\n"
  99 "  --<opt>=<val>  set internal option <opt> to integer value <val>\n"
 100 ;
 101
 102 int main (int argc, char ** argv) {
 103   bool fclosefile=false,pclosefile=false,nowit=false,nores=false,simp=false;
 104   int print=0, decision_limit=INT_MAX;
 105   const char * name = 0, * output = 0;
 106   bool satelite=false,blocked=false;
 107   FILE * file = stdin;
 108   for (int i = 1; i < argc; i++) {
 109     if (!strcmp (argv[i], "-h")) {
 110       fputs (usage, stdout);
 111       exit (0);
 112     }
 113     if (!strcmp (argv[i], "-v")) {
 114       if (verbose >= 2) {
 115         fprintf (stderr, "*** precosat: too many '-v'\n");
 116         exit (1);
 117       }
 118       verbose++;
 119       continue;
 120     }
 121     if (!strcmp (argv[i], "--verbose")) { verbose=1; continue; }
 122     if (!strcmp (argv[i], "--no-verbose")) { verbose=0; continue; }
 123     if (!strcmp (argv[i], "--verbose=0")) { verbose=0; continue; }
 124     if (!strcmp (argv[i], "--verbose=1")) { verbose=1; continue; }
 125     if (!strcmp (argv[i], "--verbose=2")) { verbose=2; continue; }
 126     if (!strcmp (argv[i], "-q")) { quiet = 1; continue; }
 127     if (!strcmp (argv[i], "-p")) { print = 1; continue; }
 128     if (!strcmp (argv[i], "-s")) { simp = true; continue; }
 129     if (!strcmp (argv[i], "--quiet")) { quiet = 1; continue; }
 130     if (!strcmp (argv[i], "--no-quiet")) { quiet = 0; continue; }
 131     if (!strcmp (argv[i], "--quiet=0")) { quiet = 0; continue; }
 132     if (!strcmp (argv[i], "--quiet=1")) { quiet = 1; continue; }
 133     if (!strcmp (argv[i], "-n")) { nowit = true; continue; }
 134     if (!strcmp (argv[i], "-N")) { nores = true; continue; }
 135     if (!strcmp (argv[i], "-k")) { blocked = true; continue; }
 136     if (!strcmp (argv[i], "-e")) { satelite = true; continue; }
 137     if (!strcmp  (argv[i], "-l")) {
 138       if (i + 1 == argc) {
 139         fprintf (stderr, "*** precosat: argument to '-l' missing\n");
 140         exit (1);
 141       }
 142       decision_limit = atoi (argv[++i]);
 143       continue;
 144     }
 145     if (!strcmp (argv[i], "-o")) {
 146       if (i + 1 == argc) {
 147         fprintf (stderr, "*** precosat: argument to '-o' missing\n");
 148         exit (1);
 149       }
 150       output = argv[++i];
 151       continue;
 152     }
 153     if (argv[i][0] == '-' && argv[i][1] == '-') continue;
 154     if (argv[i][0] == '-' || name) {
 155       fprintf (stderr, "*** precosat: invalid usage (try '-h')\n");
 156       exit (1);
 157     }
 158     name = argv[i];
 159     if (hasgzsuffix (name)) {
 160       char * cmd = (char*) malloc (strlen(name) + 100);
 161       sprintf (cmd, "gunzip -c %s 2>/dev/null", name);
 162       if ((file = popen (cmd, "r")))
 163         pclosefile = true;
 164       free (cmd);
 165     } else if ((file = fopen (name, "r")))
 166       fclosefile = true;
 167   }
 168   if (!name) name = "<stdin>";
 169   if (!file) {
 170     fprintf (stderr, "*** precosat: can not read '%s'\n", name);
 171     exit (1);
 172   }
 173   if (blocked && satelite) die ("can not use both '-e' and '-k'");
 174   if (nores) nowit = true;
 175   if (blocked || satelite) simp = true;
 176   if (simp) nowit = nores = true, print = 1, decision_limit = 0;
 177   if (quiet) verbose = 0, nowit = true;
 178   if (verbose) {
 179     precosat_banner ();
 180     printf ("c\nc reading %s\n", name);
 181     fflush (stdout);
 182   }
 183   int ch;
 184   while ((ch = getc (file)) == 'c')
 185     while ((ch = getc (file)) != '\n' && ch != EOF)
 186       ;
 187   if (ch == EOF)
 188     goto INVALID_HEADER;
 189   ungetc (ch, file);
 190   int m, n;
 191   if (fscanf (file, "p cnf %d %d\n", &m, &n) != 2) {
 192 INVALID_HEADER:
 193     fprintf (stderr, "*** precosat: invalid header\n");
 194     exit (1);
 195   }
 196   if (verbose) {
 197     printf ("c found header 'p cnf %d %d'\n", m, n);
 198     fflush (stdout);
 199   }
 200   Solver solver;
 201   solver.init (m);
 202   solverptr = &solver;
 203   setsighandlers ();
 204   for (int i = 1; i < argc; i++) {
 205     bool ok = true;
 206     if (argv[i][0] == '-' && argv[i][1] == '-') {
 207       if (argv[i][2] == 'n' && argv[i][3] == 'o' && argv[i][4] == '-') {
 208         if (!solver.set (argv[i] + 5, 0)) ok = false;
 209       } else {
 210         const char * arg = argv[i] + 2, * p;
 211         for (p = arg; *p && *p != '='; p++)
 212           ;
 213         if (*p) {
 214           assert (*p == '=');
 215           char * opt = strndup (arg, p - arg);
 216           if (!strcmp (opt, "output")) ok = solver.set (opt, p + 1);
 217           else ok = solver.set (opt, atoi (p + 1));
 218           free (opt);
 219         } else ok = solver.set (argv[i] + 2, 1);
 220       }
 221     }
 222     if (!ok) {
 223       fprintf (stderr, "*** precosat: invalid option '%s'\n", argv[i]);
 224       exit (1);
 225     }
 226   }
 227   solver.set ("verbose", verbose);
 228   solver.set ("quiet", quiet);
 229   solver.set ("print", print);
 230   if (output) solver.set ("output", output);
 231   if (blocked || satelite) {
 232     assert (simp);
 233     solver.set ("decompose",0);
 234     solver.set ("probe",0);
 235     solver.set ("otfs",0);
 236     solver.set ("elimasym", 0);
 237   }
 238   if (blocked) solver.set ("elim",0), solver.set ("blockrtc",2);
 239   if (satelite) solver.set ("block",0), solver.set ("elimrtc",2);
 240   solver.fxopts ();
 241   int lit, sign;
 242   int res = 0;
 243
 244   ch = getc (file);
 245
 246 NEXT:
 247
 248   if (ch == 'c') {
 249       while ((ch = getc (file)) != '\n')
 250         if (ch == EOF) {
 251           fprintf (stderr, "*** precosat: EOF in comment\n");
 252           resetsighandlers ();
 253           exit (1);
 254         }
 255       goto NEXT;
 256   }
 257
 258   if (ch == ' ' || ch == '\n') {
 259     ch = getc (file);
 260     goto NEXT;
 261   }
 262
 263   if (ch == EOF) goto DONE;
 264
 265   if (!n) {
 266     fprintf (stderr, "*** precosat: too many clauses\n");
 267     res = 1;
 268     goto EXIT;
 269   }
 270
 271   if ((sign = (ch == '-'))) ch = getc (file);
 272
 273   if (!isdigit (ch) || (sign && ch == '0')) {
 274     fprintf (stderr, "*** precosat: expected digit\n");
 275     res = 1;
 276     goto EXIT;
 277   }
 278
 279   lit = (ch - '0');
 280   while (isdigit (ch = getc (file))) lit = 10 * lit + (ch - '0');
 281
 282   if (lit > m) {
 283     fprintf (stderr, "*** precosat: variables exceeded\n");
 284     res = 1;
 285     goto EXIT;
 286   }
 287
 288   lit = 2 * lit + sign;
 289   solver.add (lit);
 290   if (!lit) n--;
 291
 292   goto NEXT;
 293
 294 DONE:
 295
 296   if (n) {
 297     fprintf (stderr, "*** precosat: clauses missing\n");
 298     res = 1;
 299     goto EXIT;
 300   }
 301
 302   if (pclosefile) pclose (file);
 303   if (fclosefile) fclose (file);
 304
 305   if (verbose) {
 306     printf ("c finished parsing\n");
 307     printf ("c\n"); solver.propts (); printf ("c\n");
 308     printf ("c starting search after %.1f seconds\n", solver.seconds ());
 309     if (decision_limit == INT_MAX) printf ("c no decision limit\n");
 310     else printf ("c search limited to %d decisions\n", decision_limit);
 311     fflush (stdout);
 312   }
 313
 314   res = solver.solve (decision_limit);
 315
 316   if (verbose) {
 317     printf ("c\n");
 318     fflush (stdout);
 319   }
 320
 321   if (res > 0) {
 322     if (!solver.satisfied ()) {
 323       if (!quiet) printf ("c ERROR\n");
 324       abort ();
 325     }
 326     if (!quiet && !nores) printf ("s SATISFIABLE\n");
 327     if (!nowit) {
 328       fflush (stdout);
 329       if (m) fputs ("v", stdout);
 330       for (int i = 1; i <= m; i++) {
 331         if (i % 8) fputc (' ', stdout);
 332         else fputs ("\nv ", stdout);
 333         printf ("%d", (solver.val (2 * i) < 0) ? -i : i);
 334       }
 335       if (m) fputc ('\n', stdout);
 336       fputs ("v 0\n", stdout);
 337     }
 338     res = 10;
 339   } else if (res < 0) {
 340     assert (res < 0);
 341     if (!quiet && !nores) printf ("s UNSATISFIABLE\n");
 342     res = 20;
 343   } else if (!quiet && !nores)
 344     printf ("s UNKNOWN\n");
 345
 346   if (!quiet) fflush (stdout);
 347
 348 EXIT:
 349   resetsighandlers ();
 350   if (verbose) {
 351     printf ("c\n");
 352     solver.prstats ();
 353   }
 354
 355 #ifndef NDEBUG
 356   solver.reset ();
 357 #endif
 358
 359   return res;
 360 }