Remove AssignIF from AssignStack

src/assign/learning_rate.rs

@@ -1,10 +1,7 @@
-/// Var Rewarding based on Learning Rate Rewarding and Reason Side Rewarding
-use {
-    super::stack::AssignStack,
-    crate::{types::*, var_vector::*},
-};
+//! Var Rewarding based on Learning Rate Rewarding and Reason Side Rewarding
+// use crate::{types::*, var_vector::*};
 
-impl ActivityIF<VarId> for AssignStack {
+/* impl ActivityIF<VarId> for AssignStack {
     #[inline]
     fn activity(&self, vi: VarId) -> f64 {
         // self.var[vi].reward
@@ -39,4 +36,4 @@ impl ActivityIF<VarId> for AssignStack {
     fn update_activity_tick(&mut self) {
         self.tick += 1;
     }
-}
+}*/

src/assign/mod.rs

@@ -35,8 +35,8 @@ pub use self::trail_saving::TrailSavingIF;
 /// [`stack`](`crate::assign::AssignIF::stack`),
 /// [`best_assigned`](`crate::assign::AssignIF::best_assigned`), and so on.
 pub trait AssignIF:
-    ActivityIF<VarId>
-    + Instantiate
+    // ActivityIF<VarId>
+    Instantiate
     + PropagateIF
     + VarManipulateIF
     + PropertyDereference<property::Tusize, usize>

src/assign/propagate.rs

@@ -140,7 +140,8 @@ impl PropagateIF for AssignStack {
         VarRef(vi).set_level(lv);
         // self.var[vi].reason = reason;
         VarRef(vi).set_reason(reason);
-        self.reward_at_assign(vi);
+        // self.reward_at_assign(vi);
+        VarActivityManager::reward_at_assign(vi);
         debug_assert!(!self.trail.contains(&l));
         debug_assert!(!self.trail.contains(&!l));
         self.trail.push(l);
@@ -175,7 +176,8 @@ impl PropagateIF for AssignStack {
         debug_assert_eq!(VarRef(vi).reason(), AssignReason::None);
         set_assign!(self, l);
         VarRef(vi).set_reason(AssignReason::Decision(self.decision_level()));
-        self.reward_at_assign(vi);
+        // self.reward_at_assign(vi);
+        VarActivityManager::reward_at_assign(vi);
         self.trail.push(l);
         self.num_decision += 1;
         debug_assert!(self.q_head < self.trail.len());

src/assign/stack.rs

@@ -76,14 +76,14 @@ pub struct AssignStack {
     /// var activity decay
     pub(super) activity_decay: f64,
     /// the default value of var activity decay in configuration
-    #[cfg(feature = "EVSIDS")]
-    activity_decay_default: f64,
+    // #[cfg(feature = "EVSIDS")]
+    // activity_decay_default: f64,
     /// its diff
     pub(super) activity_anti_decay: f64,
-    #[cfg(feature = "EVSIDS")]
-    activity_decay_step: f64,
-    /// an index for counting elapsed time
-    pub(super) tick: usize,
+    // #[cfg(feature = "EVSIDS")]
+    // activity_decay_step: f64,
+    // /// an index for counting elapsed time
+    // pub(super) tick: usize,
 }
 
 impl Default for AssignStack {
@@ -125,7 +125,7 @@ impl Default for AssignStack {
             ppc_ema: EmaSU::new(100),
             cpr_ema: EmaSU::new(100),
 
-            tick: 0,
+            // tick: 0,
             // var: Vec::new(),
             activity_decay: 0.94,
 
@@ -370,7 +370,8 @@ impl VarManipulateIF for AssignStack {
     fn make_var_asserted(&mut self, vi: VarId) {
         // self.var[vi].reason = AssignReason::Decision(0);
         VarRef(vi).set_reason(AssignReason::Decision(0));
-        self.set_activity(vi, 0.0);
+        // self.set_activity(vi, 0.0);
+        VarRef(vi).set_activity(0.0);
         // self.remove_from_heap(vi);
         VarActivityManager::remove_from_heap(vi);
 
@@ -385,7 +386,8 @@ impl VarManipulateIF for AssignStack {
     fn make_var_eliminated(&mut self, vi: VarId) {
         if !VarRef(vi).is(FlagVar::ELIMINATED) {
             VarRef(vi).turn_on(FlagVar::ELIMINATED);
-            self.set_activity(vi, 0.0);
+            // self.set_activity(vi, 0.0);
+            VarRef(vi).set_activity(0.0);
             // self.remove_from_heap(vi);
             VarActivityManager::remove_from_heap(vi);
             debug_assert_eq!(self.decision_level(), self.root_level);

src/assign/trail_saving.rs

@@ -41,7 +41,8 @@ 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);
+                // self.reward_at_unassign(vi);
+                VarActivityManager::reward_at_unassign(vi);
                 if activity_threshold <= VarRef(vi).activity()
                 /* self.var[vi].reward */
                 {
@@ -53,7 +54,8 @@ impl TrailSavingIF for AssignStack {
         }
         for i in free..self.trail.len() {
             let vi = self.trail[i].vi();
-            self.reward_at_unassign(vi);
+            // self.reward_at_unassign(vi);
+            VarActivityManager::reward_at_unassign(vi);
             // self.insert_heap(vi);
             VarActivityManager::insert_heap(vi);
         }

src/cdb/db.rs

@@ -1059,10 +1059,10 @@ impl ClauseDBIF for ClauseDB {
             alives += 1;
             match setting {
                 ReductionType::RASonADD(_) => {
-                    perm.push(OrderedProxy::new(i, c.reverse_activity_sum(asg)));
+                    perm.push(OrderedProxy::new(i, c.reverse_activity_sum()));
                 }
                 ReductionType::RASonALL(cutoff, _) => {
-                    let value = c.reverse_activity_sum(asg);
+                    let value = c.reverse_activity_sum();
                     if cutoff < value.min(c.rank_old as f64) {
                         perm.push(OrderedProxy::new(i, value));
                     }
@@ -1387,8 +1387,8 @@ impl Clause {
         }
         falsified
     }
-    fn reverse_activity_sum(&self, asg: &impl AssignIF) -> f64 {
-        self.iter().map(|l| 1.0 - asg.activity(l.vi())).sum()
+    fn reverse_activity_sum(&self) -> f64 {
+        self.iter().map(|l| 1.0 - VarRef(l.vi()).activity()).sum()
     }
     fn lbd(&self) -> f64 {
         self.rank as f64

src/config.rs

@@ -85,8 +85,8 @@ pub struct Config {
     //
     /// Var Reward Decay Rate
     pub vrw_dcy_rat: f64,
-    /// Decay increment step.
-    pub vrw_dcy_stp: f64,
+    // /// Decay increment step.
+    // pub vrw_dcy_stp: f64,
 }
 
 impl Default for Config {

src/solver/conflict.rs

@@ -2,6 +2,7 @@
 
 #[cfg(feature = "boundary_check")]
 use crate::assign::DebugReportIF;
+use crate::vam::VarActivityManager;
 
 use {
     super::State,
@@ -137,7 +138,8 @@ pub fn handle_conflict(
         //
         //## Learnt Literal Rewarding
         //
-        asg.reward_at_analysis(lit.vi());
+        // asg.reward_at_analysis(lit.vi());
+        VarActivityManager::reward_at_analysis(lit.vi());
 
         //
         //## Reason-Side Rewarding
@@ -147,15 +149,17 @@ pub fn handle_conflict(
             AssignReason::BinaryLink(from) => {
                 let vi = from.vi();
                 if !bumped.contains(&vi) {
-                    asg.reward_at_analysis(vi);
+                    // asg.reward_at_analysis(vi);
+                    VarActivityManager::reward_at_analysis(vi);
                     bumped.push(vi);
                 }
             }
             AssignReason::Implication(r) => {
                 for l in cdb[r].iter() {
                     let vi = l.vi();
                     if !bumped.contains(&vi) {
-                        asg.reward_at_analysis(vi);
+                        // asg.reward_at_analysis(vi);
+                        VarActivityManager::reward_at_analysis(vi);
                         bumped.push(vi);
                     }
                 }
@@ -274,7 +278,8 @@ fn conflict_analyze(
         ($vi: expr) => {
             path_cnt += 1;
             //## Conflict-Side Rewarding
-            asg.reward_at_analysis($vi);
+            // asg.reward_at_analysis($vi);
+            VarActivityManager::reward_at_analysis($vi);
         };
     }
     macro_rules! trace {

src/solver/search.rs

@@ -10,6 +10,7 @@ use {
         processor::{EliminateIF, Eliminator},
         state::{Stat, State, StateIF},
         types::*,
+        vam::VarActivityManager,
         var_vector::*,
     },
 };
@@ -152,7 +153,8 @@ impl SolveIF for Solver {
                     let act = 1.0 / (VarRef::num_vars() as f64).powf(0.25);
                     for vi in VarRef::var_id_iter() {
                         if !VarRef(vi).is(FlagVar::ELIMINATED) {
-                            asg.set_activity(vi, act);
+                            // asg.set_activity(vi, act);
+                            VarRef(vi).set_activity(act);
                         }
                     }
                     asg.rebuild_order();
@@ -247,7 +249,9 @@ fn search(
         if asg.decision_level() == asg.root_level() {
             return Err(SolverError::RootLevelConflict(cc));
         }
-        asg.update_activity_tick();
+        // asg.update_activity_tick();
+        #[cfg(feature = "boundary_check")]
+        VarActivityManager::update_activity_tick();
         #[cfg(feature = "clause_rewarding")]
         cdb.update_activity_tick();
         if 1 < handle_conflict(asg, cdb, state, &cc)? {
@@ -275,7 +279,8 @@ 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);
+                // 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 {
                 // a beginning of a new cycle
@@ -352,7 +357,8 @@ 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);
+                        // 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") {
                         let mut elim = Eliminator::instantiate(&state.config, &state.cnf);

src/vam.rs

@@ -11,12 +11,14 @@ use crate::assign::TrailSavingIF;
 pub struct VarActivityManager {
     decay: f64,
     anti_decay: f64,
+    #[cfg(feature = "boundary_check")]
     tick: usize,
 }
 
 pub static mut VAM: VarActivityManager = VarActivityManager {
     decay: 0.95,
     anti_decay: 0.05,
+    #[cfg(feature = "boundary_check")]
     tick: 0,
 };
 
@@ -99,7 +101,8 @@ impl VarActivityManager {
     // pub fn pop_top_var(asg: &mut AssignStack) -> VarId {
     //     unsafe { VAR_HEAP.get_heap_root(asg) }
     // }
-    pub fn increment_tick() {
+    #[cfg(feature = "boundary_check")]
+    pub fn update_activity_tick() {
         unsafe {
             VAM.tick += 1;
         }