diff --git a/src/cdb/db.rs b/src/cdb/db.rs index 34b632970..f2724876e 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -78,8 +78,6 @@ pub struct ClauseDB { /// Literal Block Entanglement /// EMA of LBD of clauses used in conflict analysis (dependency graph) pub(super) lb_entanglement: Ema2, - /// cutoff value will be used in the next `reduce` - pub(super) reduction_threshold: DecisionLevel, // //## incremental solving @@ -149,7 +147,6 @@ impl Instantiate for ClauseDB { activity_anti_decay: 1.0 - config.crw_dcy_rat, lbd_temp: vec![0; nv + 1], - reduction_threshold: 128, ..ClauseDB::default() } } diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index 70ea5f577..d24469bd8 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -165,7 +165,6 @@ impl Default for ClauseDB { num_reduction: 0, num_reregistration: 0, lb_entanglement: Ema2::new(1_000).with_slow(80_000).with_value(2.0), - reduction_threshold: 128, #[cfg(all(feature = "clause_elimination", not(feature = "incremental_solver")))] eliminated_permanent: Vec::new(), @@ -272,7 +271,6 @@ impl ClauseDBIF for ClauseDB { self.clause[ci].search_from = 0; self.clause[ci].rank_old = self[ci].rank; self.lbd.update(self[ci].rank); - self.reduction_threshold = self.reduction_threshold.min(self[ci].rank); self.num_clause += 1; if learnt { if len2 { @@ -573,7 +571,6 @@ impl ClauseDBIF for ClauseDB { } } } - self.reduction_threshold = 128; // let keep = perm.len().max(alives); // if perm.is_empty() { // return;