getting a solution with the simple synthesizer

synth/.gitignore

@@ -0,0 +1,4 @@
+basic.smt
+flamegraph.svg
+perf.data
+perf.data.old

synth/Cargo.toml

@@ -13,3 +13,6 @@ memmap2 = "0.9.0"
 num-bigint = "0.4.4"
 num-traits = "0.2.17"
 serde_json = { version = "1.0.108", features = ["preserve_order"] }
+
+[profile.release]
+debug = 1

synth/src/basic.rs

@@ -2,10 +2,11 @@
 // released under BSD 3-Clause License
 // author: Kevin Laeufer <[email protected]>
 
-use crate::repair::{RepairAssignment, RepairVars};
+use crate::repair::{RepairAssignment, RepairVars, CHANGE_COUNT_WIDTH};
 use crate::testbench::Testbench;
 use crate::Solver;
 use easy_smt as smt;
+use easy_smt::Response;
 use libpatron::ir::*;
 use libpatron::mc::{Simulator, SmtSolverCmd, TransitionSystemEncoding, UnrollSmtEncoding};
 use libpatron::sim::interpreter::ValueRef;
@@ -25,6 +26,7 @@ pub fn basic_repair(
     sim: &impl Simulator,
     tb: &Testbench,
     conf: &BasicConfig,
+    change_count_ref: ExprRef,
 ) -> Result<Option<Vec<RepairAssignment>>> {
     let mut smt_ctx = create_smt_ctx(&conf.solver, conf.dump_file.as_deref())?;
 
@@ -36,17 +38,72 @@ pub fn basic_repair(
     // constrain starting state to that from the simulator
     constrain_starting_state(sys, synth_vars, sim, &enc, &mut smt_ctx)?;
 
+    let start_unroll = std::time::Instant::now();
     // unroll system and constrain inputs and outputs
     for _ in 0..(tb.step_count() - 1) {
         enc.unroll(&mut smt_ctx)?;
     }
+    if conf.verbose {
+        println!(
+            "Took {:?} to unroll",
+            std::time::Instant::now() - start_unroll
+        );
+    }
+
+    let start_apply_const = std::time::Instant::now();
     tb.apply_constraints(&mut smt_ctx, &enc)?;
+    if conf.verbose {
+        println!(
+            "Took {:?} to apply constraints",
+            std::time::Instant::now() - start_apply_const
+        );
+    }
 
     // check to see if a solution exists
+    let start_check = std::time::Instant::now();
     let r = smt_ctx.check()?;
-    println!("{r:?}");
+    let check_duration = std::time::Instant::now() - start_check;
+    if conf.verbose {
+        println!("Check-Sat took {check_duration:?}");
+    }
+    match r {
+        // cannot find a repair
+        Response::Unsat | Response::Unknown => return Ok(None),
+        Response::Sat => {} // OK, continue
+    }
+
+    // find a minimal repair
+    let min_num_changes = minimize_changes(&mut smt_ctx, change_count_ref, &enc)?;
+    if conf.verbose {
+        println!("Found a minimal solution with {min_num_changes} changes.")
+    }
+
+    let solution = synth_vars.read_assignment(&mut smt_ctx, &enc);
+    Ok(Some(vec![solution]))
+}
 
-    Ok(None)
+fn minimize_changes(
+    smt_ctx: &mut smt::Context,
+    change_count_ref: ExprRef,
+    enc: &impl TransitionSystemEncoding,
+) -> Result<u32> {
+    let mut num_changes = 1u32;
+    let change_count_expr = enc.get_at(smt_ctx, change_count_ref, 0);
+    loop {
+        let constraint = smt_ctx.eq(
+            change_count_expr,
+            smt_ctx.binary(CHANGE_COUNT_WIDTH as usize, num_changes),
+        );
+        match smt_ctx.check_assuming([constraint])? {
+            Response::Sat => {
+                // found a solution
+                return Ok(num_changes);
+            }
+            Response::Unsat => {}
+            Response::Unknown => panic!("SMT solver returned unknown!"),
+        }
+        num_changes += 1;
+    }
 }
 
 fn constrain_starting_state(

synth/src/main.rs

@@ -103,7 +103,7 @@ fn main() {
     }
 
     // add a change count to the system
-    add_change_count(&mut ctx, &mut sys, &synth_vars.change);
+    let change_count_ref = add_change_count(&mut ctx, &mut sys, &synth_vars.change);
 
     // print system
     if args.verbose {
@@ -158,6 +158,7 @@ fn main() {
     sim.restore_snapshot(start_state);
 
     // call to the synthesizer
+    let start_synth = std::time::Instant::now();
     let repair = if args.incremental {
         todo!("implement incremental synthesizer")
     } else {
@@ -166,17 +167,22 @@ fn main() {
             verbose: args.verbose,
             dump_file: Some("basic.smt".to_string()),
         };
-        basic_repair(&ctx, &sys, &synth_vars, &sim, &tb, &conf)
+        basic_repair(&ctx, &sys, &synth_vars, &sim, &tb, &conf, change_count_ref)
             .expect("failed to execute basic synthesizer")
     };
+    let synth_duration = std::time::Instant::now() - start_synth;
+    if args.verbose {
+        println!("Synthesizer took {synth_duration:?}");
+    }
 
     // print status
     let (status, solutions) = match repair {
         None => ("cannot-repair", json!([])),
         Some(assignments) => {
             let mut res = Vec::with_capacity(assignments.len());
             for aa in assignments.iter() {
-                res.push(synth_vars.to_json(&ctx, aa));
+                let assignment_json = synth_vars.to_json(&ctx, aa);
+                res.push(json!({"assignment": assignment_json}));
             }
             ("success", json!(res))
         }

synth/src/repair.rs

@@ -112,7 +112,7 @@ pub struct RepairAssignment {
 }
 
 const CHANGE_COUNT_OUTPUT_NAME: &str = "__change_count";
-const CHANGE_COUNT_WIDTH: WidthInt = 16;
+pub const CHANGE_COUNT_WIDTH: WidthInt = 16;
 
 pub fn add_change_count(
     ctx: &mut Context,