Clean up

src/assign/propagate.rs

@@ -57,11 +57,8 @@ impl PropagateIF for AssignStack {
     fn assign_at_root_level(&mut self, l: Lit) -> MaybeInconsistent {
         self.cancel_until(self.root_level);
         let vi = l.vi();
-        // debug_assert!(vi < self.var.len());
-        // debug_assert!(!self.var[vi].is(FlagVar::ELIMINATED));
         debug_assert!(!VarRef(vi).is(FlagVar::ELIMINATED));
         debug_assert!(self.trail_lim.is_empty());
-        // self.var[vi].level = self.root_level;
         VarRef(vi).set_level(self.root_level);
         match VarRef(vi).assign() {
             None => {
@@ -96,26 +93,20 @@ impl PropagateIF for AssignStack {
         #[cfg(feature = "chrono_BT")] lv: DecisionLevel,
     ) {
         debug_assert!(usize::from(l) != 0, "Null literal is about to be enqueued");
-        // debug_assert!(l.vi() < self.var.len());
         // The following doesn't hold anymore by using chronoBT.
         // assert!(self.trail_lim.is_empty() || !cid.is_none());
         let vi = l.vi();
-        // debug_assert!(!self.var[vi].is(FlagVar::ELIMINATED));
         debug_assert!(!VarRef(vi).is(FlagVar::ELIMINATED));
         debug_assert_eq!(VarRef(vi).assign(), None);
-        // debug_assert_eq!(self.var[vi].reason, AssignReason::None);
         debug_assert_eq!(VarRef(vi).reason(), AssignReason::None);
         debug_assert!(self.trail.iter().all(|rl| *rl != l));
         VarRef::set_lit(l);
 
         #[cfg(not(feature = "chrono_BT"))]
         let lv = self.decision_level();
 
-        // self.var[vi].level = lv;
         VarRef(vi).set_level(lv);
-        // self.var[vi].reason = reason;
         VarRef(vi).set_reason(reason);
-        // self.reward_at_assign(vi);
         VarActivityManager::reward_at_assign(vi);
         debug_assert!(!self.trail.contains(&l));
         debug_assert!(!self.trail.contains(&!l));
@@ -134,7 +125,6 @@ impl PropagateIF for AssignStack {
     }
     fn assign_by_decision(&mut self, l: Lit) {
         debug_assert_ne!(VarRef(l.vi()).assign(), Some(!bool::from(l)));
-        // debug_assert!(l.vi() < self.var.len());
         debug_assert!(!self.trail.contains(&l));
         debug_assert!(
             !self.trail.contains(&!l),
@@ -149,7 +139,6 @@ impl PropagateIF for AssignStack {
         debug_assert_eq!(VarRef(vi).reason(), AssignReason::None);
         VarRef::set_lit(l);
         VarRef(vi).set_reason(AssignReason::Decision(self.decision_level()));
-        // self.reward_at_assign(vi);
         VarActivityManager::reward_at_assign(vi);
         self.trail.push(l);
         self.num_decisions += 1;
@@ -179,7 +168,6 @@ impl PropagateIF for AssignStack {
                 VarRef(l.vi()).assign().is_some(),
                 "cancel_until found unassigned var in trail {}",
                 l.vi(),
-                // &self.var[l.vi()],
             );
             let vi = l.vi();
             #[cfg(feature = "debug_propagation")]

src/assign/stack.rs

@@ -148,7 +148,6 @@ impl Instantiate for AssignStack {
             SolverEvent::Eliminate(vi) => {
                 debug_assert_eq!(self.decision_level(), self.root_level());
                 debug_assert!(self.trail.iter().all(|l| l.vi() != vi));
-                // self.trail.retain(|l| l.vi() != vi);
                 self.num_eliminated_vars += 1;
             }
             SolverEvent::Stage(scale) => {

src/assign/trail_saving.rs

@@ -39,24 +39,17 @@ impl TrailSavingIF for AssignStack {
                 // }
 
                 self.trail_saved.push(l);
-                // self.var[vi].reason_saved = self.var[vi].reason;
                 VarRef(vi).set_reason_saved(VarRef(vi).reason());
-                // self.reward_at_unassign(vi);
                 VarActivityManager::reward_at_unassign(vi);
-                if activity_threshold <= VarRef(vi).activity()
-                /* self.var[vi].reward */
-                {
-                    // self.insert_heap(vi);
+                if activity_threshold <= VarRef(vi).activity() {
                     VarActivityManager::insert_heap(vi);
                 }
             }
             free = lim2;
         }
         for i in free..self.trail.len() {
             let vi = self.trail[i].vi();
-            // self.reward_at_unassign(vi);
             VarActivityManager::reward_at_unassign(vi);
-            // self.insert_heap(vi);
             VarActivityManager::insert_heap(vi);
         }
     }
@@ -86,7 +79,6 @@ impl TrailSavingIF for AssignStack {
                 }
                 // reason refinement by ignoring this dependecy
                 (None, AssignReason::Implication(c)) if q < cdb[c].rank => {
-                    // self.insert_heap(vi);
                     VarActivityManager::insert_heap(vi);
                     return self.truncate_trail_saved(i + 1);
                 }
@@ -122,7 +114,6 @@ impl TrailSavingIF for AssignStack {
                 }
                 (_, AssignReason::Decision(lvl)) => {
                     debug_assert_ne!(0, lvl);
-                    // self.insert_heap(vi);
                     VarActivityManager::insert_heap(vi);
                     return self.truncate_trail_saved(i + 1);
                 }
@@ -135,7 +126,6 @@ impl TrailSavingIF for AssignStack {
     fn clear_saved_trail(&mut self) {
         for j in 0..self.trail_saved.len() {
             let l = self.trail_saved[j];
-            // self.insert_heap(l.vi());
             VarActivityManager::insert_heap(l.vi());
         }
         self.trail_saved.clear();

src/cdb/vivify.rs

@@ -68,7 +68,6 @@ impl VivifyIF for ClauseDB {
             debug_assert!(clits.iter().all(|l| !clits.contains(&!*l)));
             let mut decisions: Vec<Lit> = Vec::new();
             for lit in clits.iter().copied() {
-                // assert!(!asg.var(lit.vi()).is(FlagVar::ELIMINATED));
                 match VarRef::lit_assigned(!lit) {
                     //## Rule 1
                     Some(false) => (),

src/processor/simplify.rs

@@ -271,10 +271,7 @@ impl EliminateIF for Eliminator {
         {
             for (i, _) in asg.var_iter().enumerate().skip(1) {
                 if asg.reason(i) != AssignReason::None {
-                    assert_eq!(
-                        asg.level(i),
-                        asg.derefer(assign::property::Tusize::RootLevel) as DecisionLevel
-                    );
+                    assert_eq!(asg.level(i), asg.root_level() as DecisionLevel,);
                     // asg.reason(v.index) = AssignReason::None;
                 }
             }
@@ -287,7 +284,7 @@ impl EliminateIF for Eliminator {
             self.subsume_literal_limit =
                 state.config.elm_cls_lim + cdb.lb_entanglement().get() as usize;
             debug_assert!(!cdb.lb_entanglement().get().is_nan());
-            // self.eliminate_combination_limit = cdb.derefer(cdb::property::Tf64::LiteralBlockEntanglement);
+            // self.eliminate_combination_limit = cdb.lb_entanglement().get() as usize;
             self.eliminate(asg, cdb, state)?;
         } else {
             asg.propagate_sandbox(cdb)

src/solver/search.rs

@@ -282,7 +282,6 @@ fn search(
             if cfg!(feature = "reward_annealing") {
                 let base = state.stm.current_stage() - state.stm.cycle_starting_stage();
                 let decay_index: f64 = (20 + 2 * base) as f64;
-                // asg.update_activity_decay((decay_index - 1.0) / decay_index);
                 VarActivityManager::set_activity_decay((decay_index - 1.0) / decay_index);
             }
             if let Some(new_segment) = next_stage {
@@ -360,7 +359,6 @@ fn search(
                     {
                         let base = state.stm.current_segment();
                         let decay_index: f64 = (20 + 2 * base) as f64;
-                        // asg.update_activity_decay((decay_index - 1.0) / decay_index);
                         VarActivityManager::set_activity_decay((decay_index - 1.0) / decay_index);
                     }
                     if cfg!(feature = "clause_elimination") {

src/vam.rs

@@ -181,7 +181,6 @@ impl VarSelectIF for VarActivityManager {
                     VarRef(*vi).set_activity(
                         VarRef(*vi).activity() * VAM.activity_decay + VAM.activity_anti_decay,
                     );
-                    // self.update_heap(*vi);
                     VarActivityManager::update_heap(*vi);
                 }
             }
@@ -197,15 +196,12 @@ impl VarSelectIF for VarActivityManager {
         }
     }
     fn update_order(v: VarId) {
-        // self.update_heap(v);
         VarActivityManager::update_heap(v);
     }
     fn rebuild_order() {
-        // self.clear_heap();
         VarActivityManager::clear_heap();
         for vi in VarRef::var_id_iter() {
             if VarRef(vi).assign().is_none() && !VarRef(vi).is(FlagVar::ELIMINATED) {
-                // self.insert_heap(vi);
                 VarActivityManager::insert_heap(vi);
             }
         }

src/var_vector.rs

@@ -65,15 +65,17 @@ impl VarRef {
         }
     }
     pub fn rescale_activity(scaling: f64) {
-        for i in VarRef::var_id_iter() {
-            VarRef(i).set_activity(VarRef(i).activity() * scaling);
+        unsafe {
+            for i in VarRef::var_id_iter() {
+                VAR_VECTOR.get_unchecked_mut(i).activity *= scaling;
+            }
         }
     }
     /// set `vi`s status to asserted.
     pub fn make_var_asserted(vi: VarId) {
         unsafe {
-            VAR_VECTOR[vi].reason = AssignReason::Decision(0);
-            VAR_VECTOR[vi].activity = 0.0;
+            VAR_VECTOR.get_unchecked_mut(vi).reason = AssignReason::Decision(0);
+            VAR_VECTOR.get_unchecked_mut(vi).activity = 0.0;
         }
         VarActivityManager::remove_from_heap(vi);
 
@@ -86,18 +88,19 @@ impl VarRef {
     /// return true if `vi` is just eliminated.
     pub fn make_var_eliminated(vi: VarId) -> bool {
         unsafe {
-            if VAR_VECTOR[vi].is(FlagVar::ELIMINATED) {
+            let v = VAR_VECTOR.get_unchecked_mut(vi);
+            if v.is(FlagVar::ELIMINATED) {
                 #[cfg(feature = "boundary_check")]
                 panic!("double elimination");
                 false
             } else {
-                VAR_VECTOR[vi].turn_on(FlagVar::ELIMINATED);
-                VAR_VECTOR[vi].activity = 0.0;
+                v.turn_on(FlagVar::ELIMINATED);
+                v.activity = 0.0;
                 VarActivityManager::remove_from_heap(vi);
 
                 #[cfg(feature = "boundary_check")]
                 {
-                    self.var[vi].timestamp = self.tick;
+                    v.timestamp = self.tick;
                 }
                 true
             }