Reorganize visibilities

ChangeLog.md

@@ -3,6 +3,9 @@
 - Remove feature 'incremental_solver'
 - Remove feature 'EVSIDS'
 - Use `static mut` vars. So splr is non-thread-safe now.
+- Refactor visivility of modules and structs
+  - Rename `property` to `stats`
+  - Use struct names directly instead of trait requirements
 
 ## 0.17.6, 2025-02-01
 

src/assign/mod.rs

@@ -7,12 +7,13 @@ mod ema;
 mod propagate;
 /// assignment management
 mod stack;
+/// properties
+pub mod stats;
 /// trail saving
 mod trail_saving;
 
 pub use self::{
     propagate::PropagateIF,
-    property::*,
     stack::{AssignStack, VarManipulateIF},
 };
 use {crate::types::*, std::fmt};
@@ -110,124 +111,3 @@ impl DebugReportIF for Clause {
         l
     }
 }
-
-pub mod property {
-    use super::stack::AssignStack;
-    use crate::{types::*, var_vector::VarRef};
-
-    #[derive(Clone, Copy, Debug, Eq, PartialEq)]
-    pub enum Tusize {
-        NumConflict,
-        NumDecision,
-        NumPropagation,
-        NumRephase,
-        NumRestart,
-        //
-        //## var stat
-        //
-        NumAssertedVar,
-        NumEliminatedVar,
-        NumReconflict,
-        NumRepropagation,
-        /// the number of vars in `the unreachable core'
-        NumUnassertedVar,
-        NumUnassignedVar,
-        NumUnreachableVar,
-        RootLevel,
-    }
-
-    pub const USIZES: [Tusize; 13] = [
-        Tusize::NumConflict,
-        Tusize::NumDecision,
-        Tusize::NumPropagation,
-        Tusize::NumRephase,
-        Tusize::NumRestart,
-        Tusize::NumAssertedVar,
-        Tusize::NumEliminatedVar,
-        Tusize::NumReconflict,
-        Tusize::NumRepropagation,
-        Tusize::NumUnassertedVar,
-        Tusize::NumUnassignedVar,
-        Tusize::NumUnreachableVar,
-        Tusize::RootLevel,
-    ];
-
-    impl PropertyDereference<Tusize, usize> for AssignStack {
-        #[inline]
-        fn derefer(&self, k: Tusize) -> usize {
-            match k {
-                Tusize::NumConflict => self.num_conflict,
-                Tusize::NumDecision => self.num_decision,
-                Tusize::NumPropagation => self.num_propagation,
-                Tusize::NumRephase => self.num_rephase,
-                Tusize::NumRestart => self.num_restart,
-                Tusize::NumAssertedVar => self.num_asserted_vars,
-                Tusize::NumEliminatedVar => self.num_eliminated_vars,
-                Tusize::NumReconflict => self.num_reconflict,
-                Tusize::NumRepropagation => self.num_repropagation,
-                Tusize::NumUnassertedVar => {
-                    VarRef::num_vars() - self.num_asserted_vars - self.num_eliminated_vars
-                }
-                Tusize::NumUnassignedVar => {
-                    VarRef::num_vars()
-                        - self.num_asserted_vars
-                        - self.num_eliminated_vars
-                        - self.trail.len()
-                }
-                Tusize::NumUnreachableVar => VarRef::num_vars() - self.num_best_assign,
-                Tusize::RootLevel => self.root_level as usize,
-            }
-        }
-    }
-
-    #[derive(Clone, Copy, Debug, Eq, PartialEq)]
-    pub enum Tf64 {
-        AverageVarActivity,
-        CurrentWorkingSetSize,
-    }
-
-    pub const F64S: [Tf64; 2] = [Tf64::AverageVarActivity, Tf64::CurrentWorkingSetSize];
-
-    impl PropertyDereference<Tf64, f64> for AssignStack {
-        #[inline]
-        fn derefer(&self, k: Tf64) -> f64 {
-            match k {
-                Tf64::AverageVarActivity => 0.0,    // self.activity_averaged,
-                Tf64::CurrentWorkingSetSize => 0.0, // self.cwss,
-            }
-        }
-    }
-
-    #[derive(Clone, Copy, Debug, Eq, PartialEq)]
-    pub enum TEma {
-        AssignRate,
-        DecisionPerConflict,
-        PropagationPerConflict,
-        ConflictPerRestart,
-        ConflictPerBaseRestart,
-        BestPhaseDivergenceRate,
-    }
-
-    pub const EMAS: [TEma; 6] = [
-        TEma::AssignRate,
-        TEma::DecisionPerConflict,
-        TEma::PropagationPerConflict,
-        TEma::ConflictPerRestart,
-        TEma::ConflictPerBaseRestart,
-        TEma::BestPhaseDivergenceRate,
-    ];
-
-    impl PropertyReference<TEma, EmaView> for AssignStack {
-        #[inline]
-        fn refer(&self, k: TEma) -> &EmaView {
-            match k {
-                TEma::AssignRate => self.assign_rate.as_view(),
-                TEma::DecisionPerConflict => self.dpc_ema.as_view(),
-                TEma::PropagationPerConflict => self.ppc_ema.as_view(),
-                TEma::ConflictPerRestart => self.cpr_ema.as_view(),
-                TEma::ConflictPerBaseRestart => self.cpr_ema.as_view(),
-                TEma::BestPhaseDivergenceRate => self.bp_divergence_ema.as_view(),
-            }
-        }
-    }
-}

src/assign/propagate.rs

@@ -145,7 +145,7 @@ impl PropagateIF for AssignStack {
         // self.reward_at_assign(vi);
         VarActivityManager::reward_at_assign(vi);
         self.trail.push(l);
-        self.num_decision += 1;
+        self.num_decisions += 1;
         debug_assert!(self.q_head < self.trail.len());
     }
     fn cancel_until(&mut self, lv: DecisionLevel) {
@@ -224,8 +224,8 @@ impl PropagateIF for AssignStack {
         self.trail_lim.truncate(lv as usize);
         // assert!(lim < self.q_head) doesn't hold sometimes in chronoBT.
         if lv == self.root_level {
-            self.num_restart += 1;
-            self.cpr_ema.update(self.num_conflict);
+            self.num_restarts += 1;
+            self.cpr_ema.update(self.num_conflicts);
         } else {
             #[cfg(feature = "assign_rate")]
             self.assign_rate.update(
@@ -283,9 +283,9 @@ impl PropagateIF for AssignStack {
 
         macro_rules! conflict_path {
             ($lit: expr, $reason: expr) => {
-                self.dpc_ema.update(self.num_decision);
-                self.ppc_ema.update(self.num_propagation);
-                self.num_conflict += 1;
+                self.dpc_ema.update(self.num_decisions);
+                self.ppc_ema.update(self.num_propagations);
+                self.num_conflicts += 1;
                 return Err(($lit, $reason));
             };
         }
@@ -311,11 +311,11 @@ impl PropagateIF for AssignStack {
         macro_rules! from_saved_trail {
             () => {
                 if let cc @ Err(_) = self.reuse_saved_trail(cdb) {
-                    self.num_propagation += 1;
-                    self.num_conflict += 1;
+                    self.num_propagations += 1;
+                    self.num_conflicts += 1;
                     self.num_reconflict += 1;
-                    self.dpc_ema.update(self.num_decision);
-                    self.ppc_ema.update(self.num_propagation);
+                    self.dpc_ema.update(self.num_decisions);
+                    self.ppc_ema.update(self.num_propagations);
                     return cc;
                 }
             };
@@ -328,7 +328,7 @@ impl PropagateIF for AssignStack {
         let dl = self.decision_level();
         from_saved_trail!();
         while let Some(p) = self.trail.get(self.q_head) {
-            self.num_propagation += 1;
+            self.num_propagations += 1;
             self.q_head += 1;
             #[cfg(feature = "debug_propagation")]
             {
@@ -360,7 +360,10 @@ impl PropagateIF for AssignStack {
                 match VarRef::lit_assigned(blocker) {
                     Some(true) => (),
                     Some(false) => {
-                        check_in!(cid, Propagate::EmitConflict(self.num_conflict + 1, blocker));
+                        check_in!(
+                            cid,
+                            Propagate::EmitConflict(self.num_conflicts + 1, blocker)
+                        );
                         conflict_path!(blocker, minimized_reason!(propagating));
                     }
                     None => {
@@ -753,7 +756,7 @@ impl AssignStack {
                 }
             }
         }
-        self.build_best_at = self.num_propagation;
+        self.build_best_at = self.num_propagations;
         #[cfg(feature = "rephase")]
         {
             self.phase_age = 0;

src/assign/stack.rs

@@ -19,7 +19,7 @@ pub struct AssignStack {
     pub(super) trail_lim: Vec<usize>,
     /// the-number-of-assigned-and-propagated-vars + 1
     pub(super) q_head: usize,
-    pub root_level: DecisionLevel,
+    pub(super) root_level: DecisionLevel,
 
     #[cfg(feature = "trail_saving")]
     pub(super) trail_saved: Vec<Lit>,
@@ -44,7 +44,7 @@ pub struct AssignStack {
     //
     //## Stage
     //
-    pub stage_scale: usize,
+    pub(super) stage_scale: usize,
 
     //## Elimanated vars
     //
@@ -54,13 +54,13 @@ pub struct AssignStack {
     //## Statistics
     //
     /// the number of asserted vars.
-    pub num_asserted_vars: usize,
+    pub(super) num_asserted_vars: usize,
     /// the number of eliminated vars.
-    pub num_eliminated_vars: usize,
-    pub(super) num_decision: usize,
-    pub(super) num_propagation: usize,
-    pub num_conflict: usize,
-    pub(super) num_restart: usize,
+    pub(super) num_eliminated_vars: usize,
+    pub(super) num_decisions: usize,
+    pub(super) num_propagations: usize,
+    pub(super) num_conflicts: usize,
+    pub(super) num_restarts: usize,
     /// Assign rate EMA
     pub(super) assign_rate: ProgressASG,
     /// Decisions Per Conflict
@@ -101,10 +101,10 @@ impl Default for AssignStack {
 
             num_asserted_vars: 0,
             num_eliminated_vars: 0,
-            num_decision: 0,
-            num_propagation: 0,
-            num_conflict: 0,
-            num_restart: 0,
+            num_decisions: 0,
+            num_propagations: 0,
+            num_conflicts: 0,
+            num_restarts: 0,
             assign_rate: ProgressASG::default(),
             dpc_ema: EmaSU::new(100),
             ppc_ema: EmaSU::new(100),
@@ -179,6 +179,48 @@ impl AssignStack {
     pub fn root_level(&self) -> DecisionLevel {
         self.root_level
     }
+    pub fn num_asserted_vars(&self) -> usize {
+        self.num_asserted_vars
+    }
+    pub fn num_eliminated_vars(&self) -> usize {
+        self.num_eliminated_vars
+    }
+    pub fn num_decisions(&self) -> usize {
+        self.num_decisions
+    }
+    pub fn num_propagations(&self) -> usize {
+        self.num_propagations
+    }
+    pub fn num_conflicts(&self) -> usize {
+        self.num_conflicts
+    }
+    pub fn num_restart(&self) -> usize {
+        self.num_restarts
+    }
+    pub fn num_unasserted_vars(&self) -> usize {
+        VarRef::num_vars() - self.num_asserted_vars - self.num_eliminated_vars
+    }
+    pub fn num_unassigned_vars(&self) -> usize {
+        VarRef::num_vars() - self.num_asserted_vars - self.num_eliminated_vars - self.trail.len()
+    }
+    pub fn num_unreachable_vars(&self) -> usize {
+        VarRef::num_vars() - self.num_best_assign
+    }
+    pub fn assign_rate(&self) -> &EmaView {
+        self.assign_rate.as_view()
+    }
+    /// EMA of Decision/Conflict
+    pub fn dpc_ema(&self) -> &EmaView {
+        self.dpc_ema.as_view()
+    }
+    /// EMA of Propagation/Conflict
+    pub fn ppc_ema(&self) -> &EmaView {
+        self.ppc_ema.as_view()
+    }
+    /// EMA of Conflict/Restart
+    pub fn cpr_ema(&self) -> &EmaView {
+        self.cpr_ema.as_view()
+    }
     /// return the i-th element in the stack.
     pub fn stack(&self, i: usize) -> Lit {
         self.trail[i]
@@ -228,7 +270,7 @@ impl AssignStack {
     }
     /// return the largest number of assigned vars.
     pub fn best_assigned(&self) -> Option<usize> {
-        (self.build_best_at == self.num_propagation)
+        (self.build_best_at == self.num_propagations)
             .then_some(VarRef::num_vars() - self.num_best_assign)
     }
     /// return `true` if no best_phases
@@ -455,7 +497,7 @@ impl AssignStack {
             return;
         }
         self.check_consistency_of_best_phases();
-        if self.derefer(super::property::Tusize::NumUnassertedVar) <= self.best_phases.len() {
+        if self.num_unasserted_vars() <= self.best_phases.len() {
             self.best_phases.clear();
             return;
         }