Fixing LSIDS update in varreplacer

src/varreplacer.cpp

@@ -125,48 +125,48 @@ void VarReplacer::printReplaceStats() const
     }
 }
 
+// Updating activities/data about variables.
+// Given: a V b
+//       -a V -b
+// Means: a = ~b
+//        a is replaced by ~b
+// Then:  orig = a
+//        replaced_with = ~b
 void VarReplacer::update_vardata_and_activities(
-    const uint32_t orig
-    , const uint32_t replaced_with
+    const Lit orig
+    , const Lit replaced_with
 ) {
+    uint32_t orig_var = orig.var();
+    uint32_t replaced_with_var = replaced_with.var();
+
     //Not replaced_with, or not replaceable, so skip
-    if (orig == replaced_with
-        || solver->varData[replaced_with].removed == Removed::decomposed
-        || solver->varData[replaced_with].removed == Removed::elimed
+    if (orig_var == replaced_with_var
+        || solver->varData[replaced_with_var].removed == Removed::decomposed
+        || solver->varData[replaced_with_var].removed == Removed::elimed
     ) {
         return;
     }
 
     //Has already been handled previously, just skip
-    if (solver->varData[orig].removed == Removed::replaced) {
+    if (solver->varData[orig_var].removed == Removed::replaced) {
         return;
     }
 
     //Okay, so unset decision, and set the other one decision
-    assert(orig != replaced_with);
-    solver->varData[orig].removed = Removed::replaced;
-    assert(solver->varData[replaced_with].removed == Removed::none);
-    assert(solver->value(replaced_with) == l_Undef);
-
-    double orig_act_vsids = solver->var_act_vsids[orig];
-    solver->var_act_vsids[replaced_with] += orig_act_vsids;
-
-    double orig_act_maple = solver->var_act_maple[orig];
-    solver->var_act_maple[replaced_with] += orig_act_maple;
-
-    assert(orig <= solver->nVars() && replaced_with <= solver->nVars());
+    assert(orig_var != replaced_with_var);
+    solver->varData[orig_var].removed = Removed::replaced;
+    assert(solver->varData[replaced_with_var].removed == Removed::none);
+    assert(solver->value(replaced_with_var) == l_Undef);
 
-    uint32_t neg_orig = Lit(orig,true).toInt();
-    uint32_t pos_orig = Lit(orig,false).toInt();
-    uint32_t neg_replaced_with = Lit(replaced_with,true).toInt();
-    uint32_t pos_replaced_with = Lit(replaced_with,false).toInt();
+    //Update activities
+    solver->var_act_vsids[replaced_with_var] += solver->var_act_vsids[orig_var];
+    solver->var_act_maple[replaced_with_var] += solver->var_act_maple[orig_var];
 
-    double orig_act_lsids_pos = solver->lit_act_lsids[pos_orig];
-    double orig_act_lsids_neg = solver->lit_act_lsids[neg_orig];
-
-    solver->lit_act_lsids[pos_replaced_with] += orig_act_lsids_pos;
-    solver->lit_act_lsids[neg_replaced_with] += orig_act_lsids_neg;
+    assert(orig_var <= solver->nVars() && replaced_with_var <= solver->nVars());
 
+    //Update LSIDS
+    solver->lit_act_lsids[replaced_with.toInt()] += solver->lit_act_lsids[orig.toInt()];
+    solver->lit_act_lsids[(~replaced_with).toInt()] += solver->lit_act_lsids[(~orig).toInt()];
 }
 
 bool VarReplacer::enqueueDelayedEnqueue()
@@ -213,8 +213,12 @@ void VarReplacer::update_all_vardata_activities()
         ; ++it, var++
     ) {
         const uint32_t orig = solver->map_outer_to_inter(var);
+        const Lit orig_lit = Lit(orig, false);
+
         const uint32_t repl = solver->map_outer_to_inter(it->var());
-        update_vardata_and_activities(orig, repl);
+        const Lit repl_lit = Lit(repl, it->sign());
+
+        update_vardata_and_activities(orig_lit, repl_lit);
     }
 }
 

src/varreplacer.h

@@ -148,8 +148,8 @@ class VarReplacer
         void attach_delayed_attach();
         void update_all_vardata_activities();
         void update_vardata_and_activities(
-            const uint32_t orig
-            , const uint32_t replaced
+            const Lit orig
+            , const Lit replaced
         );
         bool enqueueDelayedEnqueue();