From 689641386ddb8a4d2f6e096c92fcaa7d3b71bcaa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Tue, 16 Apr 2024 15:33:05 -0400 Subject: [PATCH] synth: fix clippy warnings --- synth/src/basic.rs | 11 +++-------- synth/src/filters.rs | 2 +- synth/src/incremental.rs | 6 +++--- synth/src/repair.rs | 8 ++++---- synth/src/windowing.rs | 10 +++++----- 5 files changed, 16 insertions(+), 21 deletions(-) diff --git a/synth/src/basic.rs b/synth/src/basic.rs index ed5ffe9..60b5478 100644 --- a/synth/src/basic.rs +++ b/synth/src/basic.rs @@ -54,13 +54,8 @@ pub fn generate_minimal_repair( } 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( 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 index 5828ca0..b856349 100644 --- a/synth/src/filters.rs +++ b/synth/src/filters.rs @@ -23,7 +23,7 @@ pub fn can_be_repaired_from_arbitrary_state 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 index ab73be6..bc0c6b3 100644 --- a/synth/src/repair.rs +++ b/synth/src/repair.rs @@ -52,12 +52,12 @@ pub fn constrain_changes( 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( @@ -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 index c83fad9..b32d337 100644 --- 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,7 +192,7 @@ 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, )?; @@ -200,7 +200,7 @@ where 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,7 +212,7 @@ 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 { @@ -220,7 +220,7 @@ where correct_repair_tries: None, correct_repair_ns: None, }; - Ok((stats, make_result(None, &window))) + Ok((stats, make_result(None, window))) } } }