Add SolverType attribute to Prover struct and SMT solver options

Author: SeRin-Yang

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;
@@ -64,7 +64,7 @@ use z3::{
 };
 use z3rro::{
     probes::ProbeSummary,
-    prover::{ProveResult, Prover},
+    prover::{ProveResult, Prover, SolverType},
     smtlib::Smtlib,
     util::{PrefixWriter, ReasonUnknown},
 };
@@ -695,7 +695,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);
@@ -797,9 +797,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);
+    let mut prover = Prover::new(ctx, solver_type);
     if let Some(remaining) = limits_ref.time_left() {
         prover.set_timeout(remaining);
     }

src/main.rs

@@ -138,6 +138,9 @@ pub struct VerifyCommand {
 
     #[command(flatten)]
     pub debug_options: DebugOptions,
+
+    #[command(flatten)]
+    pub smt_solver_options: SMTSolverOptions,
 }
 
 #[derive(Debug, Args)]
@@ -376,6 +379,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 {

src/opt/fuzz_test.rs

@@ -2,7 +2,7 @@ use proptest::{
     prelude::*,
     test_runner::{TestCaseResult, TestRunner},
 };
-use z3rro::prover::{ProveResult, Prover};
+use z3rro::prover::{ProveResult, Prover, SolverType};
 
 use crate::{
     ast::{
@@ -201,7 +201,7 @@ 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);
+    let mut prover = Prover::new(&ctx, SolverType::Z3);
     translate
         .local_scope()
         .add_assumptions_to_prover(&mut prover);

src/opt/unfolder.rs

@@ -25,7 +25,7 @@
 use std::ops::DerefMut;
 
 use z3::SatResult;
-use z3rro::prover::Prover;
+use z3rro::prover::{Prover, SolverType};
 
 use crate::{
     ast::{
@@ -63,7 +63,7 @@ impl<'smt, 'ctx> Unfolder<'smt, 'ctx> {
             limits_ref: limits_ref.clone(),
             subst: Subst::new(ctx.tcx(), &limits_ref),
             translate: TranslateExprs::new(ctx),
-            prover: Prover::new(ctx.ctx()),
+            prover: Prover::new(ctx.ctx(), SolverType::Z3),
         }
     }
 

src/slicing/solver.rs

@@ -229,7 +229,7 @@ impl<'ctx> SliceSolver<'ctx> {
         self.prover.add_assumption(&inactive_formula);
         let res = self
             .prover
-            .check_proof_assuming(&active_toggle_values, z3rro::prover::SolverType::SWINE);
+            .check_proof_assuming(&active_toggle_values);
 
         let mut slice_searcher = SliceModelSearch::new(active_toggle_values.clone());
         if let ProveResult::Proof = res {
@@ -607,7 +607,7 @@ fn check_proof_seed<'ctx>(
     prover.set_timeout(timeout);
 
     let seed: Vec<_> = seed.iter().cloned().collect();
-    prover.check_proof_assuming(&seed, z3rro::prover::SolverType::SWINE)
+    prover.check_proof_assuming(&seed)
 }
 
 fn unsat_core_to_seed<'ctx>(

src/slicing/transform_test.rs

@@ -5,7 +5,7 @@ use std::time::{Duration, Instant};
 use itertools::Itertools;
 use z3rro::{
     model::SmtEval,
-    prover::{ProveResult, Prover},
+    prover::{ProveResult, Prover, SolverType},
 };
 
 use crate::{
@@ -128,7 +128,7 @@ fn prove_equiv(
     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);
+    let mut prover = Prover::new(&ctx, SolverType::Z3);
     translate
         .local_scope()
         .add_assumptions_to_prover(&mut prover);

z3rro/src/prover.rs

@@ -32,6 +32,7 @@ pub enum CommandError {
     ProcessError(#[from] io::Error),
 }
 
+#[derive(Debug)]
 pub enum SolverType {
     Z3,
     SWINE,
@@ -127,15 +128,17 @@ pub struct Prover<'ctx> {
     level: usize,
     /// The minimum level where an assertion was added to the solver.
     min_level_with_provables: Option<usize>,
+    smt_solver: SolverType
 }
 
 impl<'ctx> Prover<'ctx> {
     /// Create a new prover with the given [`Context`].
-    pub fn new(ctx: &'ctx Context) -> Self {
+    pub fn new(ctx: &'ctx Context, solver_type:SolverType) -> Self {
         Prover {
             solver: Solver::new(ctx),
             level: 0,
             min_level_with_provables: None,
+            smt_solver: solver_type,
         }
     }
 
@@ -159,23 +162,22 @@ impl<'ctx> Prover<'ctx> {
     }
 
     pub fn check_proof(&mut self) -> ProveResult<'ctx> {
-        self.check_proof_assuming(&[], SolverType::SWINE)
+        self.check_proof_assuming(&[])
     }
 
     /// Do the SAT check, but consider a check with no provables to be a
     /// [`ProveResult::Proof`].
     pub fn check_proof_assuming(
         &mut self,
         assumptions: &[Bool<'ctx>],
-        solver_type: SolverType,
     ) -> ProveResult<'ctx> {
         if self.min_level_with_provables.is_none() {
             return ProveResult::Proof;
         }
 
         let res;
 
-        match solver_type {
+        match self.smt_solver {
             SolverType::SWINE => {
                 let mut smtlib = self.get_smtlib();
                 smtlib.add_check_sat();
@@ -198,7 +200,6 @@ impl<'ctx> Prover<'ctx> {
                     }
                     SatResult::Sat => {
                         // TODO: Get the model from the output of SWINE
-                        println!("The Result of SWINE: sat");
                         process::exit(1)
                     }
                 }
@@ -291,7 +292,7 @@ impl<'ctx> Prover<'ctx> {
             universal.iter().map(|v| v as &dyn Ast<'ctx>).collect();
         let assertions = self.solver.get_assertions();
         let theorem = forall_const(ctx, &universal, &[], &Bool::and(ctx, &assertions).not());
-        let mut res = Prover::new(ctx);
+        let mut res = Prover::new(ctx, SolverType::Z3);
         res.add_assumption(&theorem);
         res
     }
@@ -306,12 +307,14 @@ impl<'ctx> Prover<'ctx> {
 mod test {
     use z3::{ast::Bool, Config, Context, SatResult};
 
+    use crate::prover::SolverType;
+
     use super::{ProveResult, Prover};
 
     #[test]
     fn test_prover() {
         let ctx = Context::new(&Config::default());
-        let mut prover = Prover::new(&ctx);
+        let mut prover = Prover::new(&ctx, SolverType::Z3);
         assert!(matches!(prover.check_proof(), ProveResult::Proof));
         assert_eq!(prover.check_sat(), SatResult::Sat);
 

z3rro/src/test.rs

@@ -4,7 +4,7 @@
 
 use z3::{ast::Bool, Config, Context, SatResult};
 
-use crate::prover::{ProveResult, Prover};
+use crate::prover::{ProveResult, Prover, SolverType};
 
 use super::scope::SmtScope;
 
@@ -18,7 +18,7 @@ pub fn test_prove(f: impl for<'ctx> FnOnce(&'ctx Context, &mut SmtScope<'ctx>) -
     let mut scope = SmtScope::new();
     let theorem = f(&ctx, &mut scope);
 
-    let mut prover = Prover::new(&ctx);
+    let mut prover = Prover::new(&ctx, SolverType::Z3);
     scope.add_assumptions_to_prover(&mut prover);
     assert_eq!(
         prover.check_sat(),