Better example generation

Author: msoos

src/comp_analyzer.cpp

@@ -30,7 +30,6 @@ THE SOFTWARE.
 #include <cstdint>
 #include <cstdint>
 #include <memory>
-#include <ratio>
 
 using namespace GanakInt;
 
@@ -46,7 +45,7 @@ void CompAnalyzer::calc_blocked(
     const ClauseAllocator* alloc, const vector<ClauseOfs>& long_irred_cls)
 {
   const uint32_t n = max_var+1;
-  lit_to_blocked_clids.resize(n*2);
+  clid_to_blocking_lits.resize(long_irred_cls.size()+1);
   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;
@@ -196,15 +195,14 @@ void CompAnalyzer::calc_blocked(
           }
           if (!blocked) continue; // try next var
           if (blocked) {
-            cout << "BINGO! cl: " << cl << " blocked on: " << l << " given: " << l_set << endl;
-            clids_blocked.push_back(clid);
+            /* cout << "BINGO! cl: " << cl << " blocked on: " << l << " given: " << l_set << endl; */
+            clid_to_blocking_lits[clid].push_back(l_set);
             break;
           }
         }
         for(const auto& l: cl) seen[l.raw()] = 0;
       }
       blocked_tot += clids_blocked.size();
-      lit_to_blocked_clids[l_set.raw()] = clids_blocked;
       for(const auto& l: seen_set_clear) seen_set[l.raw()] = 0;
       seen_set_clear.clear();
     }
@@ -243,26 +241,18 @@ void CompAnalyzer::initialize(
   long_clauses_data.clear();
   long_clauses_data.push_back(SENTINEL_LIT); // MUST start with a sentinel!
   vector<uint32_t> tmp;
+  std::mt19937_64 mtrand(conf.seed);
   for (const auto& off: long_irred_cls) {
     const Clause& cl = *alloc->ptr(off);
     assert(cl.size() > 2);
     const uint32_t long_cl_off = long_clauses_data.size();
 
-      Lit example_blocking = NOT_A_LIT;
-      bool found = false;
-      for (int32_t v = n-1; v >= 1; v--) {
-        for(uint32_t i2 = 0; i2 < 2; i2++) {
-          Lit b = Lit(v, i2);
-          const auto& list = lit_to_blocked_clids[b.raw()];
-          if (std::find(list.begin(), list.end(), max_clid) != list.end()) {
-            example_blocking = b;
-            cout << "Example blocking: " << example_blocking << " for cl: " << cl << " id: " << max_clid << endl;
-            found = true;
-            break;
-          }
-        }
-        if (found) break;
-      }
+    Lit example_blocking = NOT_A_LIT;
+    auto& blk_lits =clid_to_blocking_lits[max_clid];
+    if (!blk_lits.empty()) {
+      std::shuffle(blk_lits.begin(), blk_lits.end(), mtrand);
+      example_blocking = blk_lits[0];
+    }
 
     if (cl.size() > 3) {
       Lit blk_lit = cl[cl.size()/2];

src/comp_analyzer.hpp

@@ -181,7 +181,7 @@ class CompAnalyzer {
 private:
   void calc_blocked(const LiteralIndexedVector<LitWatchList> & literals,
       const ClauseAllocator* alloc, const vector<ClauseOfs>& long_irred_cls);
-  vector<vector<uint32_t>> lit_to_blocked_clids;
+  vector<vector<Lit>> clid_to_blocking_lits;
 
   // the id of the last clause
   // note that clause ID is the clause number,