Stats now, working

Author: msoos

src/comp_analyzer.cpp

@@ -213,11 +213,19 @@ bool CompAnalyzer::explore_comp(const uint32_t v, const uint32_t sup_comp_long_c
   return true;
 }
 
+void CompAnalyzer::maybe_reset_var(const uint32_t v) {
+  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++;
+  }
+}
+
 // Each variable knows the level it was visited at, and the stimestamp at the time
 // Each level knows the HIGHEST stamp it has been seen
 // When checking a var, we go to the level, see the stamp, if it's larger than the stamp of the var,
 // we need to reset the size
-
+//
 // Create a component based on variable provided
 void CompAnalyzer::record_comp(const uint32_t var, const uint32_t sup_comp_long_cls, const uint32_t sup_comp_bin_cls) {
   SLOW_DEBUG_DO(assert(is_unknown(var)));

src/comp_analyzer.hpp

@@ -176,6 +176,7 @@ class CompAnalyzer {
   uint32_t get_bin_cls() const { return archetype.num_bin_cls; }
   uint32_t get_max_var() const { return max_var; }
   CompArchetype& get_archetype() { return archetype; }
+  void maybe_reset_var(const uint32_t v);
 
 private:
   // the id of the last clause

src/comp_management.cpp

@@ -101,10 +101,13 @@ void CompManager::record_remaining_comps_for(StackLevel &top) {
   const Comp& super_comp = get_super_comp(top);
   const uint32_t new_comps_start_ofs = comp_stack.size();
 
-  if (counter->dec_level() >= 1 && !counter->check_any_new_sat(super_comp.get_trail_sz())) {
+  if (conf.do_sat_cl_check && counter->dec_level() >= 1 && !counter->check_any_new_sat(super_comp.get_trail_sz())) {
     Comp *p_new_comp = copy_comp(&super_comp, counter);
+    all_vars_in_comp(*p_new_comp, vt) ana.maybe_reset_var(*vt);
     deal_with_new_comp(top, super_comp, p_new_comp);
+    stats.no_new_sat_cls++;
   } else {
+    stats.new_sat_cls++;
     // This reinitializes archetype, sets up seen[] or all cls&vars unvisited (if unset), etc.
     // Sets all unknown vars in seen[] and sets all clauses in seen[] to unvisited
     // Also zeroes out frequency_scores. Sets num_long_cls and num_bin_cls to 0

src/counter.cpp

@@ -4280,6 +4280,6 @@ bool Counter::check_any_new_sat(uint32_t prev_trail) const {
       if (!already_sat) return true;
     }
   }
-  cout << "returning FALSE from linkin_any_sat, prev trail:" << prev_trail << " trail now: " << trail.size() << endl;
+  /* cout << "returning FALSE from linkin_any_sat, prev trail:" << prev_trail << " trail now: " << trail.size() << endl; */
   return false;
 }

src/counter_config.hpp

@@ -40,6 +40,7 @@ struct CounterConfiguration {
   int max_num_rst = -1;
   uint32_t lbd_cutoff_always_keep_cube = 3;
   uint32_t max_num_cubes_per_restart = 6;
+  int do_sat_cl_check = 1;
 
   int cache_time_update = 2;
 

src/main.cpp

@@ -133,6 +133,7 @@ void add_ganak_options()
     myopt("--appmct", conf.appmc_timeout, atof, "after K seconds");
     myopt("--epsilon", conf.appmc_epsilon, atof, "AppMC epsilon");
     myopt("--chronobt", conf.do_chronobt, atof, "ChronoBT. SAT must be DISABLED or this will fail");
+    myopt("--satclcheck", conf.do_sat_cl_check, atoi, "If no SAT clauses since last time, copy component");
 //
 // Arjun options
     myopt("--arjun", do_arjun, atoi, "Use arjun");

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, "comp not recompute due to sat  " << no_new_sat_cls << " / " << new_sat_cls << " perc: "
+      << safe_div(no_new_sat_cls, (no_new_sat_cls+new_sat_cls)));
 
   verb_print(1, "vivif: try/cls/clviv/litsravg  "
     << setw(9) << vivif_tried << " "

src/statistics.hpp

@@ -125,6 +125,8 @@ class DataAndStatistics {
   // Components
   uint64_t comp_sorts = 0;
   uint64_t comp_sizes = 0;
+  uint64_t no_new_sat_cls = 0;
+  uint64_t new_sat_cls = 0;
 
   uint64_t num_cached_comps = 0;
   uint64_t total_num_cached_comps = 0;