@@ -284,6 +284,13 @@ void CompAnalyzer::initialize(
284284 assert (cl.size () > 2 );
285285 const uint32_t long_cl_off = long_clauses_data.size ();
286286
287+ Lit example_blocking = NOT_A_LIT;
288+ auto & blk_lits = clid_to_blocking_lits[max_clid];
289+ if (!blk_lits.empty ()) {
290+ std::uniform_int_distribution<uint32_t > dist (0 , blk_lits.size ()-1 );
291+ example_blocking = blk_lits[dist (mtrand)];
292+ }
293+
287294 if (cl.size () > 3 ) {
288295 Lit blk_lit = cl[cl.size ()/2 ];
289296 for (const auto &l: cl) long_clauses_data.push_back (l);
@@ -294,7 +301,7 @@ void CompAnalyzer::initialize(
294301 ClData d;
295302 d.id = max_clid;
296303 d.blk_lit = blk_lit;
297- d.example_blocking = NOT_A_LIT ;
304+ d.example_blocking = example_blocking ;
298305 d.off = long_cl_off;
299306 unif_occ_long[var].push_back (d);
300307 }
@@ -308,7 +315,7 @@ void CompAnalyzer::initialize(
308315 ClData d;
309316 d.id = max_clid;
310317 d.blk_lit = lits[0 ];
311- d.example_blocking = NOT_A_LIT ;
318+ d.example_blocking = example_blocking ;
312319 d.off = lits[1 ].raw ();
313320 unif_occ_long[l.var ()].push_back (d);
314321 }
@@ -399,12 +406,6 @@ void CompAnalyzer::initialize(
399406 assert (unif_occ_long[v].size () == holder.size_long (v));
400407 for (uint32_t i = 0 ; i < unif_occ_long[v].size (); i++) {
401408 assert (unif_occ_long[v][i] == holder.begin_long (v)[i]);
402- auto & d = holder.begin_long (v)[i];
403- auto & blk_lits = clid_to_blocking_lits[d.id ];
404- if (!blk_lits.empty ()) {
405- std::uniform_int_distribution<uint32_t > dist (0 , blk_lits.size ()-1 );
406- d.example_blocking = blk_lits[dist (mtrand)];
407- }
408409 }
409410 }
410411 }
0 commit comments