wip: upgrade to a much newer version of patronus

synth/Cargo.toml

@@ -6,14 +6,13 @@ edition = "2021"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-clap =  { version = "4.4.11", features = ["derive"] }
-easy-smt = "0.2.1"
-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"] }
+clap =  { version = "4.5", features = ["derive"] }
+patronus = "0.32.0"
+memmap2 = "0.9.5"
+num-bigint = "0.4.6"
+num-traits = "0.2.19"
+serde = { version = "1.0", features = ["derive"] }
+serde_json = { version = "1.0", features = ["preserve_order"] }
 
 [profile.release]
 debug = 1

synth/src/basic.rs

@@ -1,13 +1,14 @@
 // Copyright 2023-2024 The Regents of the University of California
+// Copyright 2025 Cornell University
 // released under BSD 3-Clause License
-// author: Kevin Laeufer <[email protected]>
-
-use easy_smt as smt;
-use libpatron::mc::*;
+// author: Kevin Laeufer <[email protected]>
 
 use crate::repair::*;
 use crate::testbench::StepInt;
 use crate::Stats;
+use easy_smt as smt;
+use patronus::mc::*;
+use patronus::sim::Simulator;
 
 pub fn basic_repair<S: Simulator, E: TransitionSystemEncoding>(
     mut rctx: RepairContext<S, E>,

synth/src/filters.rs

@@ -1,11 +1,13 @@
 // Copyright 2023-2024 The Regents of the University of California
+// Copyright 2025 Cornell University
 // released under BSD 3-Clause License
-// author: Kevin Laeufer <laeufer@berkeley.edu>
+// author: Kevin Laeufer <laeufer@cornell.edu>
 
 use crate::repair::RepairContext;
 use crate::testbench::StepInt;
 use easy_smt::Response;
-use libpatron::mc::{Simulator, TransitionSystemEncoding};
+use patronus::mc::TransitionSystemEncoding;
+use patronus::sim::Simulator;
 
 /// Quick check with no unrolling which can tell if there is no way to repair the design with
 /// the provided repair variables.

synth/src/incremental.rs

@@ -1,17 +1,18 @@
 // Copyright 2023-2024 The Regents of the University of California
+// Copyright 2025 Cornell University
 // released under BSD 3-Clause License
-// author: Kevin Laeufer <laeufer@berkeley.edu>
+// author: Kevin Laeufer <laeufer@cornell.edu>
 
 use crate::basic::generate_minimal_repair;
+use crate::repair::*;
 use crate::testbench::{RunConfig, RunResult, StepInt, StopAt};
+use crate::Stats;
 use easy_smt::Response;
-use libpatron::mc::*;
+use patronus::mc::*;
+use patronus::sim::Simulator;
 use std::collections::HashMap;
 use std::fmt::Debug;
 
-use crate::repair::*;
-use crate::Stats;
-
 pub struct IncrementalConf {
     /// Information about the first cycle in which the bug manifests.
     pub fail_at: StepInt,

synth/src/main.rs

@@ -19,15 +19,13 @@ use crate::studies::windowing::{Windowing, WindowingConf};
 use crate::testbench::*;
 use clap::{arg, Parser, ValueEnum};
 use easy_smt as smt;
-use libpatron::ir::{
-    replace_anonymous_inputs_with_zero, simplify_expressions, Context, SerializableIrNode,
-    TransitionSystem,
-};
-use libpatron::mc::{
-    Simulator, SmtSolverCmd, TransitionSystemEncoding, UnrollSmtEncoding, BITWUZLA_CMD, YICES2_CMD,
-};
-use libpatron::sim::interpreter::InitKind;
-use libpatron::*;
+use patronus::btor2;
+use patronus::expr::{Context, SerializableIrNode};
+use patronus::mc::{TransitionSystemEncoding, UnrollSmtEncoding};
+use patronus::sim::{Interpreter, Simulator};
+use patronus::smt::{SmtLibSolver, BITWUZLA, YICES2};
+use patronus::system::transform::{replace_anonymous_inputs_with_zero, simplify_expressions};
+use patronus::system::TransitionSystem;
 use serde_json::json;
 use std::collections::HashMap;
 
@@ -100,10 +98,10 @@ pub enum Solver {
 }
 
 impl Solver {
-    pub fn cmd(&self) -> SmtSolverCmd {
+    pub fn cmd(&self) -> SmtLibSolver {
         match self {
-            Solver::Bitwuzla => BITWUZLA_CMD,
-            Solver::Yices2 => YICES2_CMD,
+            Solver::Bitwuzla => BITWUZLA,
+            Solver::Yices2 => YICES2,
         }
     }
 }
@@ -164,7 +162,7 @@ fn main() {
     }
 
     let sim_ctx = ctx.clone();
-    let mut sim = sim::interpreter::Interpreter::new(&sim_ctx, &sys);
+    let mut sim = Interpreter::new(&sim_ctx, &sys);
 
     // load testbench
     let mut tb = Testbench::load(&ctx, &sys, &args.testbench, args.verbose, args.trace_sim)
@@ -173,7 +171,7 @@ fn main() {
     // init free variables
     match args.init {
         Init::Zero => {
-            sim.init(InitKind::Zero);
+            sim.init();
             tb.define_inputs(InitKind::Zero);
         }
         Init::Random => {
@@ -328,7 +326,7 @@ fn main() {
 }
 
 pub fn start_solver(
-    cmd: &SmtSolverCmd,
+    cmd: &SmtLibSolver,
     smt_dump: Option<&str>,
     ctx: &mut Context,
     sys: &TransitionSystem,

synth/src/repair.rs

@@ -1,14 +1,17 @@
 // Copyright 2023-2024 The Regents of the University of California
+// Copyright 2025 Cornell University
 // released under BSD 3-Clause License
-// author: Kevin Laeufer <laeufer@berkeley.edu>
+// author: Kevin Laeufer <laeufer@cornell.edu>
 
 use crate::testbench::{StepInt, Testbench};
 use crate::Stats;
 use easy_smt as smt;
-use libpatron::ir::*;
-use libpatron::mc::*;
 use num_bigint::BigUint;
 use num_traits::identities::Zero;
+use patronus::expr::{ExprRef, WidthInt};
+use patronus::mc::*;
+use patronus::sim::Simulator;
+use patronus::smt::{Logic, SmtLibSolver, Solver, SolverContext};
 use serde_json::json;
 use std::str::FromStr;
 
@@ -136,31 +139,31 @@ pub fn bit_string_to_smt(smt_ctx: &mut smt::Context, bits: &str) -> smt::SExpr {
     }
 }
 
-pub fn create_smt_ctx(solver: &SmtSolverCmd, dump_file: Option<&str>) -> Result<smt::Context> {
+pub fn create_smt_ctx(
+    solver: &SmtLibSolver,
+    dump_file: Option<&str>,
+) -> Result<impl SolverContext> {
     let replay_file = if let Some(filename) = dump_file {
         Some(std::fs::File::create(filename)?)
     } else {
         None
     };
-    let mut smt_ctx = smt::ContextBuilder::new()
-        .solver(solver.name, solver.args)
-        .replay_file(replay_file)
-        .build()?;
+    let mut smt_ctx = solver.start(replay_file).unwrap();
     set_logic(&mut smt_ctx, solver)?;
     Ok(smt_ctx)
 }
 
 /// sets the correct logic depending on the solver we are using
-fn set_logic(smt_ctx: &mut smt::Context, cmd: &SmtSolverCmd) -> Result<()> {
+fn set_logic(smt_ctx: &mut impl SolverContext, cmd: &SmtLibSolver) -> Result<()> {
     // z3 only supports the non-standard as-const array syntax when the logic is set to ALL
-    let logic = if cmd.name == "z3" {
-        "ALL"
-    } else if cmd.supports_uf {
-        "QF_AUFBV"
+    let logic = if cmd.name() == "z3" {
+        Logic::All
+    } else if cmd.supports_uf() {
+        Logic::QfAufbv
     } else {
-        "QF_ABV"
+        Logic::QfAbv
     };
-    smt_ctx.set_logic(logic)
+    Ok(smt_ctx.set_logic(logic).unwrap())
 }
 
 pub struct RepairVars {

synth/src/studies/unrolling.rs

@@ -1,14 +1,15 @@
 // Copyright 2024 The Regents of the University of California
+// Copyright 2025 Cornell University
 // released under BSD 3-Clause License
-// author: Kevin Laeufer <laeufer@berkeley.edu>
+// author: Kevin Laeufer <laeufer@cornell.edu>
 //
 // we study how the length of unrolling affects the basic synthesis approach
 
 use crate::basic::generate_minimal_repair;
 use crate::repair::{RepairContext, RepairResult, RepairStatus};
 use crate::start_solver;
 use crate::testbench::{RunConfig, StepInt, StopAt};
-use libpatron::mc::{Simulator, SmtSolverCmd, UnrollSmtEncoding};
+use patronus::mc::UnrollSmtEncoding;
 use serde::Serialize;
 use std::time::Instant;
 

synth/src/studies/windowing.rs

@@ -1,6 +1,7 @@
 // Copyright 2024 The Regents of the University of California
+// Copyright 2025 Cornell University
 // released under BSD 3-Clause License
-// author: Kevin Laeufer <laeufer@berkeley.edu>
+// author: Kevin Laeufer <laeufer@cornell.edu>
 //
 // This is not a real synthesizer implementation.
 // Instead we are trying to find out which windows sizes can solve a synthesis problem.
@@ -11,7 +12,7 @@ use crate::repair::{RepairAssignment, RepairContext, RepairResult, RepairStatus,
 use crate::start_solver;
 use crate::testbench::{RunConfig, StepInt, StopAt};
 use easy_smt::Response;
-use libpatron::mc::{Simulator, SmtSolverCmd, TransitionSystemEncoding, UnrollSmtEncoding};
+use patronus::mc::{TransitionSystemEncoding, UnrollSmtEncoding};
 use serde::Serialize;
 use std::collections::HashMap;
 use std::fmt::Debug;

synth/src/testbench.rs

@@ -1,19 +1,15 @@
 // Copyright 2023-2024 The Regents of the University of California
+// Copyright 2025 Cornell University
 // released under BSD 3-Clause License
-// author: Kevin Laeufer <laeufer@berkeley.edu>
+// author: Kevin Laeufer <laeufer@cornell.edu>
 
 use crate::repair::{bit_string_to_smt, classify_state, CHANGE_COUNT_OUTPUT_NAME};
-use libpatron::ir::*;
-use libpatron::mc::{Simulator, TransitionSystemEncoding};
-use libpatron::sim::interpreter::{InitKind, InitValueGenerator};
 use num_bigint::BigUint;
+use patronus::expr::{ExprRef, WidthInt};
+use patronus::mc::TransitionSystemEncoding;
 use std::collections::HashMap;
 
 pub type Result<T> = std::io::Result<T>;
-
-// TODO: make Word in libpatron public
-pub type Word = u64;
-
 pub type StepInt = u64;
 
 pub struct Testbench {