diff --git a/src/slicing/selection.rs b/src/slicing/selection.rs index 57a0853..ee18e56 100644 --- a/src/slicing/selection.rs +++ b/src/slicing/selection.rs @@ -144,8 +144,8 @@ impl SliceAnnotation { /// by a logical or. #[derive(Debug, Clone, Default)] pub struct SliceSelection { - concordant: bool, - discordant: bool, + pub(super) concordant: bool, + pub(super) discordant: bool, pub in_slice_verify_annotation: bool, pub in_slice_error_annotation: bool, pub slice_ticks: bool, diff --git a/src/slicing/solver.rs b/src/slicing/solver.rs index 3998b3d..6210d37 100644 --- a/src/slicing/solver.rs +++ b/src/slicing/solver.rs @@ -1,5 +1,6 @@ use std::{collections::HashSet, time::Duration}; +use itertools::Itertools; use tracing::{debug, info, info_span, instrument, warn}; use z3::{ ast::{Bool, Dynamic}, @@ -268,8 +269,36 @@ impl<'ctx> SliceSolver<'ctx> { // TODO: re-use the unsat core from the proof instead of starting fresh let mut slice_searcher = SliceModelSearch::new(active_toggle_values.clone()); - let mut subset_explorer = - SubsetExploration::new(self.prover.solver().get_context(), active_toggle_values); + + let context = self.prover.solver().get_context(); + let mut subset_explorer = { + let active_toggle_values = active_toggle_values.iter().cloned().collect(); + let extensive: HashSet> = self + .slice_stmts + .stmts + .iter() + .flat_map(|(slice_stmt, var)| { + if slice_stmt.selection.concordant { + Some(var.clone()) + } else { + None + } + }) + .collect(); + let reductive: HashSet> = self + .slice_stmts + .stmts + .iter() + .flat_map(|(slice_stmt, var)| { + if slice_stmt.selection.discordant { + Some(var.clone()) + } else { + None + } + }) + .collect(); + SubsetExploration::new(context, active_toggle_values, extensive, reductive) + }; while let Some(extremal_set) = slice_next_extremal_set(&mut subset_explorer, &mut self.prover, options, limits_ref)? { @@ -536,8 +565,13 @@ fn slice_sat_binary_search<'ctx>( Ok(()) } +#[derive(Debug)] enum ExtremalSet<'ctx> { + /// This is a minimal unsat set in the following sense: we cannot remove any + /// more extensive statements without making the program fail to verify. MinimalUnsat(HashSet>), + /// This is a maximal sat set in the following sense: we cannot add any more + /// extensive statements without making the program verify. #[allow(unused)] MaximalSat(HashSet>), } @@ -555,13 +589,11 @@ pub fn slice_next_extremal_set<'ctx>( while let Some(seed) = exploration.next_set() { limits_ref.check_limits()?; - match check_proof_seed(prover, limits_ref, &seed) { + match check_proof_seed(&all_variables, prover, limits_ref, &seed) { ProveResult::Proof => { - let seed = unsat_core_to_seed(prover, &all_variables); - // now start the shrinking, then block up - let res = exploration.shrink_block_up(seed, |seed| { - match check_proof_seed(prover, limits_ref, seed) { + 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, } @@ -570,8 +602,8 @@ pub fn slice_next_extremal_set<'ctx>( } ProveResult::Counterexample(_) => { // grow the counterexample and then block down - let res = exploration.grow_block_down(seed, |seed| { - match check_proof_seed(prover, limits_ref, seed) { + let res = exploration.grow_block_sat(seed, |seed| { + match check_proof_seed(&all_variables, prover, limits_ref, seed) { ProveResult::Counterexample(_) => true, ProveResult::Proof | ProveResult::Unknown(_) => false, } @@ -594,6 +626,7 @@ pub fn slice_next_extremal_set<'ctx>( #[instrument(level = "trace", skip_all, ret)] fn check_proof_seed<'ctx>( + all_variables: &HashSet>, prover: &mut Prover<'ctx>, limits_ref: &LimitsRef, seed: &HashSet>, @@ -604,14 +637,21 @@ fn check_proof_seed<'ctx>( } prover.set_timeout(timeout); - let seed: Vec<_> = seed.iter().cloned().collect(); - prover.check_proof_assuming(&seed) + let (all_on, all_off): (HashSet<_>, HashSet<_>) = all_variables + .iter() + .cloned() + .partition(|var| seed.contains(var)); + let all_on_assumptions = all_on.iter().cloned(); + let all_off_assumptions = all_off.iter().map(Bool::not); + let all_assumptions = all_on_assumptions.chain(all_off_assumptions).collect_vec(); + + prover.check_proof_assuming(&all_assumptions) } fn unsat_core_to_seed<'ctx>( prover: &mut Prover<'ctx>, all_variables: &HashSet>, ) -> HashSet> { - let unsat_core = &prover.get_unsat_core().into_iter().collect(); - all_variables.intersection(unsat_core).cloned().collect() + let unsat_core: HashSet> = prover.get_unsat_core().into_iter().collect(); + all_variables.intersection(&unsat_core).cloned().collect() } diff --git a/src/slicing/util.rs b/src/slicing/util.rs index 68173c5..92ce66a 100644 --- a/src/slicing/util.rs +++ b/src/slicing/util.rs @@ -4,6 +4,7 @@ use std::{ ops::{RangeFrom, RangeInclusive, RangeToInclusive}, }; +use itertools::Itertools; use tracing::instrument; use z3::{ast::Bool, Context, SatResult, Solver}; @@ -149,13 +150,22 @@ fn iter_range_from_mid(range: RangeInclusive) -> Box { solver: Solver<'ctx>, variables: HashSet>, + extensive: HashSet>, + reductive: HashSet>, } impl<'ctx> SubsetExploration<'ctx> { - pub fn new(ctx: &'ctx Context, variables: impl IntoIterator>) -> Self { + pub fn new( + ctx: &'ctx Context, + variables: HashSet>, + extensive: HashSet>, + reductive: HashSet>, + ) -> Self { SubsetExploration { solver: Solver::new(ctx), - variables: HashSet::from_iter(variables), + variables, + extensive, + reductive, } } @@ -186,82 +196,189 @@ impl<'ctx> SubsetExploration<'ctx> { } } - /// Block this set, we do not want to see it again. + /// Block a set of models where all variables `all_off` are set to `false` + /// and all variables `all_on` are set to `true`. + fn block(&mut self, all_on: &HashSet>, all_off: &HashSet>) { + let ctx = self.solver.get_context(); + let all_on_constraint = Bool::and(ctx, &all_on.iter().collect_vec()); + let all_off_constraint = Bool::and(ctx, &all_off.iter().map(Bool::not).collect_vec()); + let both_constraints = Bool::and(ctx, &[all_on_constraint, all_off_constraint]); + self.solver.assert(&both_constraints.not()); + } + + /// Block an exact variable assignment, we do not want to see it again, where + /// all variables in `set` are set to `true` and all other variables are set + /// to `false`. pub fn block_this(&mut self, set: &HashSet>) { - let assignments: Vec<_> = self + let (all_on, all_off): (HashSet<_>, HashSet<_>) = self .variables .iter() - .map(|var| { - if set.contains(var) { - var.clone() - } else { - var.not() - } - }) - .collect(); - let constraint = Bool::and(self.solver.get_context(), &assignments); - self.solver.assert(&constraint.not()); + .cloned() + .partition(|var| set.contains(var)); + self.block(&all_on, &all_off); } - /// "Block down" - all values at this point or lower are considered not unsat. - fn block_down(&mut self, from_point: &HashSet>) { - // we add a constraint that says the next set must have any variable set - // to true not in the given `from_point`. - let complement: Vec<_> = self.variables.difference(from_point).collect(); - let constraint = Bool::or(self.solver.get_context(), &complement); - self.solver.assert(&constraint); + /// Block a set of models knowing that the following model is unsat: + /// `all_true` variables are set to true and all others are set to false. + /// + /// Then, we block all models of those where the enabled extensive + /// variables are a *superset* of those currently enabled and where the + /// enabled reductive variables are a *subset* of those currently enabled. + /// + /// Phrased differently: a new model must have a currently disabled + /// `reductive` variable set to true *or* a currently enabled `extensive` + /// variable set to false. + fn block_unsat(&mut self, all_true: &HashSet>) { + let all_false: HashSet> = self + .variables + .clone() + .difference(all_true) + .cloned() + .collect(); + + // turning off a reductive variable (assertion) will still result in UNSAT. + let all_on: HashSet> = all_true.difference(&self.reductive).cloned().collect(); + + // turning on an extensive variable (assumption) will still result in UNSAT. + let all_off: HashSet> = all_false.difference(&self.extensive).cloned().collect(); + + self.block(&all_on, &all_off); } - /// "Block up" - the next sets must not contain at least one of the given values. - fn block_up(&mut self, from_point: &HashSet>) { - // we add a constraint that says the next set must have any variable set - // to true not in the given `from_point`. - let negated: Vec<_> = from_point.iter().map(|var| var.not()).collect(); - let constraint = Bool::or(self.solver.get_context(), &negated); - self.solver.assert(&constraint); + /// Block a set of models knowing that the following model is sat: + /// `all_true` variables are set to true and all others are set to false. + /// + /// Then, we block all models of those where the enabled extensive + /// variables are a *subset* of those currently enabled and where the + /// enabled reductive variables are a *superset* of those currently enabled. + /// + /// Phrased differently: a new model must have a currently disabled + /// `extensive` variable set to true *or* a currently enabled `reductive` + /// variable set to false. + fn block_sat(&mut self, all_true: &HashSet>) { + let all_false: HashSet> = self + .variables + .clone() + .difference(all_true) + .cloned() + .collect(); + + // turning off an extensive variable (assumption) will still result in SAT. + let all_on: HashSet> = all_true.difference(&self.extensive).cloned().collect(); + + // turning on a reductive variable (assertion) will still result in SAT. + let all_off: HashSet> = all_false.difference(&self.reductive).cloned().collect(); + + self.block(&all_on, &all_off); } - /// Shrink this set with the given shrinking function. If the shrinking - /// function returns `Some`, we will shrink to this set. Then, we'll block - /// upwards. - #[instrument(level = "trace", skip_all, fields(seed.len = seed.len(), ret.len))] - pub fn shrink_block_up( + /// *Shrink and block* a set of models knowing that the following model is + /// unsat: `all_true` variables are set to true and all others are set to + /// false. + /// + /// For *blocking*, we use [`Self::block_unsat()`]. *Shrinking* tries to + /// remove extensive variables from the set of enabled ones. It uses the + /// `get_shrunk_core` function to check whether the shrunk set is still + /// unsatisfiable. If so, the `get_shrunk_core` function returns the + /// unsatisfiable core. If not, it returns `None`. + /// + /// We use a heuristic for shrinking: simply try to remove one extensive + /// variable after another so that the runtime is linear. We do *not* try + /// all combinations of removals. + /// + /// We could also try to *add* reductive variables here, but we do not to + /// keep it simple. + #[instrument(level = "trace", skip_all, fields(all_true.len = all_true.len(), ret.len))] + pub fn shrink_block_unsat( &mut self, - seed: HashSet>, + all_true: HashSet>, mut get_shrunk_core: impl FnMut(&HashSet>) -> Option>>, ) -> HashSet> { - let mut current = seed.clone(); - for var in seed { - if !current.remove(&var) { + let mut current = all_true.clone(); + + if let Some(shrunk_set) = get_shrunk_core(¤t) { + debug_assert!(shrunk_set.is_subset(¤t)); + + // check if we removed an extensive statement, then we don't use + // the unsat core. + if current + .difference(&shrunk_set) + .cloned() + .collect::>() + .difference(&self.extensive) + .next() + .is_some() + { + // the result was unsat (good), but we cannot use the unsat + // core because we removed stuff that's not extensive. + } else { + current = shrunk_set; + } + } + + for var in all_true.intersection(&self.extensive) { + if !current.remove(var) { continue; } if let Some(shrunk_set) = get_shrunk_core(¤t) { debug_assert!(shrunk_set.is_subset(¤t)); - current = shrunk_set; + + // check if we removed an extensive statement, then we don't use + // the unsat core. + if current + .difference(&shrunk_set) + .cloned() + .collect::>() + .difference(&self.extensive) + .next() + .is_some() + { + // the result was unsat (good), but we cannot use the unsat + // core because we removed stuff that's not extensive. + } else { + current = shrunk_set; + } } else { - current.insert(var); + // undo removal + current.insert(var.clone()); } } - self.block_up(¤t); + self.block_unsat(¤t); tracing::Span::current().record("ret.len", current.len()); current } - /// Grow this set with the given function that checks the set. Then, we - /// block downwards from this grown set. - #[instrument(level = "trace", skip_all, fields(seed.len = seed.len(), ret.len))] - pub fn grow_block_down( + /// *Grow and block* a set of models knowing that the following model is + /// sat: `all_true` variables are set to true and all others are set to + /// false. + /// + /// For *blocking*, we use [`Self::block_sat()`]. *Growing* tries to add + /// extensive variables from the set of enabled ones. It uses the + /// `check_grow` function to check whether the grown set is still + /// satisfiable. If so, the `check_grow` function returns `true` and + /// `false` otherwise. + /// + /// We use a heuristic for growing: simply try to add one extensive variable + /// after another so that the runtime is linear. We do *not* try all + /// combinations of additions. + /// + /// We could also try to *remove* reductive variables here, but we do not to + /// keep it simple. + #[instrument(level = "trace", skip_all, fields(all_true.len = all_true.len(), ret.len))] + pub fn grow_block_sat( &mut self, - seed: HashSet>, + all_true: HashSet>, mut check_grow: impl FnMut(&HashSet>) -> bool, ) -> HashSet> { - let mut current = seed.clone(); - for var in self.variables.difference(&seed) { - if check_grow(¤t) { - current.insert(var.clone()); + let mut current = all_true.clone(); + for var in self.extensive.difference(&all_true) { + current.insert(var.clone()); + if !check_grow(¤t) { + // undo addition on unsat + current.remove(var); } } - self.block_down(¤t); + self.block_sat(¤t); tracing::Span::current().record("ret.len", current.len()); current }