diff --git a/src/cdb/ema.rs b/src/cdb/ema.rs index abaed3470..a2b031d78 100644 --- 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 index b66fafe1f..a4c593314 100644 --- 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 index 2cc6c7490..056a3b7b4 100644 --- a/src/primitive/ema.rs +++ b/src/primitive/ema.rs @@ -437,4 +437,9 @@ impl Ewa2 { 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 + } }