get compiling with recent patronus changes

synth/src/basic.rs

@@ -88,6 +88,6 @@ pub fn generate_minimal_repair<S: Simulator, E: TransitionSystemEncoding, C: Sol
     let solution =
         rctx.synth_vars
             .read_assignment(rctx.ctx, &mut rctx.smt_ctx, &rctx.enc, start_step);
-    check_assuming_end(&mut rctx.smt_ctx, &rctx.solver)?;
+    check_assuming_end(&mut rctx.smt_ctx)?;
     Ok(Some((solution, min_num_changes)))
 }

synth/src/main.rs

@@ -257,7 +257,6 @@ fn main() {
         change_count_ref,
         smt_ctx,
         enc,
-        solver: args.solver.cmd(),
         verbose: args.verbose,
     };
 
@@ -295,8 +294,6 @@ fn main() {
         }
         RepairCommand::WindowingStudy => {
             let conf = WindowingConf {
-                cmd: args.solver.cmd(),
-                dump_smt: args.smt_dump.clone(),
                 fail_at,
                 max_repair_window_size: args.max_repair_window_size,
             };

synth/src/repair.rs

@@ -6,7 +6,7 @@
 use crate::testbench::{StepInt, Testbench};
 use crate::Stats;
 use baa::{BitVecOps, BitVecValue};
-use patronus::expr::{Context, ExprRef, Type, TypeCheck, WidthInt};
+use patronus::expr::{Context, ExprRef, TypeCheck, WidthInt};
 use patronus::mc::*;
 use patronus::sim::Simulator;
 use patronus::smt::{CheckSatResponse, Logic, SmtLibSolver, Solver, SolverContext};
@@ -38,7 +38,6 @@ pub struct RepairContext<'a, S: Simulator, E: TransitionSystemEncoding, C: Solve
     pub change_count_ref: ExprRef,
     pub smt_ctx: C,
     pub enc: E,
-    pub solver: SmtLibSolver,
     pub verbose: bool,
 }
 
@@ -61,7 +60,7 @@ pub fn minimize_changes<S: Simulator, E: TransitionSystemEncoding, C: SolverCont
     let mut num_changes = 1u32;
     loop {
         let constraint = constrain_changes(rctx, num_changes, start_step);
-        match check_assuming(rctx.ctx, &mut rctx.smt_ctx, [constraint], &rctx.solver)? {
+        match check_assuming(rctx.ctx, &mut rctx.smt_ctx, [constraint])? {
             CheckSatResponse::Sat => {
                 // found a solution
                 return Ok(num_changes);
@@ -70,7 +69,7 @@ pub fn minimize_changes<S: Simulator, E: TransitionSystemEncoding, C: SolverCont
             CheckSatResponse::Unknown => panic!("SMT solver returned unknown!"),
         }
         // remove assertion for next round
-        check_assuming_end(&mut rctx.smt_ctx, &rctx.solver)?;
+        check_assuming_end(&mut rctx.smt_ctx)?;
         num_changes += 1;
     }
 }
@@ -79,14 +78,15 @@ pub fn constrain_starting_state<S: Simulator, E: TransitionSystemEncoding, C: So
     rctx: &mut RepairContext<S, E, C>,
     start_step: StepInt,
 ) -> Result<()> {
-    for (_, state) in rctx
+    for state in rctx
         .sys
-        .states()
-        .filter(|(_, s)| s.init.is_none() && !rctx.synth_vars.is_repair_var(s.symbol))
+        .states
+        .iter()
+        .filter(|s| s.init.is_none() && !rctx.synth_vars.is_repair_var(s.symbol))
     {
         let symbol = rctx.enc.get_at(rctx.ctx, state.symbol, start_step);
         let value = rctx.sim.get(state.symbol).unwrap();
-        let smt_value = rctx.ctx.lit(&value);
+        let smt_value = rctx.ctx.lit(value);
         let is_equal = rctx.ctx.equal(symbol, smt_value);
         rctx.smt_ctx.assert(rctx.ctx, is_equal)?;
     }
@@ -96,7 +96,7 @@ pub fn constrain_starting_state<S: Simulator, E: TransitionSystemEncoding, C: So
 pub fn create_smt_ctx(
     solver: &SmtLibSolver,
     dump_file: Option<&str>,
-) -> Result<impl SolverContext> {
+) -> Result<impl SolverContext + 'static> {
     let replay_file = if let Some(filename) = dump_file {
         Some(std::fs::File::create(filename)?)
     } else {
@@ -134,8 +134,8 @@ impl RepairVars {
         let mut change = Vec::new();
         let mut free = Vec::new();
 
-        for (_, state) in sys.states() {
-            let name = state.symbol.get_symbol_name(ctx).unwrap();
+        for state in sys.states.iter() {
+            let name = ctx.get_symbol_name(state.symbol).unwrap();
             match classify_state(name) {
                 StateType::ChangeVar => {
                     assert_eq!(
@@ -187,12 +187,12 @@ impl RepairVars {
 
         for (sym, value) in self.change.iter().zip(assignment.change.iter()) {
             let num_value = if *value { 1 } else { 0 };
-            let sym_name = sym.get_symbol_name(ctx).unwrap().to_string();
+            let sym_name = ctx.get_symbol_name(*sym).unwrap().to_string();
             out.insert(sym_name, json!(num_value));
         }
         for ((sym, _width), value) in self.free.iter().zip(assignment.free.iter()) {
-            let num_value = serde_json::Number::from_str(&value.to_string()).unwrap();
-            let sym_name = ctx.get_symbol_name(sym).unwrap().to_string();
+            let num_value = serde_json::Number::from_str(&value.to_dec_str()).unwrap();
+            let sym_name = ctx.get_symbol_name(*sym).unwrap().to_string();
             out.insert(sym_name, json!(num_value));
         }
 

synth/src/studies/windowing.rs

@@ -13,15 +13,13 @@ use crate::restart_solver;
 use crate::testbench::{RunConfig, StepInt, StopAt};
 use patronus::mc::{TransitionSystemEncoding, UnrollSmtEncoding};
 use patronus::sim::Simulator;
-use patronus::smt::{CheckSatResponse, SmtLibSolver, SolverContext};
+use patronus::smt::{CheckSatResponse, SolverContext};
 use serde::Serialize;
 use std::collections::HashMap;
 use std::fmt::Debug;
 use std::time::Instant;
 
 pub struct WindowingConf {
-    pub cmd: SmtLibSolver,
-    pub dump_smt: Option<String>,
     /// Information about the first cycle in which the bug manifests.
     pub fail_at: StepInt,
     /// The maximum size of the repair window.

synth/src/testbench.rs

@@ -4,7 +4,7 @@
 // author: Kevin Laeufer <[email protected]>
 
 use crate::repair::{classify_state, CHANGE_COUNT_OUTPUT_NAME};
-use baa::{BitVecOps, BitVecValue};
+use baa::{BitVecOps, BitVecValue, Value};
 use patronus::expr::{Context, ExprRef, TypeCheck, WidthInt};
 use patronus::mc::TransitionSystemEncoding;
 use patronus::sim::{InitKind, Simulator};
@@ -238,7 +238,7 @@ impl Testbench {
         if !self.signals_to_print.is_empty() {
             println!();
             for (name, expr) in self.signals_to_print.iter() {
-                if let Some(value) = sim.get(*expr) {
+                if let Some(Value::BitVec(value)) = sim.get(*expr) {
                     println!("{name}@{step_id} = {}", value.to_bit_str())
                 }
             }
@@ -249,7 +249,7 @@ impl Testbench {
         for (io, maybe_value) in self.ios.iter().zip(io_values.iter()) {
             if !io.is_input {
                 if let Some(expected_value) = maybe_value {
-                    let actual_value = sim.get(io.expr).unwrap();
+                    let actual_value: BitVecValue = sim.get(io.expr).unwrap().try_into().unwrap();
                     if *expected_value != actual_value {
                         failures.push(Failure {
                             step: step_id,