1 #include "internal.hpp"
2
3 namespace CaDiCaL {
4
5 #ifndef QUIET
6
7 /*------------------------------------------------------------------------*/
8
9 // Provide nicely formatted progress report messages while running through
10 // the 'report' function below. The code is so complex, because it should
11 // be easy to add and remove reporting of certain statistics, while at the
12 // same time proving a nicely looking format, including automatic headers.
13
14 /* The 'reports' are shown as 'c <char> ...' with '<char>' as follows:
15
16 i propagated learned unit clause
17 O backtracked after phases reset to original phase
18 F backtracked after flipping phases
19 # backtracked after randomly setting phases
20 B backtracked after resetting to best phases
21 W backtracked after local search improved phases
22 b blocked clause elimination
23 G before garbage collection
24 C after garbage collection
25 / compacted internal literals and remapped external to internal
26 c covered clause elimination
27 d decomposed binary implication graph and substituted equivalent literals
28 2 removed duplicated binary clauses
29 e bounded variable elimination round
30 I variable instantiation
31 [ start of stable search phase
32 ] end of stable search phase
33 { start of unstable search phase
34 j end of unstable search phase
35 P preprocessing round
36 L local search round
37 * start of solving without the need to restore clauses
38 + start of solving before restoring clauses
39 r start of solving after restoring clauses
40 1 end of solving returns satisfiable
41 0 end of solving returns unsatisfiable
42 ? end of solving due to interrupt
43 l lucky phase solving
44 p failed literal probing round
45 . before reducing redundant clauses
46 f flushed redundant clauses
47 - reduced redundant clauses
48 ~ start of resetting phases
49 R restart
50 s subsumed clause removal round
51 3 ternary resolution round
52 t transition reduction of binary implication graph
53 w vivified redundant and irredundant clauses
54 v vivified irredundant clauses
55
56 */
57
58 /*------------------------------------------------------------------------*/
59
60 struct Report {
61
62 const char * header;
63 char buffer[20];
64 int pos;
65
66 Report (const char * h, int precision, int min, double value);
ReportCaDiCaL::Report67 Report () { }
68
69 void print_header (char * line);
70 };
71
72 /*------------------------------------------------------------------------*/
73
print_header(char * line)74 void Report::print_header (char * line) {
75 int len = strlen (header);
76 for (int i = -1, j = pos - (len + 1)/2 - 3; i < len; i++, j++)
77 line[j] = i < 0 ? ' ' : header[i];
78 }
79
Report(const char * h,int precision,int min,double value)80 Report::Report (const char * h, int precision, int min, double value)
81 :
82 header (h)
83 {
84 char fmt[32];
85 if (precision < 0) sprintf (fmt, "%%.%df", -precision - 1);
86 else sprintf (fmt, "%%.%df", precision);
87 sprintf (buffer, fmt, value);
88 const int width = strlen (buffer);
89 if (precision < 0) strcat (buffer, "%");
90 if (width >= min) return;
91 if (precision < 0) sprintf (fmt, "%%%d.%df%%%%", min, -precision - 1);
92 else sprintf (fmt, "%%%d.%df", min, precision);
93 sprintf (buffer, fmt, value);
94 }
95
96 /*------------------------------------------------------------------------*/
97
98 // The following statistics are printed in columns, whenever 'report' is
99 // called. For instance 'reduce' with prefix '-' will call it. The other
100 // more interesting report is due to learning a unit, called iteration, with
101 // prefix 'i'. To add another statistics column, add a corresponding line
102 // here. If you want to report something else add 'report (..)' functions.
103
104 #define TIME \
105 opts.reportsolve ? solve_time () : time ()
106
107 #define MB \
108 (current_resident_set_size () / (double)(1l<<20))
109
110 #define REMAINING \
111 (percent (active (), external->max_var))
112
113 #define TRAIL \
114 (percent (averages.current.trail.slow, max_var))
115
116 #define TARGET \
117 (percent (target_assigned, max_var))
118
119 #define BEST \
120 (percent (best_assigned, max_var))
121
122 #define REPORTS \
123 /* HEADER, PRECISION, MIN, VALUE */ \
124 REPORT("seconds", 2, 5, TIME) \
125 REPORT("MB", 0, 2, MB) \
126 REPORT("level", 0, 2, averages.current.level) \
127 REPORT("reductions", 0, 1, stats.reductions) \
128 REPORT("restarts", 0, 3, stats.restarts) \
129 REPORT("conflicts", 0, 4, stats.conflicts) \
130 REPORT("redundant", 0, 4, stats.current.redundant) \
131 REPORT("trail", -1, 2, TRAIL) \
132 REPORT("glue", 0, 1, averages.current.glue.slow) \
133 REPORT("irredundant", 0, 4, stats.current.irredundant) \
134 REPORT("variables", 0, 3, active ()) \
135 REPORT("remaining", -1, 2, REMAINING) \
136
137 // Note, keep an empty line before this line (because of '\')!
138
139 #if 0 // ADDITIONAL STATISTICS TO REPORT
140
141 REPORT("best", -1, 2, BEST) \
142 REPORT("target", -1, 2, TARGET) \
143 REPORT("maxvar", 0, 2, external->max_var) \
144
145 #endif
146
147 static const int num_reports = // as compile time constant
148 #define REPORT(HEAD,PREC,MIN,EXPR) \
149 1 +
150 REPORTS
151 #undef REPORT
152 0;
153
154 /*------------------------------------------------------------------------*/
155
report(char type,int verbose)156 void Internal::report (char type, int verbose) {
157 if (!opts.report) return;
158 #ifdef LOGGING
159 if (!opts.log)
160 #endif
161 if (opts.quiet || (verbose > opts.verbose)) return;
162 if (!reported) {
163 assert (!lim.report);
164 reported = true;
165 MSG ("%stime measured in %s time %s%s",
166 tout.magenta_code (),
167 internal->opts.realtime ? "real" : "process",
168 internal->opts.reportsolve ? "in solving" : "since initialization",
169 tout.normal_code ());
170 }
171 Report reports[num_reports];
172 int n = 0;
173 #define REPORT(HEAD,PREC,MIN,EXPR) \
174 assert (n < num_reports); \
175 reports[n++] = Report (HEAD, PREC, MIN, (double)(EXPR));
176 REPORTS
177 #undef REPORT
178 if (!lim.report) {
179 print_prefix ();
180 fputc ('\n', stdout);
181 int pos = 4;
182 for (int i = 0; i < n; i++) {
183 int len = strlen (reports[i].buffer);
184 reports[i].pos = pos + (len + 1)/2;
185 pos += len + 1;
186 }
187 const int max_line = pos + 20, nrows = 3;
188 char *line = new char[max_line];
189 for (int start = 0; start < nrows; start++) {
190 int i;
191 for (i = 0; i < max_line; i++)
192 line[i] = ' ';
193 for (i = start; i < n; i += nrows)
194 reports[i].print_header (line);
195 for (i = max_line-1; line[i-1] == ' '; i--)
196 ;
197 line[i] = 0;
198 print_prefix ();
199 tout.yellow ();
200 fputs (line, stdout);
201 tout.normal ();
202 fputc ('\n', stdout);
203 }
204 print_prefix ();
205 fputc ('\n', stdout);
206 delete [] line;
207 lim.report = 19;
208 } else lim.report--;
209 print_prefix ();
210 switch (type) {
211 case '[': case ']': tout.magenta (true); break;
212 case 's': case 'v': case 'w':
213 case 't': case 'b': case 'c': tout.green (false); break;
214 case 'e': tout.green (true); break;
215 case 'p': case '2': case '3': tout.blue (false); break;
216 case 'd': tout.blue (true); break;
217 case 'z': case 'f': tout.cyan (true); break;
218 case '-': tout.normal (); break;
219 case '/': tout.yellow (true); break;
220 case '0': case '1': case '?':
221 case 'i': tout.bold (); break;
222 case 'L': case 'P': tout.bold (); tout.underline (); break;
223 }
224 fputc (type, stdout);
225 if (stable || type == ']') tout.magenta ();
226 else if (type != 'L' && type != 'P') tout.normal ();
227 for (int i = 0; i < n; i++) {
228 fputc (' ', stdout);
229 fputs (reports[i].buffer, stdout);
230 }
231 if (stable || type == 'L' || type == 'P' || type == ']') tout.normal ();
232 fputc ('\n', stdout);
233 fflush (stdout);
234 }
235
236 #else // ifndef QUIET
237
238 void Internal::report (char, int) { }
239
240 #endif
241
242 }
243