synth: fix clippy warnings

ekiwi · Apr 16, 2024 · 6896413 · 6896413
1 parent 283a5a8
commit 6896413
Show file tree

Hide file tree

Showing 5 changed files with 16 additions and 21 deletions.
diff --git a/synth/src/basic.rs b/synth/src/basic.rs
@@ -54,13 +54,8 @@ pub fn generate_minimal_repair<S: Simulator, E: TransitionSystemEncoding>(
     }
 
     let start_apply_const = std::time::Instant::now();
-    rctx.tb.apply_constraints(
-        rctx.ctx,
-        &mut rctx.smt_ctx,
-        &mut rctx.enc,
-        start_step,
-        end_step,
-    )?;
+    rctx.tb
+        .apply_constraints(rctx.ctx, &mut rctx.smt_ctx, &rctx.enc, start_step, end_step)?;
     if rctx.verbose {
         println!(
             "Took {:?} to apply constraints",
@@ -91,7 +86,7 @@ pub fn generate_minimal_repair<S: Simulator, E: TransitionSystemEncoding>(
 
     let solution =
         rctx.synth_vars
-            .read_assignment(rctx.ctx, &mut rctx.smt_ctx, &mut rctx.enc, start_step);
+            .read_assignment(rctx.ctx, &mut rctx.smt_ctx, &rctx.enc, start_step);
     check_assuming_end(&mut rctx.smt_ctx, &rctx.solver)?;
     Ok(Some((solution, min_num_changes)))
 }
diff --git a/synth/src/filters.rs b/synth/src/filters.rs
@@ -23,7 +23,7 @@ pub fn can_be_repaired_from_arbitrary_state<S: Simulator, E: TransitionSystemEnc
 
     // apply output / input constraints
     rctx.tb
-        .apply_constraints(rctx.ctx, &mut rctx.smt_ctx, &mut rctx.enc, fail_at, fail_at)?;
+        .apply_constraints(rctx.ctx, &mut rctx.smt_ctx, &rctx.enc, fail_at, fail_at)?;
 
     // let's seee if a solution exists
     let r = rctx.smt_ctx.check()?;

diff --git a/synth/src/incremental.rs b/synth/src/incremental.rs
@@ -139,15 +139,15 @@ where
                     self.rctx.synth_vars.block_assignment(
                         self.rctx.ctx,
                         &mut self.rctx.smt_ctx,
-                        &mut self.rctx.enc,
+                        &self.rctx.enc,
                         &repair,
                         step_range.start,
                     )?;
                     maybe_repair = match self.rctx.smt_ctx.check()? {
                         Response::Sat => Some(self.rctx.synth_vars.read_assignment(
                             self.rctx.ctx,
                             &mut self.rctx.smt_ctx,
-                            &mut self.rctx.enc,
+                            &self.rctx.enc,
                             step_range.start,
                         )),
                         Response::Unsat | Response::Unknown => None,
@@ -317,7 +317,7 @@ impl RepairWindow {
         past_step_size: StepInt,
         max_window_size: StepInt,
     ) -> bool {
-        let old = self.clone();
+        let old = *self;
         // when no solution is found, we update the past K
         // in order to get a more accurate starting state
         if failures.is_empty() {

diff --git a/synth/src/repair.rs b/synth/src/repair.rs
@@ -52,12 +52,12 @@ pub fn constrain_changes<S: Simulator, E: TransitionSystemEncoding>(
         rctx.change_count_ref,
         start_step,
     );
-    let constraint = rctx.smt_ctx.eq(
+    // constraint
+    rctx.smt_ctx.eq(
         change_count_expr,
         rctx.smt_ctx
             .binary(change_count_width as usize, num_changes),
-    );
-    constraint
+    )
 }
 
 pub fn minimize_changes<S: Simulator, E: TransitionSystemEncoding>(
@@ -200,7 +200,7 @@ impl RepairVars {
     }
 
     pub fn is_repair_var(&self, other: ExprRef) -> bool {
-        self.change.contains(&other) || self.free.iter().find(|(e, _)| *e == other).is_some()
+        self.change.contains(&other) || self.free.iter().any(|(e, _)| *e == other)
     }
 
     pub fn apply_to_sim(&self, sim: &mut impl Simulator, assignment: &RepairAssignment) {

diff --git a/synth/src/windowing.rs b/synth/src/windowing.rs
@@ -179,7 +179,7 @@ where
                             correct_repair_tries: Some((failures_at.len() + 1) as u64),
                             correct_repair_ns,
                         };
-                        return Ok((stats, make_result(Some(repair), &window)));
+                        return Ok((stats, make_result(Some(repair), window)));
                     }
                     Some(fail) => {
                         if verbose {
@@ -192,15 +192,15 @@ where
                 self.rctx.synth_vars.block_assignment(
                     self.rctx.ctx,
                     &mut self.rctx.smt_ctx,
-                    &mut self.rctx.enc,
+                    &self.rctx.enc,
                     &repair,
                     step_range.start,
                 )?;
                 maybe_repair = match self.rctx.smt_ctx.check()? {
                     Response::Sat => Some(self.rctx.synth_vars.read_assignment(
                         self.rctx.ctx,
                         &mut self.rctx.smt_ctx,
-                        &mut self.rctx.enc,
+                        &self.rctx.enc,
                         step_range.start,
                     )),
                     Response::Unsat | Response::Unknown => None,
@@ -212,15 +212,15 @@ where
                 correct_repair_tries: None,
                 correct_repair_ns: None,
             };
-            Ok((stats, make_result(None, &window)))
+            Ok((stats, make_result(None, window)))
         } else {
             // no repair found
             let stats = Stats {
                 minimal_repair_candidate_ns: None,
                 correct_repair_tries: None,
                 correct_repair_ns: None,
             };
-            Ok((stats, make_result(None, &window)))
+            Ok((stats, make_result(None, window)))
         }
     }
 }