backends/picosat/app.c

   1 #include "picosat.h"
   2
   3 #include <assert.h>
   4 #include <string.h>
   5 #include <ctype.h>
   6 #include <stdio.h>
   7
   8 #define GUNZIP "gunzip -c %s"
   9 #define GZIP "gzip -c -f > %s"
  10
  11 FILE * popen (const char *, const char*);
  12 int pclose (FILE *);
  13
  14 static int lineno;
  15 static FILE *input;
  16 static int inputid;
  17 static FILE *output;
  18 static int verbose;
  19 static char buffer[100];
  20 static char *bhead = buffer;
  21 static const char *eob = buffer + 80;
  22 static FILE * incremental_rup_file;
  23
  24 extern void picosat_enter (void);
  25 extern void picosat_leave (void);
  26
  27 static char page[4096];
  28 static char * top;
  29 static char * end;
  30
  31 static int
  32 next (void)
  33 {
  34   size_t bytes;
  35   int res;
  36
  37   if (top == end)
  38     {
  39       if (end < page + sizeof page)
  40         return EOF;
  41
  42       bytes = fread (page, 1, sizeof page, input);
  43       if (bytes == 0)
  44         return EOF;
  45
  46       top = page;
  47       end = page + bytes;
  48     }
  49
  50   res = *top++;
  51
  52   if (res == '\n')
  53     lineno++;
  54
  55   return res;
  56 }
  57
  58 static const char *
  59 parse (int force)
  60 {
  61   int ch, sign, lit, vars, clauses;
  62
  63   lineno = 1;
  64   inputid = fileno (input);
  65
  66 SKIP_COMMENTS:
  67   ch = next ();
  68   if (ch == 'c')
  69     {
  70       while ((ch = next ()) != EOF && ch != '\n')
  71         ;
  72       goto SKIP_COMMENTS;
  73     }
  74
  75   if (isspace (ch))
  76     goto SKIP_COMMENTS;
  77
  78   if (ch != 'p')
  79 INVALID_HEADER:
  80     return "missing or invalid 'p cnf <variables> <clauses>' header";
  81
  82   if (!isspace (next ()))
  83     goto INVALID_HEADER;
  84
  85   while (isspace (ch = next ()))
  86     ;
  87
  88   if (ch != 'c' || next () != 'n' || next () != 'f' || !isspace (next ()))
  89     goto INVALID_HEADER;
  90
  91   while (isspace (ch = next ()))
  92     ;
  93
  94   if (!isdigit (ch))
  95     goto INVALID_HEADER;
  96
  97   vars = ch - '0';
  98   while (isdigit (ch = next ()))
  99     vars = 10 * vars + (ch - '0');
 100
 101   if (!isspace (ch))
 102     goto INVALID_HEADER;
 103
 104   while (isspace (ch = next ()))
 105     ;
 106
 107   if (!isdigit (ch))
 108     goto INVALID_HEADER;
 109
 110   clauses = ch - '0';
 111   while (isdigit (ch = next ()))
 112     clauses = 10 * clauses + (ch - '0');
 113
 114   if (!isspace (ch) && ch != '\n' )
 115     goto INVALID_HEADER;
 116
 117   if (verbose)
 118     {
 119       fprintf (output, "c parsed header 'p cnf %d %d'\n", vars, clauses);
 120       fflush (output);
 121     }
 122
 123   picosat_adjust (vars);
 124
 125   if (incremental_rup_file)
 126     picosat_set_incremental_rup_file (incremental_rup_file, vars, clauses);
 127
 128   lit = 0;
 129 READ_LITERAL:
 130   ch = next ();
 131
 132   if (ch == 'c')
 133     {
 134       while ((ch = next ()) != EOF && ch != '\n')
 135         ;
 136       goto READ_LITERAL;
 137     }
 138
 139   if (ch == EOF)
 140     {
 141       if (lit)
 142         return "trailing 0 missing";
 143
 144       if (clauses && !force)
 145         return "clause missing";
 146
 147       return 0;
 148     }
 149
 150   if (isspace (ch))
 151     goto READ_LITERAL;
 152
 153   sign = 1;
 154   if (ch == '-')
 155     {
 156       sign = -1;
 157       ch = next ();
 158     }
 159
 160   if (!isdigit (ch))
 161     return "expected number";
 162
 163   lit = ch - '0';
 164   while (isdigit (ch = next ()))
 165     lit = 10 * lit + (ch - '0');
 166
 167   if (!clauses && !force)
 168     return "too many clauses";
 169
 170   if (lit)
 171     {
 172       if (lit > vars && !force)
 173         return "maximal variable index exceeded";
 174
 175       lit *= sign;
 176     }
 177   else
 178     clauses--;
 179
 180   picosat_add (lit);
 181
 182   goto READ_LITERAL;
 183 }
 184
 185 static void
 186 bflush (void)
 187 {
 188   *bhead = 0;
 189   fputs (buffer, output);
 190   fputc ('\n', output);
 191   bhead = buffer;
 192 }
 193
 194 static void
 195 printi (int i)
 196 {
 197   char *next;
 198   int l;
 199
 200 REENTER:
 201   if (bhead == buffer)
 202     *bhead++ = 'v';
 203
 204   l = sprintf (bhead, " %d", i);
 205   next = bhead + l;
 206
 207   if (next >= eob)
 208     {
 209       bflush ();
 210       goto REENTER;
 211     }
 212   else
 213     bhead = next;
 214 }
 215
 216 static void
 217 printa (void)
 218 {
 219   int max_idx = picosat_variables (), i, lit;
 220
 221   assert (bhead == buffer);
 222
 223   for (i = 1; i <= max_idx; i++)
 224     {
 225       lit = (picosat_deref (i) > 0) ? i : -i;
 226       printi (lit);
 227     }
 228
 229   printi (0);
 230   if (bhead > buffer)
 231     bflush ();
 232 }
 233
 234 static int
 235 has_suffix (const char *str, const char *suffix)
 236 {
 237   const char *tmp = strstr (str, suffix);
 238   if (!tmp)
 239     return 0;
 240
 241   return str + strlen (str) - strlen (suffix) == tmp;
 242 }
 243
 244 static void
 245 write_core_variables (FILE * file)
 246 {
 247   int i, max_idx = picosat_variables ();
 248   for (i = 1; i <= max_idx; i++)
 249     if (picosat_corelit (i))
 250       fprintf (file, "%d\n", i);
 251 }
 252
 253 static void
 254 write_to_file (const char *name, const char *type, void (*writer) (FILE *))
 255 {
 256   int pclose_file, zipped = has_suffix (name, ".gz");
 257   FILE *file;
 258   char *cmd;
 259
 260   if (zipped)
 261     {
 262       cmd = malloc (strlen (GZIP) + strlen (name));
 263       sprintf (cmd, GZIP, name);
 264       file = popen (cmd, "w");
 265       free (cmd);
 266       pclose_file = 1;
 267     }
 268   else
 269     {
 270       file = fopen (name, "w");
 271       pclose_file = 0;
 272     }
 273
 274   if (file)
 275     {
 276       if (verbose)
 277         fprintf (output,
 278                  "c\nc writing %s%s to '%s'\n",
 279                  zipped ? "gzipped " : "", type, name);
 280
 281       writer (file);
 282
 283       if (pclose_file)
 284         pclose (file);
 285       else
 286         fclose (file);
 287     }
 288   else
 289     fprintf (output, "*** picosat: can not write to '%s'\n", name);
 290 }
 291
 292 #define USAGE \
 293 "usage: picosat [ <option> ... ] [ <input> ]\n" \
 294 "\n" \
 295 "where <option> is one of the following\n" \
 296 "\n" \
 297 "  -h           print this command line option summary and exit\n" \
 298 "  --version    print version and exit\n" \
 299 "  --config     print build configuration and exit\n" \
 300 "\n" \
 301 "  -v           enable verbose output\n" \
 302 "  -f           ignore invalid header\n" \
 303 "  -n           do not print satisfying assignment\n" \
 304 "  -p           print formula in DIMACS format and exit\n" \
 305 "  -a <lit>     start with an assumption\n" \
 306 "  -l <limit>   set decision limit (no limit per default)\n" \
 307 "  -i <0/1>     force FALSE respectively TRUE as default phase\n" \
 308 "  -s <seed>    set random number generator seed (default 0)\n" \
 309 "  -o <output>  set output file (<stdout> per default)\n" \
 310 "  -t <trace>   generate compact proof trace file\n" \
 311 "  -T <trace>   generate extended proof trace file\n" \
 312 "  -r <trace>   generate reverse unit propagation proof file\n" \
 313 "  -c <core>    generate clausal core file in DIMACS format\n" \
 314 "  -V <core>    generate file listing core variables\n" \
 315 "  -U <core>    generate file listing used variables\n" \
 316 "\n" \
 317 "and <input> is an optional input file in DIMACS format.\n"
 318
 319 int
 320 picosat_main (int argc, char **argv)
 321 {
 322   int res, done, err, print_satisfying_assignment, force, print_formula;
 323   const char *compact_trace_name, *extended_trace_name, * rup_trace_name;
 324   const char * clausal_core_name, * variable_core_name;
 325   int assumption, assumptions, defaultphase;
 326   const char *input_name, *output_name;
 327   int close_input, pclose_input;
 328   int i, decision_limit;
 329   double start_time;
 330   unsigned seed;
 331   FILE *file;
 332   int trace;
 333
 334   start_time = picosat_time_stamp ();
 335
 336   clausal_core_name = 0;
 337   variable_core_name = 0;
 338   output_name = 0;
 339   compact_trace_name = 0;
 340   extended_trace_name = 0;
 341   rup_trace_name = 0;
 342   incremental_rup_file = 0;
 343   close_input = 0;
 344   pclose_input = 0;
 345   input_name = "<stdin>";
 346   input = stdin;
 347   output = stdout;
 348   verbose = 1;
 349   done = err = 0;
 350   decision_limit = -1;
 351   defaultphase = 0;
 352   assumptions = 0;
 353   force = 0;
 354   trace = 0;
 355   seed = 0;
 356
 357   top = end = page + sizeof page;
 358
 359   print_satisfying_assignment = 1;
 360   print_formula = 0;
 361
 362   for (i = 1; !done && !err && i < argc; i++)
 363     {
 364       if (!strcmp (argv[i], "-h"))
 365         {
 366           fputs (USAGE, output);
 367           done = 1;
 368         }
 369       else if (!strcmp (argv[i], "--version"))
 370         {
 371           fprintf (output, "%s\n", picosat_version ());
 372           done = 1;
 373         }
 374       else if (!strcmp (argv[i], "--config"))
 375         {
 376           fprintf (output, "%s\n", picosat_config ());
 377           done = 1;
 378         }
 379       else if (!strcmp (argv[i], "-v"))
 380         {
 381           verbose++;
 382         }
 383       else if (!strcmp (argv[i], "-f"))
 384         {
 385           force = 1;
 386         }
 387       else if (!strcmp (argv[i], "-n"))
 388         {
 389           print_satisfying_assignment = 0;
 390         }
 391       else if (!strcmp (argv[i], "-p"))
 392         {
 393           print_formula = 1;
 394         }
 395       else if (!strcmp (argv[i], "-l"))
 396         {
 397           if (++i == argc)
 398             {
 399               fprintf (output, "*** picosat: argument to '-l' missing\n");
 400               err = 1;
 401             }
 402           else
 403             decision_limit = atoi (argv[i]);
 404         }
 405       else if (!strcmp (argv[i], "-i"))
 406         {
 407           if (++i == argc)
 408             {
 409               fprintf (output, "*** picosat: argument to '-i' missing\n");
 410               err = 1;
 411             }
 412           else if (!strcmp (argv[i], "0"))
 413             {
 414               defaultphase = -1;
 415             }
 416           else if (!strcmp (argv[i], "1"))
 417             {
 418               defaultphase = 1;
 419             }
 420           else
 421             {
 422               fprintf (output, "*** picosat: invalid argument to '-i'\n");
 423               err = 1;
 424             }
 425         }
 426       else if (!strcmp (argv[i], "-a"))
 427         {
 428           if (++i == argc)
 429             {
 430               fprintf (output, "*** picosat: argument to '-a' missing\n");
 431               err = 1;
 432             }
 433           else if (!atoi (argv[i]))
 434             {
 435               fprintf (output, "*** picosat: argument to '-a' zero\n");
 436               err = 1;
 437             }
 438           else
 439             {
 440               /* Handle assumptions further down
 441                */
 442               assumptions++;
 443             }
 444         }
 445       else if (!strcmp (argv[i], "-s"))
 446         {
 447           if (++i == argc)
 448             {
 449               fprintf (output, "*** picosat: argument to '-s' missing\n");
 450               err = 1;
 451             }
 452           else
 453             seed = atoi (argv[i]);
 454         }
 455       else if (!strcmp (argv[i], "-o"))
 456         {
 457           if (output_name)
 458             {
 459               fprintf (output,
 460                        "*** picosat: "
 461                        "multiple output files '%s' and '%s'\n",
 462                        output_name, argv[i]);
 463               err = 1;
 464             }
 465           else if (++i == argc)
 466             {
 467               fprintf (output, "*** picosat: argument ot '-o' missing\n");
 468               err = 1;
 469             }
 470           else if (!(file = fopen (argv[i], "w")))
 471             {
 472               fprintf (output,
 473                        "*** picosat: "
 474                        "can not write output file '%s'\n", argv[i]);
 475               err = 1;
 476             }
 477           else
 478             {
 479               output_name = argv[i];
 480               output = file;
 481             }
 482         }
 483       else if (!strcmp (argv[i], "-t"))
 484         {
 485           if (compact_trace_name)
 486             {
 487               fprintf (output,
 488                        "*** picosat: "
 489                        "multiple compact trace files '%s' and '%s'\n",
 490                        compact_trace_name, argv[i]);
 491               err = 1;
 492             }
 493           else if (++i == argc)
 494             {
 495               fprintf (output, "*** picosat: argument ot '-t' missing\n");
 496               err = 1;
 497             }
 498           else
 499             {
 500               compact_trace_name = argv[i];
 501               trace = 1;
 502             }
 503         }
 504       else if (!strcmp (argv[i], "-T"))
 505         {
 506           if (extended_trace_name)
 507             {
 508               fprintf (output,
 509                        "*** picosat: "
 510                        "multiple extended trace files '%s' and '%s'\n",
 511                        extended_trace_name, argv[i]);
 512               err = 1;
 513             }
 514           else if (++i == argc)
 515             {
 516               fprintf (output, "*** picosat: argument ot '-T' missing\n");
 517               err = 1;
 518             }
 519           else
 520             {
 521               extended_trace_name = argv[i];
 522               trace = 1;
 523             }
 524         }
 525       else if (!strcmp (argv[i], "-r"))
 526         {
 527           if (rup_trace_name)
 528             {
 529               fprintf (output,
 530                        "*** picosat: "
 531                        "multiple RUP trace files '%s' and '%s'\n",
 532                        rup_trace_name, argv[i]);
 533               err = 1;
 534             }
 535           else if (++i == argc)
 536             {
 537               fprintf (output, "*** picosat: argument ot '-r' missing\n");
 538               err = 1;
 539             }
 540           else
 541             {
 542               rup_trace_name = argv[i];
 543               trace = 1;
 544             }
 545         }
 546       else if (!strcmp (argv[i], "-R"))
 547         {
 548           if (rup_trace_name)
 549             {
 550               fprintf (output,
 551                        "*** picosat: "
 552                        "multiple RUP trace files '%s' and '%s'\n",
 553                        rup_trace_name, argv[i]);
 554               err = 1;
 555             }
 556           else if (++i == argc)
 557             {
 558               fprintf (output, "*** picosat: argument ot '-R' missing\n");
 559               err = 1;
 560             }
 561           else if (!(file = fopen (argv[i], "w")))
 562             {
 563               fprintf (output,
 564                        "*** picosat: can not write to '%s'\n", argv[i]);
 565               err = 1;
 566             }
 567           else
 568             {
 569               rup_trace_name = argv[i];
 570               incremental_rup_file = file;
 571             }
 572         }
 573       else if (!strcmp (argv[i], "-c"))
 574         {
 575           if (clausal_core_name)
 576             {
 577               fprintf (output,
 578                        "*** picosat: "
 579                        "multiple clausal core files '%s' and '%s'\n",
 580                        clausal_core_name, argv[i]);
 581               err = 1;
 582             }
 583           else if (++i == argc)
 584             {
 585               fprintf (output, "*** picosat: argument ot '-c' missing\n");
 586               err = 1;
 587             }
 588           else
 589             {
 590               clausal_core_name = argv[i];
 591               trace = 1;
 592             }
 593         }
 594       else if (!strcmp (argv[i], "-V"))
 595         {
 596           if (variable_core_name)
 597             {
 598               fprintf (output,
 599                        "*** picosat: "
 600                        "multiple variable core files '%s' and '%s'\n",
 601                        variable_core_name, argv[i]);
 602               err = 1;
 603             }
 604           else if (++i == argc)
 605             {
 606               fprintf (output, "*** picosat: argument ot '-V' missing\n");
 607               err = 1;
 608             }
 609           else
 610             {
 611               variable_core_name = argv[i];
 612               trace = 1;
 613             }
 614         }
 615       else if (argv[i][0] == '-')
 616         {
 617           fprintf (output,
 618                    "*** picosat: "
 619                    "unknown command line option '%s' (try '-h')\n", argv[i]);
 620           err = 1;
 621         }
 622       else if (close_input || pclose_input)
 623         {
 624           fprintf (output,
 625                    "*** picosat: "
 626                    "multiple input files '%s' and '%s'\n",
 627                    input_name, argv[i]);
 628           err = 1;
 629         }
 630       else if (has_suffix (argv[i], ".gz"))
 631         {
 632           char *cmd = malloc (strlen (GUNZIP) + strlen (argv[i]));
 633           sprintf (cmd, GUNZIP, argv[i]);
 634           if ((file = popen (cmd, "r")))
 635             {
 636               input_name = argv[i];
 637               pclose_input = 1;
 638               input = file;
 639             }
 640           else
 641             {
 642               fprintf (output,
 643                        "*** picosat: "
 644                        "can not read compressed input file '%s'\n", argv[i]);
 645               err = 1;
 646             }
 647           free (cmd);
 648         }
 649       else if (!(file = fopen (argv[i], "r")))  /* TODO .gz ? */
 650         {
 651           fprintf (output,
 652                    "*** picosat: can not read input file '%s'\n", argv[i]);
 653           err = 1;
 654         }
 655       else
 656         {
 657           input_name = argv[i];
 658           close_input = 1;
 659           input = file;
 660         }
 661     }
 662
 663   res = PICOSAT_UNKNOWN;
 664
 665   if (!done && !err)
 666     {
 667       const char *err_msg;
 668
 669       if (verbose)
 670         {
 671           fprintf (output,
 672                    "c PicoSAT SAT Solver Version %s\n",
 673                    picosat_version ());
 674
 675           fprintf (output, "c %s\n", picosat_copyright ());
 676           fprintf (output, "c %s\n", picosat_config ());
 677         }
 678
 679       picosat_init ();
 680       picosat_enter ();
 681
 682       if (output_name)
 683         picosat_set_output (output);
 684
 685       picosat_set_verbosity (verbose);
 686
 687       if (verbose && (trace || defaultphase))
 688         fputs ("c\n", output);
 689
 690       if (trace)
 691         {
 692           if (verbose)
 693             fprintf (output, "c tracing proof\n");
 694           picosat_enable_trace_generation ();
 695         }
 696
 697       if (defaultphase)
 698         {
 699           if (verbose)
 700             fprintf (output,
 701                      "c using %s as default phase\n",
 702                      defaultphase < 0 ? "FALSE" : "TRUE");
 703
 704           picosat_set_global_default_phase (defaultphase);
 705         }
 706
 707       if (verbose)
 708         fprintf (output, "c\nc parsing %s\n", input_name);
 709
 710       if ((err_msg = parse (force)))
 711         {
 712           fprintf (output, "%s:%d: %s\n", input_name, lineno, err_msg);
 713           err = 1;
 714         }
 715       else
 716         {
 717           if (assumptions)
 718             {
 719               for (i = 1; i < argc; i++)
 720                 {
 721                   if (!strcmp (argv[i], "-l") ||
 722                       !strcmp (argv[i], "-s") ||
 723                       !strcmp (argv[i], "-o") ||
 724                       !strcmp (argv[i], "-t") || !strcmp (argv[i], "-c"))
 725                     {
 726                       i++;
 727                     }
 728                   else if (!strcmp (argv[i], "-a"))
 729                     {
 730                       assert (i + 1 < argc);
 731                       assumption = atoi (argv[++i]);
 732                       assert (assumption);
 733
 734                       picosat_assume (assumption);
 735
 736                       if (verbose)
 737                         fprintf (output, "c assumption %d\n", assumption);
 738                     }
 739                 }
 740             }
 741
 742           if (print_formula)
 743             {
 744               picosat_print (output);
 745             }
 746           else
 747             {
 748               if (verbose)
 749                 fprintf (output,
 750                          "c initialized %u variables\n"
 751                          "c found %u non trivial clauses\n",
 752                          picosat_variables (),
 753                          picosat_added_original_clauses ());
 754
 755               picosat_set_seed (seed);
 756               if (verbose)
 757                 fprintf (output,
 758                          "c\nc random number generator seed %u\n",
 759                          seed);
 760
 761               res = picosat_sat (decision_limit);
 762
 763               if (res == PICOSAT_UNSATISFIABLE)
 764                 {
 765                   fputs ("s UNSATISFIABLE\n", output);
 766
 767                   if (compact_trace_name)
 768                     write_to_file (compact_trace_name,
 769                                    "compact trace",
 770                                    picosat_write_compact_trace);
 771
 772                   if (extended_trace_name)
 773                     write_to_file (extended_trace_name,
 774                                    "extended trace",
 775                                    picosat_write_extended_trace);
 776
 777                   if (!incremental_rup_file && rup_trace_name)
 778                     write_to_file (rup_trace_name,
 779                                    "rup trace",
 780                                    picosat_write_rup_trace);
 781
 782                   if (clausal_core_name)
 783                     write_to_file (clausal_core_name,
 784                                    "clausal core",
 785                                    picosat_write_clausal_core);
 786
 787                   if (variable_core_name)
 788                     write_to_file (variable_core_name,
 789                                    "variable core", write_core_variables);
 790                 }
 791               else if (res == PICOSAT_SATISFIABLE)
 792                 {
 793                   fputs ("s SATISFIABLE\n", output);
 794
 795                   if (print_satisfying_assignment)
 796                     printa ();
 797                 }
 798               else
 799                 fputs ("s UNKNOWN\n", output);
 800             }
 801         }
 802
 803       if (!err && verbose)
 804         {
 805           fputs ("c\n", output);
 806           picosat_stats ();
 807           fprintf (output,
 808                    "c %.1f seconds total run time\n",
 809                    picosat_time_stamp () - start_time);
 810         }
 811
 812       picosat_leave ();
 813       picosat_reset ();
 814     }
 815
 816   if (incremental_rup_file)
 817     fclose (incremental_rup_file);
 818
 819   if (close_input)
 820     fclose (input);
 821
 822   if (pclose_input)
 823     pclose (input);
 824
 825   if (output_name)
 826     fclose (output);
 827
 828   return res;
 829 }