1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
#ifndef _logging_hpp_INCLUDED
#define _logging_hpp_INCLUDED
/*------------------------------------------------------------------------*/
#ifdef LOGGING
/*------------------------------------------------------------------------*/
#include <cstdint>
#include <vector>
namespace CaDiCaL {
// For debugging purposes and to help understanding what the solver is doing
// there is a logging facility which is compiled in by './configure -l'. It
// still has to be enabled at run-time though (again using the '-l' option
// in the stand-alone solver). It produces quite a bit of information.
using namespace std;
struct Clause;
struct Gate;
struct Internal;
struct Logger {
static void print_log_prefix (Internal *);
// Simple logging of a C-style format string.
//
static void log (Internal *, const char *fmt, ...)
CADICAL_ATTRIBUTE_FORMAT (2, 3);
// Prints the format string (with its argument) and then the clause. The
// clause can also be a zero pointer and then is interpreted as a decision
// (current decision level > 0) or unit clause (zero decision level) and
// printed accordingly.
//
static void log (Internal *, const Clause *, const char *fmt, ...)
CADICAL_ATTRIBUTE_FORMAT (3, 4);
// Same as before, except that this is meant for the global 'clause' stack
// used for new clauses (and not for reasons).
//
static void log (Internal *, const vector<int> &, const char *fmt, ...)
CADICAL_ATTRIBUTE_FORMAT (3, 4);
// Another variant, to avoid copying (without logging).
//
static void log (Internal *, const vector<int>::const_iterator &begin,
const vector<int>::const_iterator &end, const char *fmt,
...) CADICAL_ATTRIBUTE_FORMAT (4, 5);
// used for logging LRAT proof chains
//
static void log (Internal *, const vector<int64_t> &, const char *fmt,
...) CADICAL_ATTRIBUTE_FORMAT (3, 4);
static void log (Internal *, const int *, const unsigned, const char *fmt,
...) CADICAL_ATTRIBUTE_FORMAT (4, 5);
static void log_empty_line (Internal *);
static void log (Internal *, const Gate *, const char *fmt, ...)
CADICAL_ATTRIBUTE_FORMAT (3, 4);
static string loglit (Internal *, int lit);
};
} // namespace CaDiCaL
/*------------------------------------------------------------------------*/
// Make sure that 'logging' code is really not included (second case of the
// '#ifdef') if logging code is not included.
#define LOG(...) \
do { \
if (!internal->opts.log) \
break; \
Logger::log (internal, __VA_ARGS__); \
} while (0)
#define LOGLIT(lit) Logger::loglit (internal, lit).c_str ()
/*------------------------------------------------------------------------*/
#else // end of 'then' part of 'ifdef LOGGING'
/*------------------------------------------------------------------------*/
#define LOG(...) \
do { \
} while (0)
#define LOGLIT(...)
/*------------------------------------------------------------------------*/
#endif // end of 'else' part of 'ifdef LOGGING'
/*------------------------------------------------------------------------*/
#endif