make incremental synthesizer more reusable

synth/Cargo.toml

@@ -12,6 +12,7 @@ libpatron = "0.16.0"
 memmap2 = "0.9.0"
 num-bigint = "0.4.4"
 num-traits = "0.2.17"
+serde = { version = "1.0.197", features = ["derive"] }
 serde_json = { version = "1.0.108", features = ["preserve_order"] }
 
 [profile.release]

synth/src/incremental.rs

@@ -61,7 +61,13 @@ where
             }
 
             // check to see if we can reproduce the error with the simulator
-            self.update_sim_state_to_step(step_range.start);
+            let verbose = self.verbose();
+            update_sim_state_to_step(
+                &mut self.rctx,
+                &mut self.snapshots,
+                verbose,
+                step_range.start,
+            );
             let conf = RunConfig {
                 start: step_range.start,
                 stop: StopAt::first_fail_or_step(step_range.end),
@@ -74,7 +80,13 @@ where
             self.rctx.smt_ctx.push_many(1)?;
 
             // restore correct starting state for SMT encoding
-            self.update_sim_state_to_step(step_range.start);
+            let verbose = self.verbose();
+            update_sim_state_to_step(
+                &mut self.rctx,
+                &mut self.snapshots,
+                verbose,
+                step_range.start,
+            );
 
             // generate one minimal repair
             let r =
@@ -84,7 +96,7 @@ where
 
             if let Some((r0, num_changes)) = r {
                 // add a "permanent" change count constraint
-                self.constrain_changes(num_changes, step_range.start)?;
+                constrain_changes(&mut self.rctx, num_changes, step_range.start)?;
 
                 // iterate over possible solutions
                 let mut maybe_repair = Some(r0);
@@ -97,7 +109,10 @@ where
                                 .get_change_names(self.rctx.ctx, &repair)
                         );
                     }
-                    match self.test_repair(&repair).first_fail_at {
+                    let verbose = self.verbose();
+                    match test_repair(&mut self.rctx, &mut self.snapshots, verbose, &repair)
+                        .first_fail_at
+                    {
                         None => {
                             // success, we found a solution
                             correct_solutions.push(repair.clone());
@@ -176,54 +191,78 @@ where
     fn verbose(&self) -> bool {
         self.rctx.verbose
     }
+}
 
-    fn test_repair(&mut self, repair: &RepairAssignment) -> RunResult {
-        let start_step = 0;
-        self.update_sim_state_to_step(start_step);
-        self.rctx
-            .synth_vars
-            .apply_to_sim(&mut self.rctx.sim, repair);
-        let conf = RunConfig {
-            start: start_step,
-            stop: StopAt::first_fail(),
-        };
-        self.rctx.tb.run(&mut self.rctx.sim, &conf, false)
-    }
+fn test_repair<S, E>(
+    rctx: &mut RepairContext<S, E>,
+    snapshots: &mut HashMap<StepInt, S::SnapshotId>,
+    verbose: bool,
+    repair: &RepairAssignment,
+) -> RunResult
+where
+    S: Simulator,
+    E: TransitionSystemEncoding,
+    S::SnapshotId: Clone,
+{
+    let start_step = 0;
+    update_sim_state_to_step(rctx, snapshots, verbose, start_step);
+    rctx.synth_vars.apply_to_sim(&mut rctx.sim, repair);
+    let conf = RunConfig {
+        start: start_step,
+        stop: StopAt::first_fail(),
+    };
+    rctx.tb.run(&mut rctx.sim, &conf, false)
+}
 
-    fn constrain_changes(&mut self, num_changes: u32, start_step: StepInt) -> Result<()> {
-        let constraint = constrain_changes(&mut self.rctx, num_changes, start_step);
-        self.rctx.smt_ctx.assert(constraint)?;
-        Ok(())
-    }
+fn constrain_changes<S, E>(
+    rctx: &mut RepairContext<S, E>,
+    num_changes: u32,
+    start_step: StepInt,
+) -> Result<()>
+where
+    S: Simulator,
+    E: TransitionSystemEncoding,
+{
+    let constraint = crate::repair::constrain_changes(rctx, num_changes, start_step);
+    rctx.smt_ctx.assert(constraint)?;
+    Ok(())
+}
 
-    fn update_sim_state_to_step(&mut self, step: StepInt) {
-        assert!(step < self.rctx.tb.step_count());
-        if let Some(snapshot_id) = self.snapshots.get(&step) {
-            self.rctx.sim.restore_snapshot(snapshot_id.clone());
-        } else {
-            // find nearest step, _before_ the step we are going for
-            let mut nearest_step = 0;
-            let mut nearest_id = self.snapshots[&0].clone();
-            for (other_step, snapshot_id) in self.snapshots.iter() {
-                if *other_step < step && *other_step > nearest_step {
-                    nearest_step = *other_step;
-                    nearest_id = snapshot_id.clone();
-                }
+fn update_sim_state_to_step<S, E>(
+    rctx: &mut RepairContext<S, E>,
+    snapshots: &mut HashMap<StepInt, S::SnapshotId>,
+    verbose: bool,
+    step: StepInt,
+) where
+    S: Simulator,
+    E: TransitionSystemEncoding,
+    S::SnapshotId: Clone,
+{
+    assert!(step < rctx.tb.step_count());
+    if let Some(snapshot_id) = snapshots.get(&step) {
+        rctx.sim.restore_snapshot(snapshot_id.clone());
+    } else {
+        // find nearest step, _before_ the step we are going for
+        let mut nearest_step = 0;
+        let mut nearest_id = snapshots[&0].clone();
+        for (other_step, snapshot_id) in snapshots.iter() {
+            if *other_step < step && *other_step > nearest_step {
+                nearest_step = *other_step;
+                nearest_id = snapshot_id.clone();
             }
+        }
 
-            // go from nearest snapshot to the point where we want to take a snapshot
-            self.rctx.sim.restore_snapshot(nearest_id);
-            let run_conf = RunConfig {
-                start: nearest_step,
-                stop: StopAt::step(step),
-            };
-            let verbose = self.verbose();
-            self.rctx.tb.run(&mut self.rctx.sim, &run_conf, verbose);
+        // go from nearest snapshot to the point where we want to take a snapshot
+        rctx.sim.restore_snapshot(nearest_id);
+        let run_conf = RunConfig {
+            start: nearest_step,
+            stop: StopAt::step(step),
+        };
+        rctx.tb.run(&mut rctx.sim, &run_conf, verbose);
 
-            // remember the state in case we need to go back
-            let new_snapshot = self.rctx.sim.take_snapshot();
-            self.snapshots.insert(step, new_snapshot.clone());
-        }
+        // remember the state in case we need to go back
+        let new_snapshot = rctx.sim.take_snapshot();
+        snapshots.insert(step, new_snapshot.clone());
     }
 }
 

synth/src/main.rs

@@ -119,7 +119,8 @@ fn main() {
     );
 
     // load system
-    let (mut ctx, mut sys) = btor2::parse_file(&args.design).expect("Failed to load btor2 file!");
+    let (mut ctx, mut sys) = btor2::parse_file(&args.design)
+        .unwrap_or_else(|| panic!("Failed to load btor2 file `{}`!", args.design));
 
     // simplify system
     replace_anonymous_inputs_with_zero(&mut ctx, &mut sys);
@@ -341,19 +342,9 @@ fn print_no_repair(synth_vars: &RepairVars, ctx: &Context) {
     print_result(&res, synth_vars, ctx);
 }
 
-#[derive(Debug, Copy, Clone, Eq, PartialEq)]
+#[derive(Debug, Copy, Clone, Eq, PartialEq, Default)]
 pub struct Stats {
     final_past_k: StepInt,
     final_future_k: StepInt,
     solver_time: u64,
 }
-
-impl Default for Stats {
-    fn default() -> Self {
-        Self {
-            final_past_k: 0,
-            final_future_k: 0,
-            solver_time: 0,
-        }
-    }
-}

synth/src/windowing.rs

@@ -8,6 +8,7 @@
 use crate::repair::{RepairContext, RepairResult, Result};
 use crate::testbench::StepInt;
 use libpatron::mc::{Simulator, TransitionSystemEncoding};
+use serde::Serialize;
 use std::fmt::Debug;
 
 pub struct WindowingConf {
@@ -22,16 +23,78 @@ pub struct Windowing<'a, S: Simulator, E: TransitionSystemEncoding> {
     conf: WindowingConf,
 }
 
+#[derive(Debug, Serialize)]
+struct Stats {
+    /// time it took to sample the first minimal repair
+    minimal_repair_candidate_ns: Option<u64>,
+    /// number of minimal repairs sampled before we found a correct repair
+    correct_repair_tries: Option<u64>,
+    /// time to find a correct repair
+    correct_repair_ns: Option<u64>,
+}
+
+#[derive(Debug, Serialize)]
+struct WindowConf {
+    past_k: StepInt,
+    future_k: StepInt,
+    window_size: StepInt,
+    offset: StepInt,
+}
+
+impl WindowConf {
+    fn get_step_range(&self, fail_at: StepInt) -> std::ops::Range<StepInt> {
+        let start = if self.past_k < fail_at {
+            fail_at - self.past_k
+        } else {
+            0
+        };
+        let end = fail_at + self.future_k;
+        start..end
+    }
+}
+
+#[derive(Debug, Serialize)]
+struct Line {
+    conf: WindowConf,
+    stats: Stats,
+}
+
 impl<'a, S: Simulator, E: TransitionSystemEncoding> Windowing<'a, S, E>
 where
     S: Simulator,
     <S as Simulator>::SnapshotId: Clone + Debug,
 {
-    pub fn new(rctx: RepairContext<'a, S, E>, conf: WindowingConf) -> crate::repair::Result<Self> {
+    pub fn new(rctx: RepairContext<'a, S, E>, conf: WindowingConf) -> Result<Self> {
         Ok(Self { rctx, conf })
     }
 
     pub fn run(&mut self) -> Result<RepairResult> {
+        // iterate over all possible window sizes
+        for window_size in 1..=self.conf.max_repair_window_size {
+            // iterate over all window shifts that contain the output divergence step
+            for offset in 0..window_size {
+                // derive past and future k
+                let past_k = window_size - 1 + offset;
+                let future_k = window_size - 1 - past_k;
+                assert_eq!(past_k + future_k + 1, window_size);
+                let c = WindowConf {
+                    past_k,
+                    future_k,
+                    window_size,
+                    offset,
+                };
+                let (stats, _result) = self.inner(&c)?;
+                let l = Line { conf: c, stats };
+                println!("{}", serde_json::to_string(&l).unwrap());
+            }
+        }
+
         todo!()
     }
+
+    fn inner(&mut self, window: &WindowConf) -> Result<(Stats, RepairResult)> {
+        let step_range = window.get_step_range(self.conf.fail_at);
+
+        todo!();
+    }
 }