1 /*------------------------------------------------------------------------*/
2 
3 // Do include 'internal.hpp' but try to minimize internal dependencies.
4 
5 #include "internal.hpp"
6 #include "signal.hpp"
7 
8 /*------------------------------------------------------------------------*/
9 
10 namespace CaDiCaL {
11 
12 class Solver;
13 class File;
14 
15 // A wrapper app which makes up the CaDiCaL stand alone solver.  It in
16 // essence only consists of the 'App::main' function.  So this class
17 // contains code, which is not required if only the library interface in
18 // 'Solver' is used.  It further uses static data structures in order to
19 // have a signal handler catch signals.
20 //
21 // It is thus neither thread-safe nor reentrant.  If you want to use
22 // multiple instances of the solver use the 'Solver' interface directly
23 // which is thread-safe and reentrant among different solver instances.
24 
25 class App : public Handler, public Terminator {
26 
27   // Global solver.
28 
29   Solver * solver;
30   int time_limit;
31   int max_var;
32   int strict;   // 0=force, 1=relaxed, 2=strict
33   bool timesup;
34 
35   // Printing.
36 
37   void print_usage (bool all = false);
38   void print_witness (FILE *);
39 
40   // Option handling.
41 
verbose()42   bool verbose () { return get ("verbose") && !get ("quiet"); }
43 
44   int  get (const char*);
45   bool set (const char*);
46   bool set (const char*, int);
47 
48 public:
49 
50   App ();
51   ~App ();
52 
terminate()53   bool terminate () { return timesup; }
54 
55 #ifndef QUIET
56   void signal_message (const char * msg, int sig);
57 #endif
58   void catch_signal (int sig);
59   void catch_alarm ();
60 
61   int main (int arg, char ** argv);
62 };
63 
64 /*------------------------------------------------------------------------*/
65 
print_usage(bool all)66 void App::print_usage (bool all) {
67   printf (
68 "usage: cadical [ <option> ... ] [ <dimacs> [ <proof> ] ]\n"
69 "\n"
70 "where '<option>' is one of the following common options\n"
71 "\n"
72 "  -h             list of common options \n"
73 "  --help         list of advanced options\n"
74 "  --version      print version\n"
75 "\n"
76 "  -n             do not print witness%s\n"
77 #ifndef QUIET
78 "  -v             increase verbosity%s\n"
79 "  -q             be quiet%s\n"
80 #endif
81 "\n"
82 "  -t <sec>       set wall clock time limit\n"
83 ,
84   all ? " (same as '--no-witness')": ""
85 #ifndef QUIET
86   , all ? " (see also '--verbose')": ""
87   , all ? " (same as '--quiet')" : ""
88 #endif
89   );
90 
91   if (all) {    // Print complete list of options.
92 
93     printf (
94 "\n"
95 "or one of the less common options\n"
96 "\n"
97 "  -O<level>      increase limits by '10^<level>' (default level '0')\n"
98 "  -P<rounds>     enable preprocessing initially (default '0' rounds)\n"
99 "  -L<rounds>     run local search initialially (default '0' rounds)\n"
100 "\n"
101 "  -c <limit>     limit the number of conflicts (default unlimited)\n"
102 "  -d <limit>     limit the number of decisions (default unlimited)\n"
103 "\n"
104 "  -o <dimacs>    write simplified CNF in DIMACS format to file\n"
105 "  -e <extend>    write reconstruction/extension stack to file\n"
106 #ifdef LOGGING
107 "  -l             enable logging messages (same as '--log')\n"
108 #endif
109 "\n"
110 "  -f | --force   parse completely broken DIMACS header\n"
111 "  --strict       enforce strict parsing\n"
112 "\n"
113 "  -s <sol>       read solution in competition output format\n"
114 "                 to check consistency of learned clauses\n"
115 "                 during testing and debugging\n"
116 "\n"
117 "  --colors       force colored output\n"
118 "  --no-colors    disable colored output to terminal\n"
119 "  --no-witness   do not print witness (see also '-n' above)\n"
120 "\n"
121 "  --build        print build configuration\n"
122 "  --copyright    print copyright information\n"
123 "\n"
124 "or '<option>' is one of the following advanced internal options\n"
125 "\n");
126 
127     solver->usage ();
128 
129     fputs (
130 "\n"
131 "The internal options have their default value printed in brackets\n"
132 "after their description.  They can also be used in the form\n"
133 "'--<name>' which is equivalent to '--<name>=1' and in the form\n"
134 "'--no-<name>' which is equivalent to '--<name>=0'.  One can also\n"
135 "use 'true' instead of '1', 'false' instead of '0', as well as\n"
136 "numbers with positive exponent such as '1e3' instead of '1000'.\n"
137 "\n"
138 "Alternatively option values can also be specified in the header\n"
139 "of the DIMACS file, e.g., 'c --elim=false', or through environment\n"
140 "variables, such as 'CADICAL_ELIM=false'.  The embedded options in\n"
141 "the DIMACS file have highest priority, followed by command line\n"
142 "options and then values specified through environment variables.\n",
143      stdout);
144 
145     printf (
146 "\n"
147 "There are also the following pre-defined configurations of options\n"
148 "\n");
149 
150     solver->configurations ();
151   }
152 
153   // Common to both complete and common option usage.
154   //
155   fputs (
156 "\n"
157 "The input is read from '<dimacs>' assumed to be in DIMACS format.\n"
158 "If '<proof>' is given then a DRAT proof is written to that file.\n",
159    stdout);
160 
161   if (all) {
162     fputs (
163 "\n"
164 "If '<dimacs>' is missing then the solver reads from '<stdin>',\n"
165 "also if '-' is used as input path name '<dimacs>'.  Similarly,\n"
166 "if '-' is specified as '<proof>' path then a proof is generated\n"
167 "and printed to '<stdout>'.\n"
168 "\n"
169 "By default the proof is stored in the binary DRAT format unless\n"
170 "the option '--no-binary' is specified or the proof is written\n"
171 "to  '<stdout>' and '<stdout>' is connected to a terminal.\n"
172 "\n"
173 "The input is assumed to be compressed if it is given explicitly\n"
174 "and has a '.gz', '.bz2', '.xz' or '.7z' suffix.  The same applies\n"
175 "to the output file.  In order to use compression and decompression\n"
176 "the corresponding utilities 'gzip', 'bzip', 'xz', and '7z' (depending\n"
177 "on the format) are required and need to be installed on the system.\n",
178     stdout);
179   }
180 }
181 
182 /*------------------------------------------------------------------------*/
183 
184 // Pretty print competition format witness with 'v' lines.
185 //
print_witness(FILE * file)186 void App::print_witness (FILE * file) {
187   int c = 0, i = 0, tmp;
188   do {
189     if (!c) fputc ('v', file), c = 1;
190     if (i++ == max_var) tmp = 0;
191     else tmp = solver->val (i) < 0 ? -i : i;
192     char str[20];
193     sprintf (str, " %d", tmp);
194     int l = strlen (str);
195     if (c + l > 78) fputs ("\nv", file), c = 1;
196     fputs (str, file);
197     c += l;
198   } while (tmp);
199   if (c) fputc ('\n', file);
200 }
201 
202 /*------------------------------------------------------------------------*/
203 
204 // Wrapper around option setting.
205 
get(const char * o)206 int App::get (const char * o) { return solver->get (o); }
set(const char * o,int v)207 bool App::set (const char * o, int v) { return solver->set (o, v); }
set(const char * arg)208 bool App::set (const char * arg) { return solver->set_long_option (arg); }
209 
210 /*------------------------------------------------------------------------*/
211 
212 // Short-cut for errors to avoid a hard 'exit'.
213 
214 #define APPERR(...) \
215 do { solver->error (__VA_ARGS__); } while (0)
216 
217 /*------------------------------------------------------------------------*/
218 
main(int argc,char ** argv)219 int App::main (int argc, char ** argv) {
220   const char * proof_path = 0, * solution_path = 0, * dimacs_path = 0;
221   const char * output_path = 0, * extension_path = 0, * config = 0;
222   int i, res = 0, optimize = 0, preprocessing = 0, localsearch = 0;
223   bool proof_specified = false, dimacs_specified = false;
224   int conflict_limit = -1, decision_limit = -1;
225   bool witness = true, less = false;
226   const char * dimacs_name, * err;
227   for (i = 1; i < argc; i++) {
228     if (!strcmp (argv[i], "-h")) {
229       print_usage ();
230       return 0;
231     } else if (!strcmp (argv[i], "--help")) {
232       print_usage (true);
233       return 0;
234     } else if (!strcmp (argv[i], "--version")) {
235       printf ("%s\n", CaDiCaL::version ());
236       return 0;
237     } else if (!strcmp (argv[i], "--build")) {
238       tout.disable ();
239       Solver::build (stdout, "");
240       return 0;
241     } else if (!strcmp (argv[i], "--copyright")) {
242       printf ("%s\n", copyright ());
243       return 0;
244     } else if (!strcmp (argv[i], "-")) {
245       if (proof_specified) APPERR ("too many arguments");
246       else if (!dimacs_specified) dimacs_specified = true;
247       else                         proof_specified = true;
248     } else if (!strcmp (argv[i], "-s")) {
249       if (++i == argc) APPERR ("argument to '-s' missing");
250       else if (solution_path)
251         APPERR ("multiple solution file options '-s %s' and '-s %s'",
252           solution_path, argv[i]);
253       else solution_path = argv[i];
254     } else if (!strcmp (argv[i], "-o")) {
255       if (++i == argc) APPERR ("argument to '-o' missing");
256       else if (output_path)
257         APPERR ("multiple output file options '-o %s' and '-o %s'",
258           output_path, argv[i]);
259       else if (!File::writable (argv[i]))
260         APPERR ("output file '%s' not writable", argv[i]);
261       else output_path = argv[i];
262     } else if (!strcmp (argv[i], "-e")) {
263       if (++i == argc) APPERR ("argument to '-e' missing");
264       else if (extension_path)
265         APPERR ("multiple extension file options '-e %s' and '-e %s'",
266           extension_path, argv[i]);
267       else if (!File::writable (argv[i]))
268         APPERR ("extension file '%s' not writable", argv[i]);
269       else extension_path = argv[i];
270     } else if (is_color_option (argv[i])) {
271       tout.force_colors ();
272       terr.force_colors ();
273     } else if (is_no_color_option (argv[i])) {
274       tout.force_no_colors ();
275       terr.force_no_colors ();
276     } else if (!strcmp (argv[i], "--witness") ||
277                !strcmp (argv[i], "--witness=true") ||
278                !strcmp (argv[i], "--witness=1"))
279       witness = true;
280     else if (!strcmp (argv[i], "-n") ||
281              !strcmp (argv[i], "--no-witness") ||
282              !strcmp (argv[i], "--witness=false") ||
283              !strcmp (argv[i], "--witness=0"))
284       witness = false;
285     else if (!strcmp (argv[i], "--less")) {             // EXPERIMENTAL!
286       if (less) APPERR ("multiple '--less' options");
287       else if (!isatty (1))
288         APPERR ("'--less' without '<stdout>' connected to terminal");
289       else less = true;
290     } else if (!strcmp (argv[i], "-c")) {
291       if (++i == argc) APPERR ("argument to '-c' missing");
292       else if (conflict_limit >= 0)
293         APPERR ("multiple conflict limit options '-c %d' and '-c %s'",
294           conflict_limit, argv[i]);
295       else if (!parse_int_str (argv[i], conflict_limit))
296         APPERR ("invalid argument in '-c %s'", argv[i]);
297       else if (conflict_limit < 0)
298         APPERR ("invalid conflict limit");
299     } else if (!strcmp (argv[i], "-d")) {
300       if (++i == argc) APPERR ("argument to '-d' missing");
301       else if (decision_limit >= 0)
302         APPERR ("multiple decision limit options '-d %d' and '-d %s'",
303           decision_limit, argv[i]);
304       else if (!parse_int_str (argv[i], decision_limit))
305         APPERR ("invalid argument in '-d %s'", argv[i]);
306       else if (decision_limit < 0)
307         APPERR ("invalid decision limit");
308     } else if (!strcmp (argv[i], "-t")) {
309       if (++i == argc) APPERR ("argument to '-t' missing");
310       else if (time_limit >= 0)
311         APPERR ("multiple time limit options '-t %d' and '-t %s'",
312           time_limit, argv[i]);
313       else if (!parse_int_str (argv[i], time_limit))
314         APPERR ("invalid argument in '-d %s'", argv[i]);
315       else if (time_limit < 0)
316         APPERR ("invalid time limit");
317     }
318 #ifndef QUIET
319     else if (!strcmp (argv[i], "-q")) set ("--quiet");
320     else if (!strcmp (argv[i], "-v"))
321       solver->set ("verbose", get ("verbose") + 1);
322 #endif
323 #ifdef LOGGING
324     else if (!strcmp (argv[i], "-l")) set ("--log");
325 #endif
326     else if (!strcmp (argv[i], "-f") ||
327              !strcmp (argv[i], "--force") ||
328              !strcmp (argv[i], "--force=1") ||
329              !strcmp (argv[i], "--force=true")) strict = 0;
330     else if (!strcmp (argv[i], "--strict") ||
331              !strcmp (argv[i], "--strict=1") ||
332              !strcmp (argv[i], "--strict=true")) strict = 2;
333     else if (argv[i][0] == '-' && argv[i][1] == 'O') {
334       if (!parse_int_str (argv[i] + 2, optimize) ||
335           optimize < 0 || optimize > 3)
336         APPERR ("invalid optimization option '%s' (expected '-O[0..3]')",
337           argv[i]);
338     } else if (argv[i][0] == '-' && argv[i][1] == 'P') {
339       if (!parse_int_str (argv[i] + 2, preprocessing) || preprocessing < 0)
340         APPERR ("invalid preprocessing option '%s' (expected '-P<int>')",
341           argv[i]);
342     } else if (argv[i][0] == '-' && argv[i][1] == 'L') {
343       if (!parse_int_str (argv[i] + 2, localsearch) || localsearch < 0)
344         APPERR ("invalid local search option '%s' (expected '-L<int>')",
345           argv[i]);
346     } else if (argv[i][0] == '-' && argv[i][1] == '-' &&
347                solver->is_valid_configuration (argv[i] + 2)) {
348       if (config)
349          APPERR ("can not use two configurations '--%s' and '%s'",
350            config, argv[i]);
351       config = argv[i] + 2;
352     } else if (set (argv[i])) { /* nothing do be done */ }
353     else if (argv[i][0] == '-') APPERR ("invalid option '%s'", argv[i]);
354     else if (proof_specified) APPERR ("too many arguments");
355     else if (dimacs_specified) {
356       if (!File::writable (argv[i]))
357         APPERR ("DRAT proof file '%s' not writable", argv[i]);
358       proof_specified = true;
359       proof_path = argv[i];
360     } else dimacs_specified = true, dimacs_path = argv[i];
361   }
362 
363   // The '--less' option is not fully functional yet.  It only works as
364   // expected if you let the solver run until it exits.  The goal is to have
365   // a similar experience as the default with 'git diff' if the terminal is
366   // too small for the message.
367   //
368   // TODO: add proper forking, waiting, signal catching & propagating ...
369   //
370   FILE * less_pipe;
371   if (less) {
372     assert (isatty (1));
373     less_pipe = popen ("less -r", "w");
374     if (!less_pipe)
375       APPERR ("could not execute and open pipe to 'less -r' command");
376     dup2 (fileno (less_pipe), 1);
377   } else less_pipe = 0;
378 
379   if (dimacs_specified && dimacs_path && !File::exists (dimacs_path))
380     APPERR ("DIMACS input file '%s' does not exist", dimacs_path);
381   if (solution_path && !File::exists (solution_path))
382     APPERR ("solution file '%s' does not exist", solution_path);
383   if (dimacs_specified && dimacs_path &&
384       proof_specified && proof_path &&
385       !strcmp (dimacs_path, proof_path) && strcmp (dimacs_path, "-"))
386     APPERR ("DIMACS input file '%s' also specified as DRAT proof file",
387       dimacs_path);
388   if (solution_path && !get ("check")) set ("--check");
389 #ifndef QUIET
390   if (!get ("quiet")) {
391     solver->section ("banner");
392     solver->message ("%sCaDiCaL Radically Simplified CDCL SAT Solver%s",
393       tout.bright_magenta_code (), tout.normal_code ());
394     solver->message ("%s%s%s",
395       tout.bright_magenta_code (), copyright (), tout.normal_code ());
396     solver->message ();
397     CaDiCaL::Solver::build (stdout, "c ");
398   }
399 #endif
400   if (config) {
401     solver->section ("config");
402     assert (Config::has (config));
403     solver->message ("using '%s' configuration (%s)",
404       config, Config::description (config));
405     solver->configure (config);
406   }
407   if (preprocessing > 0 || localsearch > 0 ||
408       time_limit >= 0 || conflict_limit >= 0 || decision_limit >= 0) {
409     solver->section ("limit");
410     if (preprocessing > 0) {
411       solver->message (
412         "enabling %d initial rounds of preprocessing", preprocessing);
413       solver->limit ("preprocessing", preprocessing);
414     }
415     if (localsearch > 0) {
416       solver->message (
417         "enabling %d initial rounds of local search", localsearch);
418       solver->limit ("localsearch", localsearch);
419     }
420     if (time_limit >= 0) {
421       solver->message (
422         "setting time limit to %d seconds real time",
423         time_limit);
424       Signal::alarm (time_limit);
425       solver->connect_terminator (this);
426     }
427     if (conflict_limit >= 0) {
428       solver->message ("setting conflict limit to %d conflicts",
429         conflict_limit);
430       bool succeeded = solver->limit ("conflicts", conflict_limit);
431       assert (succeeded), (void) succeeded;
432     }
433     if (decision_limit >= 0) {
434       solver->message ("setting decision limit to %d decisions",
435         decision_limit);
436       bool succeeded = solver->limit ("decisions", decision_limit);
437       assert (succeeded), (void) succeeded;
438     }
439   }
440   if (verbose () || proof_specified) solver->section ("proof tracing");
441   if (proof_specified) {
442     if (!proof_path) {
443       const bool force_binary = (isatty (1) && get ("binary"));
444       if (force_binary) set ("--no-binary");
445       solver->message ("writing %s proof trace to %s'<stdout>'%s",
446         (get ("binary") ? "binary" : "non-binary"),
447         tout.green_code (), tout.normal_code ());
448       if (force_binary)
449         solver->message (
450           "connected to terminal thus non-binary proof forced");
451       solver->trace_proof (stdout, "<stdout>");
452     } else if (!solver->trace_proof (proof_path))
453       APPERR ("can not open and write DRAT proof to '%s'", proof_path);
454     else
455       solver->message (
456         "writing %s proof trace to %s'%s'%s",
457         (get ("binary") ? "binary" : "non-binary"),
458         tout.green_code (), proof_path, tout.normal_code ());
459   } else solver->verbose (1, "will not generate nor write DRAT proof");
460   solver->section ("parsing input");
461   dimacs_name = dimacs_path ? dimacs_path : "<stdin>";
462   string help;
463   if (!dimacs_path) {
464     help += " ";
465     help += tout.magenta_code ();
466     help += "(use '-h' for a list of common options)";
467     help += tout.normal_code ();
468   }
469   solver->message ("reading DIMACS file from %s'%s'%s%s",
470     tout.green_code (), dimacs_name, tout.normal_code (), help.c_str ());
471   if (dimacs_path)
472        err = solver->read_dimacs (dimacs_path, max_var, strict);
473   else err = solver->read_dimacs (stdin, dimacs_name, max_var, strict);
474   if (err) APPERR ("%s", err);
475   if (solution_path) {
476     solver->section ("parsing solution");
477     solver->message ("reading solution file from '%s'", solution_path);
478     if ((err = solver->read_solution (solution_path)))
479       APPERR ("%s", err);
480   }
481 
482   solver->section ("options");
483   if (optimize > 0) {
484     solver->optimize (optimize);
485     solver->message ();
486   }
487   solver->options ();
488 
489   solver->section ("solving");
490   res = solver->solve ();
491 
492   if (proof_specified) solver->close_proof_trace ();
493 
494   if (output_path) {
495     solver->section ("writing output");
496     solver->message ("writing simplified CNF to DIMACS file %s'%s'%s",
497       tout.green_code (), output_path, tout.normal_code ());
498     err = solver->write_dimacs (output_path, max_var);
499     if (err) APPERR ("%s", err);
500   }
501 
502   if (extension_path) {
503     solver->section ("writing extension");
504     solver->message ("writing extension stack to %s'%s'%s",
505       tout.green_code (), extension_path, tout.normal_code ());
506     err = solver->write_extension (extension_path);
507     if (err) APPERR ("%s", err);
508   }
509 
510   solver->section ("result");
511   if (res == 10) {
512     printf ("s SATISFIABLE\n");
513     if (witness) {
514       fflush (stdout);
515       print_witness (stdout);
516     }
517   } else if (res == 20) printf ("s UNSATISFIABLE\n");
518   else printf ("c UNKNOWN\n");
519   fflush (stdout);
520   solver->statistics ();
521   solver->section ("shutting down");
522   solver->message ("exit %d", res);
523   if (less_pipe) {
524     close (1);
525     pclose (less_pipe);
526   }
527   return res;
528 }
529 
App()530 App::App () :
531   time_limit (-1), max_var (0), strict (1), timesup (false)
532 {
533   CaDiCaL::Options::report_default_value = 1;
534   solver = new Solver;
535   Signal::set (this);
536 }
537 
~App()538 App::~App () {
539   Signal::reset ();
540   delete solver;
541 }
542 
543 #ifndef QUIET
544 
signal_message(const char * msg,int sig)545 void App::signal_message (const char * msg, int sig) {
546   solver->message (
547     "%s%s %ssignal %d%s (%s)%s",
548     tout.red_code (), msg,
549     tout.bright_red_code (), sig,
550     tout.red_code (), Signal::name (sig),
551     tout.normal_code ());
552 }
553 
554 #endif
555 
catch_signal(int sig)556 void App::catch_signal (int sig) {
557 #ifndef QUIET
558   if (!get ("quiet")) {
559     solver->message ();
560     signal_message ("caught", sig);
561     solver->section ("result");
562     solver->message ("UNKNOWN");
563     solver->statistics ();
564     solver->message ();
565     signal_message ("raising", sig);
566   }
567 #else
568   (void) sig;
569 #endif
570 }
571 
catch_alarm()572 void App::catch_alarm () {
573 
574   // Both approaches work. We keep them here for illustration purposes.
575   //
576   // solver->terminate (); // immediate asynchronous call into solver
577   timesup = true;          // wait for solver to call 'App::terminate ()'
578 }
579 
580 } // end of 'namespace CaDiCaL'
581 
main(int argc,char ** argv)582 int main (int argc, char ** argv) {
583   CaDiCaL::App app;
584   return app.main (argc, argv);
585 }
586