20250202 refactor primitive types

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "splr"
-version = "0.18.0-dev0"
+version = "0.18.0-dev1"
 authors = ["Narazaki Shuji <[email protected]>"]
 description = "A modern CDCL SAT solver in Rust"
 edition = "2021"

src/assign/mod.rs

@@ -17,15 +17,12 @@ mod select;
 mod stack;
 /// trail saving
 mod trail_saving;
-/// var struct and its methods
-mod var;
 
 pub use self::{
     propagate::PropagateIF,
     property::*,
     select::VarSelectIF,
-    stack::AssignStack,
-    var::{Var, VarManipulateIF},
+    stack::{AssignStack, VarManipulateIF},
 };
 use {
     crate::{cdb::ClauseDBIF, types::*},

src/assign/stack.rs

@@ -1,11 +1,12 @@
-/// main struct AssignStack
+//! main struct AssignStack
 use {
-    super::{
-        ema::ProgressASG, heap::VarHeapIF, heap::VarIdHeap, AssignIF, PropagateIF, Var,
-        VarManipulateIF,
-    },
+    super::{ema::ProgressASG, heap::VarHeapIF, heap::VarIdHeap, AssignIF, PropagateIF, Var},
     crate::{cdb::ClauseDBIF, types::*},
-    std::{fmt, ops::Range, slice::Iter},
+    std::{
+        fmt,
+        ops::Range,
+        slice::{Iter, IterMut},
+    },
 };
 
 #[cfg(any(feature = "best_phases_tracking", feature = "rephase"))]
@@ -461,3 +462,156 @@ mod tests {
         assert_eq!(asg.assigned(lit(-3)), None);
     }
 }
+
+/// Var manipulation
+pub trait VarManipulateIF {
+    /// return the assignment of var.
+    fn assign(&self, vi: VarId) -> Option<bool>;
+    /// return *the value* of a literal.
+    fn assigned(&self, l: Lit) -> Option<bool>;
+    /// return the assign level of var.
+    fn level(&self, vi: VarId) -> DecisionLevel;
+    /// return the reason of assignment.
+    fn reason(&self, vi: VarId) -> AssignReason;
+    /// return the var.
+    fn var(&self, vi: VarId) -> &Var;
+    /// return the var.
+    fn var_mut(&mut self, vi: VarId) -> &mut Var;
+    /// return an iterator over Vars.
+    fn var_iter(&self) -> Iter<'_, Var>;
+    /// return an mutable iterator over Vars.
+    fn var_iter_mut(&mut self) -> IterMut<'_, Var>;
+    /// set var status to asserted.
+    fn make_var_asserted(&mut self, vi: VarId);
+    /// set var status to eliminated.
+    fn make_var_eliminated(&mut self, vi: VarId);
+}
+
+impl VarManipulateIF for AssignStack {
+    fn assigned(&self, l: Lit) -> Option<bool> {
+        match self.var[l.vi()].assign {
+            Some(x) if !bool::from(l) => Some(!x),
+            x => x,
+        }
+    }
+    #[inline]
+    fn assign(&self, vi: VarId) -> Option<bool> {
+        #[cfg(feature = "unsafe_access")]
+        unsafe {
+            self.var.get_unchecked(vi).assign
+        }
+        #[cfg(not(feature = "unsafe_access"))]
+        self.assign[vi]
+    }
+    #[inline]
+    fn level(&self, vi: VarId) -> DecisionLevel {
+        #[cfg(feature = "unsafe_access")]
+        unsafe {
+            self.var.get_unchecked(vi).level
+        }
+        #[cfg(not(feature = "unsafe_access"))]
+        self.level[vi]
+    }
+    #[inline]
+    fn reason(&self, vi: VarId) -> AssignReason {
+        #[cfg(feature = "unsafe_access")]
+        unsafe {
+            self.var.get_unchecked(vi).reason
+        }
+        #[cfg(not(feature = "unsafe_access"))]
+        self.reason[vi]
+    }
+    #[inline]
+    fn var(&self, vi: VarId) -> &Var {
+        #[cfg(feature = "unsafe_access")]
+        unsafe {
+            self.var.get_unchecked(vi)
+        }
+        #[cfg(not(feature = "unsafe_access"))]
+        &self.var[vi]
+    }
+    #[inline]
+    fn var_mut(&mut self, vi: VarId) -> &mut Var {
+        #[cfg(feature = "unsafe_access")]
+        unsafe {
+            self.var.get_unchecked_mut(vi)
+        }
+        #[cfg(not(feature = "unsafe_access"))]
+        &mut self.var[vi]
+    }
+    fn var_iter(&self) -> Iter<'_, Var> {
+        self.var.iter()
+    }
+    fn var_iter_mut(&mut self) -> IterMut<'_, Var> {
+        self.var.iter_mut()
+    }
+    fn make_var_asserted(&mut self, vi: VarId) {
+        self.var[vi].reason = AssignReason::Decision(0);
+        self.set_activity(vi, 0.0);
+        self.remove_from_heap(vi);
+
+        #[cfg(feature = "boundary_check")]
+        {
+            self.var[vi].timestamp = self.tick;
+        }
+
+        #[cfg(feature = "best_phases_tracking")]
+        self.check_best_phase(vi);
+    }
+    fn make_var_eliminated(&mut self, vi: VarId) {
+        if !self.var[vi].is(FlagVar::ELIMINATED) {
+            self.var[vi].turn_on(FlagVar::ELIMINATED);
+            self.set_activity(vi, 0.0);
+            self.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;
+
+            #[cfg(feature = "boundary_check")]
+            {
+                self.var[vi].timestamp = self.tick;
+            }
+
+            #[cfg(feature = "trace_elimination")]
+            {
+                let lv = self.level[vi];
+                if self.root_level == self.level[vi] && self.assign[vi].is_some() {
+                    panic!("v:{}, dl:{}", self.var[vi], self.decision_level());
+                }
+                if !(self.root_level < self.level[vi] || self.assign[vi].is_none()) {
+                    panic!(
+                        "v:{}, lvl:{} => {}, dl:{}, assign:{:?} ",
+                        self.var[vi],
+                        lv,
+                        self.level[vi],
+                        self.decision_level(),
+                        self.assign[vi],
+                    );
+                }
+                debug_assert!(self.root_level < self.level[vi] || self.assign[vi].is_none());
+            }
+        } else {
+            #[cfg(feature = "boundary_check")]
+            panic!("double elimination");
+        }
+    }
+}
+
+#[cfg(feature = "best_phases_tracking")]
+impl AssignStack {
+    /// check usability of the saved best phase.
+    /// return `true` if the current best phase got invalid.
+    fn check_best_phase(&mut self, vi: VarId) -> bool {
+        if let Some((b, _)) = self.best_phases.get(&vi) {
+            debug_assert!(self.var[vi].assign.is_some());
+            if self.var[vi].assign != Some(*b) {
+                if self.root_level == self.var[vi].level {
+                    self.best_phases.clear();
+                    self.num_best_assign = self.num_asserted_vars + self.num_eliminated_vars;
+                }
+                return true;
+            }
+        }
+        false
+    }
+}