Allow command line control, better printing

Author: msoos

src/comp_analyzer.cpp

@@ -46,6 +46,8 @@ void CompAnalyzer::calc_blocked(
 {
   const uint32_t n = max_var+1;
   clid_to_blocking_lits.resize(long_irred_cls.size()+1);
+  if (!conf.do_blocked_clauses) return;
+
   if (counter->get_opt_indep_support_end() >= max_var+1) {
     verb_print(1, "No need to calculate blocked clauses, as all vars are opt independent");
     return;
@@ -232,6 +234,7 @@ void CompAnalyzer::initialize(
   auto long_irred_cls = _long_irred_cls;
   std::stable_sort(long_irred_cls.begin(), long_irred_cls.end(), mysorter);
   calc_blocked(watches, alloc, long_irred_cls);
+  uint32_t example_blocked_cls = 0;
 
   max_clid = 1;
   max_tri_clid = 1;
@@ -252,6 +255,8 @@ void CompAnalyzer::initialize(
     if (!blk_lits.empty()) {
       std::shuffle(blk_lits.begin(), blk_lits.end(), mtrand);
       example_blocking = blk_lits[0];
+      verb_print(5, "Example blocking: " << example_blocking << " for cl: " << cl);
+      example_blocked_cls++;
     }
 
     if (cl.size() > 3) {
@@ -290,6 +295,8 @@ void CompAnalyzer::initialize(
     /* cout << endl; */
     max_clid++;
   }
+  verb_print(1, "Example blocked cls: " << example_blocked_cls << " / " << long_irred_cls.size()
+      << " = " << (double)example_blocked_cls/(double)long_irred_cls.size()*100 << "%");
   /* cout << "max clid: " << max_clid << " max_tri_clid: " << max_tri_clid << endl;; */
   debug_print(COLBLBACK "Built occ list in CompAnalyzer::initialize.");
 

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_blocked_clauses = 1;
 
   int cache_time_update = 2;
 

src/main.cpp

@@ -132,6 +132,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("--blocked", conf.do_blocked_clauses, atof, "Blocked clauses, semi-dynamic, with example lit");
 //
 // Arjun options
     myopt("--arjun", do_arjun, atoi, "Use arjun");