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