From 4084a70485eeb0f78b7a13187053997d66a19405 Mon Sep 17 00:00:00 2001
From: Jacob Lifshay <programmerjake@gmail.com>
Date: Thu, 3 Oct 2024 01:43:46 -0700
Subject: [PATCH] switch default solver to z3

---
 crates/fayalite/src/cli.rs     | 18 +++---------------
 crates/fayalite/src/testing.rs |  4 +++-
 2 files changed, 6 insertions(+), 16 deletions(-)

diff --git a/crates/fayalite/src/cli.rs b/crates/fayalite/src/cli.rs
index cbef722..b0b818c 100644
--- a/crates/fayalite/src/cli.rs
+++ b/crates/fayalite/src/cli.rs
@@ -419,8 +419,8 @@ pub struct FormalArgs {
     pub mode: FormalMode,
     #[arg(long, default_value_t = Self::DEFAULT_DEPTH)]
     pub depth: u64,
-    #[arg(long)]
-    pub solver: Option<String>,
+    #[arg(long, default_value = "z3")]
+    pub solver: String,
     #[arg(long)]
     pub smtbmc_extra_args: Vec<String>,
     #[command(flatten)]
@@ -479,18 +479,6 @@ impl FormalArgs {
             solver,
             _formal_adjust_args: _,
         } = self;
-        struct OptArg<T>(Option<T>);
-        impl<T: fmt::Display> fmt::Display for OptArg<T> {
-            fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-                if let Some(v) = &self.0 {
-                    f.write_str(" ")?;
-                    v.fmt(f)
-                } else {
-                    Ok(())
-                }
-            }
-        }
-        let space_solver = OptArg(solver.as_ref());
         let smtbmc_options = smtbmc_extra_args.join(" ");
         let top_module = &output.verilog.firrtl.top_module;
         let mut retval = format!(
@@ -500,7 +488,7 @@ impl FormalArgs {
             wait on\n\
             \n\
             [engines]\n\
-            smtbmc{space_solver} -- -- {smtbmc_options}\n\
+            smtbmc {solver} -- -- {smtbmc_options}\n\
             \n\
             [script]\n"
         );
diff --git a/crates/fayalite/src/testing.rs b/crates/fayalite/src/testing.rs
index a647f47..07252f1 100644
--- a/crates/fayalite/src/testing.rs
+++ b/crates/fayalite/src/testing.rs
@@ -115,6 +115,8 @@ pub fn assert_formal<M>(
     args.verilog.debug = true;
     args.mode = mode;
     args.depth = depth;
-    args.solver = solver.map(String::from);
+    if let Some(solver) = solver {
+        args.solver = solver.into();
+    }
     args.run(module).expect("testing::assert_formal() failed");
 }