Add StageManager::segment_progress_ratio

src/cdb/ema.rs

@@ -14,7 +14,7 @@ pub struct ProgressLBD {
 impl Default for ProgressLBD {
     fn default() -> ProgressLBD {
         ProgressLBD {
-            ema: Ewa2::new(0.0).with_value(16.0),
+            ema: Ewa2::new(0.0),
             num: 0,
             sum: 0,
         }
@@ -24,7 +24,7 @@ impl Default for ProgressLBD {
 impl Instantiate for ProgressLBD {
     fn instantiate(_config: &Config, _: &CNFDescription) -> Self {
         ProgressLBD {
-            ema: Ewa2::new(0.0).with_slow(LBD_EWA_SLOW).with_value(16.0),
+            ema: Ewa2::new(0.0).with_slow(LBD_EWA_SLOW),
             ..ProgressLBD::default()
         }
     }

src/primitive/ema.rs

@@ -17,13 +17,6 @@ pub trait EmaIF {
     }
 }
 
-pub trait EmaSingleIF: EmaIF {
-    /// return the current value.
-    fn get(&self) -> f64 {
-        self.get_fast()
-    }
-}
-
 /// API for Exponential Moving Average, EMA, like `get`, `reset`, `update` and so on.
 pub trait EmaMutIF: EmaIF {
     /// the type of the argument of `update`.
@@ -437,9 +430,4 @@ impl<const N: usize> Ewa2<N> {
         self.sx = 1.0 - self.se;
         self
     }
-    pub fn with_value(mut self, val: f64) -> Self {
-        self.ema.fast = val;
-        self.ema.slow = val;
-        self
-    }
 }

src/solver/stage.rs

@@ -152,20 +152,18 @@ impl StageManager {
     pub fn current_segment(&self) -> usize {
         self.segment
     }
-    /// returns a recommending number of redicible learnt clauses, based on
-    /// the length of span.
-    pub fn num_reducible(&self, reducing_factor: f64) -> usize {
-        let span: f64 = self.span_ema.get();
-        let keep = span.powf(1.0 - reducing_factor) as usize;
-        (span as usize).saturating_sub(keep)
-    }
     /// returns the maximum factor so far.
     /// None: `luby_iter.max_value` holds the maximum value so far.
     /// This means it is the value found at the last segment.
     /// So the current value should be the next value, which is the double.
     pub fn max_scale(&self) -> usize {
         self.max_scale_of_segment
     }
+    /// returns (0, 1]
+    pub fn segment_progress_ratio(&self) -> f64 {
+        (2 * (self.cycle - self.segment_starting_cycle + 1)) as f64
+            / self.max_scale_of_segment as f64
+    }
     pub fn cycle_starting_stage(&self) -> usize {
         self.cycle_starting_stage
     }
@@ -181,4 +179,11 @@ impl StageManager {
     pub fn set_span_base(&mut self, span_base: f64) {
         self.span_base = span_base;
     }
+    /// returns a recommending number of redicible learnt clauses, based on
+    /// the length of span.
+    pub fn num_reducible(&self, reducing_factor: f64) -> usize {
+        let span: f64 = self.span_ema.get();
+        let keep = span.powf(1.0 - reducing_factor) as usize;
+        (span as usize).saturating_sub(keep)
+    }
 }

src/state.rs

@@ -559,7 +559,11 @@ impl StateIF for State {
         println!(
             // "\x1B[2K        misc|ccut:{}, vdcy:{}, core:{}, /ppc:{}",
             "\x1B[2K{:>12}|ccut:{}, vdcy:{}, core:{}, /ppc:{}",
-            format!("Luby{}", self.stm.current_segment(),),
+            format!(
+                "Luby{},{:>4.2}",
+                self.stm.current_segment(),
+                self.stm.segment_progress_ratio(),
+            ),
             fm!(
                 "{:>9.4}",
                 self,