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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
#ifndef _stats_hpp_INCLUDED
#define _stats_hpp_INCLUDED
#include <cstdlib>
namespace CaDiCaL {
struct Internal;
struct Stats {
Internal *internal;
int64_t vars; // internal initialized variables
int64_t conflicts; // generated conflicts in 'propagate'
int64_t decisions; // number of decisions in 'decide'
struct {
int64_t cover; // propagated during covered clause elimination
int64_t instantiate; // propagated during variable instantiation
int64_t probe; // propagated during probing
int64_t search; // propagated literals during search
int64_t transred; // propagated during transitive reduction
int64_t vivify; // propagated during vivification
int64_t walk; // propagated during local search
} propagations;
struct {
int64_t ext_cb; // number of times any external callback was called
int64_t eprop_call; // number of times external_propagate was called
int64_t eprop_prop; // number of times external propagate propagated
int64_t
eprop_conf; // number of times ex-propagate was already falsified
int64_t eprop_expl; // number of times external propagate was explained
int64_t
elearn_call; // number of times external clause learning was tried
int64_t elearned; // learned external clauses (incl. eprop explanations)
int64_t
elearn_prop; // number of learned and propagating external clauses
int64_t
elearn_conf; // number of learned and conflicting external clauses
int64_t echeck_call; // number of checking found complete solutions
} ext_prop;
int64_t condassinit; // initial assigned literals
int64_t condassirem; // initial assigned literals for blocked
int64_t condassrem; // remaining assigned literals for blocked
int64_t condassvars; // sum of active variables at initial assignment
int64_t condautinit; // initial literals in autarky part
int64_t condautrem; // remaining literals in autarky part for blocked
int64_t condcands; // globally blocked candidate clauses
int64_t condcondinit; // initial literals in conditional part
int64_t condcondrem; // remaining literals in conditional part for blocked
int64_t conditioned; // globally blocked clauses eliminated
int64_t conditionings; // globally blocked clause eliminations
int64_t condprops; // propagated unassigned literals
struct {
int64_t block; // block marked literals
int64_t elim; // elim marked variables
int64_t subsume; // subsume marked variables
int64_t ternary; // ternary marked variables
} mark;
struct {
int64_t total;
int64_t redundant;
int64_t irredundant;
} current, added; // Clauses.
struct {
double process, real;
} time;
struct {
int64_t count; // number of covered clause elimination rounds
int64_t asymmetric; // number of asymmetric tautologies in CCE
int64_t blocked; // number of blocked covered tautologies
int64_t total; // total number of eliminated clauses
} cover;
struct {
int64_t tried;
int64_t succeeded;
struct {
int64_t one, zero;
} constant, forward, backward;
struct {
int64_t positive, negative;
} horn;
} lucky;
struct {
int64_t total; // total number of happened rephases
int64_t best; // how often reset to best phases
int64_t flipped; // how often reset phases by flipping
int64_t inverted; // how often reset to inverted phases
int64_t original; // how often reset to original phases
int64_t random; // how often randomly reset phases
int64_t walk; // phases improved through random walked
} rephased;
struct {
int64_t count;
int64_t broken;
int64_t flips;
int64_t minimum;
} walk;
struct {
int64_t count; // flushings of learned clauses counter
int64_t learned; // flushed learned clauses
int64_t hyper; // flushed hyper binary/ternary clauses
} flush;
int64_t compacts; // number of compactifications
int64_t shuffled; // shuffled queues and scores
int64_t restarts; // actual number of happened restarts
int64_t restartlevels; // levels at restart
int64_t restartstable; // actual number of happened restarts
int64_t stabphases; // number of stabilization phases
int64_t stabconflicts; // number of search conflicts during stabilizing
int64_t rescored; // number of times scores were rescored
int64_t reused; // number of reused trails
int64_t reusedlevels; // reused levels at restart
int64_t reusedstable; // number of reused trails during stabilizing
int64_t sections; // 'section' counter
int64_t chrono; // chronological backtracks
int64_t backtracks; // number of backtracks
int64_t improvedglue; // improved glue during bumping
int64_t promoted1; // promoted clauses to tier one
int64_t promoted2; // promoted clauses to tier two
int64_t bumped; // seen and bumped variables in 'analyze'
int64_t recomputed; // recomputed glues 'recompute_glue'
int64_t searched; // searched decisions in 'decide'
int64_t reductions; // 'reduce' counter
int64_t reduced; // number of reduced clauses
int64_t collected; // number of collected bytes
int64_t collections; // number of garbage collections
int64_t hbrs; // hyper binary resolvents
int64_t hbrsizes; // sum of hyper resolved base clauses
int64_t hbreds; // redundant hyper binary resolvents
int64_t hbrsubs; // subsuming hyper binary resolvents
int64_t instried; // number of tried instantiations
int64_t instantiated; // number of successful instantiations
int64_t instrounds; // number of instantiation rounds
int64_t subsumed; // number of subsumed clauses
int64_t deduplicated; // number of removed duplicated binary clauses
int64_t deduplications; // number of deduplication phases
int64_t strengthened; // number of strengthened clauses
int64_t
elimotfstr; // number of on-the-fly strengthened during elimination
int64_t subirr; // number of subsumed irredundant clauses
int64_t subred; // number of subsumed redundant clauses
int64_t subtried; // number of tried subsumptions
int64_t subchecks; // number of pair-wise subsumption checks
int64_t subchecks2; // same but restricted to binary clauses
int64_t elimotfsub; // number of on-the-fly subsumed during elimination
int64_t subsumerounds; // number of subsumption rounds
int64_t subsumephases; // number of scheduled subsumption phases
int64_t eagertried; // number of traversed eager subsumed candidates
int64_t eagersub; // number of eagerly subsumed recently learned clauses
int64_t elimres; // number of resolved clauses in BVE
int64_t elimrestried; // number of tried resolved clauses in BVE
int64_t elimrounds; // number of elimination rounds
int64_t elimphases; // number of scheduled elimination phases
int64_t elimcompleted; // number complete elimination procedures
int64_t elimtried; // number of variable elimination attempts
int64_t elimsubst; // number of eliminations through substitutions
int64_t elimgates; // number of gates found during elimination
int64_t elimequivs; // number of equivalences found during elimination
int64_t elimands; // number of AND gates found during elimination
int64_t elimites; // number of ITE gates found during elimination
int64_t elimxors; // number of XOR gates found during elimination
int64_t elimbwsub; // number of eager backward subsumed clauses
int64_t elimbwstr; // number of eager backward strengthened clauses
int64_t ternary; // number of ternary resolution phases
int64_t ternres; // number of ternary resolutions
int64_t htrs; // number of hyper ternary resolvents
int64_t htrs2; // number of binary hyper ternary resolvents
int64_t htrs3; // number of ternary hyper ternary resolvents
int64_t decompositions; // number of SCC + ELS
int64_t vivifications; // number of vivifications
int64_t vivifychecks; // checked clauses during vivification
int64_t vivifydecs; // vivification decisions
int64_t vivifyreused; // reused vivification decisions
int64_t vivifysched; // scheduled clauses for vivification
int64_t vivifysubs; // subsumed clauses during vivification
int64_t vivifystrs; // strengthened clauses during vivification
int64_t vivifystrirr; // strengthened irredundant clause
int64_t vivifystred1; // strengthened redundant clause (1)
int64_t vivifystred2; // strengthened redundant clause (2)
int64_t vivifystred3; // strengthened redundant clause (3)
int64_t vivifyunits; // units during vivification
int64_t vivifyinst; // instantiation during vivification
int64_t transreds;
int64_t transitive;
struct {
int64_t literals;
int64_t clauses;
} learned;
int64_t minimized; // minimized literals
int64_t shrunken; // shrunken literals
int64_t minishrunken; // shrunken during minimization literals
int64_t irrlits; // literals in irredundant clauses
struct {
int64_t bytes;
int64_t clauses;
int64_t literals;
} garbage;
int64_t units; // learned unit clauses
int64_t binaries; // learned binary clauses
int64_t probingphases; // number of scheduled probing phases
int64_t probingrounds; // number of probing rounds
int64_t probesuccess; // number successful probing phases
int64_t probed; // number of probed literals
int64_t failed; // number of failed literals
int64_t hyperunary; // hyper unary resolved unit clauses
int64_t probefailed; // failed literals from probing
int64_t transredunits; // units derived in transitive reduction
int64_t blockings; // number of blocked clause eliminations
int64_t blocked; // number of actually blocked clauses
int64_t blockres; // number of resolutions during blocking
int64_t blockcands; // number of clause / pivot pairs tried
int64_t blockpured; // number of clauses blocked through pure literals
int64_t blockpurelits; // number of pure literals
int64_t extensions; // number of extended witnesses
int64_t extended; // number of flipped literals during extension
int64_t weakened; // number of clauses pushed to extension stack
int64_t weakenedlen; // lengths of weakened clauses
int64_t restorations; // number of restore calls
int64_t restored; // number of restored clauses
int64_t reactivated; // number of reactivated clauses
int64_t restoredlits; // number of restored literals
int64_t preprocessings;
int64_t ilbtriggers;
int64_t ilbsuccess;
int64_t levelsreused;
int64_t literalsreused;
int64_t assumptionsreused;
struct {
int64_t fixed; // number of top level assigned variables
int64_t eliminated; // number of eliminated variables
int64_t substituted; // number of substituted variables
int64_t pure; // number of pure literals
} all, now;
struct {
int64_t strengthened; // number of clauses strengthened during OTFS
int64_t subsumed; // number of clauses subsumed by OTFS
} otfs;
int64_t unused; // number of unused variables
int64_t active; // number of active variables
int64_t inactive; // number of inactive variables
Stats ();
void print (Internal *);
};
/*------------------------------------------------------------------------*/
} // namespace CaDiCaL
#endif