From 25d26aa28931241886b10cdcbed339dc7546301d Mon Sep 17 00:00:00 2001 From: Christoph Jabs Date: Tue, 11 Jul 2023 11:59:42 +0300 Subject: [PATCH] clippy --- build.rs | 2 -- src/instances/fio/opb.rs | 2 +- src/instances/sat.rs | 4 ++-- src/solvers/cadical.rs | 18 ++++++++---------- src/solvers/glucose4/core.rs | 18 +++++++++--------- src/solvers/glucose4/simp.rs | 18 +++++++++--------- src/solvers/kissat.rs | 8 +++----- src/solvers/minisat/core.rs | 18 +++++++++--------- src/solvers/minisat/simp.rs | 18 +++++++++--------- src/types/constraints.rs | 2 +- 10 files changed, 51 insertions(+), 57 deletions(-) diff --git a/build.rs b/build.rs index 54060050..3cb94e62 100644 --- a/build.rs +++ b/build.rs @@ -90,7 +90,6 @@ fn build_cadical(repo: &str, branch: &str, commit: &str) -> bool { // We specify the build manually here instead of calling make for better portability let src_files = glob(&format!("{}/src/*.cpp", cadical_dir_str)) .unwrap() - .into_iter() .filter_map(|res| { if let Ok(p) = res { if let Some(name) = p.file_name() { @@ -166,7 +165,6 @@ fn build_kissat(repo: &str, branch: &str, commit: &str) -> bool { // We specify the build manually here instead of calling make for better portability let src_files = glob(&format!("{}/src/*.c", kissat_dir_str)) .unwrap() - .into_iter() .filter_map(|res| { if let Ok(p) = res { if let Some(name) = p.file_name() { diff --git a/src/instances/fio/opb.rs b/src/instances/fio/opb.rs index ceeb97b5..72a31d1d 100644 --- a/src/instances/fio/opb.rs +++ b/src/instances/fio/opb.rs @@ -541,7 +541,7 @@ fn write_card( write!(writer, "-1 x{} ", l.vidx() + opts.first_var_idx) } })?; - writeln!(writer, "{} {};", op, bound as isize - offset) + writeln!(writer, "{} {};", op, bound - offset) } else { let (lits, bound, op) = match card { CardConstraint::UB(constr) => { diff --git a/src/instances/sat.rs b/src/instances/sat.rs index fa29d08b..cd25b6ca 100644 --- a/src/instances/sat.rs +++ b/src/instances/sat.rs @@ -570,7 +570,7 @@ impl SatInstance { cards.push(pb.as_card_constr().unwrap()); return None; } - return Some(pb); + Some(pb) }) .collect(); let cards = cards @@ -597,7 +597,7 @@ impl SatInstance { cnf.add_clause(card.as_clause().unwrap()); return None; } - return Some(card); + Some(card) }) .collect(); if unsat { diff --git a/src/solvers/cadical.rs b/src/solvers/cadical.rs index 0dfee25d..8dccbd6f 100644 --- a/src/solvers/cadical.rs +++ b/src/solvers/cadical.rs @@ -529,14 +529,14 @@ impl<'term> Terminate<'term> for CaDiCaL<'term, '_> { { self.terminate_cb = Some(Box::new(Box::new(cb))); let cb_ptr = self.terminate_cb.as_mut().unwrap().as_mut() as *const _ as *const c_void; - unsafe { ffi::ccadical_set_terminate(self.handle, cb_ptr, ffi::ccadical_terminate_cb) } + unsafe { + ffi::ccadical_set_terminate(self.handle, cb_ptr, Some(ffi::ccadical_terminate_cb)) + } } fn detach_terminator(&mut self) { self.terminate_cb = None; - let null_cb: extern "C" fn(*const c_void) -> c_int = - unsafe { std::mem::transmute(std::ptr::null::()) }; - unsafe { ffi::ccadical_set_terminate(self.handle, std::ptr::null(), null_cb) } + unsafe { ffi::ccadical_set_terminate(self.handle, std::ptr::null(), None) } } } @@ -576,16 +576,14 @@ impl<'learn> Learn<'learn> for CaDiCaL<'_, 'learn> { self.handle, cb_ptr, max_len.try_into().unwrap(), - ffi::ccadical_learn_cb, + Some(ffi::ccadical_learn_cb), ) } } fn detach_learner(&mut self) { self.terminate_cb = None; - let null_cb: extern "C" fn(*const c_void, *const c_int) = - unsafe { std::mem::transmute(std::ptr::null::()) }; - unsafe { ffi::ccadical_set_learn(self.handle, std::ptr::null(), 0, null_cb) } + unsafe { ffi::ccadical_set_learn(self.handle, std::ptr::null(), 0, None) } } } @@ -948,13 +946,13 @@ mod ffi { pub fn ccadical_set_terminate( solver: *mut CaDiCaLHandle, state: *const c_void, - terminate: extern "C" fn(state: *const c_void) -> c_int, + terminate: Option c_int>, ); pub fn ccadical_set_learn( solver: *mut CaDiCaLHandle, state: *const c_void, max_length: c_int, - learn: extern "C" fn(state: *const c_void, clause: *const c_int), + learn: Option, ); pub fn ccadical_constrain(solver: *mut CaDiCaLHandle, lit: c_int); pub fn ccadical_constraint_failed(solver: *mut CaDiCaLHandle) -> c_int; diff --git a/src/solvers/glucose4/core.rs b/src/solvers/glucose4/core.rs index 968799e4..33eeae35 100644 --- a/src/solvers/glucose4/core.rs +++ b/src/solvers/glucose4/core.rs @@ -253,23 +253,23 @@ impl PhaseLit for GlucoseCore4 { impl LimitConflicts for GlucoseCore4 { fn limit_conflicts(&mut self, limit: Option) -> Result<(), SolverError> { - Ok(self.set_limit(Limit::Conflicts(if let Some(limit) = limit { + self.set_limit(Limit::Conflicts(if let Some(limit) = limit { limit as i64 } else { -1 - }))) + })); + Ok(()) } } impl LimitPropagations for GlucoseCore4 { fn limit_propagations(&mut self, limit: Option) -> Result<(), SolverError> { - Ok( - self.set_limit(Limit::Propagations(if let Some(limit) = limit { - limit as i64 - } else { - -1 - })), - ) + self.set_limit(Limit::Propagations(if let Some(limit) = limit { + limit as i64 + } else { + -1 + })); + Ok(()) } } diff --git a/src/solvers/glucose4/simp.rs b/src/solvers/glucose4/simp.rs index 9b15d821..f313c497 100644 --- a/src/solvers/glucose4/simp.rs +++ b/src/solvers/glucose4/simp.rs @@ -270,23 +270,23 @@ impl PhaseLit for GlucoseSimp4 { impl LimitConflicts for GlucoseSimp4 { fn limit_conflicts(&mut self, limit: Option) -> Result<(), SolverError> { - Ok(self.set_limit(Limit::Conflicts(if let Some(limit) = limit { + self.set_limit(Limit::Conflicts(if let Some(limit) = limit { limit as i64 } else { -1 - }))) + })); + Ok(()) } } impl LimitPropagations for GlucoseSimp4 { fn limit_propagations(&mut self, limit: Option) -> Result<(), SolverError> { - Ok( - self.set_limit(Limit::Propagations(if let Some(limit) = limit { - limit as i64 - } else { - -1 - })), - ) + self.set_limit(Limit::Propagations(if let Some(limit) = limit { + limit as i64 + } else { + -1 + })); + Ok(()) } } diff --git a/src/solvers/kissat.rs b/src/solvers/kissat.rs index ee8cf5e5..bc7c1ddc 100644 --- a/src/solvers/kissat.rs +++ b/src/solvers/kissat.rs @@ -292,14 +292,12 @@ impl<'term> Terminate<'term> for Kissat<'term> { { self.terminate_cb = Some(Box::new(Box::new(cb))); let cb_ptr = self.terminate_cb.as_mut().unwrap().as_mut() as *const _ as *const c_void; - unsafe { ffi::kissat_set_terminate(self.handle, cb_ptr, ffi::kissat_terminate_cb) } + unsafe { ffi::kissat_set_terminate(self.handle, cb_ptr, Some(ffi::kissat_terminate_cb)) } } fn detach_terminator(&mut self) { self.terminate_cb = None; - let null_cb: extern "C" fn(*const c_void) -> c_int = - unsafe { std::mem::transmute(std::ptr::null::()) }; - unsafe { ffi::kissat_set_terminate(self.handle, std::ptr::null(), null_cb) } + unsafe { ffi::kissat_set_terminate(self.handle, std::ptr::null(), None) } } } @@ -484,7 +482,7 @@ mod ffi { pub fn kissat_set_terminate( solver: *mut KissatHandle, state: *const c_void, - terminate: extern "C" fn(state: *const c_void) -> c_int, + terminate: Option c_int>, ); pub fn kissat_terminate(solver: *mut KissatHandle); pub fn kissat_reserve(solver: *mut KissatHandle, max_var: c_int); diff --git a/src/solvers/minisat/core.rs b/src/solvers/minisat/core.rs index d064fff6..93866e73 100644 --- a/src/solvers/minisat/core.rs +++ b/src/solvers/minisat/core.rs @@ -252,23 +252,23 @@ impl PhaseLit for MinisatCore { impl LimitConflicts for MinisatCore { fn limit_conflicts(&mut self, limit: Option) -> Result<(), SolverError> { - Ok(self.set_limit(Limit::Conflicts(if let Some(limit) = limit { + self.set_limit(Limit::Conflicts(if let Some(limit) = limit { limit as i64 } else { -1 - }))) + })); + Ok(()) } } impl LimitPropagations for MinisatCore { fn limit_propagations(&mut self, limit: Option) -> Result<(), SolverError> { - Ok( - self.set_limit(Limit::Propagations(if let Some(limit) = limit { - limit as i64 - } else { - -1 - })), - ) + self.set_limit(Limit::Propagations(if let Some(limit) = limit { + limit as i64 + } else { + -1 + })); + Ok(()) } } diff --git a/src/solvers/minisat/simp.rs b/src/solvers/minisat/simp.rs index bd4f62d2..e9f3970f 100644 --- a/src/solvers/minisat/simp.rs +++ b/src/solvers/minisat/simp.rs @@ -269,23 +269,23 @@ impl PhaseLit for MinisatSimp { impl LimitConflicts for MinisatSimp { fn limit_conflicts(&mut self, limit: Option) -> Result<(), SolverError> { - Ok(self.set_limit(Limit::Conflicts(if let Some(limit) = limit { + self.set_limit(Limit::Conflicts(if let Some(limit) = limit { limit as i64 } else { -1 - }))) + })); + Ok(()) } } impl LimitPropagations for MinisatSimp { fn limit_propagations(&mut self, limit: Option) -> Result<(), SolverError> { - Ok( - self.set_limit(Limit::Propagations(if let Some(limit) = limit { - limit as i64 - } else { - -1 - })), - ) + self.set_limit(Limit::Propagations(if let Some(limit) = limit { + limit as i64 + } else { + -1 + })); + Ok(()) } } diff --git a/src/types/constraints.rs b/src/types/constraints.rs index 868ce648..8db5749f 100644 --- a/src/types/constraints.rs +++ b/src/types/constraints.rs @@ -156,7 +156,7 @@ impl Clause { idx += 1; } } - return Some(self); + Some(self) } }