ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
cadical_stats.cpp
Go to the documentation of this file.
1// vim: set tw=300: set VIM text width to 300 characters for this file.
2#include "global.h"
3
4
5#include "internal.hpp"
6
7ABC_NAMESPACE_IMPL_START
8
9namespace CaDiCaL {
10
11/*------------------------------------------------------------------------*/
12
13Stats::Stats () {
14 time.real = absolute_real_time ();
15 time.process = absolute_process_time ();
16 walk.minimum = LONG_MAX;
17 used.resize (2);
18 used[0].resize (127);
19 used[1].resize (127);
20}
21
22/*------------------------------------------------------------------------*/
23
24#define PRT(FMT, ...) \
25 do { \
26 if (FMT[0] == ' ' && !all) \
27 break; \
28 MSG (FMT, __VA_ARGS__); \
29 } while (0)
30
31/*------------------------------------------------------------------------*/
32
33void Stats::print (Internal *internal) {
34
35#ifdef CADICAL_QUIET
36 (void) internal;
37#else
38
39 Stats &stats = internal->stats;
40
41 int all = internal->opts.verbose > 0 || internal->opts.stats;
42#ifdef LOGGING
43 if (internal->opts.log)
44 all = true;
45#endif // ifdef LOGGING
46
47 if (internal->opts.profile)
48 internal->print_profile ();
49
50 double t = internal->solve_time ();
51
52 int64_t propagations = 0;
53 propagations += stats.propagations.cover;
54 propagations += stats.propagations.probe;
55 propagations += stats.propagations.search;
56 propagations += stats.propagations.transred;
57 propagations += stats.propagations.vivify;
58 propagations += stats.propagations.walk;
59
60 int64_t vivified = stats.vivifysubs + stats.vivifystrs;
61 int64_t searchticks = stats.ticks.search[0] + stats.ticks.search[1];
62 int64_t inprobeticks = stats.ticks.vivify + stats.ticks.probe +
63 stats.ticks.factor + stats.ticks.ternary +
64 stats.ticks.sweep;
65 int64_t totalticks = searchticks + inprobeticks;
66
67 size_t extendbytes = internal->external->extension.size ();
68 extendbytes *= sizeof (int);
69
70 SECTION ("statistics");
71
72 if (all || stats.blocked) {
73 PRT ("blocked: %15" PRId64
74 " %10.2f %% of irredundant clauses",
75 stats.blocked, percent (stats.blocked, stats.added.irredundant));
76 PRT (" blockings: %15" PRId64 " %10.2f internal",
77 stats.blockings, relative (stats.conflicts, stats.blockings));
78 PRT (" candidates: %15" PRId64 " %10.2f per blocking ",
79 stats.blockcands, relative (stats.blockcands, stats.blockings));
80 PRT (" blockres: %15" PRId64 " %10.2f per candidate",
81 stats.blockres, relative (stats.blockres, stats.blockcands));
82 PRT (" pure: %15" PRId64 " %10.2f %% of all variables",
83 stats.all.pure, percent (stats.all.pure, stats.vars));
84 PRT (" pureclauses: %15" PRId64 " %10.2f per pure literal",
85 stats.blockpured, relative (stats.blockpured, stats.all.pure));
86 }
87 if (all || stats.chrono)
88 PRT ("chronological: %15" PRId64 " %10.2f %% of conflicts",
89 stats.chrono, percent (stats.chrono, stats.conflicts));
90 if (all)
91 PRT ("compacts: %15" PRId64 " %10.2f interval",
92 stats.compacts, relative (stats.conflicts, stats.compacts));
93 if (all || stats.conflicts) {
94 PRT ("conflicts: %15" PRId64 " %10.2f per second",
95 stats.conflicts, relative (stats.conflicts, t));
96 PRT (" backtracked: %15" PRId64 " %10.2f %% of conflicts",
97 stats.backtracks, percent (stats.backtracks, stats.conflicts));
98 }
99 if (all || stats.conditioned) {
100 PRT ("conditioned: %15" PRId64
101 " %10.2f %% of irredundant clauses",
102 stats.conditioned,
103 percent (stats.conditioned, stats.added.irredundant));
104 PRT (" conditionings: %15" PRId64 " %10.2f interval",
105 stats.conditionings,
106 relative (stats.conflicts, stats.conditionings));
107 PRT (" condcands: %15" PRId64 " %10.2f candidate clauses",
108 stats.condcands, relative (stats.condcands, stats.conditionings));
109 PRT (" condassinit: %17.1f %9.2f %% initial assigned",
110 relative (stats.condassinit, stats.conditionings),
111 percent (stats.condassinit, stats.condassvars));
112 PRT (" condcondinit: %17.1f %9.2f %% initial condition",
113 relative (stats.condcondinit, stats.conditionings),
114 percent (stats.condcondinit, stats.condassinit));
115 PRT (" condautinit: %17.1f %9.2f %% initial autarky",
116 relative (stats.condautinit, stats.conditionings),
117 percent (stats.condautinit, stats.condassinit));
118 PRT (" condassrem: %17.1f %9.2f %% final assigned",
119 relative (stats.condassrem, stats.conditioned),
120 percent (stats.condassrem, stats.condassirem));
121 PRT (" condcondrem: %19.3f %7.2f %% final conditional",
122 relative (stats.condcondrem, stats.conditioned),
123 percent (stats.condcondrem, stats.condassrem));
124 PRT (" condautrem: %19.3f %7.2f %% final autarky",
125 relative (stats.condautrem, stats.conditioned),
126 percent (stats.condautrem, stats.condassrem));
127 PRT (" condprops: %15" PRId64 " %10.2f per candidate",
128 stats.condprops, relative (stats.condprops, stats.condcands));
129 }
130 if (all || stats.cover.total) {
131 PRT ("covered: %15" PRId64
132 " %10.2f %% of irredundant clauses",
133 stats.cover.total,
134 percent (stats.cover.total, stats.added.irredundant));
135 PRT (" coverings: %15" PRId64 " %10.2f interval",
136 stats.cover.count, relative (stats.conflicts, stats.cover.count));
137 PRT (" asymmetric: %15" PRId64 " %10.2f %% of covered clauses",
138 stats.cover.asymmetric,
139 percent (stats.cover.asymmetric, stats.cover.total));
140 PRT (" blocked: %15" PRId64 " %10.2f %% of covered clauses",
141 stats.cover.blocked,
142 percent (stats.cover.blocked, stats.cover.total));
143 }
144 if (all || stats.decisions) {
145 PRT ("decisions: %15" PRId64 " %10.2f per second",
146 stats.decisions, relative (stats.decisions, t));
147 PRT (" searched: %15" PRId64 " %10.2f per decision",
148 stats.searched, relative (stats.searched, stats.decisions));
149 }
150 if (all || stats.all.eliminated) {
151 PRT ("eliminated: %15" PRId64 " %10.2f %% of all variables",
152 stats.all.eliminated, percent (stats.all.eliminated, stats.vars));
153 PRT (" fastelim: %15" PRId64 " %10.2f %% of eliminated",
154 stats.all.fasteliminated,
155 percent (stats.all.fasteliminated, stats.all.eliminated));
156 PRT (" elimphases: %15" PRId64 " %10.2f interval",
157 stats.elimphases, relative (stats.conflicts, stats.elimphases));
158 PRT (" elimrounds: %15" PRId64 " %10.2f per phase",
159 stats.elimrounds, relative (stats.elimrounds, stats.elimphases));
160 PRT (" elimtried: %15" PRId64 " %10.2f %% eliminated",
161 stats.elimtried, percent (stats.all.eliminated, stats.elimtried));
162 PRT (" elimgates: %15" PRId64 " %10.2f %% gates per tried",
163 stats.elimgates, percent (stats.elimgates, stats.elimtried));
164 PRT (" elimequivs: %15" PRId64 " %10.2f %% equivalence gates",
165 stats.elimequivs, percent (stats.elimequivs, stats.elimgates));
166 PRT (" elimands: %15" PRId64 " %10.2f %% and gates",
167 stats.elimands, percent (stats.elimands, stats.elimgates));
168 PRT (" elimites: %15" PRId64 " %10.2f %% if-then-else gates",
169 stats.elimites, percent (stats.elimites, stats.elimgates));
170 PRT (" elimxors: %15" PRId64 " %10.2f %% xor gates",
171 stats.elimxors, percent (stats.elimxors, stats.elimgates));
172 PRT (" elimdefs: %15" PRId64 " %10.2f %% definitions",
173 stats.definitions_extracted,
174 percent (stats.definitions_extracted, stats.elimgates));
175 PRT (" elimsubst: %15" PRId64 " %10.2f %% substituted",
176 stats.elimsubst, percent (stats.elimsubst, stats.all.eliminated));
177 PRT (" elimsubstequi: %15" PRId64 " %10.2f %% equivalence gates",
178 stats.eliminated_equi,
179 percent (stats.eliminated_equi, stats.elimsubst));
180 PRT (" elimsubstands: %15" PRId64 " %10.2f %% and gates",
181 stats.eliminated_and,
182 percent (stats.eliminated_and, stats.elimsubst));
183 PRT (" elimsubstites: %15" PRId64 " %10.2f %% if-then-else gates",
184 stats.eliminated_ite,
185 percent (stats.eliminated_ite, stats.elimsubst));
186 PRT (" elimsubstxors: %15" PRId64 " %10.2f %% xor gates",
187 stats.eliminated_xor,
188 percent (stats.eliminated_xor, stats.elimsubst));
189 PRT (" elimsubstdefs: %15" PRId64 " %10.2f %% definitions",
190 stats.eliminated_def,
191 percent (stats.eliminated_def, stats.elimsubst));
192 PRT (" elimres: %15" PRId64 " %10.2f per eliminated",
193 stats.elimres, relative (stats.elimres, stats.all.eliminated));
194 PRT (" elimrestried: %15" PRId64 " %10.2f %% per resolution",
195 stats.elimrestried, percent (stats.elimrestried, stats.elimres));
196 PRT (" def checked: %15" PRId64 " %10.2f per phase",
197 stats.definitions_checked,
198 relative (stats.definitions_checked, stats.elimphases));
199 PRT (" def extracted: %15" PRId64 " %10.2f %% per checked",
200 stats.definitions_extracted,
201 percent (stats.definitions_extracted, stats.definitions_checked));
202 PRT (" def units: %15" PRId64 " %10.2f %% per checked",
203 stats.definition_units,
204 percent (stats.definition_units, stats.definitions_checked));
205 }
206 if (all || stats.ext_prop.ext_cb) {
207 PRT ("ext.prop. calls: %15" PRId64 " %10.2f %% of queries",
208 stats.ext_prop.eprop_call,
209 percent (stats.ext_prop.eprop_call, stats.ext_prop.ext_cb));
210 PRT (" propagating: %15" PRId64 " %10.2f %% per eprop-call",
211 stats.ext_prop.eprop_prop,
212 percent (stats.ext_prop.eprop_prop, stats.ext_prop.eprop_call));
213 PRT (" explained: %15" PRId64 " %10.2f %% per eprop-call",
214 stats.ext_prop.eprop_expl,
215 percent (stats.ext_prop.eprop_expl, stats.ext_prop.eprop_call));
216 PRT (" falsified: %15" PRId64 " %10.2f %% per eprop-call",
217 stats.ext_prop.eprop_conf,
218 percent (stats.ext_prop.eprop_conf, stats.ext_prop.eprop_call));
219 PRT ("ext.clause calls:%15" PRId64 " %10.2f %% of queries",
220 stats.ext_prop.elearn_call,
221 percent (stats.ext_prop.elearn_call, stats.ext_prop.ext_cb));
222 PRT (" learned: %15" PRId64 " %10.2f %% per called",
223 stats.ext_prop.elearned,
224 percent (stats.ext_prop.elearned, stats.ext_prop.elearn_call));
225 PRT (" conflicting: %15" PRId64 " %10.2f %% per learned",
226 stats.ext_prop.elearn_conf,
227 percent (stats.ext_prop.elearn_conf, stats.ext_prop.elearned));
228 PRT (" propagating: %15" PRId64 " %10.2f %% per learned",
229 stats.ext_prop.elearn_prop,
230 percent (stats.ext_prop.elearn_prop, stats.ext_prop.elearned));
231 PRT ("ext.final check: %15" PRId64 " %10.2f %% of queries",
232 stats.ext_prop.echeck_call,
233 percent (stats.ext_prop.echeck_call, stats.ext_prop.ext_cb));
234 }
235 if (all || stats.factored) {
236 PRT ("factored: %15" PRId64 " %10.2f %% of variables",
237 stats.factored, percent (stats.factored, internal->max_var));
238 PRT (" factor: %15" PRId64 " %10.2f conflict interval",
239 stats.factor, relative (stats.conflicts, stats.factor));
240 PRT (" cls factored: %15" PRId64 " %10.2f per factored",
241 stats.factor_added, relative (stats.factor_added, factored));
242 PRT (" lits factored: %15" PRId64 " %10.2f per factored",
243 stats.literals_factored,
244 relative (stats.literals_factored, factored));
245 PRT (" cls unfactored:%15" PRId64 " %10.2f per factored",
246 stats.clauses_unfactored,
247 relative (stats.clauses_unfactored, factored));
248 PRT (" lits unfactored:%14" PRId64 " %10.2f per factored",
249 stats.literals_unfactored,
250 relative (stats.literals_unfactored, factored));
251 }
252 if (all || stats.all.fixed) {
253 PRT ("fixed: %15" PRId64 " %10.2f %% of all variables",
254 stats.all.fixed, percent (stats.all.fixed, stats.vars));
255 PRT (" failed: %15" PRId64 " %10.2f %% of all variables",
256 stats.failed, percent (stats.failed, stats.vars));
257 PRT (" probefailed: %15" PRId64 " %10.2f %% per failed",
258 stats.probefailed, percent (stats.probefailed, stats.failed));
259 PRT (" transredunits: %15" PRId64 " %10.2f %% per failed",
260 stats.transredunits, percent (stats.transredunits, stats.failed));
261 PRT (" inprobephases: %15" PRId64 " %10.2f interval",
262 stats.inprobingphases,
263 relative (stats.conflicts, stats.inprobingphases));
264 PRT (" inprobesuccess:%15" PRId64 " %10.2f %% phases",
265 stats.inprobesuccess,
266 percent (stats.inprobesuccess, stats.inprobingphases));
267 PRT (" probingrounds: %15" PRId64 " %10.2f per phase",
268 stats.probingrounds,
269 relative (stats.probingrounds, stats.inprobingphases));
270 PRT (" probed: %15" PRId64 " %10.2f per failed",
271 stats.probed, relative (stats.probed, stats.failed));
272 PRT (" hbrs: %15" PRId64 " %10.2f per probed",
273 stats.hbrs, relative (stats.hbrs, stats.probed));
274 PRT (" hbrsizes: %15" PRId64 " %10.2f per hbr",
275 stats.hbrsizes, relative (stats.hbrsizes, stats.hbrs));
276 PRT (" hbreds: %15" PRId64 " %10.2f %% per hbr",
277 stats.hbreds, percent (stats.hbreds, stats.hbrs));
278 PRT (" hbrsubs: %15" PRId64 " %10.2f %% per hbr",
279 stats.hbrsubs, percent (stats.hbrsubs, stats.hbrs));
280 }
281 PRT (" units: %15" PRId64 " %10.2f interval", stats.units,
282 relative (stats.conflicts, stats.units));
283 PRT (" binaries: %15" PRId64 " %10.2f interval",
284 stats.binaries, relative (stats.conflicts, stats.binaries));
285 if (all || stats.flush.learned) {
286 PRT ("flushed: %15" PRId64 " %10.2f %% per conflict",
287 stats.flush.learned,
288 percent (stats.flush.learned, stats.conflicts));
289 PRT (" hyper: %15" PRId64 " %10.2f %% per conflict",
290 stats.flush.hyper, relative (stats.flush.hyper, stats.conflicts));
291 PRT (" flushings: %15" PRId64 " %10.2f interval",
292 stats.flush.count, relative (stats.conflicts, stats.flush.count));
293 }
294 if (all || stats.instantiated) {
295 PRT ("instantiated: %15" PRId64 " %10.2f %% of tried",
296 stats.instantiated, percent (stats.instantiated, stats.instried));
297 PRT (" instrounds: %15" PRId64 " %10.2f %% of elimrounds",
298 stats.instrounds, percent (stats.instrounds, stats.elimrounds));
299 }
300 if (all || stats.conflicts) {
301 PRT ("learned: %15" PRId64 " %10.2f %% per conflict",
302 stats.learned.clauses,
303 percent (stats.learned.clauses, stats.conflicts));
304 PRT ("@ bumped: %15" PRId64 " %10.2f per learned",
305 stats.bumped, relative (stats.bumped, stats.learned.clauses));
306 PRT (" recomputed: %15" PRId64 " %10.2f %% per learned",
307 stats.recomputed,
308 percent (stats.recomputed, stats.learned.clauses));
309 PRT (" promoted1: %15" PRId64 " %10.2f %% per learned",
310 stats.promoted1, percent (stats.promoted1, stats.learned.clauses));
311 PRT (" promoted2: %15" PRId64 " %10.2f %% per learned",
312 stats.promoted2, percent (stats.promoted2, stats.learned.clauses));
313 PRT (" improvedglue: %15" PRId64 " %10.2f %% per learned",
314 stats.improvedglue,
315 percent (stats.improvedglue, stats.learned.clauses));
316 }
317 if (all || stats.lucky.succeeded) {
318 PRT ("lucky: %15" PRId64 " %10.2f %% of tried",
319 stats.lucky.succeeded,
320 percent (stats.lucky.succeeded, stats.lucky.tried));
321 PRT (" constantzero %15" PRId64 " %10.2f %% of tried",
322 stats.lucky.constant.zero,
323 percent (stats.lucky.constant.zero, stats.lucky.tried));
324 PRT (" constantone %15" PRId64 " %10.2f %% of tried",
325 stats.lucky.constant.one,
326 percent (stats.lucky.constant.one, stats.lucky.tried));
327 PRT (" backwardone %15" PRId64 " %10.2f %% of tried",
328 stats.lucky.backward.one,
329 percent (stats.lucky.backward.one, stats.lucky.tried));
330 PRT (" backwardzero %15" PRId64 " %10.2f %% of tried",
331 stats.lucky.backward.zero,
332 percent (stats.lucky.backward.zero, stats.lucky.tried));
333 PRT (" forwardone %15" PRId64 " %10.2f %% of tried",
334 stats.lucky.forward.one,
335 percent (stats.lucky.forward.one, stats.lucky.tried));
336 PRT (" forwardzero %15" PRId64 " %10.2f %% of tried",
337 stats.lucky.forward.zero,
338 percent (stats.lucky.forward.zero, stats.lucky.tried));
339 PRT (" positivehorn %15" PRId64 " %10.2f %% of tried",
340 stats.lucky.horn.positive,
341 percent (stats.lucky.horn.positive, stats.lucky.tried));
342 PRT (" negativehorn %15" PRId64 " %10.2f %% of tried",
343 stats.lucky.horn.negative,
344 percent (stats.lucky.horn.negative, stats.lucky.tried));
345 }
346 PRT (" extendbytes: %15zd %10.2f bytes and MB", extendbytes,
347 extendbytes / (double) (1l << 20));
348 if (all || stats.learned.clauses)
349 PRT ("learned_lits: %15" PRId64 " %10.2f %% learned literals",
350 stats.learned.literals,
351 percent (stats.learned.literals, stats.learned.literals));
352 PRT ("minimized: %15" PRId64 " %10.2f %% learned literals",
353 stats.minimized, percent (stats.minimized, stats.learned.literals));
354 PRT ("shrunken: %15" PRId64 " %10.2f %% learned literals",
355 stats.shrunken, percent (stats.shrunken, stats.learned.literals));
356 PRT ("minishrunken: %15" PRId64 " %10.2f %% learned literals",
357 stats.minishrunken,
358 percent (stats.minishrunken, stats.learned.literals));
359
360 if (all || stats.conflicts) {
361 PRT ("otfs: %15" PRId64 " %10.2f %% of conflict",
362 stats.otfs.subsumed + stats.otfs.strengthened,
363 percent (stats.otfs.subsumed + stats.otfs.strengthened,
364 stats.conflicts));
365 PRT (" subsumed %15" PRId64 " %10.2f %% of conflict",
366 stats.otfs.subsumed,
367 percent (stats.otfs.subsumed, stats.conflicts));
368 PRT (" strengthened %15" PRId64 " %10.2f %% of conflict",
369 stats.otfs.strengthened,
370 percent (stats.otfs.strengthened, stats.conflicts));
371 }
372
373 PRT ("propagations: %15" PRId64 " %10.2f M per second",
374 propagations, relative (propagations / 1e6, t));
375 PRT (" coverprops: %15" PRId64 " %10.2f %% of propagations",
376 stats.propagations.cover,
377 percent (stats.propagations.cover, propagations));
378 PRT (" probeprops: %15" PRId64 " %10.2f %% of propagations",
379 stats.propagations.probe,
380 percent (stats.propagations.probe, propagations));
381 PRT (" searchprops: %15" PRId64 " %10.2f %% of propagations",
382 stats.propagations.search,
383 percent (stats.propagations.search, propagations));
384 PRT (" transredprops: %15" PRId64 " %10.2f %% of propagations",
385 stats.propagations.transred,
386 percent (stats.propagations.transred, propagations));
387 PRT (" vivifyprops: %15" PRId64 " %10.2f %% of propagations",
388 stats.propagations.vivify,
389 percent (stats.propagations.vivify, propagations));
390 PRT (" walkprops: %15" PRId64 " %10.2f %% of propagations",
391 stats.propagations.walk,
392 percent (stats.propagations.walk, propagations));
393 if (all || stats.reactivated) {
394 PRT ("reactivated: %15" PRId64 " %10.2f %% of all variables",
395 stats.reactivated, percent (stats.reactivated, stats.vars));
396 }
397 if (all || stats.reduced) {
398 PRT ("reduced: %15" PRId64 " %10.2f %% per conflict",
399 stats.reduced, percent (stats.reduced, stats.conflicts));
400 PRT (" reductions: %15" PRId64 " %10.2f interval",
401 stats.reductions, relative (stats.conflicts, stats.reductions));
402 PRT (" sqrt scheme: %15" PRId64 " %10.2f %% reductions",
403 stats.reduced_sqrt,
404 relative (stats.reduced_sqrt, stats.reductions));
405 PRT (" prct scheme: %15" PRId64 " %10.2f %% reductions",
406 stats.reduced_prct,
407 relative (stats.reduced_prct, stats.reductions));
408 PRT (" collections: %15" PRId64 " %10.2f interval",
409 stats.collections, relative (stats.conflicts, stats.collections));
410 }
411 if (all || stats.rephased.total) {
412 PRT ("rephased: %15" PRId64 " %10.2f interval",
413 stats.rephased.total,
414 relative (stats.conflicts, stats.rephased.total));
415 PRT (" rephasedbest: %15" PRId64 " %10.2f %% rephased best",
416 stats.rephased.best,
417 percent (stats.rephased.best, stats.rephased.total));
418 PRT (" rephasedflip: %15" PRId64 " %10.2f %% rephased flipping",
419 stats.rephased.flipped,
420 percent (stats.rephased.flipped, stats.rephased.total));
421 PRT (" rephasedinv: %15" PRId64 " %10.2f %% rephased inverted",
422 stats.rephased.inverted,
423 percent (stats.rephased.inverted, stats.rephased.total));
424 PRT (" rephasedorig: %15" PRId64 " %10.2f %% rephased original",
425 stats.rephased.original,
426 percent (stats.rephased.original, stats.rephased.total));
427 PRT (" rephasedrand: %15" PRId64 " %10.2f %% rephased random",
428 stats.rephased.random,
429 percent (stats.rephased.random, stats.rephased.total));
430 PRT (" rephasedwalk: %15" PRId64 " %10.2f %% rephased walk",
431 stats.rephased.walk,
432 percent (stats.rephased.walk, stats.rephased.total));
433 }
434 if (all)
435 PRT ("rescored: %15" PRId64 " %10.2f interval",
436 stats.rescored, relative (stats.conflicts, stats.rescored));
437 if (all || stats.restarts) {
438 PRT ("restarts: %15" PRId64 " %10.2f interval",
439 stats.restarts, relative (stats.conflicts, stats.restarts));
440 PRT (" reused: %15" PRId64 " %10.2f %% per restart",
441 stats.reused, percent (stats.reused, stats.restarts));
442 PRT (" reusedlevels: %15" PRId64 " %10.2f %% per restart levels",
443 stats.reusedlevels,
444 percent (stats.reusedlevels, stats.restartlevels));
445 }
446 if (all || stats.restored) {
447 PRT ("restored: %15" PRId64 " %10.2f %% per weakened",
448 stats.restored, percent (stats.restored, stats.weakened));
449 PRT (" restorations: %15" PRId64 " %10.2f %% per extension",
450 stats.restorations,
451 percent (stats.restorations, stats.extensions));
452 PRT (" literals: %15" PRId64 " %10.2f per restored clause",
453 stats.restoredlits, relative (stats.restoredlits, stats.restored));
454 }
455 if (all || stats.stabphases) {
456 PRT ("stabilizing: %15" PRId64 " %10.2f %% of conflicts",
457 stats.stabphases, percent (stats.stabconflicts, stats.conflicts));
458 PRT (" restartstab: %15" PRId64 " %10.2f %% of all restarts",
459 stats.restartstable,
460 percent (stats.restartstable, stats.restarts));
461 PRT (" reusedstab: %15" PRId64 " %10.2f %% per stable restarts",
462 stats.reusedstable,
463 percent (stats.reusedstable, stats.restartstable));
464 }
465 if (all || stats.all.substituted) {
466 PRT ("substituted: %15" PRId64 " %10.2f %% of all variables",
467 stats.all.substituted,
468 percent (stats.all.substituted, stats.vars));
469 PRT (" decompositions:%15" PRId64 " %10.2f per phase",
470 stats.decompositions,
471 relative (stats.decompositions, stats.inprobingphases));
472 }
473 if (all || stats.sweep_equivalences) {
474 PRT ("sweep equivs: %15" PRId64 " %10.2f %% of swept variables",
475 stats.sweep_equivalences,
476 percent (stats.sweep_equivalences, stats.sweep_variables));
477 PRT (" sweepings: %15" PRId64 " %10.2f vars per sweeping",
478 stats.sweep, relative (stats.sweep_variables, stats.sweep));
479 PRT (" swept vars: %15" PRId64 " %10.2f %% of all variables",
480 stats.sweep_variables,
481 percent (stats.sweep_variables, stats.vars));
482 PRT (" sweep units: %15" PRId64 " %10.2f %% of all variables",
483 stats.sweep_units, percent (stats.sweep_units, stats.vars));
484 PRT (" solved: %15" PRId64 " %10.2f per swept variable",
485 stats.sweep_solved,
486 relative (stats.sweep_solved, stats.sweep_variables));
487 PRT (" sat: %15" PRId64 " %10.2f %% solved",
488 stats.sweep_sat, percent (stats.sweep_sat, stats.sweep_solved));
489 PRT (" unsat: %15" PRId64 " %10.2f %% solved",
490 stats.sweep_unsat,
491 percent (stats.sweep_unsat, stats.sweep_solved));
492 PRT (" backbone solved:%14" PRId64 " %10.2f %% solved",
493 stats.sweep_solved_backbone,
494 percent (stats.sweep_solved_backbone, stats.sweep_solved));
495 PRT (" sat: %15" PRId64 " %10.2f %% backbone solved",
496 stats.sweep_sat_backbone,
497 percent (stats.sweep_sat_backbone, stats.sweep_solved_backbone));
498 PRT (" unsat: %15" PRId64 " %10.2f %% backbone solved",
499 stats.sweep_unsat_backbone,
500 percent (stats.sweep_unsat_backbone, stats.sweep_solved_backbone));
501 PRT (" unknown: %15" PRId64 " %10.2f %% backbone solved",
502 stats.sweep_unknown_backbone,
503 percent (stats.sweep_unknown_backbone,
504 stats.sweep_solved_backbone));
505 PRT (" fixed: %15" PRId64 " %10.2f per swept variable",
506 stats.sweep_fixed_backbone,
507 relative (stats.sweep_fixed_backbone, stats.sweep_variables));
508 PRT (" flip: %15" PRId64 " %10.2f per swept variable",
509 stats.sweep_flip_backbone,
510 relative (stats.sweep_flip_backbone, stats.sweep_variables));
511 PRT (" flipped: %15" PRId64 " %10.2f %% of backbone flip",
512 stats.sweep_flipped_backbone,
513 percent (stats.sweep_flipped_backbone, stats.sweep_flip_backbone));
514 PRT (" equiv solved: %15" PRId64 " %10.2f %% solved",
515 stats.sweep_solved_equivalences,
516 percent (stats.sweep_solved_equivalences, stats.sweep_solved));
517 PRT (" sat: %15" PRId64 " %10.2f %% equiv solved",
518 stats.sweep_sat_equivalences,
519 percent (stats.sweep_sat_equivalences,
520 stats.sweep_solved_equivalences));
521 PRT (" unsat: %15" PRId64 " %10.2f %% equiv solved",
522 stats.sweep_unsat_equivalences,
523 percent (stats.sweep_unsat_equivalences,
524 stats.sweep_solved_equivalences));
525 PRT (" unknown: %15" PRId64 " %10.2f %% equiv solved",
526 stats.sweep_unknown_equivalences,
527 percent (stats.sweep_unknown_equivalences,
528 stats.sweep_solved_equivalences));
529 PRT (" flip: %15" PRId64 " %10.2f per swept variable",
530 stats.sweep_flip_equivalences,
531 relative (stats.sweep_flip_equivalences, stats.sweep_variables));
532 PRT (" flipped: %15" PRId64 " %10.2f %% of equiv flip",
533 stats.sweep_flipped_equivalences,
534 percent (stats.sweep_flipped_equivalences,
535 stats.sweep_flip_equivalences));
536 PRT (" depth: %15" PRId64 " %10.2f per swept variable",
537 stats.sweep_depth,
538 relative (stats.sweep_depth, stats.sweep_variables));
539 PRT (" environment: %15" PRId64 " %10.2f per swept variable",
540 stats.sweep_environment,
541 relative (stats.sweep_environment, stats.sweep_variables));
542 PRT (" clauses: %15" PRId64 " %10.2f per swept variable",
543 stats.sweep_clauses,
544 relative (stats.sweep_clauses, stats.sweep_variables));
545 PRT (" completed: %15" PRId64 " %10.2f sweeps to complete",
546 stats.sweep_completed,
547 relative (stats.sweep, stats.sweep_completed));
548 }
549 if (all || stats.subsumed) {
550 PRT ("subsumed: %15" PRId64 " %10.2f %% of all clauses",
551 stats.subsumed, percent (stats.subsumed, stats.added.total));
552 PRT (" subsumephases: %15" PRId64 " %10.2f interval",
553 stats.subsumephases,
554 relative (stats.conflicts, stats.subsumephases));
555 PRT (" subsumerounds: %15" PRId64 " %10.2f per phase",
556 stats.subsumerounds,
557 relative (stats.subsumerounds, stats.subsumephases));
558 PRT (" deduplicated: %15" PRId64 " %10.2f %% per subsumed",
559 stats.deduplicated, percent (stats.deduplicated, stats.subsumed));
560 PRT (" transreds: %15" PRId64 " %10.2f interval",
561 stats.transreds, relative (stats.conflicts, stats.transreds));
562 PRT (" transitive: %15" PRId64 " %10.2f %% per subsumed",
563 stats.transitive, percent (stats.transitive, stats.subsumed));
564 PRT (" subirr: %15" PRId64 " %10.2f %% of subsumed",
565 stats.subirr, percent (stats.subirr, stats.subsumed));
566 PRT (" subred: %15" PRId64 " %10.2f %% of subsumed",
567 stats.subred, percent (stats.subred, stats.subsumed));
568 PRT (" subtried: %15" PRId64 " %10.2f tried per subsumed",
569 stats.subtried, relative (stats.subtried, stats.subsumed));
570 PRT (" subchecks: %15" PRId64 " %10.2f per tried",
571 stats.subchecks, relative (stats.subchecks, stats.subtried));
572 PRT (" subchecks2: %15" PRId64 " %10.2f %% per subcheck",
573 stats.subchecks2, percent (stats.subchecks2, stats.subchecks));
574 PRT (" elimotfsub: %15" PRId64 " %10.2f %% of subsumed",
575 stats.elimotfsub, percent (stats.elimotfsub, stats.subsumed));
576 PRT (" elimbwsub: %15" PRId64 " %10.2f %% of subsumed",
577 stats.elimbwsub, percent (stats.elimbwsub, stats.subsumed));
578 PRT (" eagersub: %15" PRId64 " %10.2f %% of subsumed",
579 stats.eagersub, percent (stats.eagersub, stats.subsumed));
580 PRT (" eagertried: %15" PRId64 " %10.2f tried per eagersub",
581 stats.eagertried, relative (stats.eagertried, stats.eagersub));
582 }
583 if (all || stats.strengthened) {
584 PRT ("strengthened: %15" PRId64 " %10.2f %% of all clauses",
585 stats.strengthened,
586 percent (stats.strengthened, stats.added.total));
587 PRT (" elimotfstr: %15" PRId64 " %10.2f %% of strengthened",
588 stats.elimotfstr, percent (stats.elimotfstr, stats.strengthened));
589 PRT (" elimbwstr: %15" PRId64 " %10.2f %% of strengthened",
590 stats.elimbwstr, percent (stats.elimbwstr, stats.strengthened));
591 }
592 if (all || stats.htrs) {
593 PRT ("ternary: %15" PRId64 " %10.2f %% of resolved",
594 stats.htrs, percent (stats.htrs, stats.ternres));
595 PRT (" phases: %15" PRId64 " %10.2f interval",
596 stats.ternary, relative (stats.conflicts, stats.ternary));
597 PRT (" htr3: %15" PRId64
598 " %10.2f %% ternary hyper ternres",
599 stats.htrs3, percent (stats.htrs3, stats.htrs));
600 PRT (" htr2: %15" PRId64 " %10.2f %% binary hyper ternres",
601 stats.htrs2, percent (stats.htrs2, stats.htrs));
602 }
603 PRT ("ticks: %15" PRId64 " %10.2f propagation", totalticks,
604 relative (totalticks, stats.propagations.search));
605 PRT (" searchticks: %15" PRId64 " %10.2f %% totalticks",
606 searchticks, percent (searchticks, totalticks));
607 PRT (" stableticks: %15" PRId64 " %10.2f %% searchticks",
608 stats.ticks.search[1], percent (stats.ticks.search[1], searchticks));
609 PRT (" unstableticks:%15" PRId64 " %10.2f %% searchticks",
610 stats.ticks.search[0], percent (stats.ticks.search[0], searchticks));
611 PRT (" inprobeticks: %15" PRId64 " %10.2f %% totalticks",
612 inprobeticks, percent (inprobeticks, totalticks));
613 PRT (" factorticks: %15" PRId64 " %10.2f %% searchticks",
614 stats.ticks.factor, percent (stats.ticks.factor, searchticks));
615 PRT (" probeticks: %15" PRId64 " %10.2f %% searchticks",
616 stats.ticks.probe, percent (stats.ticks.probe, searchticks));
617 PRT (" sweepticks: %15" PRId64 " %10.2f %% searchticks",
618 stats.ticks.sweep, percent (stats.ticks.sweep, searchticks));
619 PRT (" ternaryticks: %15" PRId64 " %10.2f %% searchticks",
620 stats.ticks.ternary, percent (stats.ticks.ternary, searchticks));
621 PRT (" vivifyticks: %15" PRId64 " %10.2f %% searchticks",
622 stats.ticks.vivify, percent (stats.ticks.vivify, searchticks));
623 if (all) {
624 PRT ("tier recomputed: %15" PRId64 " %10.2f interval",
625 stats.tierecomputed,
626 relative (stats.conflicts, stats.tierecomputed));
627 }
628 if (all || stats.ilbtriggers) {
629 PRT ("trail reuses: %15" PRId64 " %10.2f %% of incremental calls",
630 stats.ilbsuccess, percent (stats.ilbsuccess, stats.ilbtriggers));
631 PRT (" levels: %15" PRId64 " %10.2f per reuse",
632 stats.levelsreused,
633 relative (stats.levelsreused, stats.ilbsuccess));
634 PRT (" literals: %15" PRId64 " %10.2f per reuse",
635 stats.literalsreused,
636 relative (stats.literalsreused, stats.ilbsuccess));
637 PRT (" assumptions: %15" PRId64 " %10.2f per reuse",
638 stats.assumptionsreused,
639 relative (stats.assumptionsreused, stats.ilbsuccess));
640 }
641 if (all || vivified) {
642 PRT ("vivified: %15" PRId64 " %10.2f %% of all clauses",
643 vivified, percent (vivified, stats.added.total));
644 PRT (" vivifications: %15" PRId64 " %10.2f interval",
645 stats.vivifications,
646 relative (stats.conflicts, stats.vivifications));
647 PRT (" vivifychecks: %15" PRId64 " %10.2f %% per conflict",
648 stats.vivifychecks, percent (stats.vivifychecks, stats.conflicts));
649 PRT (" vivifysched: %15" PRId64 " %10.2f %% checks per scheduled",
650 stats.vivifysched,
651 percent (stats.vivifychecks, stats.vivifysched));
652 PRT (" vivifyunits: %15" PRId64 " %10.2f %% per vivify check",
653 stats.vivifyunits,
654 percent (stats.vivifyunits, stats.vivifychecks));
655 PRT (" vivifyinst: %15" PRId64 " %10.2f %% per vivify check",
656 stats.vivifyinst, percent (stats.vivifyinst, stats.vivifychecks));
657 PRT (" vivifysubs: %15" PRId64 " %10.2f %% per subsumed",
658 stats.vivifysubs, percent (stats.vivifysubs, stats.subsumed));
659 PRT (" vivifysubred: %15" PRId64 " %10.2f %% per subs",
660 stats.vivifysubred,
661 percent (stats.vivifysubred, stats.vivifysubs));
662 PRT (" vivifysubirr: %15" PRId64 " %10.2f %% per subs",
663 stats.vivifysubirr,
664 percent (stats.vivifysubirr, stats.vivifysubs));
665 PRT (" vivifystrs: %15" PRId64 " %10.2f %% per strengthened",
666 stats.vivifystrs, percent (stats.vivifystrs, stats.strengthened));
667 PRT (" vivifystrirr: %15" PRId64 " %10.2f %% per vivifystrs",
668 stats.vivifystrirr,
669 percent (stats.vivifystrirr, stats.vivifystrs));
670 PRT (" vivifystred1: %15" PRId64 " %10.2f %% per vivifystrs",
671 stats.vivifystred1,
672 percent (stats.vivifystred1, stats.vivifystrs));
673 PRT (" vivifystred2: %15" PRId64 " %10.2f %% per viviyfstrs",
674 stats.vivifystred2,
675 percent (stats.vivifystred2, stats.vivifystrs));
676 PRT (" vivifystred3: %15" PRId64 " %10.2f %% per vivifystrs",
677 stats.vivifystred3,
678 percent (stats.vivifystred3, stats.vivifystrs));
679 PRT (" vivifydemote: %15" PRId64 " %10.2f %% per vivifystrs",
680 stats.vivifydemote,
681 percent (stats.vivifydemote, stats.vivifystrs));
682 PRT (" vivifydecs: %15" PRId64 " %10.2f per checks",
683 stats.vivifydecs, relative (stats.vivifydecs, stats.vivifychecks));
684 PRT (" vivifyreused: %15" PRId64 " %10.2f %% per decision",
685 stats.vivifyreused,
686 percent (stats.vivifyreused, stats.vivifydecs));
687 }
688 if (all || stats.walk.count) {
689 PRT ("walked: %15" PRId64 " %10.2f interval",
690 stats.walk.count, relative (stats.conflicts, stats.walk.count));
691#ifndef CADICAL_QUIET
692 if (internal->profiles.walk.value > 0)
693 PRT (" flips: %15" PRId64 " %10.2f M per second",
694 stats.walk.flips,
695 relative (1e-6 * stats.walk.flips,
696 internal->profiles.walk.value));
697 else
698#endif
699 PRT (" flips: %15" PRId64 " %10.2f per walk",
700 stats.walk.flips, relative (stats.walk.flips, stats.walk.count));
701 if (stats.walk.minimum < LONG_MAX)
702 PRT (" minimum: %15" PRId64 " %10.2f %% clauses",
703 stats.walk.minimum,
704 percent (stats.walk.minimum, stats.added.irredundant));
705 PRT (" broken: %15" PRId64 " %10.2f per flip",
706 stats.walk.broken, relative (stats.walk.broken, stats.walk.flips));
707 }
708 if (all || stats.weakened) {
709 PRT ("weakened: %15" PRId64 " %10.2f average size",
710 stats.weakened, relative (stats.weakenedlen, stats.weakened));
711 PRT (" extensions: %15" PRId64 " %10.2f interval",
712 stats.extensions, relative (stats.conflicts, stats.extensions));
713 PRT (" flipped: %15" PRId64 " %10.2f per weakened",
714 stats.extended, relative (stats.extended, stats.weakened));
715 }
716
717 if (all || stats.congruence.gates) {
718 PRT ("congruence: %15" PRId64 " %10.2f interval",
719 stats.congruence.rounds,
720 relative (stats.conflicts, stats.congruence.rounds));
721 PRT (" units: %15" PRId64 " %10.2f per congruent",
722 stats.congruence.units,
723 relative (stats.congruence.units, stats.congruence.congruent));
724 PRT (" cong-and: %15" PRId64 " %10.2f per found gates",
725 stats.congruence.ands,
726 relative (stats.congruence.ands, stats.congruence.gates));
727 PRT (" cong-ite: %15" PRId64 " %10.2f per found gates",
728 stats.congruence.ites,
729 relative (stats.congruence.ites, stats.congruence.gates));
730 PRT (" cong-xor: %15" PRId64 " %10.2f per found gates",
731 stats.congruence.xors,
732 relative (stats.congruence.xors, stats.congruence.gates));
733 PRT (" congruent: %15" PRId64 " %10.2f per round",
734 stats.congruence.congruent,
735 relative (stats.congruence.rounds, stats.congruence.congruent));
736 PRT (" unaries: %15" PRId64 " %10.2f per round",
737 stats.congruence.unaries,
738 relative (stats.congruence.rounds, stats.congruence.unaries));
739 PRT (" rewri.-ands: %15" PRId64 " %10.2f per round",
740 stats.congruence.rewritten_ands,
741 relative (stats.congruence.rounds,
742 stats.congruence.rewritten_ands));
743 PRT (" subsumed: %15" PRId64 " %10.2f per round",
744 stats.congruence.subsumed,
745 relative (stats.congruence.rounds, stats.congruence.subsumed));
746 }
747
748 LINE ();
749 MSG ("%sseconds are measured in %s time for solving%s",
750 tout.magenta_code (), internal->opts.realtime ? "real" : "process",
751 tout.normal_code ());
752
753#endif // ifndef CADICAL_QUIET
754}
755
756void Internal::print_resource_usage () {
757#ifndef CADICAL_QUIET
758 SECTION ("resources");
759 uint64_t m = maximum_resident_set_size ();
760 MSG ("total process time since initialization: %12.2f seconds",
761 internal->process_time ());
762 MSG ("total real time since initialization: %12.2f seconds",
763 internal->real_time ());
764 MSG ("maximum resident set size of process: %12.2f MB",
765 m / (double) (1l << 20));
766#endif
767}
768
769/*------------------------------------------------------------------------*/
770
771void Checker::print_stats () {
772
773 if (!stats.added && !stats.deleted)
774 return;
775
776 SECTION ("checker statistics");
777
778 MSG ("checks: %15" PRId64 "", stats.checks);
779 MSG ("assumptions: %15" PRId64 " %10.2f per check",
780 stats.assumptions, relative (stats.assumptions, stats.checks));
781 MSG ("propagations: %15" PRId64 " %10.2f per check",
782 stats.propagations, relative (stats.propagations, stats.checks));
783 MSG ("original: %15" PRId64 " %10.2f %% of all clauses",
784 stats.original, percent (stats.original, stats.added));
785 MSG ("derived: %15" PRId64 " %10.2f %% of all clauses",
786 stats.derived, percent (stats.derived, stats.added));
787 MSG ("deleted: %15" PRId64 " %10.2f %% of all clauses",
788 stats.deleted, percent (stats.deleted, stats.added));
789 MSG ("insertions: %15" PRId64 " %10.2f %% of all clauses",
790 stats.insertions, percent (stats.insertions, stats.added));
791 MSG ("collections: %15" PRId64 " %10.2f deleted per collection",
792 stats.collections, relative (stats.collections, stats.deleted));
793 MSG ("collisions: %15" PRId64 " %10.2f per search",
794 stats.collisions, relative (stats.collisions, stats.searches));
795 MSG ("searches: %15" PRId64 "", stats.searches);
796 MSG ("units: %15" PRId64 "", stats.units);
797}
798
799void LratChecker::print_stats () {
800
801 if (!stats.added && !stats.deleted)
802 return;
803
804 SECTION ("lrat checker statistics");
805
806 MSG ("checks: %15" PRId64 "", stats.checks);
807 MSG ("insertions: %15" PRId64 " %10.2f %% of all clauses",
808 stats.insertions, percent (stats.insertions, stats.added));
809 MSG ("original: %15" PRId64 " %10.2f %% of all clauses",
810 stats.original, percent (stats.original, stats.added));
811 MSG ("derived: %15" PRId64 " %10.2f %% of all clauses",
812 stats.derived, percent (stats.derived, stats.added));
813 MSG ("deleted: %15" PRId64 " %10.2f %% of all clauses",
814 stats.deleted, percent (stats.deleted, stats.added));
815 MSG ("finalized: %15" PRId64 " %10.2f %% of all clauses",
816 stats.finalized, percent (stats.finalized, stats.added));
817 MSG ("collections: %15" PRId64 " %10.2f deleted per collection",
818 stats.collections, relative (stats.collections, stats.deleted));
819 MSG ("collisions: %15" PRId64 " %10.2f per search",
820 stats.collisions, relative (stats.collisions, stats.searches));
821 MSG ("searches: %15" PRId64 "", stats.searches);
822}
823
824} // namespace CaDiCaL
825
826ABC_NAMESPACE_IMPL_END
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
PRT
#define PRT(FMT,...)
Definition cadical_stats.cpp:24
CaDiCaL::Checker::print_stats
void print_stats() override
Definition cadical_stats.cpp:771
CaDiCaL::LratChecker::print_stats
void print_stats() override
Definition cadical_stats.cpp:799
MSG
#define MSG(...)
Definition message.hpp:49
LINE
#define LINE()
Definition message.hpp:46
SECTION
#define SECTION(...)
Definition message.hpp:55
CaDiCaL::relative
double relative(double a, double b)
Definition util.hpp:20
CaDiCaL::absolute_process_time
double absolute_process_time()
Definition cadical_resources.cpp:89
CaDiCaL::maximum_resident_set_size
uint64_t maximum_resident_set_size()
Definition cadical_resources.cpp:133
CaDiCaL::absolute_real_time
double absolute_real_time()
Definition cadical_resources.cpp:78
CaDiCaL::tout
Terminal tout(stdout)
Definition terminal.hpp:97
CaDiCaL::percent
double percent(double a, double b)
Definition util.hpp:21
CaDiCaL::Internal::internal
Internal * internal
Definition internal.hpp:311
CaDiCaL::Stats::echeck_call
int64_t echeck_call
Definition stats.hpp:60
CaDiCaL::Stats::sweep_clauses
int64_t sweep_clauses
Definition stats.hpp:289
CaDiCaL::Stats::sweep_unsat_backbone
int64_t sweep_unsat_backbone
Definition stats.hpp:273
CaDiCaL::Stats::literalsreused
int64_t literalsreused
Definition stats.hpp:322
CaDiCaL::Stats::search
int64_t search
Definition stats.hpp:29
CaDiCaL::Stats::sweep_completed
int64_t sweep_completed
Definition stats.hpp:283
CaDiCaL::Stats::random
int64_t random
Definition stats.hpp:119
CaDiCaL::Stats::count
int64_t count
Definition stats.hpp:96
CaDiCaL::Stats::eagersub
int64_t eagersub
Definition stats.hpp:209
CaDiCaL::Stats::reductions
int64_t reductions
Definition stats.hpp:157
CaDiCaL::Stats::hbreds
int64_t hbreds
Definition stats.hpp:165
CaDiCaL::Stats::cover
int64_t cover
Definition stats.hpp:26
CaDiCaL::Stats::sweep_unknown_backbone
int64_t sweep_unknown_backbone
Definition stats.hpp:274
CaDiCaL::Stats::elearned
int64_t elearned
Definition stats.hpp:54
CaDiCaL::Stats::vivifysubs
int64_t vivifysubs
Definition stats.hpp:238
CaDiCaL::Stats::sweep
int64_t sweep
Definition stats.hpp:39
CaDiCaL::Stats::stabconflicts
int64_t stabconflicts
Definition stats.hpp:142
CaDiCaL::Stats::vivify
int64_t vivify
Definition stats.hpp:31
CaDiCaL::Stats::instantiated
int64_t instantiated
Definition stats.hpp:168
CaDiCaL::Stats::failed
int64_t failed
Definition stats.hpp:298
CaDiCaL::Stats::ticks
struct CaDiCaL::Stats::@061276032307236342017375135353356007315031134117 ticks
CaDiCaL::Stats::blockcands
int64_t blockcands
Definition stats.hpp:305
CaDiCaL::Stats::vivifystrirr
int64_t vivifystrirr
Definition stats.hpp:242
CaDiCaL::Stats::chrono
int64_t chrono
Definition stats.hpp:149
CaDiCaL::Stats::flush
struct CaDiCaL::Stats::@237104076152062225360176065350072343126300147267 flush
CaDiCaL::Stats::rounds
int64_t rounds
Definition stats.hpp:352
CaDiCaL::Stats::forward
struct CaDiCaL::Stats::@006041325075001155043001213057243236244366226026::@056227323115101117026301242125007064165116265217 forward
CaDiCaL::Stats::sweep_unsat
int64_t sweep_unsat
Definition stats.hpp:286
CaDiCaL::Stats::definitions_checked
int64_t definitions_checked
Definition stats.hpp:183
CaDiCaL::Stats::sweep_sat_equivalences
int64_t sweep_sat_equivalences
Definition stats.hpp:277
CaDiCaL::Stats::eprop_expl
int64_t eprop_expl
Definition stats.hpp:50
CaDiCaL::Stats::literals_unfactored
int64_t literals_unfactored
Definition stats.hpp:195
CaDiCaL::Stats::rescored
int64_t rescored
Definition stats.hpp:144
CaDiCaL::Stats::subchecks2
int64_t subchecks2
Definition stats.hpp:203
CaDiCaL::Stats::vivifystrs
int64_t vivifystrs
Definition stats.hpp:241
CaDiCaL::Stats::horn
struct CaDiCaL::Stats::@006041325075001155043001213057243236244366226026::@212260103163155063110346373325077304202321014304 horn
CaDiCaL::Stats::original
int64_t original
Definition stats.hpp:118
CaDiCaL::Stats::elimbwsub
int64_t elimbwsub
Definition stats.hpp:225
CaDiCaL::Stats::constant
struct CaDiCaL::Stats::@006041325075001155043001213057243236244366226026::@056227323115101117026301242125007064165116265217 constant
CaDiCaL::Stats::shrunken
int64_t shrunken
Definition stats.hpp:257
CaDiCaL::Stats::best
int64_t best
Definition stats.hpp:115
CaDiCaL::Stats::vivifystred2
int64_t vivifystred2
Definition stats.hpp:244
CaDiCaL::Stats::sweep_depth
int64_t sweep_depth
Definition stats.hpp:287
CaDiCaL::Stats::propagations
struct CaDiCaL::Stats::@050077033200170237247264105345125030032067160331 propagations
CaDiCaL::Stats::condautrem
int64_t condautrem
Definition stats.hpp:68
CaDiCaL::Stats::factor
int64_t factor
Definition stats.hpp:37
CaDiCaL::Stats::all
struct CaDiCaL::Stats::@075300034234301162006241302064117220275364173077 all
CaDiCaL::Stats::htrs2
int64_t htrs2
Definition stats.hpp:230
CaDiCaL::Stats::sweep_environment
int64_t sweep_environment
Definition stats.hpp:288
CaDiCaL::Stats::ext_prop
struct CaDiCaL::Stats::@131073373030174132251116003114050064203351146304 ext_prop
CaDiCaL::Stats::backward
struct CaDiCaL::Stats::@006041325075001155043001213057243236244366226026::@056227323115101117026301242125007064165116265217 backward
CaDiCaL::Stats::definition_units
int64_t definition_units
Definition stats.hpp:185
CaDiCaL::Stats::hyper
int64_t hyper
Definition stats.hpp:133
CaDiCaL::Stats::decompositions
int64_t decompositions
Definition stats.hpp:232
CaDiCaL::Stats::eliminated_def
int64_t eliminated_def
Definition stats.hpp:180
CaDiCaL::Stats::sweep_flipped_backbone
int64_t sweep_flipped_backbone
Definition stats.hpp:270
CaDiCaL::Stats::sweep_solved_equivalences
int64_t sweep_solved_equivalences
Definition stats.hpp:280
CaDiCaL::Stats::blockpured
int64_t blockpured
Definition stats.hpp:306
CaDiCaL::Stats::units
int64_t units
Definition stats.hpp:292
CaDiCaL::Stats::used
std::vector< std::vector< uint64_t > > used
Definition stats.hpp:343
CaDiCaL::Stats::conditionings
int64_t conditionings
Definition stats.hpp:74
CaDiCaL::Stats::transredunits
int64_t transredunits
Definition stats.hpp:301
CaDiCaL::Stats::reactivated
int64_t reactivated
Definition stats.hpp:314
CaDiCaL::Stats::reduced
int64_t reduced
Definition stats.hpp:158
CaDiCaL::Stats::sweep_unsat_equivalences
int64_t sweep_unsat_equivalences
Definition stats.hpp:278
CaDiCaL::Stats::elimands
int64_t elimands
Definition stats.hpp:222
CaDiCaL::Stats::literals_factored
int64_t literals_factored
Definition stats.hpp:193
CaDiCaL::Stats::lucky
struct CaDiCaL::Stats::@006041325075001155043001213057243236244366226026 lucky
CaDiCaL::Stats::sweep_solved_backbone
int64_t sweep_solved_backbone
Definition stats.hpp:271
CaDiCaL::Stats::restoredlits
int64_t restoredlits
Definition stats.hpp:315
CaDiCaL::Stats::flipped
int64_t flipped
Definition stats.hpp:116
CaDiCaL::Stats::ext_cb
int64_t ext_cb
Definition stats.hpp:45
CaDiCaL::Stats::xors
int64_t xors
Definition stats.hpp:349
CaDiCaL::Stats::subsumephases
int64_t subsumephases
Definition stats.hpp:207
CaDiCaL::Stats::internal
Internal * internal
Definition stats.hpp:18
CaDiCaL::Stats::sweep_equivalences
int64_t sweep_equivalences
Definition stats.hpp:281
CaDiCaL::Stats::fasteliminated
int64_t fasteliminated
Definition stats.hpp:329
CaDiCaL::Stats::vivifications
int64_t vivifications
Definition stats.hpp:233
CaDiCaL::Stats::rewritten_ands
int64_t rewritten_ands
Definition stats.hpp:355
CaDiCaL::Stats::bumped
int64_t bumped
Definition stats.hpp:154
CaDiCaL::Stats::rephased
struct CaDiCaL::Stats::@246203077277062075200175215017131147270334133037 rephased
CaDiCaL::Stats::extended
int64_t extended
Definition stats.hpp:309
CaDiCaL::Stats::collections
int64_t collections
Definition stats.hpp:162
CaDiCaL::Stats::substituted
int64_t substituted
Definition stats.hpp:330
CaDiCaL::Stats::condprops
int64_t condprops
Definition stats.hpp:75
CaDiCaL::Stats::otfs
struct CaDiCaL::Stats::@074136255052016312214346246351114007302142377037 otfs
CaDiCaL::Stats::blockres
int64_t blockres
Definition stats.hpp:304
CaDiCaL::Stats::restartstable
int64_t restartstable
Definition stats.hpp:140
CaDiCaL::Stats::elimrestried
int64_t elimrestried
Definition stats.hpp:212
CaDiCaL::Stats::condcondrem
int64_t condcondrem
Definition stats.hpp:71
CaDiCaL::Stats::htrs3
int64_t htrs3
Definition stats.hpp:231
CaDiCaL::Stats::sweep_flip_equivalences
int64_t sweep_flip_equivalences
Definition stats.hpp:275
CaDiCaL::Stats::blocked
int64_t blocked
Definition stats.hpp:98
CaDiCaL::Stats::subsumed
int64_t subsumed
Definition stats.hpp:170
CaDiCaL::Stats::condassrem
int64_t condassrem
Definition stats.hpp:65
CaDiCaL::Stats::probed
int64_t probed
Definition stats.hpp:297
CaDiCaL::Stats::elimphases
int64_t elimphases
Definition stats.hpp:215
CaDiCaL::Stats::subirr
int64_t subirr
Definition stats.hpp:199
CaDiCaL::Stats::pure
int64_t pure
Definition stats.hpp:331
CaDiCaL::Stats::learned
int64_t learned
Definition stats.hpp:132
CaDiCaL::Stats::sweep_flip_backbone
int64_t sweep_flip_backbone
Definition stats.hpp:268
CaDiCaL::Stats::succeeded
int64_t succeeded
Definition stats.hpp:104
CaDiCaL::Stats::vivifychecks
int64_t vivifychecks
Definition stats.hpp:234
CaDiCaL::Stats::ternary
int64_t ternary
Definition stats.hpp:40
CaDiCaL::Stats::deduplicated
int64_t deduplicated
Definition stats.hpp:171
CaDiCaL::Stats::ilbsuccess
int64_t ilbsuccess
Definition stats.hpp:320
CaDiCaL::Stats::levelsreused
int64_t levelsreused
Definition stats.hpp:321
CaDiCaL::Stats::fixed
int64_t fixed
Definition stats.hpp:327
CaDiCaL::Stats::promoted2
int64_t promoted2
Definition stats.hpp:153
CaDiCaL::Stats::eprop_call
int64_t eprop_call
Definition stats.hpp:46
CaDiCaL::Stats::reusedstable
int64_t reusedstable
Definition stats.hpp:147
CaDiCaL::Stats::vivifyinst
int64_t vivifyinst
Definition stats.hpp:248
CaDiCaL::Stats::congruent
int64_t congruent
Definition stats.hpp:351
CaDiCaL::Stats::compacts
int64_t compacts
Definition stats.hpp:136
CaDiCaL::Stats::walk
int64_t walk
Definition stats.hpp:32
CaDiCaL::Stats::elearn_call
int64_t elearn_call
Definition stats.hpp:52
CaDiCaL::Stats::gates
int64_t gates
Definition stats.hpp:346
CaDiCaL::Stats::elearn_prop
int64_t elearn_prop
Definition stats.hpp:56
CaDiCaL::Stats::conditioned
int64_t conditioned
Definition stats.hpp:73
CaDiCaL::Stats::stabphases
int64_t stabphases
Definition stats.hpp:141
CaDiCaL::Stats::probefailed
int64_t probefailed
Definition stats.hpp:300
CaDiCaL::Stats::promoted1
int64_t promoted1
Definition stats.hpp:152
CaDiCaL::Stats::condassinit
int64_t condassinit
Definition stats.hpp:63
CaDiCaL::Stats::searched
int64_t searched
Definition stats.hpp:156
CaDiCaL::Stats::condautinit
int64_t condautinit
Definition stats.hpp:67
CaDiCaL::Stats::vivifysubred
int64_t vivifysubred
Definition stats.hpp:239
CaDiCaL::Stats::elimequivs
int64_t elimequivs
Definition stats.hpp:221
CaDiCaL::Stats::decisions
int64_t decisions
Definition stats.hpp:23
CaDiCaL::Stats::inprobingphases
int64_t inprobingphases
Definition stats.hpp:294
CaDiCaL::Stats::vivifystred1
int64_t vivifystred1
Definition stats.hpp:243
CaDiCaL::Stats::elimbwstr
int64_t elimbwstr
Definition stats.hpp:226
CaDiCaL::Stats::inprobesuccess
int64_t inprobesuccess
Definition stats.hpp:296
CaDiCaL::Stats::recomputed
int64_t recomputed
Definition stats.hpp:155
CaDiCaL::Stats::sweep_sat
int64_t sweep_sat
Definition stats.hpp:285
CaDiCaL::Stats::subtried
int64_t subtried
Definition stats.hpp:201
CaDiCaL::Stats::added
struct CaDiCaL::Stats::@036153126312240145270023376176313373126261335272 added
CaDiCaL::Stats::eprop_conf
int64_t eprop_conf
Definition stats.hpp:48
CaDiCaL::Stats::clauses_unfactored
int64_t clauses_unfactored
Definition stats.hpp:194
CaDiCaL::Stats::vivifysched
int64_t vivifysched
Definition stats.hpp:237
CaDiCaL::Stats::elimotfsub
int64_t elimotfsub
Definition stats.hpp:204
CaDiCaL::Stats::restartlevels
int64_t restartlevels
Definition stats.hpp:139
CaDiCaL::Stats::vivifysubirr
int64_t vivifysubirr
Definition stats.hpp:240
CaDiCaL::Stats::probingrounds
int64_t probingrounds
Definition stats.hpp:295
CaDiCaL::Stats::one
int64_t one
Definition stats.hpp:106
CaDiCaL::Stats::elimgates
int64_t elimgates
Definition stats.hpp:220
CaDiCaL::Stats::vivifydemote
int64_t vivifydemote
Definition stats.hpp:249
CaDiCaL::Stats::eliminated_equi
int64_t eliminated_equi
Definition stats.hpp:175
CaDiCaL::Stats::vivifystred3
int64_t vivifystred3
Definition stats.hpp:245
CaDiCaL::Stats::hbrsubs
int64_t hbrsubs
Definition stats.hpp:166
CaDiCaL::Stats::vivifyunits
int64_t vivifyunits
Definition stats.hpp:246
CaDiCaL::Stats::hbrs
int64_t hbrs
Definition stats.hpp:163
CaDiCaL::Stats::ites
int64_t ites
Definition stats.hpp:348
CaDiCaL::Stats::negative
int64_t negative
Definition stats.hpp:109
CaDiCaL::Stats::eliminated_ite
int64_t eliminated_ite
Definition stats.hpp:178
CaDiCaL::Stats::print
void print(Internal *)
Definition cadical_stats.cpp:33
CaDiCaL::Stats::inverted
int64_t inverted
Definition stats.hpp:117
CaDiCaL::Stats::sweep_flipped_equivalences
int64_t sweep_flipped_equivalences
Definition stats.hpp:276
CaDiCaL::Stats::elearn_conf
int64_t elearn_conf
Definition stats.hpp:58
CaDiCaL::Stats::weakenedlen
int64_t weakenedlen
Definition stats.hpp:311
CaDiCaL::Stats::positive
int64_t positive
Definition stats.hpp:109
CaDiCaL::Stats::factored
int64_t factored
Definition stats.hpp:189
CaDiCaL::Stats::sweep_units
int64_t sweep_units
Definition stats.hpp:267
CaDiCaL::Stats::reusedlevels
int64_t reusedlevels
Definition stats.hpp:146
CaDiCaL::Stats::assumptionsreused
int64_t assumptionsreused
Definition stats.hpp:323
CaDiCaL::Stats::instried
int64_t instried
Definition stats.hpp:167
CaDiCaL::Stats::condassvars
int64_t condassvars
Definition stats.hpp:66
CaDiCaL::Stats::weakened
int64_t weakened
Definition stats.hpp:310
CaDiCaL::Stats::sweep_fixed_backbone
int64_t sweep_fixed_backbone
Definition stats.hpp:269
CaDiCaL::Stats::vivifyreused
int64_t vivifyreused
Definition stats.hpp:236
CaDiCaL::Stats::reduced_prct
int64_t reduced_prct
Definition stats.hpp:160
CaDiCaL::Stats::elimxors
int64_t elimxors
Definition stats.hpp:224
CaDiCaL::Stats::factor_added
int64_t factor_added
Definition stats.hpp:190
CaDiCaL::Stats::instrounds
int64_t instrounds
Definition stats.hpp:169
CaDiCaL::Stats::condcands
int64_t condcands
Definition stats.hpp:69
CaDiCaL::Stats::transitive
int64_t transitive
Definition stats.hpp:251
CaDiCaL::Stats::subsumerounds
int64_t subsumerounds
Definition stats.hpp:206
CaDiCaL::Stats::unaries
int64_t unaries
Definition stats.hpp:354
CaDiCaL::Stats::elimotfstr
int64_t elimotfstr
Definition stats.hpp:197
CaDiCaL::Stats::zero
int64_t zero
Definition stats.hpp:106
CaDiCaL::Stats::blockings
int64_t blockings
Definition stats.hpp:302
CaDiCaL::Stats::subred
int64_t subred
Definition stats.hpp:200
CaDiCaL::Stats::total
int64_t total
Definition stats.hpp:86
CaDiCaL::Stats::restarts
int64_t restarts
Definition stats.hpp:138
CaDiCaL::Stats::restorations
int64_t restorations
Definition stats.hpp:312
CaDiCaL::Stats::reused
int64_t reused
Definition stats.hpp:145
CaDiCaL::Stats::elimres
int64_t elimres
Definition stats.hpp:211
CaDiCaL::Stats::improvedglue
int64_t improvedglue
Definition stats.hpp:151
CaDiCaL::Stats::binaries
int64_t binaries
Definition stats.hpp:293
CaDiCaL::Stats::definitions_extracted
int64_t definitions_extracted
Definition stats.hpp:184
CaDiCaL::Stats::congruence
struct CaDiCaL::Stats::@024120302142116110306311132366150123164053300365 congruence
CaDiCaL::Stats::hbrsizes
int64_t hbrsizes
Definition stats.hpp:164
CaDiCaL::Stats::condassirem
int64_t condassirem
Definition stats.hpp:64
CaDiCaL::Stats::elimites
int64_t elimites
Definition stats.hpp:223
CaDiCaL::Stats::tried
int64_t tried
Definition stats.hpp:103
CaDiCaL::Stats::sweep_sat_backbone
int64_t sweep_sat_backbone
Definition stats.hpp:272
CaDiCaL::Stats::ternres
int64_t ternres
Definition stats.hpp:228
CaDiCaL::Stats::transreds
int64_t transreds
Definition stats.hpp:250
CaDiCaL::Stats::eagertried
int64_t eagertried
Definition stats.hpp:208
CaDiCaL::Stats::minimized
int64_t minimized
Definition stats.hpp:256
CaDiCaL::Stats::extensions
int64_t extensions
Definition stats.hpp:308
CaDiCaL::Stats::vars
int64_t vars
Definition stats.hpp:20
CaDiCaL::Stats::restored
int64_t restored
Definition stats.hpp:313
CaDiCaL::Stats::strengthened
int64_t strengthened
Definition stats.hpp:173
CaDiCaL::Stats::eliminated
int64_t eliminated
Definition stats.hpp:328
CaDiCaL::Stats::elimtried
int64_t elimtried
Definition stats.hpp:218
CaDiCaL::Stats::minishrunken
int64_t minishrunken
Definition stats.hpp:258
CaDiCaL::Stats::htrs
int64_t htrs
Definition stats.hpp:229
CaDiCaL::Stats::eprop_prop
int64_t eprop_prop
Definition stats.hpp:47
CaDiCaL::Stats::transred
int64_t transred
Definition stats.hpp:30
CaDiCaL::Stats::sweep_unknown_equivalences
int64_t sweep_unknown_equivalences
Definition stats.hpp:279
CaDiCaL::Stats::eliminated_and
int64_t eliminated_and
Definition stats.hpp:177
CaDiCaL::Stats::probe
int64_t probe
Definition stats.hpp:28
CaDiCaL::Stats::ands
int64_t ands
Definition stats.hpp:347
CaDiCaL::Stats::backtracks
int64_t backtracks
Definition stats.hpp:150
CaDiCaL::Stats::conflicts
int64_t conflicts
Definition stats.hpp:22
CaDiCaL::Stats::irredundant
int64_t irredundant
Definition stats.hpp:88
CaDiCaL::Stats::elimrounds
int64_t elimrounds
Definition stats.hpp:214
CaDiCaL::Stats::time
struct CaDiCaL::Stats::@004320020100036166131020046067276224372273042350 time
CaDiCaL::Stats::ilbtriggers
int64_t ilbtriggers
Definition stats.hpp:319
CaDiCaL::Stats::sweep_solved
int64_t sweep_solved
Definition stats.hpp:284
CaDiCaL::Stats::sweep_variables
int64_t sweep_variables
Definition stats.hpp:282
CaDiCaL::Stats::eliminated_xor
int64_t eliminated_xor
Definition stats.hpp:179
CaDiCaL::Stats::tierecomputed
int64_t tierecomputed
Definition stats.hpp:324
CaDiCaL::Stats::condcondinit
int64_t condcondinit
Definition stats.hpp:70
CaDiCaL::Stats::reduced_sqrt
int64_t reduced_sqrt
Definition stats.hpp:159
CaDiCaL::Stats::subchecks
int64_t subchecks
Definition stats.hpp:202
CaDiCaL::Stats::elimsubst
int64_t elimsubst
Definition stats.hpp:219
CaDiCaL::Stats::vivifydecs
int64_t vivifydecs
Definition stats.hpp:235