Store stats where they belong

Author: msoos

src/comp_analyzer.cpp

@@ -228,11 +228,7 @@ void CompAnalyzer::record_comp(const uint32_t var, const uint32_t sup_comp_long_
 
   debug_print(COLWHT "We are NOW going through all binary/tri/long clauses "
       "recursively and put into search_stack_ all the variables that are connected to var: " << var);
-  if (comps_recorded % (128*1024*1024) == 0 && reset_comps+non_reset_comps > 0) {
-    verb_print(1, "[record_comp] Tot recorded " << (comps_recorded)/1000 << "K non-reset ratio: "
-        << (double)(non_reset_comps)/(double)(reset_comps+non_reset_comps));
-  }
-  comps_recorded++;
+  stats.comps_recorded++;
 
   for (auto vt = comp_vars.begin(); vt != comp_vars.end(); vt++) {
     const auto v = *vt;
@@ -251,9 +247,9 @@ void CompAnalyzer::record_comp(const uint32_t var, const uint32_t sup_comp_long_
     if (holder.tstamp(v) < counter->get_tstamp(holder.lev(v))) {
       /* holder.size_bin(v) = holder.orig_size_bin(v); */
       holder.size_long(v) = holder.orig_size_long(v);
-      reset_comps++;
+      stats.comps_reset++;
     } else {
-      non_reset_comps++;
+      stats.comps_non_reset++;
     }
     holder.lev(v) = counter->dec_level();
     holder.tstamp(v) = counter->get_tstamp();
@@ -392,6 +388,7 @@ end_sat:;
 CompAnalyzer::CompAnalyzer(
     const LiteralIndexedVector<TriValue> & lit_values,
     Counter* _counter) :
+      stats(_counter->get_stats()),
       values(lit_values),
       conf(_counter->get_conf()),
       indep_support_end(_counter->get_indep_support_end()),

src/comp_analyzer.hpp

@@ -110,7 +110,6 @@ struct MyHolder {
   uint32_t& orig_size_long(uint32_t v) { return data[v*hstride+offset+5];}
   void pop_back_long(uint32_t v) { size_long(v)--; }
   void resize_long(uint32_t v, uint32_t sz) { size_long(v) = sz; }
-
 };
 
 // There is exactly ONE of this, inside CompManager, which is inside counter
@@ -184,9 +183,7 @@ class CompAnalyzer {
   uint32_t max_clid = 0;
   uint32_t max_tri_clid = 0;
   uint32_t max_var = 0;
-  uint64_t reset_comps = 0;
-  uint64_t non_reset_comps = 0;
-  uint32_t comps_recorded = 0;
+  DataAndStatistics& stats;
 
   MyHolder holder;
   vector<Lit> long_clauses_data;

src/counter.cpp

@@ -2189,9 +2189,6 @@ bool Counter::propagate(bool out_of_order) {
   return confl.isNull();
 }
 
-const DataAndStatistics& Counter::get_stats() const {
-  return stats; }
-
 bool Counter::lit_redundant(Lit p, uint32_t abstract_levels) {
     debug_print(__func__ << " called");
 

src/counter.hpp

@@ -196,6 +196,7 @@ class Counter {
   const FG& get_fg() const { return fg; }
   const FF& get_two() const { return two; }
   bool weighted() const { return fg->weighted(); }
+  DataAndStatistics& get_stats() { return stats; }
 
 private:
   FG fg;
@@ -259,8 +260,6 @@ class Counter {
   vector<map<Lit, Lit>> generators;
   void symm_cubes(vector<Cube>& cubes);
 
-  const DataAndStatistics& get_stats() const;
-
   //Debug stuff
   FF check_count(const bool also_incl_curr_and_later_dec = false);
   bool is_implied(const vector<Lit>& cp);

src/statistics.cpp

@@ -115,6 +115,8 @@ void DataAndStatistics::print_short(const Counter* counter, const CompCache* cac
     << setw(5) << comp_sorts/1000 << " / "
     << setw(5) << std::setprecision(8) << safe_div(comp_sizes, comp_sorts))
     << std::setprecision(2);
+  verb_print(1, "comps recordK/non-reset ratio  " << comps_recorded/1000 << " / "
+        << (double)(comps_non_reset)/(double)(comps_reset+comps_non_reset));
 
   verb_print(1, "vivif: try/cls/clviv/litsravg  "
     << setw(9) << vivif_tried << " "

src/statistics.hpp

@@ -125,6 +125,9 @@ class DataAndStatistics {
   // Components
   uint64_t comp_sorts = 0;
   uint64_t comp_sizes = 0;
+  uint64_t comps_reset = 0;
+  uint64_t comps_non_reset = 0;
+  uint32_t comps_recorded = 0;
 
   uint64_t num_cached_comps = 0;
   uint64_t total_num_cached_comps = 0;