Switch from AssignStack::var_order to vam::VAR_HEAP

src/assign/mod.rs

@@ -3,8 +3,6 @@
 
 /// Ema
 mod ema;
-/// Heap
-mod heap;
 /// Boolean constraint propagation
 mod propagate;
 /// Var rewarding

src/assign/propagate.rs

@@ -1,8 +1,8 @@
 // implement boolean constraint propagation, backjump
 // This version can handle Chronological and Non Chronological Backtrack.
 use {
-    super::{heap::VarHeapIF, AssignIF, AssignStack, VarManipulateIF},
-    crate::{cdb::ClauseDBIF, types::*, var_vector::*},
+    super::{AssignIF, AssignStack, VarManipulateIF},
+    crate::{cdb::ClauseDBIF, types::*, vam::VarActivityManager, var_vector::*},
 };
 
 #[cfg(feature = "trail_saving")]
@@ -290,7 +290,8 @@ impl PropagateIF for AssignStack {
             debug_assert!(self.root_level < VarRef(vi).level());
             unset_assign!(self, vi);
             VarRef(vi).set_reason(AssignReason::None);
-            self.insert_heap(vi);
+            // self.insert_heap(vi);
+            VarActivityManager::insert_heap(vi);
         }
         self.trail.truncate(lim);
         self.trail_lim.truncate(self.root_level as usize);

src/assign/select.rs

@@ -4,8 +4,8 @@
 use super::property;
 
 use {
-    super::{heap::VarHeapIF, stack::AssignStack},
-    crate::{types::*, var_vector::*},
+    super::stack::AssignStack,
+    crate::{types::*, vam::*, var_vector::*},
     std::collections::HashMap,
 };
 
@@ -83,7 +83,8 @@ impl VarSelectIF for AssignStack {
                 VarRef(*vi).set_activity(
                     VarRef(*vi).activity() * self.activity_decay + self.activity_anti_decay,
                 );
-                self.update_heap(*vi);
+                // self.update_heap(*vi);
+                VarActivityManager::update_heap(*vi);
             }
         }
         num_flipped
@@ -123,13 +124,16 @@ impl VarSelectIF for AssignStack {
         Lit::from((vi, VarRef(vi).is(FlagVar::PHASE)))
     }
     fn update_order(&mut self, v: VarId) {
-        self.update_heap(v);
+        // self.update_heap(v);
+        VarActivityManager::update_heap(v);
     }
     fn rebuild_order(&mut self) {
-        self.clear_heap();
+        // 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);
+                // self.insert_heap(vi);
+                VarActivityManager::insert_heap(vi);
             }
         }
     }
@@ -139,7 +143,7 @@ impl AssignStack {
     /// select a decision var
     fn select_var(&mut self) -> VarId {
         loop {
-            let vi = self.get_heap_root();
+            let vi = VarActivityManager::get_heap_root(self); // self.get_heap_root();
             if var_assign!(self, vi).is_none() && !VarRef(vi).is(FlagVar::ELIMINATED) {
                 return vi;
             }

src/assign/stack.rs

@@ -1,7 +1,7 @@
 //! main struct AssignStack
 use {
-    super::{ema::ProgressASG, heap::VarHeapIF, heap::VarIdHeap, AssignIF, PropagateIF},
-    crate::{cdb::ClauseDBIF, types::*, var_vector::*},
+    super::{ema::ProgressASG, AssignIF, PropagateIF},
+    crate::{cdb::ClauseDBIF, types::*, vam::VarActivityManager, var_vector::*},
     std::{fmt, ops::Range, slice::Iter},
 };
 
@@ -20,8 +20,7 @@ pub struct AssignStack {
     /// the-number-of-assigned-and-propagated-vars + 1
     pub(super) q_head: usize,
     pub root_level: DecisionLevel,
-    pub(super) var_order: VarIdHeap, // Variable Order
-
+    // pub(super) var_order: VarIdHeap, // Variable Order
     #[cfg(feature = "trail_saving")]
     pub(super) trail_saved: Vec<Lit>,
 
@@ -94,8 +93,7 @@ impl Default for AssignStack {
             trail_lim: Vec::new(),
             q_head: 0,
             root_level: 0,
-            var_order: VarIdHeap::default(),
-
+            // var_order: VarIdHeap::default(),
             #[cfg(feature = "trail_saving")]
             trail_saved: Vec::new(),
 
@@ -161,8 +159,7 @@ impl Instantiate for AssignStack {
         let nv = cnf.num_of_variables;
         AssignStack {
             trail: Vec::with_capacity(nv),
-            var_order: VarIdHeap::new(nv),
-
+            // var_order: VarIdHeap::new(nv),
             #[cfg(feature = "trail_saving")]
             trail_saved: Vec::with_capacity(nv),
 
@@ -198,7 +195,8 @@ impl Instantiate for AssignStack {
                 self.clear_saved_trail();
             }
             SolverEvent::NewVar => {
-                self.expand_heap();
+                // self.expand_heap();
+                VarActivityManager::expand_heap();
                 // self.var.push(Var::default());
             }
             SolverEvent::Reinitialize => {
@@ -373,7 +371,8 @@ impl VarManipulateIF for AssignStack {
         // self.var[vi].reason = AssignReason::Decision(0);
         VarRef(vi).set_reason(AssignReason::Decision(0));
         self.set_activity(vi, 0.0);
-        self.remove_from_heap(vi);
+        // self.remove_from_heap(vi);
+        VarActivityManager::remove_from_heap(vi);
 
         #[cfg(feature = "boundary_check")]
         {
@@ -387,7 +386,8 @@ impl VarManipulateIF for AssignStack {
         if !VarRef(vi).is(FlagVar::ELIMINATED) {
             VarRef(vi).turn_on(FlagVar::ELIMINATED);
             self.set_activity(vi, 0.0);
-            self.remove_from_heap(vi);
+            // self.remove_from_heap(vi);
+            VarActivityManager::remove_from_heap(vi);
             debug_assert_eq!(self.decision_level(), self.root_level);
             self.trail.retain(|l| l.vi() != vi);
             self.num_eliminated_vars += 1;
@@ -457,6 +457,7 @@ mod tests {
             ..CNFDescription::default()
         };
         VarRef::initialize(4);
+        VarActivityManager::initialize();
         let mut asg = AssignStack::instantiate(&config, &cnf);
         // [] + 1 => [1]
         assert!(asg.assign_at_root_level(lit(1)).is_ok());

src/assign/trail_saving.rs

@@ -2,8 +2,8 @@
 /// implement boolean constraint propagation, backjump
 /// This version can handle Chronological and Non Chronological Backtrack.
 use {
-    super::{heap::VarHeapIF, AssignStack, PropagateIF},
-    crate::{cdb::ClauseDBIF, types::*, var_vector::*},
+    super::{AssignStack, PropagateIF},
+    crate::{cdb::ClauseDBIF, types::*, vam::VarActivityManager, var_vector::*},
 };
 
 #[cfg(feature = "chrono_BT")]
@@ -45,15 +45,17 @@ impl TrailSavingIF for AssignStack {
                 if activity_threshold <= VarRef(vi).activity()
                 /* self.var[vi].reward */
                 {
-                    self.insert_heap(vi);
+                    // self.insert_heap(vi);
+                    VarActivityManager::insert_heap(vi);
                 }
             }
             free = lim2;
         }
         for i in free..self.trail.len() {
             let vi = self.trail[i].vi();
             self.reward_at_unassign(vi);
-            self.insert_heap(vi);
+            // self.insert_heap(vi);
+            VarActivityManager::insert_heap(vi);
         }
     }
     fn reuse_saved_trail(&mut self, cdb: &impl ClauseDBIF) -> PropagationResult {
@@ -83,7 +85,8 @@ impl TrailSavingIF for AssignStack {
                 }
                 // reason refinement by ignoring this dependecy
                 (None, AssignReason::Implication(c)) if q < cdb[c].rank => {
-                    self.insert_heap(vi);
+                    // self.insert_heap(vi);
+                    VarActivityManager::insert_heap(vi);
                     return self.truncate_trail_saved(i + 1);
                 }
                 (None, AssignReason::Implication(cid)) => {
@@ -116,7 +119,8 @@ impl TrailSavingIF for AssignStack {
                 }
                 (_, AssignReason::Decision(lvl)) => {
                     debug_assert_ne!(0, lvl);
-                    self.insert_heap(vi);
+                    // self.insert_heap(vi);
+                    VarActivityManager::insert_heap(vi);
                     return self.truncate_trail_saved(i + 1);
                 }
                 _ => unreachable!("from_saved_trail"),
@@ -128,7 +132,8 @@ 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());
+            // self.insert_heap(l.vi());
+            VarActivityManager::insert_heap(l.vi());
         }
         self.trail_saved.clear();
     }

src/solver/build.rs

@@ -5,6 +5,7 @@ use {
         assign::{AssignIF, AssignStack, PropagateIF},
         cdb::{ClauseDB, ClauseDBIF},
         types::*,
+        vam::*,
         var_vector::*,
     },
 };
@@ -119,6 +120,7 @@ impl Instantiate for Solver {
     ///```
     fn instantiate(config: &Config, cnf: &CNFDescription) -> Solver {
         VarRef::initialize(cnf.num_of_variables);
+        VarActivityManager::initialize();
         Solver {
             asg: AssignStack::instantiate(config, cnf),
             cdb: ClauseDB::instantiate(config, cnf),

src/vam.rs

@@ -1,3 +1,4 @@
+//! Variable Activity Manager with idempotent heap
 #![allow(static_mut_refs)]
 use {
     crate::{assign::AssignStack, types::*, var_vector::*},
@@ -27,7 +28,7 @@ static mut VAR_HEAP: VarIdHeap = VarIdHeap {
 impl VarActivityManager {
     pub fn initialize() {
         unsafe {
-            VAR_HEAP.clear();
+            VAR_HEAP = VarIdHeap::new(VarRef::num_vars());
         }
     }
     pub fn set_activity_decay(decay: f64) {
@@ -55,19 +56,49 @@ impl VarActivityManager {
             VarRef(vi).update_activity(VAM.decay, VAM.anti_decay);
         }
     }
-    pub fn add_var(vi: VarId) {
+
+    pub fn clear_heap() {
+        unsafe {
+            VAR_HEAP.clear_heap();
+        }
+    }
+    pub fn expand_heap() {
+        unsafe {
+            VAR_HEAP.expand_heap();
+        }
+    }
+    pub fn insert_heap(vi: VarId) {
         unsafe {
             VAR_HEAP.insert_heap(vi);
         }
     }
-    pub fn remove_var(vi: VarId) {
+    pub fn update_heap(vi: VarId) {
         unsafe {
-            VAR_HEAP.remove_from_heap(vi);
+            VAR_HEAP.update_heap(vi);
         }
     }
-    pub fn pop_top_var(asg: &mut AssignStack) -> VarId {
+    pub fn get_heap_root(asg: &mut AssignStack) -> VarId {
         unsafe { VAR_HEAP.get_heap_root(asg) }
     }
+    pub fn remove_from_heap(vi: VarId) {
+        unsafe {
+            VAR_HEAP.remove_from_heap(vi);
+        }
+    }
+
+    // pub fn add_var(vi: VarId) {
+    //     unsafe {
+    //         VAR_HEAP.insert_heap(vi);
+    //     }
+    // }
+    // pub fn remove_var(vi: VarId) {
+    //     unsafe {
+    //         VAR_HEAP.remove_from_heap(vi);
+    //     }
+    // }
+    // pub fn pop_top_var(asg: &mut AssignStack) -> VarId {
+    //     unsafe { VAR_HEAP.get_heap_root(asg) }
+    // }
     pub fn increment_tick() {
         unsafe {
             VAM.tick += 1;