Implement execution of swine-z3 on SMT2 files

src/driver.rs

@@ -53,7 +53,7 @@ use crate::{
         vcgen::Vcgen,
     },
     version::write_detailed_version_info,
-    DebugOptions, SliceOptions, SliceVerifyMethod, VerifyCommand, VerifyError,
+    DebugOptions, SliceOptions, SliceVerifyMethod, VerifyCommand, VerifyError, SMTSolverType,
 };
 
 use ariadne::ReportKind;
@@ -65,7 +65,7 @@ use z3::{
 use z3rro::{
     model::InstrumentedModel,
     probes::ProbeSummary,
-    prover::{IncrementalMode, ProveResult, Prover},
+    prover::{IncrementalMode, ProveResult, Prover, SolverType},
     smtlib::Smtlib,
     util::{PrefixWriter, ReasonUnknown},
 };
@@ -696,7 +696,7 @@ impl<'ctx> SmtVcUnit<'ctx> {
         let span = info_span!("SAT check");
         let _entered = span.enter();
 
-        let prover = mk_valid_query_prover(limits_ref, ctx, translate, &self.vc);
+        let prover = mk_valid_query_prover(limits_ref, ctx, translate, &self.vc, options.smt_solver_options.smt_solver);
 
         if options.debug_options.probe {
             let goal = Goal::new(ctx, false, false, false);
@@ -823,9 +823,15 @@ fn mk_valid_query_prover<'smt, 'ctx>(
     ctx: &'ctx Context,
     smt_translate: &TranslateExprs<'smt, 'ctx>,
     valid_query: &Bool<'ctx>,
+    smt_solver: SMTSolverType,
 ) -> Prover<'ctx> {
+    let solver_type = match smt_solver {
+        SMTSolverType::Swine => SolverType::SWINE,
+        SMTSolverType::Z3 => SolverType::Z3,            
+    };
+
     // create the prover and set the params
-    let mut prover = Prover::new(ctx, IncrementalMode::Native);
+    let mut prover = Prover::new(ctx, IncrementalMode::Native, solver_type);
     if let Some(remaining) = limits_ref.time_left() {
         prover.set_timeout(remaining);
     }

src/main.rs

@@ -39,7 +39,7 @@ use tokio::task::JoinError;
 use tracing::{error, info, warn};
 
 use vc::explain::VcExplanation;
-use z3rro::{prover::ProveResult, util::ReasonUnknown};
+use z3rro::{prover::{ProveResult, ProverCommandError}, util::ReasonUnknown};
 
 pub mod ast;
 mod driver;
@@ -138,6 +138,9 @@ pub struct VerifyCommand {
 
     #[command(flatten)]
     pub debug_options: DebugOptions,
+
+    #[command(flatten)]
+    pub smt_solver_options: SMTSolverOptions,
 }
 
 #[derive(Debug, Args)]
@@ -380,6 +383,22 @@ pub struct DebugOptions {
     pub probe: bool,
 }
 
+#[derive(Debug, Default, Args)]
+#[command(next_help_heading = "SMT Solver Options")]
+pub struct SMTSolverOptions {
+    #[arg(long, default_value = "z3")]
+    pub smt_solver: SMTSolverType,
+}
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, ValueEnum)]
+pub enum SMTSolverType {
+    #[default]
+    #[value(name = "z3")]
+    Z3,
+    #[value(name = "swine")]
+    Swine,
+}
+
 #[derive(Debug, Default, Args)]
 #[command(next_help_heading = "Slicing Options")]
 pub struct SliceOptions {
@@ -533,6 +552,10 @@ fn finalize_verify_result(
             tracing::error!("Interrupted");
             ExitCode::from(130) // 130 seems to be a standard exit code for CTRL+C
         }
+        Err(VerifyError::ProverError(err)) => {
+            eprintln!("{}", err.to_string());
+            ExitCode::from(1)
+        }
     }
 }
 
@@ -612,6 +635,8 @@ pub enum VerifyError {
     /// The verifier was interrupted.
     #[error("interrupted")]
     Interrupted,
+    #[error("{0}")]
+    ProverError(#[from] ProverCommandError),
 }
 
 /// Verify a list of `user_files`. The `options.files` value is ignored here.

src/opt/fuzz_test.rs

@@ -2,7 +2,8 @@ use proptest::{
     prelude::*,
     test_runner::{TestCaseResult, TestRunner},
 };
-use z3rro::prover::{IncrementalMode, ProveResult, Prover};
+
+use z3rro::prover::{IncrementalMode, ProveResult, Prover, SolverType};
 
 use crate::{
     ast::{
@@ -201,22 +202,25 @@ fn prove_equiv(expr: Expr, optimized: Expr, tcx: &TyCtx) -> TestCaseResult {
     let smt_ctx = SmtCtx::new(&ctx, tcx);
     let mut translate = TranslateExprs::new(&smt_ctx);
     let eq_expr_z3 = translate.t_bool(&eq_expr);
-    let mut prover = Prover::new(&ctx, IncrementalMode::Native);
+    let mut prover = Prover::new(&ctx, IncrementalMode::Native, SolverType::Z3);
     translate
         .local_scope()
         .add_assumptions_to_prover(&mut prover);
     prover.add_provable(&eq_expr_z3);
     let x = match prover.check_proof() {
-        ProveResult::Proof => Ok(()),
-        ProveResult::Counterexample => {
+        Ok(ProveResult::Proof) => Ok(()),
+        Ok(ProveResult::Counterexample) => {
             let model = prover.get_model().unwrap();
             Err(TestCaseError::fail(format!(
                 "rewrote {} ...into... {}, but those are not equivalent:\n{}",
                 expr, optimized, model
             )))
         }
-        ProveResult::Unknown(reason) => {
+        Ok(ProveResult::Unknown(reason)) => {
             Err(TestCaseError::fail(format!("unknown result ({})", reason)))
+        },
+        Err(err) => {
+            Err(TestCaseError::fail(format!("{}", err)))
         }
     };
     x

src/opt/unfolder.rs

@@ -25,7 +25,7 @@
 use std::ops::DerefMut;
 
 use z3::SatResult;
-use z3rro::prover::{IncrementalMode, Prover};
+use z3rro::prover::{IncrementalMode, Prover, SolverType};
 
 use crate::{
     ast::{
@@ -60,7 +60,7 @@ impl<'smt, 'ctx> Unfolder<'smt, 'ctx> {
         // it's important that we use the native incremental mode here, because
         // the performance benefit from the unfolder relies on many very fast
         // SAT checks.
-        let prover = Prover::new(ctx.ctx(), IncrementalMode::Native);
+        let prover = Prover::new(ctx.ctx(), IncrementalMode::Native, SolverType::Z3);
 
         Unfolder {
             subst: Subst::new(ctx.tcx(), &limits_ref),