From a057b5806e6182c53a99e3b5a6b9e80cf2aed7ab Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Fri, 10 Jan 2025 14:40:11 +0900 Subject: [PATCH] cargo clippy (1.84) --- src/assign/mod.rs | 4 ++-- src/cdb/clause.rs | 5 +++++ src/cdb/mod.rs | 7 ------- src/processor/mod.rs | 2 +- src/processor/simplify.rs | 12 ++++++------ 5 files changed, 14 insertions(+), 16 deletions(-) diff --git a/src/assign/mod.rs b/src/assign/mod.rs index 92e801865..badd53734 100644 --- a/src/assign/mod.rs +++ b/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; diff --git a/src/cdb/clause.rs b/src/cdb/clause.rs index cbeb0a768..2f48981f9 100644 --- a/src/cdb/clause.rs +++ b/src/cdb/clause.rs @@ -333,4 +333,9 @@ impl Clause { } self.rank } + pub fn extended_lbd(&self) -> f64 { + let l: f64 = self.len() as f64; + let r: f64 = self.rank as f64; + r + (l - r) / (l - r + 1.0) + } } diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index 466a52c91..78a869fb8 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -521,13 +521,6 @@ impl ClauseDBIF for ClauseDB { /// reduce the number of 'learnt' or *removable* clauses. #[cfg(feature = "keep_just_used_clauses")] fn reduce(&mut self, asg: &mut impl AssignIF, threshold: f64) { - impl Clause { - fn extended_lbd(&self) -> f64 { - let l: f64 = self.len() as f64; - let r: f64 = self.rank as f64; - r + (l - r) / (l - r + 1.0) - } - } // let ClauseDB { // ref mut clause, // ref mut lbd_temp, diff --git a/src/processor/mod.rs b/src/processor/mod.rs index 61b179c26..afe79ac0a 100644 --- a/src/processor/mod.rs +++ b/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); diff --git a/src/processor/simplify.rs b/src/processor/simplify.rs index aa288c214..9cc097344 100644 --- a/src/processor/simplify.rs +++ b/src/processor/simplify.rs @@ -510,9 +510,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, ci: ClauseIndex, c: &mut Clause) { @@ -537,9 +537,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) {