synth: add option to limit the number of solutions per window size

ekiwi · Jan 6, 2024 · 9f9e29b · 9f9e29b
1 parent 901219b
commit 9f9e29b
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 2 deletions.
diff --git a/synth/src/incremental.rs b/synth/src/incremental.rs
@@ -13,10 +13,16 @@ use crate::repair::*;
 use crate::Stats;
 
 pub struct IncrementalConf {
+    /// Information about the first cycle in which the bug manifests.
     pub fail_at: StepInt,
+    /// Number by which the window is expanded into the past.
     pub pask_k_step_size: StepInt,
+    /// The maximum size of the repair window.
     pub max_repair_window_size: StepInt,
+    /// The maximum number of correct solutions that should be generated.
     pub max_solutions: usize,
+    /// The maximum number of incorrect solution to try before enlarging the repair window.
+    pub max_incorrect_solutions_per_window_size: Option<usize>,
 }
 
 pub struct IncrementalRepair<'a, S: Simulator, E: TransitionSystemEncoding> {
@@ -104,20 +110,27 @@ where
                                 println!("New fail at: {fail}");
                             }
                             failures_at.push(fail);
+                            if let Some(max_sol) = self.conf.max_incorrect_solutions_per_window_size
+                            {
+                                if failures_at.len() >= max_sol {
+                                    println!("Reached the maximum number of incorrect solutions. Going to increase the window.");
+                                    break;
+                                }
+                            }
                         }
                     }
                     // try to find a different solution
                     self.rctx.synth_vars.block_assignment(
                         self.rctx.ctx,
-                        &mut self.rctx.smt_ctx,
+                        self.rctx.smt_ctx,
                         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,
+                            self.rctx.smt_ctx,
                             self.rctx.enc,
                             step_range.start,
                         )),

diff --git a/synth/src/main.rs b/synth/src/main.rs
@@ -76,6 +76,11 @@ struct Args {
     max_repair_window_size: u64,
     #[arg(long, help = "file to write all SMT commands to")]
     smt_dump: Option<String>,
+    #[arg(
+        long,
+        help = "the maximum number of incorrect solution to try before enlarging the repair window"
+    )]
+    max_incorrect_solutions_per_window_size: Option<usize>,
 }
 
 #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, ValueEnum)]
@@ -243,6 +248,7 @@ fn main() {
             pask_k_step_size: args.pask_k_step_size,
             max_repair_window_size: args.max_repair_window_size,
             max_solutions: 1,
+            max_incorrect_solutions_per_window_size: args.max_incorrect_solutions_per_window_size,
         };
         let mut snapshots = HashMap::new();
         snapshots.insert(0, start_state);