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

2020-07-28 07:32:37 阅读：305 来源： 互联网

标签：10.2 stats 代码 number PRT int64 15 CaDiCal

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-6stats.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

本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享；
2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关；
3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关；
4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除；
5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。

ICode9

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