1 #include "internal.hpp"
2
3 /*------------------------------------------------------------------------*/
4
5 namespace CaDiCaL {
6
7 /*------------------------------------------------------------------------*/
8
9 // See corresponding header file 'cadical.hpp' (!) for more information.
10 //
11 // Again, to avoid confusion, note that, 'cadical.hpp' is the header file of
12 // this file 'solver.cpp', since we want to call the application and main
13 // file 'cadical.cpp', while at the same time using 'cadical.hpp' as the
14 // main header file of the library (and not 'solver.hpp').
15
16 /*------------------------------------------------------------------------*/
17 #ifdef LOGGING
18
19 // Needs to be kept in sync with the color schemes used in 'logging.cpp'.
20 //
21 #define api_code blue_code // API call color
22 #define log_code magenta_code // standard/default logging color
23 #define emph_code bright_magenta_code // emphasized logging color
24
25 #endif
26 /*------------------------------------------------------------------------*/
27
28 // Log state transitions.
29
30 #define STATE(S) \
31 do { \
32 assert (is_power_of_two (S)); \
33 if (_state == S) break; \
34 _state = S; \
35 LOG ("API enters state %s" #S "%s", \
36 tout.emph_code (), tout.normal_code ()); \
37 } while (0)
38
transition_to_unknown_state()39 void Solver::transition_to_unknown_state () {
40 if (state () == CONFIGURING) {
41 LOG ("API leaves state %sCONFIGURING%s",
42 tout.emph_code (), tout.normal_code ());
43 if (internal->opts.check &&
44 internal->opts.checkproof) {
45 internal->check ();
46 }
47 } else if (state () == SATISFIED) {
48 LOG ("API leaves state %sSATISFIED%s",
49 tout.emph_code (), tout.normal_code ());
50 external->reset_assumptions ();
51 } else if (state () == UNSATISFIED) {
52 LOG ("API leaves state %sUNSATISFIED%s",
53 tout.emph_code (), tout.normal_code ());
54 external->reset_assumptions ();
55 }
56 if (state () != UNKNOWN) STATE (UNKNOWN);
57 }
58
59 /*------------------------------------------------------------------------*/
60 #ifdef LOGGING
61 /*------------------------------------------------------------------------*/
62
63 // The following logging code is useful for debugging mostly (or trying to
64 // understand what the solver is actually doing). It needs to be enabled
65 // during configuration using the '-l' option for './configure', which
66 // forces 'LOGGING' to be defined during compilation. This includes all the
67 // logging code, which then still needs to enabled during run-time with the
68 // '-l' or 'log' option.
69
70 static void
log_api_call(Internal * internal,const char * name,const char * suffix)71 log_api_call (Internal * internal,
72 const char * name, const char * suffix) {
73 Logger::log (internal, "API call %s'%s ()'%s %s",
74 tout.api_code (), name, tout.log_code (), suffix);
75 }
76
77 static void
log_api_call(Internal * internal,const char * name,int arg,const char * suffix)78 log_api_call (Internal * internal,
79 const char * name, int arg, const char * suffix) {
80 Logger::log (internal, "API call %s'%s (%d)'%s %s",
81 tout.api_code (), name, arg, tout.log_code (), suffix);
82 }
83
84 static void
log_api_call(Internal * internal,const char * name,const char * arg,const char * suffix)85 log_api_call (Internal * internal,
86 const char * name, const char * arg, const char * suffix) {
87 Logger::log (internal, "API call %s'%s (\"%s\")'%s %s",
88 tout.api_code (), name, arg, tout.log_code (), suffix);
89 }
90
91 static void
log_api_call(Internal * internal,const char * name,const char * a1,int a2,const char * s)92 log_api_call (Internal * internal,
93 const char * name, const char * a1, int a2, const char * s) {
94 Logger::log (internal, "API call %s'%s (\"%s\", %d)'%s %s",
95 tout.api_code (), name, a1, a2, tout.log_code (), s);
96 }
97
98 /*------------------------------------------------------------------------*/
99
100 // We factored out API call begin/end logging and use overloaded functions.
101
102 static void
log_api_call_begin(Internal * internal,const char * name)103 log_api_call_begin (Internal * internal, const char * name) {
104 Logger::log_empty_line (internal);
105 log_api_call (internal, name, "started");
106 }
107
108 static void
log_api_call_begin(Internal * internal,const char * name,int arg)109 log_api_call_begin (Internal * internal, const char * name, int arg) {
110 Logger::log_empty_line (internal);
111 log_api_call (internal, name, arg, "started");
112 }
113
114 static void
log_api_call_begin(Internal * internal,const char * name,const char * arg)115 log_api_call_begin (Internal * internal,
116 const char * name, const char * arg) {
117 Logger::log_empty_line (internal);
118 log_api_call (internal, name, arg, "started");
119 }
120
121 static void
log_api_call_begin(Internal * internal,const char * name,const char * arg1,int arg2)122 log_api_call_begin (Internal * internal, const char * name,
123 const char * arg1, int arg2) {
124 Logger::log_empty_line (internal);
125 log_api_call (internal, name, arg1, arg2, "started");
126 }
127
128 /*------------------------------------------------------------------------*/
129
130 static void
log_api_call_end(Internal * internal,const char * name)131 log_api_call_end (Internal * internal, const char * name)
132 {
133 log_api_call (internal, name, "succeeded");
134 }
135
136 static void
log_api_call_end(Internal * internal,const char * name,int lit)137 log_api_call_end (Internal * internal, const char * name, int lit) {
138 log_api_call (internal, name, lit, "succeeded");
139 }
140
141 static void
log_api_call_end(Internal * internal,const char * name,const char * arg)142 log_api_call_end (Internal * internal,
143 const char * name, const char * arg) {
144 Logger::log_empty_line (internal);
145 log_api_call (internal, name, arg, "succeeded");
146 }
147
148 static void
log_api_call_end(Internal * internal,const char * name,const char * arg,bool res)149 log_api_call_end (Internal * internal, const char * name,
150 const char * arg,
151 bool res)
152 {
153 log_api_call (internal, name, arg, res ? "succeeded" : "failed");
154 }
155
156 static void
log_api_call_end(Internal * internal,const char * name,const char * arg,int val,bool res)157 log_api_call_end (Internal * internal, const char * name,
158 const char * arg, int val,
159 bool res)
160 {
161 log_api_call (internal, name, arg, val, res ? "succeeded" : "failed");
162 }
163
164 static void
log_api_call_returns(Internal * internal,const char * name,bool res)165 log_api_call_returns (Internal * internal, const char * name, bool res) {
166 log_api_call (internal, name,
167 res ? "returns 'true'" : "returns 'false'");
168 }
169
170 static void
log_api_call_returns(Internal * internal,const char * name,int res)171 log_api_call_returns (Internal * internal, const char * name, int res) {
172 char fmt[32];
173 sprintf (fmt, "returns '%d'", res);
174 log_api_call (internal, name, fmt);
175 }
176
177 static void
log_api_call_returns(Internal * internal,const char * name,int64_t res)178 log_api_call_returns (Internal * internal, const char * name, int64_t res) {
179 char fmt[32];
180 sprintf (fmt, "returns '%" PRId64 "'", res);
181 log_api_call (internal, name, fmt);
182 }
183
184 static void
log_api_call_returns(Internal * internal,const char * name,int lit,int res)185 log_api_call_returns (Internal * internal,
186 const char * name, int lit, int res) {
187 char fmt[32];
188 sprintf (fmt, "returns '%d'", res);
189 log_api_call (internal, name, lit, fmt);
190 }
191
192 static void
log_api_call_returns(Internal * internal,const char * name,const char * arg,bool res)193 log_api_call_returns (Internal * internal,
194 const char * name, const char * arg, bool res) {
195 log_api_call (internal, name, arg,
196 res ? "returns 'true'" : "returns 'false'");
197 }
198
199 static void
log_api_call_returns(Internal * internal,const char * name,int lit,bool res)200 log_api_call_returns (Internal * internal,
201 const char * name, int lit, bool res) {
202 log_api_call (internal, name, lit,
203 res ? "returns 'true'" : "returns 'false'");
204 }
205
206 static void
log_api_call_returns(Internal * internal,const char * name,const char * arg,const char * res)207 log_api_call_returns (Internal * internal,
208 const char * name, const char * arg, const char * res) {
209 Logger::log (internal, "API call %s'%s (\"%s\")'%s returns '%s'",
210 tout.api_code (), name, arg, tout.log_code (), res ? res : "<null>");
211 }
212
213 static void
log_api_call_returns(Internal * internal,const char * name,const char * arg1,int arg2,const char * res)214 log_api_call_returns (Internal * internal,
215 const char * name, const char * arg1, int arg2, const char * res) {
216 Logger::log (internal, "API call %s'%s (\"%s\", %d)'%s returns '%s'",
217 tout.api_code (), name, arg1, arg2, tout.log_code (),
218 res ? res : "<null>");
219 }
220
221 /*------------------------------------------------------------------------*/
222
223 #define LOG_API_CALL_BEGIN(...) \
224 do { \
225 if (!internal->opts.log) break; \
226 log_api_call_begin (internal, __VA_ARGS__); \
227 } while (0)
228
229 #define LOG_API_CALL_END(...) \
230 do { \
231 if (!internal->opts.log) break; \
232 log_api_call_end (internal, __VA_ARGS__); \
233 } while (0)
234
235 #define LOG_API_CALL_RETURNS(...) \
236 do { \
237 if (!internal->opts.log) break; \
238 log_api_call_returns (internal, __VA_ARGS__); \
239 } while (0)
240
241 /*------------------------------------------------------------------------*/
242 #else // end of 'then' part of 'ifdef LOGGING'
243 /*------------------------------------------------------------------------*/
244
245 #define LOG_API_CALL_BEGIN(...) do { } while (0)
246 #define LOG_API_CALL_END(...) do { } while (0)
247 #define LOG_API_CALL_RETURNS(...) do { } while (0)
248
249 /*------------------------------------------------------------------------*/
250 #endif // end of 'else' part of 'ifdef LOGGING'
251 /*------------------------------------------------------------------------*/
252
253 #define TRACE(...) \
254 do { \
255 if ((this == 0)) break; \
256 if ((internal == 0)) break; \
257 LOG_API_CALL_BEGIN (__VA_ARGS__); \
258 if (!trace_api_file) break; \
259 trace_api_call (__VA_ARGS__); \
260 } while (0)
261
trace_api_call(const char * s0) const262 void Solver::trace_api_call (const char * s0) const {
263 assert (trace_api_file);
264 LOG ("TRACE %s", s0);
265 fprintf (trace_api_file, "%s\n", s0);
266 fflush (trace_api_file);
267 }
268
trace_api_call(const char * s0,int i1) const269 void Solver::trace_api_call (const char * s0, int i1) const {
270 assert (trace_api_file);
271 LOG ("TRACE %s %d", s0, i1);
272 fprintf (trace_api_file, "%s %d\n", s0, i1);
273 fflush (trace_api_file);
274 }
275
276 void
trace_api_call(const char * s0,const char * s1,int i2) const277 Solver::trace_api_call (const char * s0, const char * s1, int i2) const {
278 assert (trace_api_file);
279 LOG ("TRACE %s %s %d", s0, s1, i2);
280 fprintf (trace_api_file, "%s %s %d\n", s0, s1, i2);
281 fflush (trace_api_file);
282 }
283
284 /*------------------------------------------------------------------------*/
285
286 // The global 'tracing_api' flag is used to ensure that only one solver
287 // traces to a file. Otherwise the method to use an environment variable to
288 // point to the trace file is bogus, since those different solver instances
289 // would all write to the same file producing garbage. A more sophisticated
290 // solution would use a different mechanism to tell the solver to which file
291 // to trace to, but in our experience it is quite convenient to get traces
292 // out of applications which use the solver as library by just setting an
293 // environment variable without requiring to change any application code.
294 //
295 static bool tracing_api_calls_through_environment_variable_method;
296
Solver()297 Solver::Solver () {
298
299 const char * path = getenv ("CADICAL_API_TRACE");
300 if (!path) path = getenv ("CADICALAPITRACE");
301 if (path) {
302 if (tracing_api_calls_through_environment_variable_method)
303 FATAL ("can not trace API calls of two solver instances "
304 "using environment variable 'CADICAL_API_TRACE'");
305 if (!(trace_api_file = fopen (path, "w")))
306 FATAL ("failed to open file '%s' to trace API calls "
307 "using environment variable 'CADICAL_API_TRACE'", path);
308 close_trace_api_file = true;
309 tracing_api_calls_through_environment_variable_method = true;
310 } else {
311 tracing_api_calls_through_environment_variable_method = false;
312 close_trace_api_file = false;
313 trace_api_file = 0;
314 }
315
316 _state = INITIALIZING;
317 internal = new Internal ();
318 TRACE ("init");
319 external = new External (internal);
320 STATE (CONFIGURING);
321 if (tracing_api_calls_through_environment_variable_method)
322 message ("tracing API calls to '%s'", path);
323 }
324
~Solver()325 Solver::~Solver () {
326
327 TRACE ("reset");
328 REQUIRE_VALID_OR_SOLVING_STATE ();
329 STATE (DELETING);
330
331 #ifdef LOGGING
332 //
333 // After deleting 'internal' logging does not work anymore.
334 //
335 bool logging = internal->opts.log;
336 int level = internal->level;
337 string prefix = internal->prefix;
338 #endif
339
340 delete internal;
341 delete external;
342
343 if (close_trace_api_file) {
344 close_trace_api_file = false;
345 assert (trace_api_file);
346 assert (tracing_api_calls_through_environment_variable_method);
347 fclose (trace_api_file);
348 tracing_api_calls_through_environment_variable_method = false;
349 }
350
351 #ifdef LOGGING
352 //
353 // Need to log success of this API call manually.
354 //
355 if (logging) {
356 printf ("%s%sLOG %s%d%s API call %s'reset ()'%s succeeded%s\n",
357 prefix.c_str (),
358 tout.log_code (),
359 tout.emph_code (),
360 level,
361 tout.log_code (),
362 tout.api_code (),
363 tout.log_code (),
364 tout.normal_code ());
365 fflush (stdout);
366 }
367 #endif
368 }
369
370 /*------------------------------------------------------------------------*/
371
vars()372 int Solver::vars () {
373 TRACE ("vars");
374 REQUIRE_VALID_OR_SOLVING_STATE ();
375 int res = external->max_var;
376 LOG_API_CALL_RETURNS ("vars", res);
377 return res;
378 }
379
reserve(int min_max_var)380 void Solver::reserve (int min_max_var) {
381 TRACE ("reserve", min_max_var);
382 REQUIRE_VALID_STATE ();
383 transition_to_unknown_state ();
384 external->reset_extended ();
385 external->init (min_max_var);
386 LOG_API_CALL_END ("reserve", min_max_var);
387 }
388
389 /*------------------------------------------------------------------------*/
390
trace_api_calls(FILE * file)391 void Solver::trace_api_calls (FILE * file) {
392 LOG_API_CALL_BEGIN ("trace_api_calls");
393 REQUIRE_VALID_STATE ();
394 REQUIRE (file != 0, "invalid zero file argument");
395 REQUIRE (!tracing_api_calls_through_environment_variable_method,
396 "already tracing API calls "
397 "using environment variable 'CADICAL_API_TRACE'");
398 REQUIRE (!trace_api_file, "called twice");
399 trace_api_file = file;
400 LOG_API_CALL_END ("trace_api_calls");
401 trace_api_call ("init");
402 }
403
404 /*------------------------------------------------------------------------*/
405
is_valid_option(const char * name)406 bool Solver::is_valid_option (const char * name) {
407 return Options::has (name);
408 }
409
is_valid_long_option(const char * arg)410 bool Solver::is_valid_long_option (const char * arg) {
411 string name;
412 int tmp;
413 return Options::parse_long_option (arg, name, tmp);
414 }
415
get(const char * arg)416 int Solver::get (const char * arg) {
417 REQUIRE_VALID_OR_SOLVING_STATE ();
418 return internal->opts.get (arg);
419 }
420
set(const char * arg,int val)421 bool Solver::set (const char * arg, int val) {
422 TRACE ("set", arg, val);
423 REQUIRE_VALID_STATE ();
424 if (strcmp (arg, "log") &&
425 strcmp (arg, "quiet") &&
426 strcmp (arg, "verbose")) {
427 REQUIRE (state () == CONFIGURING,
428 "can only set option 'set (\"%s\", %d)' right after initialization",
429 arg, val);
430 }
431 bool res = internal->opts.set (arg, val);
432 LOG_API_CALL_END ("set", arg, val, res);
433 return res;
434 }
435
set_long_option(const char * arg)436 bool Solver::set_long_option (const char * arg) {
437 LOG_API_CALL_BEGIN ("set", arg);
438 REQUIRE_VALID_STATE ();
439 REQUIRE (state () == CONFIGURING,
440 "can only set option '%s' right after initialization", arg);
441 bool res;
442 if (arg[0] != '-' || arg[1] != '-') res = false;
443 else {
444 int val;
445 string name;
446 res = Options::parse_long_option (arg, name, val);
447 if (res) set (name.c_str (), val);
448 }
449 LOG_API_CALL_END ("set", arg, res);
450 return res;
451 }
452
optimize(int arg)453 void Solver::optimize (int arg) {
454 LOG_API_CALL_BEGIN ("optimize", arg);
455 REQUIRE_VALID_STATE ();
456 internal->opts.optimize (arg);
457 LOG_API_CALL_END ("optimize", arg);
458 }
459
limit(const char * arg,int val)460 bool Solver::limit (const char * arg, int val) {
461 TRACE ("limit", arg, val);
462 REQUIRE_VALID_STATE ();
463 bool res = internal->limit (arg, val);
464 LOG_API_CALL_END ("limit", arg, val, res);
465 return res;
466 }
467
is_valid_limit(const char * arg)468 bool Solver::is_valid_limit (const char * arg) {
469 return Internal::is_valid_limit (arg);
470 }
471
prefix(const char * str)472 void Solver::prefix (const char * str) {
473 LOG_API_CALL_BEGIN ("prefix", str);
474 REQUIRE_VALID_STATE ();
475 internal->prefix = str;
476 LOG_API_CALL_END ("prefix", str);
477 }
478
is_valid_configuration(const char * name)479 bool Solver::is_valid_configuration (const char * name) {
480 return Config::has (name);
481 }
482
configure(const char * name)483 bool Solver::configure (const char * name) {
484 LOG_API_CALL_BEGIN ("config", name);
485 REQUIRE_VALID_STATE ();
486 REQUIRE (state () == CONFIGURING,
487 "can only set configuration '%s' right after initialization", name);
488 bool res = Config::set (*this, name);
489 LOG_API_CALL_END ("config", name, res);
490 return res;
491 }
492
493 /*===== IPASIR BEGIN =====================================================*/
494
add(int lit)495 void Solver::add (int lit) {
496 TRACE ("add", lit);
497 REQUIRE_VALID_STATE ();
498 if (lit) REQUIRE_VALID_LIT (lit);
499 transition_to_unknown_state ();
500 external->add (lit);
501 if (lit) STATE (ADDING);
502 else STATE (UNKNOWN);
503 LOG_API_CALL_END ("add", lit);
504 }
505
assume(int lit)506 void Solver::assume (int lit) {
507 TRACE ("assume", lit);
508 REQUIRE_VALID_STATE ();
509 REQUIRE_VALID_LIT (lit);
510 transition_to_unknown_state ();
511 external->assume (lit);
512 LOG_API_CALL_END ("assume", lit);
513 }
514
515 /*------------------------------------------------------------------------*/
516
call_external_solve_and_check_results()517 int Solver::call_external_solve_and_check_results () {
518 transition_to_unknown_state ();
519 assert (state () & READY);
520 STATE (SOLVING);
521 int res = external->solve ();
522 if (res == 10) STATE (SATISFIED);
523 else if (res == 20) STATE (UNSATISFIED);
524 else STATE (UNKNOWN);
525 #if 0 // EXPENSIVE ALTERNATIVE ASSUMPTION CHECKING
526 // This checks that the set of failed assumptions form a core using the
527 // external 'copy (...)' function to copy the solver, which can be trusted
528 // less, since it involves copying the extension stack too. The
529 // 'External::check_assumptions_failing' is a better alternative and can
530 // be enabled by options too. We keep this code though to have an
531 // alternative failed assumption checking available for debugging.
532 //
533 if (res == 20 && !external->assumptions.empty ()) {
534 Solver checker;
535 checker.prefix ("checker ");
536 copy (checker);
537 for (const auto & lit : external->assumptions)
538 if (failed (lit))
539 checker.add (lit), checker.add (0);
540 if (checker.solve () != 20)
541 FATAL ("copying assumption checker failed");
542 }
543 #endif
544 if (!res) external->reset_assumptions ();
545 return res;
546 }
547
solve()548 int Solver::solve () {
549 TRACE ("solve");
550 REQUIRE_VALID_STATE ();
551 REQUIRE (state () != ADDING,
552 "clause incomplete (terminating zero not added)");
553 int res = call_external_solve_and_check_results ();
554 LOG_API_CALL_RETURNS ("solve", res);
555 return res;
556 }
557
simplify(int rounds)558 int Solver::simplify (int rounds) {
559 TRACE ("simplify", rounds);
560 REQUIRE_VALID_STATE ();
561 REQUIRE (rounds >= 0,
562 "negative number of simplification rounds '%d'", rounds);
563 REQUIRE (state () != ADDING,
564 "clause incomplete (terminating zero not added)");
565 internal->limit ("conflicts", 0);
566 internal->limit ("preprocessing", rounds);
567 int res = call_external_solve_and_check_results ();
568 LOG_API_CALL_RETURNS ("simplify", rounds, res);
569 return res;
570 }
571
572 /*------------------------------------------------------------------------*/
573
val(int lit)574 int Solver::val (int lit) {
575 TRACE ("val", lit);
576 REQUIRE_VALID_STATE ();
577 REQUIRE_VALID_LIT (lit);
578 REQUIRE (state () == SATISFIED,
579 "can only get value in satisfied state");
580 int res = external->val (lit);
581 LOG_API_CALL_RETURNS ("val", lit, res);
582 return res;
583 }
584
failed(int lit)585 bool Solver::failed (int lit) {
586 TRACE ("failed", lit);
587 REQUIRE_VALID_STATE ();
588 REQUIRE_VALID_LIT (lit);
589 REQUIRE (state () == UNSATISFIED,
590 "can only get failed assumptions in unsatisfied state");
591 bool res = external->failed (lit);
592 LOG_API_CALL_RETURNS ("failed", lit, res);
593 return res;
594 }
595
fixed(int lit) const596 int Solver::fixed (int lit) const {
597 TRACE ("fixed", lit);
598 REQUIRE_VALID_STATE ();
599 REQUIRE_VALID_LIT (lit);
600 int res = external->fixed (lit);
601 LOG_API_CALL_RETURNS ("fixed", lit, res);
602 return res;
603 }
604
605 /*------------------------------------------------------------------------*/
606
terminate()607 void Solver::terminate () {
608 LOG_API_CALL_BEGIN ("terminate");
609 REQUIRE_VALID_OR_SOLVING_STATE ();
610 external->terminate ();
611 LOG_API_CALL_END ("terminate");
612 }
613
connect_terminator(Terminator * terminator)614 void Solver::connect_terminator (Terminator * terminator) {
615 LOG_API_CALL_BEGIN ("connect_terminator");
616 REQUIRE_VALID_STATE ();
617 REQUIRE (terminator, "can not connect zero terminator");
618 #ifdef LOGGING
619 if (external->terminator)
620 LOG ("connecting new terminator (disconnecting previous one)");
621 else
622 LOG ("connecting new terminator (no previous one)");
623 #endif
624 external->terminator = terminator;
625 LOG_API_CALL_END ("connect_terminator");
626 }
627
disconnect_terminator()628 void Solver::disconnect_terminator () {
629 LOG_API_CALL_BEGIN ("disconnect_terminator");
630 REQUIRE_VALID_STATE ();
631 #ifdef LOGGING
632 if (external->terminator)
633 LOG ("disconnecting previous terminator");
634 else
635 LOG ("ignoring to disconnect terminator (no previous one)");
636 #endif
637 external->terminator = 0;
638 LOG_API_CALL_END ("disconnect_terminator");
639 }
640
641 /*===== IPASIR END =======================================================*/
642
active() const643 int Solver::active () const {
644 TRACE ("active");
645 REQUIRE_VALID_STATE ();
646 int res = internal->active ();
647 LOG_API_CALL_RETURNS ("active", res);
648 return res;
649 }
650
redundant() const651 int64_t Solver::redundant () const {
652 TRACE ("redundant");
653 REQUIRE_VALID_STATE ();
654 int64_t res = internal->redundant ();
655 LOG_API_CALL_RETURNS ("redundant", res);
656 return res;
657 }
658
irredundant() const659 int64_t Solver::irredundant () const {
660 TRACE ("irredundant");
661 REQUIRE_VALID_STATE ();
662 int64_t res = internal->irredundant ();
663 LOG_API_CALL_RETURNS ("irredundant", res);
664 return res;
665 }
666
667 /*------------------------------------------------------------------------*/
668
freeze(int lit)669 void Solver::freeze (int lit) {
670 TRACE ("freeze", lit);
671 REQUIRE_VALID_STATE ();
672 REQUIRE_VALID_LIT (lit);
673 external->freeze (lit);
674 LOG_API_CALL_END ("freeze", lit);
675 }
676
melt(int lit)677 void Solver::melt (int lit) {
678 TRACE ("melt", lit);
679 REQUIRE_VALID_STATE ();
680 REQUIRE_VALID_LIT (lit);
681 REQUIRE (external->frozen (lit),
682 "can not melt completely melted literal '%d'", lit);
683 external->melt (lit);
684 LOG_API_CALL_END ("melt", lit);
685 }
686
frozen(int lit) const687 bool Solver::frozen (int lit) const {
688 TRACE ("frozen", lit);
689 REQUIRE_VALID_STATE ();
690 REQUIRE_VALID_LIT (lit);
691 bool res = external->frozen (lit);
692 LOG_API_CALL_RETURNS ("frozen", lit, res);
693 return res;
694 }
695
696 /*------------------------------------------------------------------------*/
697
trace_proof(FILE * external_file,const char * name)698 bool Solver::trace_proof (FILE * external_file, const char * name) {
699 LOG_API_CALL_BEGIN ("trace_proof", name);
700 REQUIRE_VALID_STATE ();
701 REQUIRE (state () == CONFIGURING,
702 "can only start proof tracing to '%s' right after initialization",
703 name);
704 REQUIRE (!internal->tracer, "already tracing proof");
705 File * internal_file = File::write (internal, external_file, name);
706 assert (internal_file);
707 internal->trace (internal_file);
708 LOG_API_CALL_RETURNS ("trace_proof", name, true);
709 return true;
710 }
711
trace_proof(const char * path)712 bool Solver::trace_proof (const char * path) {
713 LOG_API_CALL_BEGIN ("trace_proof", path);
714 REQUIRE_VALID_STATE ();
715 REQUIRE (state () == CONFIGURING,
716 "can only start proof tracing to '%s' right after initialization",
717 path);
718 REQUIRE (!internal->tracer, "already tracing proof");
719 File * internal_file = File::write (internal, path);
720 bool res = (internal_file != 0);
721 internal->trace (internal_file);
722 LOG_API_CALL_RETURNS ("trace_proof", path, res);
723 return res;
724 }
725
close_proof_trace()726 void Solver::close_proof_trace () {
727 LOG_API_CALL_BEGIN ("close_proof_trace");
728 REQUIRE_VALID_STATE ();
729 REQUIRE (internal->tracer, "proof is not traced");
730 REQUIRE (!internal->tracer->closed (), "proof trace already closed");
731 internal->close_trace ();
732 LOG_API_CALL_END ("close_proof_trace");
733 }
734
735 /*------------------------------------------------------------------------*/
736
build(FILE * file,const char * prefix)737 void Solver::build (FILE * file, const char * prefix) {
738
739 assert (file == stdout || file == stderr);
740
741 Terminal * terminal;
742
743 if (file == stdout) terminal = &tout;
744 else if (file == stderr) terminal = &terr;
745 else terminal = 0;
746
747 const char * v = CaDiCaL::version ();
748 const char * i = identifier ();
749 const char * c = compiler ();
750 const char * b = date ();
751 const char * f = flags ();
752
753 assert (v);
754
755 fputs (prefix, file);
756 if (terminal) terminal->magenta ();
757 fputs ("Version ", file);
758 if (terminal) terminal->normal ();
759 fputs (v, file);
760 if (i) {
761 if (terminal) terminal->magenta ();
762 fputc (' ', file);
763 fputs (i, file);
764 if (terminal) terminal->normal ();
765 }
766 fputc ('\n', file);
767
768 if (c) {
769 fputs (prefix, file);
770 if (terminal) terminal->magenta ();
771 fputs (c, file);
772 if (f) {
773 fputc (' ', file);
774 fputs (f, file);
775 }
776 if (terminal) terminal->normal ();
777 fputc ('\n', file);
778 }
779
780 if (b) {
781 fputs (prefix, file);
782 if (terminal) terminal->magenta ();
783 fputs (b, file);
784 if (terminal) terminal->normal ();
785 fputc ('\n', file);
786 }
787
788 fflush (file);
789 }
790
version()791 const char * Solver::version () { return CaDiCaL::version (); }
792
signature()793 const char * Solver::signature () { return CaDiCaL::signature (); }
794
options()795 void Solver::options () {
796 REQUIRE_VALID_STATE ();
797 internal->opts.print ();
798 }
799
usage()800 void Solver::usage () { Options::usage (); }
801
configurations()802 void Solver::configurations () { Config::usage (); }
803
statistics()804 void Solver::statistics () {
805 if (state () == DELETING) return;
806 TRACE ("stats");
807 REQUIRE_VALID_OR_SOLVING_STATE ();
808 internal->print_stats ();
809 LOG_API_CALL_END ("stats");
810 }
811
812 /*------------------------------------------------------------------------*/
813
read_dimacs(File * file,int & vars,int strict)814 const char * Solver::read_dimacs (File * file, int & vars, int strict) {
815 REQUIRE_VALID_STATE ();
816 REQUIRE (state () == CONFIGURING,
817 "can only read DIMACS file right after initialization");
818 Parser * parser = new Parser (this, file);
819 const char * err = parser->parse_dimacs (vars, strict);
820 delete parser;
821 return err;
822 }
823
824 const char *
read_dimacs(FILE * external_file,const char * name,int & vars,int strict)825 Solver::read_dimacs (FILE * external_file,
826 const char * name, int & vars, int strict) {
827 LOG_API_CALL_BEGIN ("read_dimacs", name);
828 REQUIRE_VALID_STATE ();
829 REQUIRE (state () == CONFIGURING,
830 "can only read DIMACS file right after initialization");
831 File * file = File::read (internal, external_file, name);
832 assert (file);
833 const char * err = read_dimacs (file, vars, strict);
834 delete file;
835 LOG_API_CALL_RETURNS ("read_dimacs", name, err);
836 return err;
837 }
838
839 const char *
read_dimacs(const char * path,int & vars,int strict)840 Solver::read_dimacs (const char * path, int & vars, int strict) {
841 LOG_API_CALL_BEGIN ("read_dimacs", path);
842 REQUIRE_VALID_STATE ();
843 REQUIRE (state () == CONFIGURING,
844 "can only read DIMACS file right after initialization");
845 File * file = File::read (internal, path);
846 if (!file)
847 return internal->error_message.init (
848 "failed to read DIMACS file '%s'", path);
849 const char * err = read_dimacs (file, vars, strict);
850 delete file;
851 LOG_API_CALL_RETURNS ("read_dimacs", path, err);
852 return err;
853 }
854
read_solution(const char * path)855 const char * Solver::read_solution (const char * path) {
856 LOG_API_CALL_BEGIN ("solution", path);
857 REQUIRE_VALID_STATE ();
858 File * file = File::read (internal, path);
859 if (!file) return internal->error_message.init (
860 "failed to read solution file '%s'", path);
861 Parser * parser = new Parser (this, file);
862 const char * err = parser->parse_solution ();
863 delete parser;
864 delete file;
865 if (!err) external->check_assignment (&External::sol);
866 LOG_API_CALL_RETURNS ("read_solution", path, err);
867 return err;
868 }
869
870 /*------------------------------------------------------------------------*/
871
dump_cnf()872 void Solver::dump_cnf () {
873 TRACE ("dump");
874 REQUIRE_INITIALIZED ();
875 internal->dump ();
876 LOG_API_CALL_END ("dump");
877 }
878
879 /*------------------------------------------------------------------------*/
880
traverse_clauses(ClauseIterator & it) const881 bool Solver::traverse_clauses (ClauseIterator & it) const {
882 LOG_API_CALL_BEGIN ("traverse_clauses");
883 REQUIRE_VALID_STATE ();
884 bool res = external->traverse_all_frozen_units_as_clauses (it) &&
885 internal->traverse_clauses (it);
886 LOG_API_CALL_RETURNS ("traverse_clauses", res);
887 return res;
888 }
889
traverse_witnesses_backward(WitnessIterator & it) const890 bool Solver::traverse_witnesses_backward (WitnessIterator & it) const {
891 LOG_API_CALL_BEGIN ("traverse_witnesses_backward");
892 REQUIRE_VALID_STATE ();
893 bool res = external->traverse_all_non_frozen_units_as_witnesses (it) &&
894 external->traverse_witnesses_backward (it);
895 LOG_API_CALL_RETURNS ("traverse_witnesses_backward", res);
896 return res;
897 }
898
traverse_witnesses_forward(WitnessIterator & it) const899 bool Solver::traverse_witnesses_forward (WitnessIterator & it) const {
900 LOG_API_CALL_BEGIN ("traverse_witnesses_forward");
901 REQUIRE_VALID_STATE ();
902 bool res = external->traverse_witnesses_forward (it) &&
903 external->traverse_all_non_frozen_units_as_witnesses (it);
904 LOG_API_CALL_RETURNS ("traverse_witnesses_forward", res);
905 return res;
906 }
907
908 /*------------------------------------------------------------------------*/
909
910 class ClauseCounter : public ClauseIterator {
911 public:
912 int vars;
913 int64_t clauses;
ClauseCounter()914 ClauseCounter () : vars (0), clauses (0) { }
clause(const vector<int> & c)915 bool clause (const vector<int> & c) {
916 for (const auto & lit : c) {
917 assert (lit != INT_MIN);
918 int idx = abs (lit);
919 if (idx > vars) vars = idx;
920 }
921 clauses++;
922 return true;
923 }
924 };
925
926 class ClauseWriter : public ClauseIterator {
927 File * file;
928 public:
ClauseWriter(File * f)929 ClauseWriter (File * f) : file (f) { }
clause(const vector<int> & c)930 bool clause (const vector<int> & c) {
931 for (const auto & lit : c) {
932 if (!file->put (lit)) return false;
933 if (!file->put (' ')) return false;
934 }
935 return file->put ("0\n");
936 }
937 };
938
write_dimacs(const char * path,int min_max_var)939 const char * Solver::write_dimacs (const char * path, int min_max_var) {
940 LOG_API_CALL_BEGIN ("write_dimacs", path, min_max_var);
941 REQUIRE_VALID_STATE ();
942 ClauseCounter counter;
943 (void) traverse_clauses (counter);
944 LOG ("found maximal variable %d and %" PRId64 " clauses",
945 counter.vars, counter.clauses);
946 #ifndef QUIET
947 const double start = internal->time ();
948 #endif
949 File * file = File::write (internal, path);
950 const char * res = 0;
951 if (file) {
952 int actual_max_vars = max (min_max_var, counter.vars);
953 MSG ("writing %s'p cnf %d %" PRId64 "'%s header",
954 tout.green_code (), actual_max_vars, counter.clauses,
955 tout.normal_code ());
956 file->put ("p cnf ");
957 file->put (actual_max_vars);
958 file->put (' ');
959 file->put (counter.clauses);
960 file->put ('\n');
961 ClauseWriter writer (file);
962 if (!traverse_clauses (writer))
963 res = internal->error_message.init (
964 "writing to DIMACS file '%s' failed", path);
965 delete file;
966 } else res = internal->error_message.init (
967 "failed to open DIMACS file '%s' for writing", path);
968 #ifndef QUIET
969 if (!res) {
970 const double end = internal->time ();
971 MSG ("wrote %" PRId64 " clauses in %.2f seconds %s time",
972 counter.clauses, end - start,
973 internal->opts.realtime ? "real" : "process");
974 }
975 #endif
976 LOG_API_CALL_RETURNS ("write_dimacs", path, min_max_var, res);
977 return res;
978 }
979
980 /*------------------------------------------------------------------------*/
981
982 struct WitnessWriter : public WitnessIterator {
983 File * file;
984 int64_t witnesses;
WitnessWriterCaDiCaL::WitnessWriter985 WitnessWriter (File * f) : file (f), witnesses (0) { }
writeCaDiCaL::WitnessWriter986 bool write (const vector<int> & a) {
987 for (const auto & lit : a) {
988 if (!file->put (lit)) return false;
989 if (!file->put (' ')) return false;
990 }
991 return file->put ('0');
992 }
witnessCaDiCaL::WitnessWriter993 bool witness (const vector<int> & c, const vector<int> & w) {
994 if (!write (c)) return false;
995 if (!file->put (' ')) return false;
996 if (!write (w)) return false;
997 if (!file->put ('\n')) return false;
998 witnesses++;
999 return true;
1000 }
1001 };
1002
write_extension(const char * path)1003 const char * Solver::write_extension (const char * path) {
1004 LOG_API_CALL_BEGIN ("write_extension", path);
1005 REQUIRE_VALID_STATE ();
1006 const char * res = 0;
1007 #ifndef QUIET
1008 const double start = internal->time ();
1009 #endif
1010 File * file = File::write (internal, path);
1011 WitnessWriter writer (file);
1012 if (file) {
1013 if (!traverse_witnesses_backward (writer))
1014 res = internal->error_message.init (
1015 "writing to DIMACS file '%s' failed", path);
1016 delete file;
1017 } else res = internal->error_message.init (
1018 "failed to open extension file '%s' for writing", path);
1019 #ifndef QUIET
1020 if (!res) {
1021 const double end = internal->time ();
1022 MSG ("wrote %" PRId64 " witnesses in %.2f seconds %s time",
1023 writer.witnesses, end - start,
1024 internal->opts.realtime ? "real" : "process");
1025 }
1026 #endif
1027 LOG_API_CALL_RETURNS ("write_extension", path, res);
1028 return res;
1029 }
1030
1031 /*------------------------------------------------------------------------*/
1032
1033 struct ClauseCopier : public ClauseIterator {
1034 Solver & dst;
1035 public:
ClauseCopierCaDiCaL::ClauseCopier1036 ClauseCopier (Solver & d) : dst (d) { }
clauseCaDiCaL::ClauseCopier1037 bool clause (const vector<int> & c) {
1038 for (const auto & lit : c)
1039 dst.add (lit);
1040 dst.add (0);
1041 return true;
1042 }
1043 };
1044
1045 struct WitnessCopier : public WitnessIterator {
1046 External * dst;
1047 public:
WitnessCopierCaDiCaL::WitnessCopier1048 WitnessCopier (External * d) : dst (d) { }
witnessCaDiCaL::WitnessCopier1049 bool witness (const vector<int> & c, const vector<int> & w) {
1050 dst->push_external_clause_and_witness_on_extension_stack (c, w);
1051 return true;
1052 }
1053 };
1054
copy(Solver & other) const1055 void Solver::copy (Solver & other) const {
1056 ClauseCopier clause_copier (other);
1057 traverse_clauses (clause_copier);
1058 WitnessCopier witness_copier (other.external);
1059 traverse_witnesses_forward (witness_copier);
1060 }
1061
1062 /*------------------------------------------------------------------------*/
1063
section(const char * title)1064 void Solver::section (const char * title) {
1065 if (state () == DELETING) return;
1066 #ifdef QUIET
1067 (void) title;
1068 #endif
1069 REQUIRE_INITIALIZED ();
1070 SECTION (title);
1071 }
1072
message(const char * fmt,...)1073 void Solver::message (const char * fmt, ...) {
1074 if (state () == DELETING) return;
1075 #ifdef QUIET
1076 (void) fmt;
1077 #else
1078 REQUIRE_INITIALIZED ();
1079 va_list ap;
1080 va_start (ap, fmt);
1081 internal->vmessage (fmt, ap);
1082 va_end (ap);
1083 #endif
1084 }
1085
message()1086 void Solver::message () {
1087 if (state () == DELETING) return;
1088 REQUIRE_INITIALIZED ();
1089 #ifndef QUIET
1090 internal->message ();
1091 #endif
1092 }
1093
verbose(int level,const char * fmt,...)1094 void Solver::verbose (int level, const char * fmt, ...) {
1095 if (state () == DELETING) return;
1096 REQUIRE_VALID_OR_SOLVING_STATE ();
1097 #ifdef QUIET
1098 (void) level;
1099 (void) fmt;
1100 #else
1101 va_list ap;
1102 va_start (ap, fmt);
1103 internal->vverbose (level, fmt, ap);
1104 va_end (ap);
1105 #endif
1106 }
1107
error(const char * fmt,...)1108 void Solver::error (const char * fmt, ...) {
1109 if (state () == DELETING) return;
1110 REQUIRE_INITIALIZED ();
1111 va_list ap;
1112 va_start (ap, fmt);
1113 internal->verror (fmt, ap);
1114 va_end (ap);
1115 }
1116
1117 }
1118