其他分享
首页 > 其他分享> > 5.CaDiCal代码解读——CaDiCal的internal相关代码--stats.hpp-stats.cpp

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

作者:互联网

stats.hpp定义了结构体类型Stats——通过这个定义可以看到各种参数的使用情况

stats.cpp给出了Stats的部分实现和其它类型定义的有关stats的函数:   

 void Stats::print (Internal * internal)

     void Internal::print_resource_usage ();

     void Checker::print_stats ()


 

 

 
  //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 }

 

   

标签:10.2,stats,代码,number,PRT,int64,15,CaDiCal
来源: https://www.cnblogs.com/yuweng1689/p/13388879.html