ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
statistics.c
Go to the documentation of this file.
1#include "global.h"
2
3#if !defined(KISSAT_QUIET) || !defined(KISSAT_NDEBUG)
4#include "internal.h"
5#endif
6
7#ifndef KISSAT_QUIET
8
9#include "resources.h"
10#include "tiers.h"
11#include "utilities.h"
12
13#include <inttypes.h>
14#include <stdbool.h>
15#include <stdio.h>
16#include <string.h>
17
18ABC_NAMESPACE_IMPL_START
19
20void kissat_print_glue_usage (kissat *solver) {
21 const int64_t stable = solver->statistics.clauses_used_stable;
22 const int64_t focused = solver->statistics.clauses_used_focused;
23 if (!stable && !focused)
24 printf ("%sno clauses used at all\n", solver->prefix);
25 else {
26 if (focused)
27 kissat_print_tier_usage_statistics (solver, false);
28 if (focused && stable)
29 printf ("c\n");
30 if (stable)
31 kissat_print_tier_usage_statistics (solver, true);
32 }
33 fflush (stdout);
34}
35
36// clang-format off
37
38void
39kissat_statistics_print (kissat * solver, bool verbose)
40{
41 statistics *statistics = &solver->statistics;
42
43 const double time = kissat_process_time ();
44 size_t variables = solver->statistics.variables_original;
45#ifdef METRICS
46 const double rss = kissat_maximum_resident_set_size ();
47#endif
48
49/*------------------------------------------------------------------------*/
50
51#define RELATIVE(FIRST,SECOND) \
52 kissat_average (statistics->FIRST, statistics->SECOND)
53
54/*------------------------------------------------------------------------*/
55
56#define CONF_INT(NAME) \
57 RELATIVE (conflicts, NAME)
58
59#define SWEEPS_PER_COMPLETED(NAME) \
60 RELATIVE (sweep, NAME)
61
62#define NO_SECONDARY(NAME) \
63 0
64
65/*------------------------------------------------------------------------*/
66
67#define PER_BACKBONE(NAME) \
68 RELATIVE (NAME, backbone_computations)
69
70#define PER_BACKBONE_UNIT(NAME) \
71 RELATIVE (NAME, backbone_units)
72
73#define PER_CLOSURE(NAME) \
74 RELATIVE(NAME, closures)
75
76#define PER_CLS_ADDED(NAME) \
77 RELATIVE (NAME, clauses_added)
78
79#define PER_CLS_FACTORED(NAME) \
80 RELATIVE (NAME, clauses_factored)
81
82#define PER_CLS_LEARNED(NAME) \
83 RELATIVE (NAME, clauses_learned)
84
85#define PER_CLS_UNFACTORED(NAME) \
86 RELATIVE (NAME, clauses_unfactored)
87
88#define PER_CONFLICT(NAME) \
89 RELATIVE (NAME, conflicts)
90
91#define PER_CONGRANDS(NAME) \
92 RELATIVE (NAME, congruent_gates_ands)
93
94#define PER_CONGRGATES(NAME) \
95 RELATIVE (NAME, congruent_gates)
96
97#define PER_CONGRITES(NAME) \
98 RELATIVE (NAME, congruent_gates_ites)
99
100#define PER_CONGRLOOKUP(NAME) \
101 RELATIVE (NAME, congruent_lookups)
102
103#define PER_CONGRXORS(NAME) \
104 RELATIVE (NAME, congruent_gates_xors)
105
106#define PER_FIXED(NAME) \
107 RELATIVE (NAME, units)
108
109#ifndef STATISTICS
110#define PER_FLIPPED(NAME) \
111 -1
112#else
113#define PER_FLIPPED(NAME) \
114 RELATIVE (NAME, flipped)
115#endif
116
117#define PER_FORWARD_CHECK(NAME) \
118 RELATIVE (NAME, forward_checks)
119
120#define PER_KITTEN_PROP(NAME) \
121 RELATIVE (NAME, kitten_propagations)
122
123#define PER_KITTEN_SOLVED(NAME) \
124 RELATIVE (NAME, kitten_solved)
125
126#define PER_PROPAGATION(NAME) \
127 RELATIVE (NAME, propagations)
128
129#define PER_RESTART(NAME) \
130 RELATIVE (NAME, restarts)
131
132#define PER_SECOND(NAME) \
133 kissat_average (statistics->NAME, time)
134
135#define PER_SWEEP_VARIABLES(NAME) \
136 kissat_average (statistics->NAME, statistics->sweep_variables)
137
138#define PER_VARIABLE(NAME) \
139 kissat_average (statistics->NAME, variables)
140
141#define PER_VIVIFICATION(NAME) \
142 RELATIVE (NAME, vivifications)
143
144#define PER_VIVIFY_CHECK(NAME) \
145 RELATIVE (NAME, vivify_checks)
146
147#if 0 //ndef STATISTICS
148#define PER_WALKS(NAME) \
149 -1
150#else
151#define PER_WALKS(NAME) \
152 RELATIVE (NAME, walks)
153#endif
154
155/*------------------------------------------------------------------------*/
156
157#define PERCENT(FIRST,SECOND) \
158 kissat_percent (statistics->FIRST, statistics->SECOND)
159
160/*------------------------------------------------------------------------*/
161
162#define PCNT_ARENA_RESIZED(NAME) \
163 PERCENT (NAME, arena_resized)
164
165#define PCNT_CLS_ADDED(NAME) \
166 PERCENT (NAME, clauses_added)
167
168#define PCNT_CLS_IMPROVED(NAME) \
169 PERCENT (NAME, clauses_improved)
170
171#define PCNT_CLS_IMPROVED(NAME) \
172 PERCENT (NAME, clauses_improved)
173
174#define PCNT_CLS_FACTORED(NAME) \
175 PERCENT (NAME, clauses_factored)
176
177#define PCNT_CLS_LEARNED(NAME) \
178 PERCENT (NAME, clauses_learned)
179
180#define PCNT_CLS_ORIGINAL(NAME) \
181 PERCENT (NAME, clauses_original)
182
183#define PCNT_CLS_REDUCED(NAME) \
184 PERCENT (NAME, clauses_reduced)
185
186#define PCNT_CLS_USED(NAME) \
187 PERCENT (NAME, clauses_used)
188
189#define PCNT_COLLECTIONS(NAME) \
190 PERCENT (NAME, garbage_collections)
191
192#define PCNT_CONFLICTS(NAME) \
193 PERCENT (NAME, conflicts)
194
195#define PCNT_CONGRCOLS(NAME) \
196 PERCENT (NAME, congruent_collisions)
197
198#define PCNT_CONGRGATES(NAME) \
199 PERCENT (NAME, congruent_gates)
200
201#define PCNT_CONGRLOOKUP(NAME) \
202 PERCENT (NAME, congruent_lookups)
203
204#define PCNT_CONGRMATCHED(NAME) \
205 PERCENT (NAME, congruent_matched)
206
207#define PCNT_CONGREWR(NAME) \
208 PERCENT (NAME, congruent_rewritten)
209
210#define PCNT_CONGRSIMPS(NAME) \
211 PERCENT (NAME, congruent_simplified)
212
213#define PCNT_CONGRUENT(NAME) \
214 PERCENT (NAME, congruent)
215
216#define PCNT_CONGRUNARY(NAME) \
217 PERCENT (NAME, congruent_unary)
218
219#define PCNT_DECISIONS(NAME) \
220 PERCENT (NAME, decisions)
221
222#define PCNT_DEFRAGS(NAME) \
223 PERCENT (NAME, defragmentations)
224
225#define PCNT_ELIM_ATTEMPTS(NAME) \
226 PERCENT (NAME, eliminate_attempted)
227
228#define PCNT_ELIMINATED(NAME) \
229 PERCENT (NAME, eliminated)
230
231#define PCNT_EXTRACTED(NAME) \
232 PERCENT (NAME, gates_extracted)
233
234#define PCNT_IRREDUNDANT(NAME) \
235 PERCENT (NAME, clauses_irredundant)
236
237#define PCNT_KITTEN_FLIP(NAME) \
238 PERCENT (NAME, kitten_flip)
239
240#define PCNT_KITTEN_SOLVED(NAME) \
241 PERCENT (NAME, kitten_solved)
242
243#define PCNT_LITS_DEDUCED(NAME) \
244 PERCENT (NAME, literals_deduced)
245
246#define PCNT_LITS_SHRUNKEN(NAME) \
247 PERCENT (NAME, literals_shrunken)
248
249#define PCNT_PROPS(NAME) \
250 PERCENT (NAME, propagations)
251
252#define PCNT_REDUCTIONS(NAME) \
253 PERCENT (NAME, reductions)
254
255#define PCNT_REDUNDANT_CLAUSES(NAME) \
256 PERCENT (NAME, clauses_redundant)
257
258#define PCNT_REORDERED(NAME) \
259 PERCENT (NAME, reordered)
260
261#define PCNT_REPHASED(NAME) \
262 PERCENT (NAME, rephased)
263
264#define PCNT_RESIDENT_SET(NAME) \
265 kissat_percent (statistics->NAME, rss)
266
267#define PCNT_RESTARTS(NAME) \
268 PERCENT (NAME, restarts)
269
270#define PCNT_RESTARTS_LEVELS(NAME) \
271 PERCENT (NAME, restarts_levels)
272
273#define PCNT_SEARCHES(NAME) \
274 PERCENT (NAME, searches)
275
276#define PCNT_STRENGTHENED(NAME) \
277 PERCENT (NAME, strengthened)
278
279#define PCNT_SUBSUMED(NAME) \
280 PERCENT (NAME, subsumed)
281
282#define PCNT_SUBSUMPTION_CHECK(NAME) \
283 PERCENT (NAME, subsumption_checks)
284
285#define PCNT_SWEEP_FLIP_BACKBONE(NAME) \
286 PERCENT (NAME, sweep_flip_backbone)
287
288#define PCNT_SWEEP_FLIP_EQUIVALENCES(NAME) \
289 PERCENT (NAME, sweep_flip_equivalences)
290
291#define PCNT_SWEEP_SOLVED_BACKBONE(NAME) \
292 PERCENT (NAME, sweep_solved_backbone)
293
294#define PCNT_SWEEP_SOLVED_EQUIVALENCES(NAME) \
295 PERCENT (NAME, sweep_solved_equivalences)
296
297#define PCNT_SWEEP_SOLVED(NAME) \
298 PERCENT (NAME, sweep_solved)
299
300#ifndef STATISTICS
301#define PCNT_TICKS(NAME) \
302 -1
303#else
304#define PCNT_TICKS(NAME) \
305 PERCENT (NAME, ticks)
306#endif
307
308#define PCNT_VARIABLES(NAME) \
309 kissat_percent (statistics->NAME, variables)
310
311#define PCNT_VIVIFIED(NAME) \
312 PERCENT (NAME, vivified)
313
314#define PCNT_VIVIFY_IMP(NAME) \
315 PERCENT (NAME, vivified_implied)
316
317#define PCNT_VIVIFY_INST(NAME) \
318 PERCENT (NAME, vivified_instantiated)
319
320#define PCNT_VIVIFY_CHECK(NAME) \
321 PERCENT (NAME, vivify_checks)
322
323#define PCNT_VIVIFY_PROBES(NAME) \
324 PERCENT (NAME, vivify_probes)
325
326#define PCNT_VIVIFY_SHRUNKEN(NAME) \
327 PERCENT (NAME, vivified_shrunken)
328
329#define PCNT_VIVIFY_SUB(NAME) \
330 PERCENT (NAME, vivified_subsumed)
331
332#define PCNT_WALKS(NAME) \
333 PERCENT (NAME, walks)
334
335#define COUNTER(NAME,VERBOSE,OTHER,UNITS,TYPE) \
336 if (verbose || !VERBOSE || (VERBOSE == 1 && statistics->NAME)) \
337 PRINT_STAT (#NAME, statistics->NAME, OTHER(NAME), UNITS, TYPE);
338#define IGNORE(...)
339
340 METRICS_COUNTERS_AND_STATISTICS
341
342#undef COUNTER
343#undef METRIC
344#undef STATISTIC
345
346 fflush (stdout);
347}
348
349// clang-format on
350
351ABC_NAMESPACE_IMPL_END
352
353#elif defined(KISSAT_NDEBUG)
354
355ABC_NAMESPACE_IMPL_START
356
357int kissat_statistics_dummy_to_avoid_warning;
358
359ABC_NAMESPACE_IMPL_END
360
361#endif
362
363/*------------------------------------------------------------------------*/
364
365#ifndef KISSAT_NDEBUG
366
367#include "inlinevector.h"
368
369ABC_NAMESPACE_IMPL_START
370
371void kissat_check_statistics (kissat *solver) {
372 if (solver->inconsistent)
373 return;
374
375 size_t redundant = 0;
376 size_t irredundant = 0;
377 size_t arena_garbage = 0;
378
379 for (all_clauses (c)) {
380 if (c->garbage) {
381 arena_garbage += kissat_actual_bytes_of_clause (c);
382 continue;
383 }
384 if (c->redundant)
385 redundant++;
386 else
387 irredundant++;
388 }
389
390 size_t binary = 0;
391
392 if (solver->watching) {
393 for (all_literals (lit)) {
394 watches *watches = &WATCHES (lit);
395
396 for (all_binary_blocking_watches (watch, *watches)) {
397 if (watch.type.binary) {
398 binary++;
399 }
400 }
401 }
402 } else {
403 for (all_literals (lit)) {
404 watches *watches = &WATCHES (lit);
405
406 for (all_binary_large_watches (watch, *watches)) {
407 if (watch.type.binary) {
408 binary++;
409 }
410 }
411 }
412 }
413
414 KISSAT_assert (!(binary & 1));
415 binary /= 2;
416
417 statistics *statistics = &solver->statistics_;
418 KISSAT_assert (statistics->clauses_binary == binary);
419 KISSAT_assert (statistics->clauses_redundant == redundant);
420 KISSAT_assert (statistics->clauses_irredundant == irredundant);
421#ifdef METRICS
422 KISSAT_assert (statistics->arena_garbage == arena_garbage);
423#else
424 (void) arena_garbage;
425#endif
426}
427
428ABC_NAMESPACE_IMPL_END
429
430#endif
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
irredundant
pcover irredundant()
all_literals
#define all_literals(LIT)
Definition internal.h:274
all_clauses
#define all_clauses(C)
Definition internal.h:279
KISSAT_assert
#define KISSAT_assert(ignore)
Definition global.h:13
solver
#define solver
Definition kitten.c:211
lit
int lit
Definition satVec.h:130
kissat_statistics_dummy_to_avoid_warning
ABC_NAMESPACE_IMPL_START int kissat_statistics_dummy_to_avoid_warning
Definition statistics.c:357
METRICS_COUNTERS_AND_STATISTICS
#define METRICS_COUNTERS_AND_STATISTICS
Definition statistics.h:12
kissat_check_statistics
#define kissat_check_statistics(...)
Definition statistics.h:464
binary_tagged_literal::binary
bool binary
Definition watch.h:23
kissat_print_tier_usage_statistics
void kissat_print_tier_usage_statistics(kissat *solver, bool stable)
Definition tiers.c:76
watch
Definition watch.h:41
watch::type
watch_type type
Definition watch.h:42
all_binary_blocking_watches
#define all_binary_blocking_watches(WATCH, WATCHES)
Definition watch.h:151
watches
vector watches
Definition watch.h:49
all_binary_large_watches
#define all_binary_large_watches(WATCH, WATCHES)
Definition watch.h:158
WATCHES
#define WATCHES(LIT)
Definition watch.h:137