Give initial values to ClauseDB::{lbd, lb_entanglement}

shnarazk · Sep 19, 2024 · 00c256c · 00c256c
1 parent b27d3de
commit 00c256c
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 4 deletions.
diff --git a/src/cdb/ema.rs b/src/cdb/ema.rs
@@ -14,7 +14,7 @@ pub struct ProgressLBD {
 impl Default for ProgressLBD {
     fn default() -> ProgressLBD {
         ProgressLBD {
-            ema: Ewa2::new(0.0),
+            ema: Ewa2::new(0.0).with_value(16.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),
+            ema: Ewa2::new(0.0).with_slow(LBD_EWA_SLOW).with_value(16.0),
             ..ProgressLBD::default()
         }
     }

diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs
@@ -164,7 +164,7 @@ impl Default for ClauseDB {
             num_learnt: 0,
             num_reduction: 0,
             num_reregistration: 0,
-            lb_entanglement: Ema2::new(1_000).with_slow(80_000).with_value(2.0),
+            lb_entanglement: Ema2::new(1_000).with_slow(80_000).with_value(16.0),
 
             #[cfg(all(feature = "clause_elimination", not(feature = "incremental_solver")))]
             eliminated_permanent: Vec::new(),
@@ -514,7 +514,7 @@ impl ClauseDBIF for ClauseDB {
             ..
         } = self;
         let c = &mut clause[ci];
-        let rank = c.update_lbd(asg, lbd_temp);
+        let rank: DecisionLevel = c.update_lbd(asg, lbd_temp);
         let learnt = c.is(FlagClause::LEARNT);
         if learnt {
             #[cfg(feature = "keep_just_used_clauses")]

diff --git a/src/primitive/ema.rs b/src/primitive/ema.rs
@@ -437,4 +437,9 @@ 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
+    }
 }