chore(solver): fix clippy lints

plaans · Dec 20, 2024 · 489f353 · 489f353
1 parent f365f5d
commit 489f353
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 11 deletions.
diff --git a/solver/src/core/state/domains.rs b/solver/src/core/state/domains.rs
@@ -429,18 +429,18 @@ impl Domains {
         explanation.push(self.presence(literal));
 
         if cause != Origin::ASSUMPTION {
-        // However, `literal` does not hold in the current state and we need to replace it.
-        // Thus we replace it with a set of literals `x_1 & ... & x_m` such that
-        // `x_1 & ... & x_m -> literal`
-        self.add_implying_literals_to_explanation(literal, cause, &mut explanation, explainer);
-        debug_assert!(explanation.lits.iter().copied().all(|l| self.entails(l)));
+            // However, `literal` does not hold in the current state and we need to replace it.
+            // Thus we replace it with a set of literals `x_1 & ... & x_m` such that
+            // `x_1 & ... & x_m -> literal`
+            self.add_implying_literals_to_explanation(literal, cause, &mut explanation, explainer);
+            debug_assert!(explanation.lits.iter().copied().all(|l| self.entails(l)));
         }
         // now all disjuncts hold in the current state
         // we then transform this clause to be in the first unique implication point (1UIP) form.
         let mut conflict = self.refine_explanation(explanation, explainer);
 
         if cause == Origin::ASSUMPTION {
-            conflict.clause = Disjunction::new([conflict.clause.literals(), &vec![!literal]].concat());
+            conflict.clause = Disjunction::new([conflict.clause.literals(), &[!literal]].concat());
         }
         conflict
     }
@@ -552,7 +552,6 @@ impl Domains {
         }
 
         self.queue.clear();
-        let mut result_as_litset = LitSet::new();// ::with_capacity(num_assumptions);
 
         loop {
             for l in explanation.lits.drain(..) {
@@ -581,7 +580,7 @@ impl Domains {
         };
         let mut result_as_expl = Explanation::new();
         for l in result_as_litset.literals() { result_as_expl.push(l); }
-        return result_as_expl;
+        result_as_expl
 
     }
 

diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs
@@ -595,7 +595,7 @@ impl<Lbl: Label> Solver<Lbl> {
             SolveResult::ExternalSolution(s) => Ok(Ok(s)),
             SolveResult::Unsat(conflict) => {
                 let unsat_core = self.model.state.extract_unsat_core(conflict, &mut self.reasoners);
-                return Ok(Err(unsat_core));
+                Ok(Err(unsat_core))
             }
         }
     }
@@ -843,7 +843,7 @@ impl<Lbl: Label> Solver<Lbl> {
 
         if let Some(dl) = self.backtrack_level_for_clause(expl.literals(), last_assumption_dec_lvl) {
             // inform the brancher that we are in a conflict state
-            self.brancher.conflict(&expl, &self.model, &mut self.reasoners, dl);
+            self.brancher.conflict(expl, &self.model, &mut self.reasoners, dl);
             // backtrack
             self.restore(dl);
             // println!("conflict:");
@@ -875,7 +875,6 @@ impl<Lbl: Label> Solver<Lbl> {
     ///  - propagating in the current state
     ///    - return if no conflict was detected
     ///    - otherwise: learn a conflicting clause, backtrack up the decision tree and repeat the process.
-    #[must_use]
     pub fn propagate_and_backtrack_to_consistent(&mut self, last_assumption_dec_lvl: DecLvl) -> Result<(), Conflict> {
         loop {
             match self.propagate() {