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, SMTSolverType, SliceOptions, SliceVerifyMethod, VerifyCommand, VerifyError,
 };
 
 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,13 @@ 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.clone(),
+        );
 
         if options.debug_options.probe {
             let goal = Goal::new(ctx, false, false, false);
@@ -823,9 +829,18 @@ 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::InternalZ3 => SolverType::InternalZ3,
+        SMTSolverType::ExternalZ3 => SolverType::ExternalZ3,
+        SMTSolverType::Swine => SolverType::SWINE,
+        SMTSolverType::CVC5 => SolverType::CVC5,
+        SMTSolverType::Yices => SolverType::YICES,
+    };
+
     // 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,10 @@ 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 +141,9 @@ pub struct VerifyCommand {
 
     #[command(flatten)]
     pub debug_options: DebugOptions,
+
+    #[command(flatten)]
+    pub smt_solver_options: SMTSolverOptions,
 }
 
 #[derive(Debug, Args)]
@@ -380,6 +386,28 @@ pub struct DebugOptions {
     pub probe: bool,
 }
 
+#[derive(Debug, Default, Args)]
+#[command(next_help_heading = "SMT Solver Options")]
+pub struct SMTSolverOptions {
+    #[arg(long, default_value = "default")]
+    pub smt_solver: SMTSolverType,
+}
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, ValueEnum)]
+pub enum SMTSolverType {
+    #[default]
+    #[value(name = "default")]
+    InternalZ3,
+    #[value(name = "z3")]
+    ExternalZ3,
+    #[value(name = "swine")]
+    Swine,
+    #[value(name = "cvc5")]
+    CVC5,
+    #[value(name = "yices")]
+    Yices,
+}
+
 #[derive(Debug, Default, Args)]
 #[command(next_help_heading = "Slicing Options")]
 pub struct SliceOptions {
@@ -533,6 +561,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 +644,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,23 +202,24 @@ 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::InternalZ3);
     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::InternalZ3);
 
         Unfolder {
             subst: Subst::new(ctx.tcx(), &limits_ref),
@@ -98,7 +98,7 @@ impl<'smt, 'ctx> Unfolder<'smt, 'ctx> {
             // here we want to do a SAT check and not a proof search. if the
             // expression is e.g. `false`, then we want to get `Unsat` from the
             // solver and not `Proof`!
-            if this.prover.check_sat() == SatResult::Unsat {
+            if this.prover.check_sat() == Ok(SatResult::Unsat) {
                 tracing::trace!(solver=?this.prover, "eliminated zero expr");
                 None
             } else {

src/slicing/solver.rs

@@ -9,16 +9,16 @@ use z3::{
 };
 use z3rro::{
     model::{InstrumentedModel, ModelConsistency},
-    prover::{ProveResult, Prover},
+    prover::{ProveResult, Prover, ProverCommandError, SolverType},
     util::ReasonUnknown,
 };
 
 use crate::{
     ast::{ExprBuilder, Span},
-    resource_limits::{LimitError, LimitsRef},
+    resource_limits::LimitsRef,
     slicing::{
         model::{SliceMode, SliceModel},
-        util::{PartialMinimizeResult, SubsetExploration},
+        util::{at_most_k, PartialMinimizeResult, SubsetExploration},
     },
     smt::translate_exprs::TranslateExprs,
     VerifyError,
@@ -218,7 +218,10 @@ impl<'ctx> SliceSolver<'ctx> {
             options,
             limits_ref,
         )?;
-        if exists_forall_solver.check_sat() == SatResult::Sat {
+        let sat_res = exists_forall_solver
+            .check_sat()
+            .map_err(|err| VerifyError::ProverError(err))?;
+        if sat_res == SatResult::Sat {
             let model = exists_forall_solver.get_model().unwrap();
             let slice_model =
                 SliceModel::from_model(SliceMode::Verify, &self.slice_stmts, selection, &model);
@@ -251,7 +254,7 @@ impl<'ctx> SliceSolver<'ctx> {
         let res = self.prover.check_proof_assuming(&active_toggle_values);
 
         let mut slice_searcher = SliceModelSearch::new(active_toggle_values.clone());
-        if let ProveResult::Proof = res {
+        if let Ok(ProveResult::Proof) = res {
             slice_searcher.found_active(self.prover.get_unsat_core());
         }
 
@@ -351,7 +354,10 @@ impl<'ctx> SliceSolver<'ctx> {
         self.prover.push();
 
         slice_sat_binary_search(&mut self.prover, &active_toggle_values, options, limits_ref)?;
-        let res = self.prover.check_proof();
+        let res = self
+            .prover
+            .check_proof()
+            .map_err(|err| VerifyError::ProverError(err))?;
         let model = if let Some(model) = self.prover.get_model() {
             assert!(matches!(
                 res,
@@ -469,8 +475,13 @@ fn slice_sat_binary_search<'ctx>(
         prover.push();
 
         let ctx = prover.get_context();
-        let at_most_n_true = Bool::pb_le(ctx, &slice_vars, at_most_n as i32);
-        prover.add_assumption(&at_most_n_true);
+        if !slice_vars.is_empty() {
+            let at_most_n_true = match prover.get_smt_solver() {
+                SolverType::CVC5 | SolverType::YICES => at_most_k(ctx, at_most_n as i64, active_slice_vars),
+                _ => Bool::pb_le(ctx, &slice_vars, at_most_n as i32),
+            };
+            prover.add_assumption(&at_most_n_true);
+        }
     };
 
     // TODO: we could have min_least_bound set to 1 if we could conclude for
@@ -506,7 +517,10 @@ fn slice_sat_binary_search<'ctx>(
         if let Some(timeout) = limits_ref.time_left() {
             prover.set_timeout(timeout);
         }
-        let res = prover.check_sat();
+
+        let res = prover
+            .check_sat()
+            .map_err(|err| VerifyError::ProverError(err))?;
 
         entered.record("res", tracing::field::debug(res));
 
@@ -571,7 +585,9 @@ fn slice_sat_binary_search<'ctx>(
             if let Some(timeout) = limits_ref.time_left() {
                 prover.set_timeout(timeout);
             }
-            let res = prover.check_sat();
+            let res = prover
+                .check_sat()
+                .map_err(|err| VerifyError::ProverError(err))?;
             if minimize.min_accept().is_some() {
                 assert!(res == SatResult::Sat || res == SatResult::Unknown);
             } else if minimize.max_reject().is_some() {
@@ -593,7 +609,7 @@ pub fn slice_unsat_search<'ctx>(
     prover: &mut Prover<'ctx>,
     options: &SliceSolveOptions,
     limits_ref: &LimitsRef,
-) -> Result<Option<Vec<Bool<'ctx>>>, LimitError> {
+) -> Result<Option<Vec<Bool<'ctx>>>, VerifyError> {
     let mut slice_searcher =
         SliceModelSearch::new(exploration.variables().iter().cloned().collect_vec());
     let all_variables = exploration.variables().clone();
@@ -602,14 +618,15 @@ pub fn slice_unsat_search<'ctx>(
         limits_ref.check_limits()?;
 
         match check_proof_seed(&all_variables, prover, limits_ref, &seed) {
-            ProveResult::Proof => {
+            Ok(ProveResult::Proof) => {
                 // now start the shrinking, then block up
-                let res = exploration.shrink_block_unsat(seed, |seed| {
-                    match check_proof_seed(&all_variables, prover, limits_ref, seed) {
-                        ProveResult::Proof => Some(unsat_core_to_seed(prover, &all_variables)),
-                        ProveResult::Counterexample | ProveResult::Unknown(_) => None,
-                    }
-                });
+                let res_seed = match check_proof_seed(&all_variables, prover, limits_ref, &seed) {
+                    Ok(ProveResult::Proof) => Some(unsat_core_to_seed(prover, &all_variables)),
+                    Ok(ProveResult::Counterexample) | Ok(ProveResult::Unknown(_)) => None,
+                    Err(err) => return Err(VerifyError::ProverError(err)),
+                };
+
+                let res = exploration.shrink_block_unsat(seed, |_| res_seed.clone());
 
                 let res_vec: Vec<_> = res.iter().cloned().collect();
                 slice_searcher.found_active(res_vec);
@@ -620,16 +637,17 @@ pub fn slice_unsat_search<'ctx>(
                     SliceMinimality::Size => exploration.block_at_least(res.len()),
                 }
             }
-            ProveResult::Counterexample => {
+            Ok(ProveResult::Counterexample) => {
                 // grow the counterexample and then block down
-                exploration.grow_block_sat(seed, |seed| {
-                    match check_proof_seed(&all_variables, prover, limits_ref, seed) {
-                        ProveResult::Counterexample => true,
-                        ProveResult::Proof | ProveResult::Unknown(_) => false,
-                    }
-                });
+                let res_seed = match check_proof_seed(&all_variables, prover, limits_ref, &seed) {
+                    Ok(ProveResult::Counterexample) => true,
+                    Ok(ProveResult::Proof) | Ok(ProveResult::Unknown(_)) => false,
+                    Err(err) => return Err(VerifyError::ProverError(err)),
+                };
+
+                exploration.grow_block_sat(seed, |_| res_seed);
             }
-            ProveResult::Unknown(_) => {
+            Ok(ProveResult::Unknown(_)) => {
                 exploration.block_this(&seed);
 
                 match options.unknown {
@@ -643,6 +661,7 @@ pub fn slice_unsat_search<'ctx>(
                     }
                 }
             }
+            Err(err) => return Err(VerifyError::ProverError(err)),
         }
     }
 
@@ -655,7 +674,7 @@ fn check_proof_seed<'ctx>(
     prover: &mut Prover<'ctx>,
     limits_ref: &LimitsRef,
     seed: &IndexSet<Bool<'ctx>>,
-) -> ProveResult {
+) -> Result<ProveResult, ProverCommandError> {
     let mut timeout = Duration::from_millis(100);
     if let Some(time_left) = limits_ref.time_left() {
         timeout = timeout.min(time_left);