slicing: add minimal unsat subset algorithm, default to unsat core

src/driver.rs

@@ -35,7 +35,7 @@ use crate::{
     slicing::{
         model::SliceModel,
         selection::SliceSelection,
-        solver::SliceSolver,
+        solver::{SliceSolveOptions, SliceSolver},
         transform::{SliceStmts, StmtSliceVisitor},
     },
     smt::{
@@ -651,25 +651,41 @@ impl<'ctx> SmtVcUnit<'ctx> {
         let smtlib = get_smtlib(options, &prover);
 
         let mut slice_solver = SliceSolver::new(slice_vars.clone(), translate, prover);
-        let (result, mut slice_model) = slice_solver.slice_while_failing(limits_ref)?;
+        let failing_slice_options = SliceSolveOptions {
+            globally_optimal: true,
+            continue_on_unknown: false,
+        };
+        let (result, mut slice_model) =
+            slice_solver.slice_while_failing(&failing_slice_options, limits_ref)?;
         if matches!(result, ProveResult::Proof) && options.slice_options.slice_verify {
             match options.slice_options.slice_verify_via {
-                Some(SliceVerifyMethod::ExistsForall) => {
-                    if translate.ctx.uninterpreteds().is_empty() {
-                        slice_model = slice_solver.exists_verified_slice(limits_ref)?;
-                    } else {
-                        tracing::warn!("There are uninterpreted sorts, functions, or axioms present. Slicing for correctness is disabled because it does not support them.");
-                    }
+                SliceVerifyMethod::UnsatCore => {
+                    slice_model = slice_solver.verified_slice_unsat_core(limits_ref)?;
+                }
+                SliceVerifyMethod::MinimalUnsatSubset => {
+                    let slice_options = SliceSolveOptions {
+                        globally_optimal: false,
+                        continue_on_unknown: true,
+                    };
+                    slice_model = slice_solver.verified_slice_mus(&slice_options, limits_ref)?;
                 }
-                Some(SliceVerifyMethod::UnsatCore) => {
-                    slice_model = slice_solver.verified_slice_core(limits_ref)?;
+                SliceVerifyMethod::SmallestUnsatSubset => {
+                    let slice_options = SliceSolveOptions {
+                        globally_optimal: true,
+                        continue_on_unknown: true,
+                    };
+                    slice_model = slice_solver.verified_slice_mus(&slice_options, limits_ref)?;
                 }
-                None => {
+                SliceVerifyMethod::ExistsForall => {
+                    let slice_options = SliceSolveOptions {
+                        globally_optimal: false,
+                        continue_on_unknown: false,
+                    };
                     if translate.ctx.uninterpreteds().is_empty() {
-                        slice_model = slice_solver.exists_verified_slice(limits_ref)?;
+                        slice_model =
+                            slice_solver.exists_verified_slice(&slice_options, limits_ref)?;
                     } else {
-                        tracing::warn!("There are uninterpreted sorts, functions, or axioms present. Slicing for correctness will only use unsat cores and will yield nonoptimal results.");
-                        slice_model = slice_solver.verified_slice_core(limits_ref)?;
+                        tracing::warn!("There are uninterpreted sorts, functions, or axioms present. Slicing for correctness is disabled because it does not support them.");
                     }
                 }
             }

src/main.rs

@@ -209,24 +209,34 @@ pub struct SliceOptions {
 
     /// If slicing for correctness is enabled, slice via these methods. If none
     /// is given, the best method is chosen automatically.
-    #[structopt(long, possible_values = SliceVerifyMethod::variants())]
-    pub slice_verify_via: Option<SliceVerifyMethod>,
+    #[structopt(long, possible_values = SliceVerifyMethod::variants(), default_value = "core")]
+    pub slice_verify_via: SliceVerifyMethod,
 }
 
-#[derive(Debug)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
 pub enum SliceVerifyMethod {
+    /// Slice for correctness using unsat cores. This approach does not minimize
+    /// the result. However, it is applicable all the time and has a very small
+    /// overhead. All other methods are much slower or not always applicable.
+    #[default]
+    UnsatCore,
+    /// Slice by doing a search for minimal unsatisfiable subsets. The result
+    /// might not be globally optimal - the method returns the first slice from
+    /// which nothing can be removed without making the program not verify anymore.
+    MinimalUnsatSubset,
+    /// Slice by doing a search for the smallest unsatisfiable subset. This will
+    /// enumerate all minimal unsat subsets and return the globally smallest one.
+    SmallestUnsatSubset,
     /// Slice for correctness by encoding a direct exists-forall query into the
     /// SMT solver and then run the minimization algorithm. This approach does
-    /// not support uninterpreted functions.
+    /// not support using uninterpreted functions. This approach is usually not
+    /// good.
     ExistsForall,
-    /// Slice for correctness using unsat cores. This approach currently does
-    /// not try to minimize the result.
-    UnsatCore,
 }
 
 impl SliceVerifyMethod {
-    fn variants() -> &'static [&'static str] {
-        &["exists-forall", "unsat-core"]
+    const fn variants() -> &'static [&'static str] {
+        &["core", "mus", "sus", "exists-forall"]
     }
 }
 
@@ -235,8 +245,10 @@ impl FromStr for SliceVerifyMethod {
 
     fn from_str(s: &str) -> Result<Self, Self::Err> {
         match s {
+            "core" => Ok(Self::UnsatCore),
+            "mus" => Ok(Self::MinimalUnsatSubset),
+            "sus" => Ok(Self::SmallestUnsatSubset),
             "exists-forall" => Ok(Self::ExistsForall),
-            "unsat-core" => Ok(Self::UnsatCore),
             _ => Err(InvalidSliceVerifyMethod),
         }
     }