5.CaDiCal代码解读——CaDiCal的internal相关代码--stats.hpp-stats.cpp

  //stats.hpp
  1
 #ifndef _stats_hpp_INCLUDED
  2 #define _stats_hpp_INCLUDED
  3 
  4 #include <cstdlib>
  5 
  6 namespace CaDiCaL {
  7 
  8 struct Internal;
  9 
 10 struct Stats {
 11 
 12   Internal * internal;
 13 
 14   int64_t vars;         // internal initialized variables
 15 
 16   int64_t conflicts;    // generated conflicts in 'propagate'
 17   int64_t decisions;    // number of decisions in 'decide'
 18 
 19   struct {
 20     int64_t cover;      // propagated during covered clause elimination
 21     int64_t instantiate;// propagated during variable instantiation
 22     int64_t probe;      // propagated during probing
 23     int64_t search;     // propagated literals during search
 24     int64_t transred;   // propagated during transitive reduction
 25     int64_t vivify;     // propagated during vivification
 26     int64_t walk;       // propagated during local search
 27   } propagations;
 28 
 29   long condassinit;  // initial assigned literals
 30   long condassirem;  // initial assigned literals for blocked
 31   long condassrem;   // remaining assigned literals for blocked
 32   long condassvars;  // sum of active variables at initial assignment
 33   long condautinit;  // initial literals in autarky part
 34   long condautrem;   // remaining literals in autarky part for blocked
 35   long condcands;    // globally blocked candidate clauses
 36   long condcondinit; // initial literals in conditional part
 37   long condcondrem;  // remaining literals in conditional part for blocked
 38   long conditioned;  // globally blocked clauses eliminated
 39   long conditionings;// globally blocked clause eliminations
 40   long condprops;    // propagated unassigned literals
 41 
 42   struct {
 43     int64_t block;      // block marked literals
 44     int64_t elim;       // elim marked variables
 45     int64_t subsume;    // subsume marked variables
 46     int64_t ternary;    // ternary marked variables
 47   } mark;
 48 
 49   struct {
 50     int64_t total;
 51     int64_t redundant;
 52     int64_t irredundant;
 53   } current, added;  // Clauses.
 54 
 55   struct { double process, real; } time;
 56 
 57   struct {
 58     int64_t count;      // number of covered clause elimination rounds
 59     int64_t asymmetric; // number of asymmetric tautologies in CCE
 60     int64_t blocked;    // number of blocked covered tautologies
 61     int64_t total;      // total number of eliminated clauses
 62   } cover;
 63 
 64   struct {
 65     int64_t tried;
 66     int64_t succeeded;
 67     struct { int64_t one, zero; } constant, forward, backward;
 68     struct { int64_t positive, negative; } horn;
 69   } lucky;
 70 
 71   struct {
 72     int64_t total;      // total number of happened rephases
 73     int64_t best;       // how often reset to best phases
 74     int64_t flipped;    // how often reset phases by flipping
 75     int64_t inverted;   // how often reset to inverted phases
 76     int64_t original;   // how often reset to original phases
 77     int64_t random;     // how often randomly reset phases
 78     int64_t walk;       // phases improved through random walked
 79   } rephased;
 80 
 81   struct {
 82     int64_t count;
 83     int64_t broken;
 84     int64_t flips;
 85     int64_t minimum;
 86   } walk;
 87 
 88   struct {
 89     int64_t count;      // flushings of learned clauses counter
 90     int64_t learned;    // flushed learned clauses
 91     int64_t hyper;      // flushed hyper binary/ternary clauses
 92   } flush;
 93 
 94   int64_t compacts;     // number of compactifications
 95   int64_t shuffled;     // shuffled queues and scores
 96   int64_t restarts;     // actual number of happened restarts
 97   int64_t restartlevels;// levels at restart
 98   int64_t restartstable;// actual number of happened restarts
 99   int64_t stabphases;   // number of stabilization phases
100   int64_t stabconflicts;// number of search conflicts during stabilizing
101   int64_t rescored;     // number of times scores were rescored
102   int64_t reused;       // number of reused trails
103   int64_t reusedlevels; // reused levels at restart
104   int64_t reusedstable; // number of reused trails during stabilizing
105   int64_t sections;     // 'section' counter
106   int64_t chrono;       // chronological backtracks
107   int64_t backtracks;   // number of backtracks
108   int64_t improvedglue; // improved glue during bumping
109   int64_t promoted1;    // promoted clauses to tier one
110   int64_t promoted2;    // promoted clauses to tier two
111   int64_t bumped;       // seen and bumped variables in 'analyze'
112   int64_t recomputed;   // recomputed glues 'recompute_glue'
113   int64_t searched;     // searched decisions in 'decide'
114   int64_t reductions;   // 'reduce' counter
115   int64_t reduced;      // number of reduced clauses
116   int64_t collected;    // number of collected bytes
117   int64_t collections;  // number of garbage collections
118   int64_t hbrs;         // hyper binary resolvents
119   int64_t hbrsizes;     // sum of hyper resolved base clauses
120   int64_t hbreds;       // redundant hyper binary resolvents
121   int64_t hbrsubs;      // subsuming hyper binary resolvents
122   int64_t instried;     // number of tried instantiations
123   int64_t instantiated; // number of successful instantiations
124   int64_t instrounds;   // number of instantiation rounds
125   int64_t subsumed;     // number of subsumed clauses
126   int64_t deduplicated; // number of removed duplicated binary clauses
127   int64_t deduplications;//number of deduplication phases
128   int64_t strengthened; // number of strengthened clauses
129   int64_t elimotfstr;   // number of on-the-fly strengthened during elimination
130   int64_t subirr;       // number of subsumed irredundant clauses
131   int64_t subred;       // number of subsumed redundant clauses
132   int64_t subtried;     // number of tried subsumptions
133   int64_t subchecks;    // number of pair-wise subsumption checks
134   int64_t subchecks2;   // same but restricted to binary clauses
135   int64_t elimotfsub;   // number of on-the-fly subsumed during elimination
136   int64_t subsumerounds;// number of subsumption rounds
137   int64_t subsumephases;// number of scheduled subsumption phases
138   int64_t eagertried;   // number of traversed eager subsumed candidates
139   int64_t eagersub;     // number of eagerly subsumed recently learned clauses
140   int64_t elimres;      // number of resolved clauses in BVE
141   int64_t elimrestried; // number of tried resolved clauses in BVE
142   int64_t elimrounds;   // number of elimination rounds
143   int64_t elimphases;   // number of scheduled elimination phases
144   int64_t elimcompleted;// number complete elimination procedures
145   int64_t elimtried;    // number of variable elimination attempts
146   int64_t elimsubst;    // number of eliminations through substitutions
147   int64_t elimgates;    // number of gates found during elimination
148   int64_t elimequivs;   // number of equivalences found during elimination
149   int64_t elimands;     // number of AND gates found during elimination
150   int64_t elimites;     // number of ITE gates found during elimination
151   int64_t elimxors;     // number of XOR gates found during elimination
152   int64_t elimbwsub;    // number of eager backward subsumed clauses
153   int64_t elimbwstr;    // number of eager backward strengthened clauses
154   int64_t ternary;      // number of ternary resolution phases
155   int64_t ternres;      // number of ternary resolutions
156   int64_t htrs;         // number of hyper ternary resolvents
157   int64_t htrs2;        // number of binary hyper ternary resolvents
158   int64_t htrs3;        // number of ternary hyper ternary resolvents
159   int64_t decompositions; // number of SCC + ELS
160   int64_t vivifications;  // number of vivifications
161   int64_t vivifychecks; // checked clauses during vivification
162   int64_t vivifydecs;   // vivification decisions
163   int64_t vivifyreused; // reused vivification decisions
164   int64_t vivifysched;  // scheduled clauses for vivification
165   int64_t vivifysubs;   // subsumed clauses during vivification
166   int64_t vivifystrs;   // strengthened clauses during vivification
167   int64_t vivifystrirr; // strengthened irredundant clause
168   int64_t vivifystred1; // strengthened redundant clause (1)
169   int64_t vivifystred2; // strengthened redundant clause (2)
170   int64_t vivifystred3; // strengthened redundant clause (3)
171   int64_t vivifyunits;  // units during vivification
172   int64_t transreds;
173   int64_t transitive;
174   struct {
175     int64_t literals;
176     int64_t clauses;
177   } learned;
178   int64_t minimized;    // minimized literals
179   int64_t irrbytes;     // bytes of irredundant clauses
180   int64_t garbage;      // bytes current irredundant garbage clauses
181   int64_t units;        // learned unit clauses
182   int64_t binaries;     // learned binary clauses
183   int64_t probingphases;// number of scheduled probing phases
184   int64_t probingrounds;// number of probing rounds
185   int64_t probesuccess; // number successful probing phases
186   int64_t probed;       // number of probed literals
187   int64_t failed;       // number of failed literals
188   int64_t hyperunary;   // hyper unary resolved unit clauses
189   int64_t probefailed;  // failed literals from probing
190   int64_t transredunits;// units derived in transitive reduction
191   int64_t blockings;    // number of blocked clause eliminations
192   int64_t blocked;      // number of actually blocked clauses
193   int64_t blockres;     // number of resolutions during blocking
194   int64_t blockcands;   // number of clause / pivot pairs tried
195   int64_t blockpured;   // number of clauses blocked through pure literals
196   int64_t blockpurelits;// number of pure literals
197   int64_t extensions;   // number of extended witnesses
198   int64_t extended;     // number of flipped literals during extension
199   int64_t weakened;     // number of clauses pushed to extension stack
200   int64_t weakenedlen;  // lengths of weakened clauses
201   int64_t restorations; // number of restore calls
202   int64_t restored;     // number of restored clauses
203   int64_t reactivated;  // number of reactivated clauses
204   int64_t restoredlits; // number of restored literals
205 
206   int64_t preprocessings;
207 
208   struct {
209     int64_t fixed;       // number of top level assigned variables
210     int64_t eliminated;  // number of eliminated variables
211     int64_t substituted; // number of substituted variables
212     int64_t pure;        // number of pure literals
213   } all, now;
214 
215   int64_t unused;        // number of unused variables
216   int64_t active;        // number of active variables
217   int64_t inactive;      // number of inactive variables
218 
219   Stats ();
220 
221   void print (Internal *);
222 };
223 
224 /*------------------------------------------------------------------------*/
225 
226 }
227 
228 #endif

  //stats.cpp

  1 // vim: set tw=300: set VIM text width to 300 characters for this file.
  2 
  3 #include "internal.hpp"
  4 
  5 namespace CaDiCaL {
  6 
  7 /*------------------------------------------------------------------------*/
  8 
  9 Stats::Stats () {
 10   memset (this, 0, sizeof *this);
 11   time.real = absolute_real_time ();
 12   time.process = absolute_process_time ();
 13   walk.minimum = LONG_MAX;
 14 }
 15 
 16 /*------------------------------------------------------------------------*/
 17 
 18 #define PRT(FMT,...) \
 19 do { \
 20   if (FMT[0] == ' ' && !all) break; \
 21   MSG (FMT, __VA_ARGS__); \
 22 } while (0)
 23 
 24 /*------------------------------------------------------------------------*/
 25 
 26 void Stats::print (Internal * internal) {
 27 
 28 #ifdef QUIET
 29   (void) internal;
 30 #else
 31 
 32   Stats & stats = internal->stats;
 33 
 34   int all = internal->opts.verbose > 0;
 35 #ifdef LOGGING
 36   if (internal->opts.log) all = true;
 37 #endif // ifdef LOGGING
 38 
 39   if (internal->opts.profile) internal->print_profile ();
 40 
 41   double t = internal->solve_time ();
 42 
 43   int64_t propagations = 0;
 44   propagations += stats.propagations.cover;
 45   propagations += stats.propagations.probe;
 46   propagations += stats.propagations.search;
 47   propagations += stats.propagations.transred;
 48   propagations += stats.propagations.vivify;
 49   propagations += stats.propagations.walk;
 50 
 51   int64_t vivified = stats.vivifysubs + stats.vivifystrs;
 52 
 53   size_t extendbytes = internal->external->extension.size ();
 54   extendbytes *= sizeof (int);
 55 
 56   SECTION ("statistics");
 57 
 58   if (all || stats.blocked) {
 59   PRT ("blocked:         %15" PRId64 "   %10.2f %%  of irredundant clauses", stats.blocked, percent (stats.blocked, stats.added.irredundant));
 60   PRT ("  blockings:     %15" PRId64 "   %10.2f    internal", stats.blockings, relative (stats.conflicts, stats.blockings));
 61   PRT ("  candidates:    %15" PRId64 "   %10.2f    per blocking ", stats.blockcands, relative (stats.blockcands, stats.blockings));
 62   PRT ("  blockres:      %15" PRId64 "   %10.2f    per candidate", stats.blockres, relative (stats.blockres, stats.blockcands));
 63   PRT ("  pure:          %15" PRId64 "   %10.2f %%  of all variables", stats.all.pure, percent (stats.all.pure, stats.vars));
 64   PRT ("  pureclauses:   %15" PRId64 "   %10.2f    per pure literal", stats.blockpured, relative (stats.blockpured, stats.all.pure));
 65   }
 66   if (all || stats.chrono)
 67   PRT ("chronological:   %15" PRId64 "   %10.2f %%  of conflicts", stats.chrono, percent (stats.chrono, stats.conflicts));
 68   if (all)
 69   PRT ("compacts:        %15" PRId64 "   %10.2f    interval", stats.compacts, relative (stats.conflicts, stats.compacts));
 70   if (all || stats.conflicts) {
 71   PRT ("conflicts:       %15" PRId64 "   %10.2f    per second", stats.conflicts, relative (stats.conflicts, t));
 72   PRT ("  backtracked:   %15" PRId64 "   %10.2f %%  of conflicts", stats.backtracks, percent (stats.backtracks, stats.conflicts));
 73   }
 74   if (all || stats.conditioned) {
 75   PRT ("conditioned:     %15ld   %10.2f %%  of irredundant clauses", stats.conditioned, percent (stats.conditioned, stats.added.irredundant));
 76   PRT ("  conditionings: %15ld   %10.2f    interval", stats.conditionings, relative (stats.conflicts, stats.conditionings));
 77   PRT ("  condcands:     %15ld   %10.2f    candidate clauses", stats.condcands, relative (stats.condcands, stats.conditionings));
 78   PRT ("  condassinit:   %17.1f  %9.2f %%  initial assigned", relative (stats.condassinit, stats.conditionings), percent (stats.condassinit, stats.condassvars));
 79   PRT ("  condcondinit:  %17.1f  %9.2f %%  initial condition", relative (stats.condcondinit, stats.conditionings), percent (stats.condcondinit, stats.condassinit));
 80   PRT ("  condautinit:   %17.1f  %9.2f %%  initial autarky", relative (stats.condautinit, stats.conditionings), percent (stats.condautinit, stats.condassinit));
 81   PRT ("  condassrem:    %17.1f  %9.2f %%  final assigned", relative (stats.condassrem, stats.conditioned), percent (stats.condassrem, stats.condassirem));
 82   PRT ("  condcondrem:   %19.3f  %7.2f %%  final conditional", relative (stats.condcondrem, stats.conditioned), percent (stats.condcondrem, stats.condassrem));
 83   PRT ("  condautrem:    %19.3f  %7.2f %%  final autarky", relative (stats.condautrem, stats.conditioned), percent (stats.condautrem, stats.condassrem));
 84   PRT ("  condprops:     %15ld   %10.2f    per candidate", stats.condprops, relative (stats.condprops, stats.condcands));
 85   }
 86   if (all || stats.cover.total) {
 87   PRT ("covered:         %15" PRId64 "   %10.2f %%  of irredundant clauses", stats.cover.total, percent (stats.cover.total, stats.added.irredundant));
 88   PRT ("  coverings:     %15" PRId64 "   %10.2f    interval", stats.cover.count, relative (stats.conflicts, stats.cover.count));
 89   PRT ("  asymmetric:    %15" PRId64 "   %10.2f %%  of covered clauses", stats.cover.asymmetric, percent (stats.cover.asymmetric, stats.cover.total));
 90   PRT ("  blocked:       %15" PRId64 "   %10.2f %%  of covered clauses", stats.cover.blocked, percent (stats.cover.blocked, stats.cover.total));
 91   }
 92   if (all || stats.decisions) {
 93   PRT ("decisions:       %15" PRId64 "   %10.2f    per second", stats.decisions, relative (stats.decisions, t));
 94   PRT ("  searched:      %15" PRId64 "   %10.2f    per decision", stats.searched, relative (stats.searched, stats.decisions));
 95   }
 96   if (all || stats.all.eliminated) {
 97   PRT ("eliminated:      %15" PRId64 "   %10.2f %%  of all variables", stats.all.eliminated, percent (stats.all.eliminated, stats.vars));
 98   PRT ("  elimphases:    %15" PRId64 "   %10.2f    interval", stats.elimphases, relative (stats.conflicts, stats.elimphases));
 99   PRT ("  elimrounds:    %15" PRId64 "   %10.2f    per phase", stats.elimrounds, relative (stats.elimrounds, stats.elimphases));
100   PRT ("  elimtried:     %15" PRId64 "   %10.2f %%  eliminated", stats.elimtried, percent (stats.all.eliminated, stats.elimtried));
101   PRT ("  elimgates:     %15" PRId64 "   %10.2f %%  gates per tried", stats.elimgates, percent (stats.elimgates, stats.elimtried));
102   PRT ("  elimequivs:    %15" PRId64 "   %10.2f %%  equivalence gates", stats.elimequivs, percent (stats.elimequivs, stats.elimgates));
103   PRT ("  elimands:      %15" PRId64 "   %10.2f %%  and gates", stats.elimands, percent (stats.elimands, stats.elimgates));
104   PRT ("  elimites:      %15" PRId64 "   %10.2f %%  if-then-else gates", stats.elimites, percent (stats.elimites, stats.elimgates));
105   PRT ("  elimxors:      %15" PRId64 "   %10.2f %%  xor gates", stats.elimxors, percent (stats.elimxors, stats.elimgates));
106   PRT ("  elimsubst:     %15" PRId64 "   %10.2f %%  substituted", stats.elimsubst, percent (stats.elimsubst, stats.all.eliminated));
107   PRT ("  elimres:       %15" PRId64 "   %10.2f    per eliminated", stats.elimres, relative (stats.elimres, stats.all.eliminated));
108   PRT ("  elimrestried:  %15" PRId64 "   %10.2f %%  per resolution", stats.elimrestried, percent (stats.elimrestried, stats.elimres));
109   }
110   if (all || stats.all.fixed) {
111   PRT ("fixed:           %15" PRId64 "   %10.2f %%  of all variables", stats.all.fixed, percent (stats.all.fixed, stats.vars));
112   PRT ("  failed:        %15" PRId64 "   %10.2f %%  of all variables", stats.failed, percent (stats.failed, stats.vars));
113   PRT ("  probefailed:   %15" PRId64 "   %10.2f %%  per failed", stats.probefailed, percent (stats.probefailed, stats.failed));
114   PRT ("  transredunits: %15" PRId64 "   %10.2f %%  per failed", stats.transredunits, percent (stats.transredunits, stats.failed));
115   PRT ("  probingphases: %15" PRId64 "   %10.2f    interval", stats.probingphases, relative (stats.conflicts, stats.probingphases));
116   PRT ("  probesuccess:  %15" PRId64 "   %10.2f %%  phases", stats.probesuccess, percent (stats.probesuccess, stats.probingphases));
117   PRT ("  probingrounds: %15" PRId64 "   %10.2f    per phase", stats.probingrounds, relative (stats.probingrounds, stats.probingphases));
118   PRT ("  probed:        %15" PRId64 "   %10.2f    per failed", stats.probed, relative (stats.probed, stats.failed));
119   PRT ("  hbrs:          %15" PRId64 "   %10.2f    per probed", stats.hbrs, relative (stats.hbrs, stats.probed));
120   PRT ("  hbrsizes:      %15" PRId64 "   %10.2f    per hbr", stats.hbrsizes, relative (stats.hbrsizes, stats.hbrs));
121   PRT ("  hbreds:        %15" PRId64 "   %10.2f %%  per hbr", stats.hbreds, percent (stats.hbreds, stats.hbrs));
122   PRT ("  hbrsubs:       %15" PRId64 "   %10.2f %%  per hbr", stats.hbrsubs, percent (stats.hbrsubs, stats.hbrs));
123   }
124   PRT ("  units:         %15" PRId64 "   %10.2f    interval", stats.units, relative (stats.conflicts, stats.units));
125   PRT ("  binaries:      %15" PRId64 "   %10.2f    interval", stats.binaries, relative (stats.conflicts, stats.binaries));
126   if (all || stats.flush.learned) {
127   PRT ("flushed:         %15" PRId64 "   %10.2f %%  per conflict", stats.flush.learned, percent (stats.flush.learned, stats.conflicts));
128   PRT ("  hyper:         %15" PRId64 "   %10.2f %%  per conflict", stats.flush.hyper, relative (stats.flush.hyper, stats.conflicts));
129   PRT ("  flushings:     %15" PRId64 "   %10.2f    interval", stats.flush.count, relative (stats.conflicts, stats.flush.count));
130   }
131   if (all || stats.instantiated) {
132   PRT ("instantiated:    %15" PRId64 "   %10.2f %%  of tried", stats.instantiated, percent (stats.instantiated, stats.instried));
133   PRT ("  instrounds:    %15" PRId64 "   %10.2f %%  of elimrounds", stats.instrounds, percent (stats.instrounds, stats.elimrounds));
134   }
135   if (all || stats.conflicts) {
136   PRT ("learned:         %15" PRId64 "   %10.2f %%  per conflict", stats.learned.clauses, percent (stats.learned.clauses, stats.conflicts));
137   PRT ("  bumped:        %15" PRId64 "   %10.2f    per learned", stats.bumped, relative (stats.bumped, stats.learned.clauses));
138   PRT ("  recomputed:    %15" PRId64 "   %10.2f %%  per learned", stats.recomputed, percent (stats.recomputed, stats.learned.clauses));
139   PRT ("  promoted1:     %15" PRId64 "   %10.2f %%  per learned", stats.promoted1, percent (stats.promoted1, stats.learned.clauses));
140   PRT ("  promoted2:     %15" PRId64 "   %10.2f %%  per learned", stats.promoted2, percent (stats.promoted2, stats.learned.clauses));
141   PRT ("  improvedglue:  %15" PRId64 "   %10.2f %%  per learned", stats.improvedglue, percent (stats.improvedglue, stats.learned.clauses));
142   }
143   if (all || stats.lucky.succeeded) {
144   PRT ("lucky:           %15" PRId64 "   %10.2f %%  of tried", stats.lucky.succeeded, percent (stats.lucky.succeeded, stats.lucky.tried));
145   PRT ("  constantzero   %15" PRId64 "   %10.2f %%  of tried", stats.lucky.constant.zero, percent (stats.lucky.constant.zero, stats.lucky.tried));
146   PRT ("  constantone    %15" PRId64 "   %10.2f %%  of tried", stats.lucky.constant.one, percent (stats.lucky.constant.one, stats.lucky.tried));
147   PRT ("  backwardone    %15" PRId64 "   %10.2f %%  of tried", stats.lucky.backward.one, percent (stats.lucky.backward.one, stats.lucky.tried));
148   PRT ("  backwardzero   %15" PRId64 "   %10.2f %%  of tried", stats.lucky.backward.zero, percent (stats.lucky.backward.zero, stats.lucky.tried));
149   PRT ("  forwardone     %15" PRId64 "   %10.2f %%  of tried", stats.lucky.forward.one, percent (stats.lucky.forward.one, stats.lucky.tried));
150   PRT ("  forwardzero    %15" PRId64 "   %10.2f %%  of tried", stats.lucky.forward.zero, percent (stats.lucky.forward.zero, stats.lucky.tried));
151   PRT ("  positivehorn   %15" PRId64 "   %10.2f %%  of tried", stats.lucky.horn.positive, percent (stats.lucky.horn.positive, stats.lucky.tried));
152   PRT ("  negativehorn   %15" PRId64 "   %10.2f %%  of tried", stats.lucky.horn.negative, percent (stats.lucky.horn.negative, stats.lucky.tried));
153   }
154   PRT ("  extendbytes:   %15" PRId64 "   %10.2f    bytes and MB", extendbytes, extendbytes/(double)(1l<<20));
155   if (all || stats.learned.clauses)
156   PRT ("minimized:       %15" PRId64 "   %10.2f %%  learned literals", stats.minimized, percent (stats.minimized, stats.learned.literals));
157   PRT ("propagations:    %15" PRId64 "   %10.2f M  per second", propagations, relative (propagations/1e6, t));
158   PRT ("  coverprops:    %15" PRId64 "   %10.2f %%  of propagations", stats.propagations.cover, percent (stats.propagations.cover, propagations));
159   PRT ("  probeprops:    %15" PRId64 "   %10.2f %%  of propagations", stats.propagations.probe, percent (stats.propagations.probe, propagations));
160   PRT ("  searchprops:   %15" PRId64 "   %10.2f %%  of propagations", stats.propagations.search, percent (stats.propagations.search, propagations));
161   PRT ("  transredprops: %15" PRId64 "   %10.2f %%  of propagations", stats.propagations.transred, percent (stats.propagations.transred, propagations));
162   PRT ("  vivifyprops:   %15" PRId64 "   %10.2f %%  of propagations", stats.propagations.vivify, percent (stats.propagations.vivify, propagations));
163   PRT ("  walkprops:     %15" PRId64 "   %10.2f %%  of propagations", stats.propagations.walk, percent (stats.propagations.walk, propagations));
164   if (all || stats.reactivated) {
165   PRT ("reactivated:     %15" PRId64 "   %10.2f %%  of all variables", stats.reactivated, percent (stats.reactivated, stats.vars));
166   }
167   if (all || stats.reduced) {
168   PRT ("reduced:         %15" PRId64 "   %10.2f %%  per conflict", stats.reduced, percent (stats.reduced, stats.conflicts));
169   PRT ("  reductions:    %15" PRId64 "   %10.2f    interval", stats.reductions, relative (stats.conflicts, stats.reductions));
170   PRT ("  collections:   %15" PRId64 "   %10.2f    interval", stats.collections, relative (stats.conflicts, stats.collections));
171   }
172   if (all || stats.rephased.total) {
173   PRT ("rephased:        %15" PRId64 "   %10.2f    interval", stats.rephased.total, relative (stats.conflicts, stats.rephased.total));
174   PRT ("  rephasedbest:  %15" PRId64 "   %10.2f %%  rephased best", stats.rephased.best, percent (stats.rephased.best, stats.rephased.total));
175   PRT ("  rephasedflip:  %15" PRId64 "   %10.2f %%  rephased flipping", stats.rephased.flipped, percent (stats.rephased.flipped, stats.rephased.total));
176   PRT ("  rephasedinv:   %15" PRId64 "   %10.2f %%  rephased inverted", stats.rephased.inverted, percent (stats.rephased.inverted, stats.rephased.total));
177   PRT ("  rephasedorig:  %15" PRId64 "   %10.2f %%  rephased original", stats.rephased.original, percent (stats.rephased.original, stats.rephased.total));
178   PRT ("  rephasedrand:  %15" PRId64 "   %10.2f %%  rephased random", stats.rephased.random, percent (stats.rephased.random, stats.rephased.total));
179   PRT ("  rephasedwalk:  %15" PRId64 "   %10.2f %%  rephased walk", stats.rephased.walk, percent (stats.rephased.walk, stats.rephased.total));
180   }
181   if (all)
182   PRT ("rescored:        %15" PRId64 "   %10.2f    interval", stats.rescored, relative (stats.conflicts, stats.rescored));
183   if (all || stats.restarts) {
184   PRT ("restarts:        %15" PRId64 "   %10.2f    interval", stats.restarts, relative (stats.conflicts, stats.restarts));
185   PRT ("  reused:        %15" PRId64 "   %10.2f %%  per restart", stats.reused, percent (stats.reused, stats.restarts));
186   PRT ("  reusedlevels:  %15" PRId64 "   %10.2f %%  per restart levels", stats.reusedlevels, percent (stats.reusedlevels, stats.restartlevels));
187   }
188   if (all || stats.restored) {
189   PRT ("restored:        %15" PRId64 "   %10.2f %%  per weakened", stats.restored, percent (stats.restored, stats.weakened));
190   PRT ("  restorations:  %15" PRId64 "   %10.2f %%  per extension", stats.restorations, percent (stats.restorations, stats.extensions));
191   PRT ("  literals:      %15" PRId64 "   %10.2f    per restored clause", stats.restoredlits, relative (stats.restoredlits, stats.restored));
192   }
193   if (all || stats.stabphases) {
194   PRT ("stabilizing:     %15" PRId64 "   %10.2f %%  of conflicts", stats.stabphases, percent (stats.stabconflicts, stats.conflicts));
195   PRT ("  restartstab:   %15" PRId64 "   %10.2f %%  of all restarts", stats.restartstable, percent (stats.restartstable, stats.restarts));
196   PRT ("  reusedstab:    %15" PRId64 "   %10.2f %%  per stable restarts", stats.reusedstable, percent (stats.reusedstable, stats.restartstable));
197   }
198   if (all || stats.all.substituted) {
199   PRT ("substituted:     %15" PRId64 "   %10.2f %%  of all variables", stats.all.substituted, percent (stats.all.substituted, stats.vars));
200   PRT ("  decompositions:%15" PRId64 "   %10.2f    per phase", stats.decompositions, relative (stats.decompositions, stats.probingphases));
201   }
202   if (all || stats.subsumed) {
203   PRT ("subsumed:        %15" PRId64 "   %10.2f %%  of all clauses", stats.subsumed, percent (stats.subsumed, stats.added.total));
204   PRT ("  subsumephases: %15" PRId64 "   %10.2f    interval", stats.subsumephases, relative (stats.conflicts, stats.subsumephases));
205   PRT ("  subsumerounds: %15" PRId64 "   %10.2f    per phase", stats.subsumerounds, relative (stats.subsumerounds, stats.subsumephases));
206   PRT ("  deduplicated:  %15" PRId64 "   %10.2f %%  per subsumed", stats.deduplicated, percent (stats.deduplicated, stats.subsumed));
207   PRT ("  transreds:     %15" PRId64 "   %10.2f    interval", stats.transreds, relative (stats.conflicts, stats.transreds));
208   PRT ("  transitive:    %15" PRId64 "   %10.2f %%  per subsumed", stats.transitive, percent (stats.transitive, stats.subsumed));
209   PRT ("  subirr:        %15" PRId64 "   %10.2f %%  of subsumed", stats.subirr, percent (stats.subirr, stats.subsumed));
210   PRT ("  subred:        %15" PRId64 "   %10.2f %%  of subsumed", stats.subred, percent (stats.subred, stats.subsumed));
211   PRT ("  subtried:      %15" PRId64 "   %10.2f    tried per subsumed", stats.subtried, relative (stats.subtried, stats.subsumed));
212   PRT ("  subchecks:     %15" PRId64 "   %10.2f    per tried", stats.subchecks, relative (stats.subchecks, stats.subtried));
213   PRT ("  subchecks2:    %15" PRId64 "   %10.2f %%  per subcheck", stats.subchecks2, percent (stats.subchecks2, stats.subchecks));
214   PRT ("  elimotfsub:    %15" PRId64 "   %10.2f %%  of subsumed", stats.elimotfsub, percent (stats.elimotfsub, stats.subsumed));
215   PRT ("  elimbwsub:     %15" PRId64 "   %10.2f %%  of subsumed", stats.elimbwsub, percent (stats.elimbwsub, stats.subsumed));
216   PRT ("  eagersub:      %15" PRId64 "   %10.2f %%  of subsumed", stats.eagersub, percent (stats.eagersub, stats.subsumed));
217   PRT ("  eagertried:    %15" PRId64 "   %10.2f    tried per eagersub", stats.eagertried, relative (stats.eagertried, stats.eagersub));
218   }
219   if (all || stats.strengthened) {
220   PRT ("strengthened:    %15" PRId64 "   %10.2f %%  of all clauses", stats.strengthened, percent (stats.strengthened, stats.added.total));
221   PRT ("  elimotfstr:    %15" PRId64 "   %10.2f %%  of strengthened", stats.elimotfstr, percent (stats.elimotfstr, stats.strengthened));
222   PRT ("  elimbwstr:     %15" PRId64 "   %10.2f %%  of strengthened", stats.elimbwstr, percent (stats.elimbwstr, stats.strengthened));
223   }
224   if (all || stats.htrs) {
225   PRT ("ternary:         %15" PRId64 "   %10.2f %%  of resolved", stats.htrs, percent (stats.htrs, stats.ternres));
226   PRT ("  phases:        %15" PRId64 "   %10.2f    interval", stats.ternary, relative (stats.conflicts, stats.ternary));
227   PRT ("  htr3:          %15" PRId64 "   %10.2f %%  ternary hyper ternres", stats.htrs3, percent (stats.htrs3, stats.htrs));
228   PRT ("  htr2:          %15" PRId64 "   %10.2f %%  binary hyper ternres", stats.htrs2, percent (stats.htrs2, stats.htrs));
229   }
230   if (all || vivified) {
231   PRT ("vivified:        %15" PRId64 "   %10.2f %%  of all clauses", vivified, percent (vivified, stats.added.total));
232   PRT ("  vivifications: %15" PRId64 "   %10.2f    interval", stats.vivifications, relative (stats.conflicts, stats.vivifications));
233   PRT ("  vivifychecks:  %15" PRId64 "   %10.2f %%  per conflict", stats.vivifychecks, percent (stats.vivifychecks, stats.conflicts));
234   PRT ("  vivifysched:   %15" PRId64 "   %10.2f %%  checks per scheduled", stats.vivifysched, percent (stats.vivifychecks, stats.vivifysched));
235   PRT ("  vivifyunits:   %15" PRId64 "   %10.2f %%  per vivify check", stats.vivifyunits, percent (stats.vivifyunits, stats.vivifychecks));
236   PRT ("  vivifysubs:    %15" PRId64 "   %10.2f %%  per subsumed", stats.vivifysubs, percent (stats.vivifysubs, stats.subsumed));
237   PRT ("  vivifystrs:    %15" PRId64 "   %10.2f %%  per strengthened", stats.vivifystrs, percent (stats.vivifystrs, stats.strengthened));
238   PRT ("  vivifystrirr:  %15" PRId64 "   %10.2f %%  per vivifystrs", stats.vivifystrirr, percent (stats.vivifystrirr, stats.vivifystrs));
239   PRT ("  vivifystred1:  %15" PRId64 "   %10.2f %%  per vivifystrs", stats.vivifystred1, percent (stats.vivifystred1, stats.vivifystrs));
240   PRT ("  vivifystred2:  %15" PRId64 "   %10.2f %%  per vivifystrs", stats.vivifystred2, percent (stats.vivifystred2, stats.vivifystrs));
241   PRT ("  vivifystred3:  %15" PRId64 "   %10.2f %%  per vivifystrs", stats.vivifystred3, percent (stats.vivifystred3, stats.vivifystrs));
242   PRT ("  vivifydecs:    %15" PRId64 "   %10.2f    per checks", stats.vivifydecs, relative (stats.vivifydecs, stats.vivifychecks));
243   PRT ("  vivifyreused:  %15" PRId64 "   %10.2f %%  per decision", stats.vivifyreused, percent (stats.vivifyreused, stats.vivifydecs));
244   }
245   if (all || stats.walk.count) {
246   PRT ("walked:          %15" PRId64 "   %10.2f    interval", stats.walk.count, relative (stats.conflicts, stats.walk.count));
247 #ifndef QUIET
248   if (internal->profiles.walk.value > 0)
249   PRT ("  flips:         %15" PRId64 "   %10.2f M  per second", stats.walk.flips, relative (1e-6*stats.walk.flips, internal->profiles.walk.value));
250   else
251 #endif
252   PRT ("  flips:         %15" PRId64 "   %10.2f    per walk", stats.walk.flips, relative (stats.walk.flips, stats.walk.count));
253   if (stats.walk.minimum < LONG_MAX)
254   PRT ("  minimum:       %15" PRId64 "   %10.2f %%  clauses", stats.walk.minimum, percent (stats.walk.minimum, stats.added.irredundant));
255   PRT ("  broken:        %15" PRId64 "   %10.2f    per flip", stats.walk.broken, relative (stats.walk.broken, stats.walk.flips));
256   }
257   if (all || stats.weakened) {
258   PRT ("weakened:        %15" PRId64 "   %10.2f    average size", stats.weakened, relative (stats.weakenedlen, stats.weakened));
259   PRT ("  extensions:    %15" PRId64 "   %10.2f    interval", stats.extensions, relative (stats.conflicts, stats.extensions));
260   PRT ("  flipped:       %15" PRId64 "   %10.2f    per weakened", stats.extended, relative (stats.extended, stats.weakened));
261   }
262 
263   MSG ("");
264   MSG ("%sseconds are measured in %s time for solving%s",
265     tout.magenta_code (),
266       internal->opts.realtime ? "real" : "process",
267     tout.normal_code ());
268 
269 #endif // ifndef QUIET
270 }
271 
272 void Internal::print_resource_usage () {
273 #ifndef QUIET
274   SECTION ("resources");
275   uint64_t m = maximum_resident_set_size ();
276   MSG ("total process time since initialization: %12.2f    seconds", internal->process_time ());
277   MSG ("total real time since initialization:    %12.2f    seconds", internal->real_time ());
278   MSG ("maximum resident set size of process:    %12.2f    MB", m/(double)(1l<<20));
279 #endif
280 }
281 
282 /*------------------------------------------------------------------------*/
283 
284 void Checker::print_stats () {
285 
286   if (!stats.added && !stats.deleted) return;
287 
288   SECTION ("checker statistics");
289 
290   MSG ("checks:          %15" PRId64 "", stats.checks);
291   MSG ("assumptions:     %15" PRId64 "   %10.2f    per check", stats.assumptions, relative (stats.assumptions, stats.checks));
292   MSG ("propagations:    %15" PRId64 "   %10.2f    per check", stats.propagations, relative (stats.propagations, stats.checks));
293   MSG ("original:        %15" PRId64 "   %10.2f %%  of all clauses", stats.original, percent (stats.original, stats.added));
294   MSG ("derived:         %15" PRId64 "   %10.2f %%  of all clauses", stats.derived, percent (stats.derived, stats.added));
295   MSG ("deleted:         %15" PRId64 "   %10.2f %%  of all clauses", stats.deleted, percent (stats.deleted, stats.added));
296   MSG ("insertions:      %15" PRId64 "   %10.2f %%  of all clauses", stats.insertions, percent (stats.insertions, stats.added));
297   MSG ("collections:     %15" PRId64 "   %10.2f    deleted per collection", stats.collections, relative (stats.collections, stats.deleted));
298   MSG ("collisions:      %15" PRId64 "   %10.2f    per search", stats.collisions, relative (stats.collisions, stats.searches));
299   MSG ("searches:        %15" PRId64 "", stats.searches);
300   MSG ("units:           %15" PRId64 "", stats.units);
301 }
302 
303 }