Remove all '&impl's and '&mut impl's

shnarazk · Feb 7, 2025 · 1abb88b · 1abb88b
1 parent de73d33
commit 1abb88b
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 13 deletions.
diff --git a/src/assign/stack.rs b/src/assign/stack.rs
@@ -1,7 +1,7 @@
 //! main struct AssignStack
 use {
     super::{ema::ProgressASG, PropagateIF},
-    crate::{cdb::ClauseDBIF, types::*, vam::VarActivityManager, var_vector::*},
+    crate::{cdb::ClauseDB, types::*, vam::VarActivityManager, var_vector::*},
     std::{fmt, ops::Range, slice::Iter},
 };
 
@@ -238,7 +238,7 @@ impl AssignStack {
     }
     /// inject assignments for eliminated vars.
     #[allow(unused_variables)]
-    pub fn extend_model(&self, cdb: &mut impl ClauseDBIF) -> Vec<Option<bool>> {
+    pub fn extend_model(&self, cdb: &mut ClauseDB) -> Vec<Option<bool>> {
         let lits = &self.eliminated;
 
         #[cfg(feature = "trace_elimination")]

diff --git a/src/assign/trail_saving.rs b/src/assign/trail_saving.rs
@@ -3,7 +3,7 @@
 /// This version can handle Chronological and Non Chronological Backtrack.
 use {
     super::{AssignStack, PropagateIF},
-    crate::{cdb::ClauseDBIF, types::*, vam::VarActivityManager, var_vector::*},
+    crate::{cdb::ClauseDB, types::*, vam::VarActivityManager, var_vector::*},
 };
 
 #[cfg(feature = "chrono_BT")]
@@ -12,7 +12,7 @@ use super::AssignIF;
 /// Methods on trail saving.
 pub trait TrailSavingIF {
     fn save_trail(&mut self, to_lvl: DecisionLevel);
-    fn reuse_saved_trail(&mut self, cdb: &impl ClauseDBIF) -> PropagationResult;
+    fn reuse_saved_trail(&mut self, cdb: &ClauseDB) -> PropagationResult;
     fn clear_saved_trail(&mut self);
 }
 
@@ -60,7 +60,7 @@ impl TrailSavingIF for AssignStack {
             VarActivityManager::insert_heap(vi);
         }
     }
-    fn reuse_saved_trail(&mut self, cdb: &impl ClauseDBIF) -> PropagationResult {
+    fn reuse_saved_trail(&mut self, cdb: &ClauseDB) -> PropagationResult {
         let q = self.stage_scale.trailing_zeros() as u16
             + (cdb.derefer(crate::cdb::property::Tf64::LiteralBlockEntanglement) as u16) / 2;
 

diff --git a/src/cdb/binary.rs b/src/cdb/binary.rs
@@ -66,7 +66,7 @@ pub trait BinaryLinkIF {
     /// add new var
     fn add_new_var(&mut self);
     // /// sort links based on var activities
-    // fn reorder(&mut self, asg: &impl AssignIF);
+    // fn reorder(&mut self, asg: &AssignStack);
 }
 
 impl BinaryLinkIF for BinaryLinkDB {
@@ -99,7 +99,7 @@ impl BinaryLinkIF for BinaryLinkDB {
         }
     }
     /*
-    fn reorder(&mut self, asg: &impl AssignIF) {
+    fn reorder(&mut self, asg: &AssignStack) {
         let nv = self.list.len() / 2;
         let thr: f64 = (1usize..nv).map(|i| asg.activity(i)).sum::<f64>()
             / (1usize..nv)

diff --git a/src/processor/simplify.rs b/src/processor/simplify.rs
@@ -390,7 +390,7 @@ impl Eliminator {
     // Due to a potential bug of killing clauses and difficulty about
     // synchronization between 'garbage_collect' and clearing occur lists,
     // 'stop' should purge all occur lists to purge any dead clauses for now.
-    fn stop(&mut self, cdb: &mut impl ClauseDBIF) {
+    fn stop(&mut self, cdb: &mut ClauseDB) {
         let force: bool = true;
         self.clear_clause_queue(cdb);
         self.clear_var_queue();
@@ -602,7 +602,7 @@ impl Eliminator {
         c.turn_on(FlagClause::ENQUEUED);
     }
     /// clear eliminator's clause queue.
-    fn clear_clause_queue(&mut self, cdb: &mut impl ClauseDBIF) {
+    fn clear_clause_queue(&mut self, cdb: &mut ClauseDB) {
         for cid in &self.clause_queue {
             cdb[*cid].turn_off(FlagClause::ENQUEUED);
         }

diff --git a/src/processor/subsume.rs b/src/processor/subsume.rs
@@ -3,7 +3,7 @@ use {
     super::{EliminateIF, Eliminator},
     crate::{
         assign::{AssignStack, PropagateIF},
-        cdb::ClauseDBIF,
+        cdb::{ClauseDB, ClauseDBIF},
         types::*,
         var_vector::*,
     },
@@ -20,7 +20,7 @@ impl Eliminator {
     pub fn try_subsume(
         &mut self,
         asg: &mut AssignStack,
-        cdb: &mut impl ClauseDBIF,
+        cdb: &mut ClauseDB,
         cid: ClauseId,
         did: ClauseId,
     ) -> MaybeInconsistent {
@@ -54,7 +54,7 @@ impl Eliminator {
 }
 
 /// returns a literal if these clauses can be merged by the literal.
-fn have_subsuming_lit(cdb: &mut impl ClauseDBIF, cid: ClauseId, other: ClauseId) -> Subsumable {
+fn have_subsuming_lit(cdb: &mut ClauseDB, cid: ClauseId, other: ClauseId) -> Subsumable {
     debug_assert!(!other.is_lifted_lit());
     if cid.is_lifted_lit() {
         let l = Lit::from(cid);
@@ -92,7 +92,7 @@ fn have_subsuming_lit(cdb: &mut impl ClauseDBIF, cid: ClauseId, other: ClauseId)
 /// - calls `enqueue_var`
 fn strengthen_clause(
     asg: &mut AssignStack,
-    cdb: &mut impl ClauseDBIF,
+    cdb: &mut ClauseDB,
     elim: &mut Eliminator,
     cid: ClauseId,
     l: Lit,