cargo clippy (1.84)

src/assign/mod.rs

@@ -1,5 +1,5 @@
-/// Module `assign` implements Boolean Constraint Propagation and decision var selection.
-/// This version can handle Chronological and Non Chronological Backtrack.
+// Module `assign` implements Boolean Constraint Propagation and decision var selection.
+// This version can handle Chronological and Non Chronological Backtrack.
 
 /// Ema
 mod ema;

src/assign/propagate.rs

@@ -765,7 +765,7 @@ impl AssignStack {
         assert_ne!(self.assigned(b0), Some(false));
         assert_ne!(self.assigned(b1), Some(false));
     }
-    ///
+    /// a specialized `propagate` to clean up the stack
     fn propagate_at_root_level(&mut self, cdb: &mut impl ClauseDBIF) -> MaybeInconsistent {
         let mut num_propagated = 0;
         while num_propagated < self.trail.len() {

src/assign/select.rs

@@ -1,4 +1,4 @@
-/// Decision var selection
+// Decision var selection
 
 #[cfg(feature = "rephase")]
 use super::property;

src/cdb/clause.rs

@@ -257,4 +257,7 @@ impl Clause {
         self.rank = cnt;
         cnt as usize
     }
+    pub fn reverse_activity_sum(&self, asg: &impl AssignIF) -> f64 {
+        self.iter().map(|l| 1.0 - asg.activity(l.vi())).sum()
+    }
 }

src/cdb/db.rs

@@ -935,7 +935,7 @@ impl ClauseDBIF for ClauseDB {
         if learnt {
             #[cfg(feature = "just_used")]
             c.turn_on(FlagClause::USED);
-            #[cfg(feature = "clause_rewading")]
+            #[cfg(feature = "clause_rewarding")]
             self.reward_at_analysis(cid);
         }
         if 1 < rank {
@@ -945,14 +945,6 @@ impl ClauseDBIF for ClauseDB {
     }
     /// reduce the number of 'learnt' or *removable* clauses.
     fn reduce(&mut self, asg: &mut impl AssignIF, setting: ReductionType) {
-        impl Clause {
-            fn reverse_activity_sum(&self, asg: &impl AssignIF) -> f64 {
-                self.iter().map(|l| 1.0 - asg.activity(l.vi())).sum()
-            }
-            fn lbd(&self) -> f64 {
-                self.rank as f64
-            }
-        }
         let ClauseDB {
             ref mut clause,
             ref mut lbd_temp,
@@ -1004,7 +996,7 @@ impl ClauseDBIF for ClauseDB {
                     }
                 }
                 ReductionType::LBDonADD(_) => {
-                    perm.push(OrderedProxy::new(i, c.lbd()));
+                    perm.push(OrderedProxy::new(i, c.rank as f64));
                 }
                 ReductionType::LBDonALL(cutoff, _) => {
                     let value = c.rank.min(c.rank_old);

src/config.rs

@@ -427,21 +427,21 @@ pub mod property {
 
     #[derive(Clone, Copy, Debug, Eq, PartialEq)]
     pub enum Tf64 {
-        #[cfg(feature = "clase_rewarding")]
+        #[cfg(feature = "clause_rewarding")]
         ClauseRewardDecayRate,
         VarRewardDecayRate,
     }
 
-    #[cfg(not(feature = "clase_rewarding"))]
+    #[cfg(not(feature = "clause_rewarding"))]
     pub const F64S: [Tf64; 1] = [Tf64::VarRewardDecayRate];
-    #[cfg(feature = "clase_rewarding")]
+    #[cfg(feature = "clause_rewarding")]
     pub const F64S: [Tf64; 2] = [Tf64::ClauseRewardDecayRate, Tf64::VarRewardDecayRate];
 
     impl PropertyDereference<Tf64, f64> for Config {
         #[inline]
         fn derefer(&self, k: Tf64) -> f64 {
             match k {
-                #[cfg(feature = "clase_rewarding")]
+                #[cfg(feature = "clause_rewarding")]
                 Tf64::ClauseRewardDecayRate => self.crw_dcy_rat,
                 Tf64::VarRewardDecayRate => self.vrw_dcy_rat,
             }

src/processor/heap.rs

@@ -10,6 +10,7 @@ pub trait VarOrderIF {
     fn insert(&mut self, occur: &[LitOccurs], vi: VarId, upward: bool);
     fn is_empty(&self) -> bool;
     fn select_var(&mut self, occur: &[LitOccurs], asg: &impl AssignIF) -> Option<VarId>;
+    #[allow(dead_code)]
     fn rebuild(&mut self, asg: &impl AssignIF, occur: &[LitOccurs]);
 }
 
@@ -37,7 +38,7 @@ impl LitOccurs {
     }
     pub fn activity(&self) -> usize {
         if self.aborted {
-            std::usize::MAX
+            usize::MAX
         } else {
             self.pos_occurs.len().min(self.neg_occurs.len())
         }

src/processor/mod.rs

@@ -41,7 +41,7 @@ use {
 /// use crate::{splr::config::Config, splr::types::*};
 /// use crate::splr::processor::{Eliminator, EliminateIF};
 /// use crate::splr::solver::Solver;
-
+///
 /// let mut s = Solver::instantiate(&Config::default(), &CNFDescription::default());
 /// let mut elim = Eliminator::instantiate(&s.state.config, &s.state.cnf);
 /// assert_eq!(elim.is_running(), false);
@@ -57,6 +57,7 @@ pub trait EliminateIF: Instantiate {
     /// simplify database by:
     /// * removing satisfiable clauses
     /// * calling exhaustive simplifier that tries **clause subsumption** and **variable elimination**.
+    ///
     /// Note: `force_run` is used only at the beginning of `solve' for simple satisfiability check
     ///
     /// # Errors

src/processor/simplify.rs

@@ -594,9 +594,9 @@ impl Eliminator {
         self.enqueue_var(asg, l.vi(), true);
     }
 
-    ///
-    /// clause queue operations
-    ///
+    //
+    // clause queue operations
+    //
 
     /// enqueue a clause into eliminator's clause queue.
     pub fn enqueue_clause(&mut self, cid: ClauseId, c: &mut Clause) {
@@ -621,9 +621,9 @@ impl Eliminator {
         self.clause_queue.len()
     }
 
-    ///
-    /// var queue operations
-    ///
+    //
+    // var queue operations
+    //
 
     /// clear eliminator's var queue
     fn clear_var_queue(&mut self, asg: &mut impl AssignIF) {

src/solver/conflict.rs

@@ -83,7 +83,7 @@ pub fn handle_conflict(
     let new_learnt = &mut state.new_learnt;
     let learnt_len = new_learnt.len();
     if learnt_len == 0 {
-        #[cfg(debug)]
+        #[cfg(feature = "boundary_check")]
         {
             println!(
                 "empty learnt at {}({}) by {:?}",
@@ -407,7 +407,7 @@ fn conflict_analyze(
         //
         // set the index of the next literal to trail_index
         //
-        #[allow(clippy::blocks_in_if_conditions)]
+        #[allow(clippy::blocks_in_conditions)]
         while {
             let vi = asg.stack(trail_index).vi();
             boundary_check!(

src/state.rs

@@ -120,7 +120,7 @@ pub struct State {
     /// hold conflicting user-defined *assumed* literals for UNSAT problems
     pub conflicts: Vec<Lit>,
 
-    #[cfg(feature = "chronoBT")]
+    #[cfg(feature = "chrono_BT")]
     /// chronoBT threshold
     pub chrono_bt_threshold: DecisionLevel,
 
@@ -164,7 +164,7 @@ impl Default for State {
             #[cfg(feature = "support_user_assumption")]
             conflicts: Vec::new(),
 
-            #[cfg(feature = "chronoBT")]
+            #[cfg(feature = "chrono_BT")]
             chrono_bt_threshold: 100,
 
             last_asg: 0,

src/types.rs

@@ -46,22 +46,18 @@ pub trait ActivityIF<Ix> {
     fn set_activity(&mut self, ix: Ix, val: f64);
     /// modify one's activity at conflict analysis in `conflict_analyze` in [`solver`](`crate::solver`).
     fn reward_at_analysis(&mut self, _ix: Ix) {
-        #[cfg(debug)]
         todo!()
     }
     /// modify one's activity at value assignment in assign.
     fn reward_at_assign(&mut self, _ix: Ix) {
-        #[cfg(debug)]
         todo!()
     }
     /// modify one's activity at value assignment in unit propagation.
     fn reward_at_propagation(&mut self, _ix: Ix) {
-        #[cfg(debug)]
         todo!()
     }
     /// modify one's activity at value un-assignment in [`cancel_until`](`crate::assign::PropagateIF::cancel_until`).
     fn reward_at_unassign(&mut self, _ix: Ix) {
-        #[cfg(debug)]
         todo!()
     }
     /// update reward decay.