Remove ClauseDB::reduction_threshold

shnarazk · Sep 16, 2024 · 8926570 · 8926570
1 parent 5855bcf
commit 8926570
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 6 deletions.
diff --git 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
@@ -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;