From b3b1b055a05d2e9a4ea86e82c8fdaa8b3fb5bc0b Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Wed, 12 Feb 2025 17:08:05 +0100 Subject: [PATCH] fix: allow reification of lazy reasons --- .../conflict_analysis_context.rs | 73 +++++---- .../minimisers/recursive_minimiser.rs | 9 +- .../resolvers/resolution_resolver.rs | 39 +++-- .../engine/constraint_satisfaction_solver.rs | 33 ++-- .../contexts/propagation_context.rs | 5 +- pumpkin-solver/src/engine/cp/reason.rs | 141 ++++++++++++++---- pumpkin-solver/src/engine/cp/test_solver.rs | 15 +- pumpkin-solver/src/engine/debug_helper.rs | 19 ++- .../time_table/propagation_handler.rs | 17 +-- 9 files changed, 226 insertions(+), 125 deletions(-) diff --git a/pumpkin-solver/src/engine/conflict_analysis/conflict_analysis_context.rs b/pumpkin-solver/src/engine/conflict_analysis/conflict_analysis_context.rs index 66f7a074..956af136 100644 --- a/pumpkin-solver/src/engine/conflict_analysis/conflict_analysis_context.rs +++ b/pumpkin-solver/src/engine/conflict_analysis/conflict_analysis_context.rs @@ -58,7 +58,7 @@ impl Debug for ConflictAnalysisContext<'_> { } } -impl<'a> ConflictAnalysisContext<'a> { +impl ConflictAnalysisContext<'_> { /// Returns the last decision which was made by the solver. pub(crate) fn find_last_decision(&mut self) -> Option { self.assignments.find_last_decision() @@ -132,15 +132,20 @@ impl<'a> ConflictAnalysisContext<'a> { /// Returns the reason for a propagation; if it is implied then the reason will be the decision /// which implied the predicate. + #[allow( + clippy::too_many_arguments, + reason = "borrow checker complains either here or elsewhere" + )] pub(crate) fn get_propagation_reason( predicate: Predicate, assignments: &Assignments, current_nogood: CurrentNogood<'_>, - reason_store: &'a mut ReasonStore, - propagators: &'a mut PropagatorStore, - proof_log: &'a mut ProofLog, + reason_store: &mut ReasonStore, + propagators: &mut PropagatorStore, + proof_log: &mut ProofLog, unit_nogood_step_ids: &HashMap, - ) -> &'a [Predicate] { + reason_out: &mut (impl Extend + AsRef<[Predicate]>), + ) { // TODO: this function could be put into the reason store // Note that this function can only be called with propagations, and never decision @@ -156,9 +161,8 @@ impl<'a> ConflictAnalysisContext<'a> { // there would be only one predicate from the current decision level. For this // reason, it is safe to assume that in the following, that any input predicate is // indeed a propagated predicate. - reason_store.helper.clear(); if assignments.is_initial_bound(predicate) { - return reason_store.helper.as_slice(); + return; } let trail_position = assignments @@ -179,11 +183,17 @@ impl<'a> ConflictAnalysisContext<'a> { let explanation_context = ExplanationContext::new(assignments, current_nogood); - let reason = reason_store - .get_or_compute(reason_ref, explanation_context, propagators) - .expect("reason reference should not be stale"); + let reason_exists = reason_store.get_or_compute( + reason_ref, + explanation_context, + propagators, + reason_out, + ); + + assert!(reason_exists, "reason reference should not be stale"); + if propagator_id == ConstraintSatisfactionSolver::get_nogood_propagator_id() - && reason.is_empty() + && reason_out.as_ref().is_empty() { // This means that a unit nogood was propagated, we indicate that this nogood step // was used @@ -207,12 +217,10 @@ impl<'a> ConflictAnalysisContext<'a> { // Otherwise we log the inference which was used to derive the nogood let _ = proof_log.log_inference( constraint_tag, - reason.iter().copied(), + reason_out.as_ref().iter().copied(), Some(predicate), ); } - reason - // The predicate is implicitly due as a result of a decision. } // 2) The predicate is true due to a propagation, and not explicitly on the trail. // It is necessary to further analyse what was the reason for setting the predicate true. @@ -240,7 +248,7 @@ impl<'a> ConflictAnalysisContext<'a> { // todo: could consider lifting here, since the trail bound // might be too strong. if trail_lower_bound > input_lower_bound { - reason_store.helper.push(trail_entry.predicate); + reason_out.extend(std::iter::once(trail_entry.predicate)); } // Otherwise, the input bound is strictly greater than the trailed // bound. This means the reason is due to holes in the domain. @@ -270,8 +278,8 @@ impl<'a> ConflictAnalysisContext<'a> { domain_id, not_equal_constant: input_lower_bound - 1, }; - reason_store.helper.push(one_less_bound_predicate); - reason_store.helper.push(not_equals_predicate); + reason_out.extend(std::iter::once(one_less_bound_predicate)); + reason_out.extend(std::iter::once(not_equals_predicate)); } } ( @@ -291,7 +299,7 @@ impl<'a> ConflictAnalysisContext<'a> { // so it safe to take the reason from the trail. // todo: lifting could be used here pumpkin_assert_simple!(trail_lower_bound > not_equal_constant); - reason_store.helper.push(trail_entry.predicate); + reason_out.extend(std::iter::once(trail_entry.predicate)); } ( Predicate::LowerBound { @@ -323,8 +331,8 @@ impl<'a> ConflictAnalysisContext<'a> { domain_id, upper_bound: equality_constant, }; - reason_store.helper.push(predicate_lb); - reason_store.helper.push(predicate_ub); + reason_out.extend(std::iter::once(predicate_lb)); + reason_out.extend(std::iter::once(predicate_ub)); } ( Predicate::UpperBound { @@ -344,7 +352,7 @@ impl<'a> ConflictAnalysisContext<'a> { // reason for the input predicate. // todo: lifting could be applied here. if trail_upper_bound < input_upper_bound { - reason_store.helper.push(trail_entry.predicate); + reason_out.extend(std::iter::once(trail_entry.predicate)); } else { // I think it cannot be that the bounds are equal, since otherwise we // would have found the predicate explicitly on the trail. @@ -365,8 +373,8 @@ impl<'a> ConflictAnalysisContext<'a> { domain_id, not_equal_constant: input_upper_bound + 1, }; - reason_store.helper.push(new_ub_predicate); - reason_store.helper.push(not_equal_predicate); + reason_out.extend(std::iter::once(new_ub_predicate)); + reason_out.extend(std::iter::once(not_equal_predicate)); } } ( @@ -387,7 +395,7 @@ impl<'a> ConflictAnalysisContext<'a> { // The bound was set past the not equals, so we can safely returns the trail // reason. todo: can do lifting here. - reason_store.helper.push(trail_entry.predicate); + reason_out.extend(std::iter::once(trail_entry.predicate)); } ( Predicate::UpperBound { @@ -422,8 +430,8 @@ impl<'a> ConflictAnalysisContext<'a> { domain_id, upper_bound: equality_constant, }; - reason_store.helper.push(predicate_lb); - reason_store.helper.push(predicate_ub); + reason_out.extend(std::iter::once(predicate_lb)); + reason_out.extend(std::iter::once(predicate_ub)); } ( Predicate::NotEqual { @@ -457,8 +465,8 @@ impl<'a> ConflictAnalysisContext<'a> { not_equal_constant: input_lower_bound - 1, }; - reason_store.helper.push(new_lb_predicate); - reason_store.helper.push(new_not_equals_predicate); + reason_out.extend(std::iter::once(new_lb_predicate)); + reason_out.extend(std::iter::once(new_not_equals_predicate)); } ( Predicate::NotEqual { @@ -492,8 +500,8 @@ impl<'a> ConflictAnalysisContext<'a> { not_equal_constant: input_upper_bound + 1, }; - reason_store.helper.push(new_ub_predicate); - reason_store.helper.push(new_not_equals_predicate); + reason_out.extend(std::iter::once(new_ub_predicate)); + reason_out.extend(std::iter::once(new_not_equals_predicate)); } ( Predicate::NotEqual { @@ -522,15 +530,14 @@ impl<'a> ConflictAnalysisContext<'a> { upper_bound: equality_constant, }; - reason_store.helper.push(predicate_lb); - reason_store.helper.push(predicate_ub); + reason_out.extend(std::iter::once(predicate_lb)); + reason_out.extend(std::iter::once(predicate_ub)); } _ => unreachable!( "Unreachable combination of {} and {}", trail_entry.predicate, predicate ), }; - reason_store.helper.as_slice() } } } diff --git a/pumpkin-solver/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs b/pumpkin-solver/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs index 52b6534b..47b3c174 100644 --- a/pumpkin-solver/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs +++ b/pumpkin-solver/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs @@ -117,7 +117,8 @@ impl RecursiveMinimiser { // Due to ownership rules, we have to take ownership of the reason. // TODO: Reuse the allocation if it becomes a bottleneck. - let reason = ConflictAnalysisContext::get_propagation_reason( + let mut reason = vec![]; + ConflictAnalysisContext::get_propagation_reason( input_predicate, context.assignments, CurrentNogood::from(current_nogood), @@ -125,10 +126,10 @@ impl RecursiveMinimiser { context.propagators, context.proof_log, context.unit_nogood_step_ids, - ) - .to_vec(); + &mut reason, + ); - for antecedent_predicate in reason { + for antecedent_predicate in reason.iter().copied() { // Root assignments can be safely ignored. if context .assignments diff --git a/pumpkin-solver/src/engine/conflict_analysis/resolvers/resolution_resolver.rs b/pumpkin-solver/src/engine/conflict_analysis/resolvers/resolution_resolver.rs index e5f11b59..46b95cd0 100644 --- a/pumpkin-solver/src/engine/conflict_analysis/resolvers/resolution_resolver.rs +++ b/pumpkin-solver/src/engine/conflict_analysis/resolvers/resolution_resolver.rs @@ -39,6 +39,8 @@ pub(crate) struct ResolutionResolver { recursive_minimiser: RecursiveMinimiser, /// Whether the resolver employs 1-UIP or all-decision learning. mode: AnalysisMode, + /// Re-usable buffer which reasons are written into. + reason_buffer: Vec, } #[derive(Debug, Clone, Copy, Default)] @@ -138,7 +140,8 @@ impl ConflictResolver for ResolutionResolver { // However, this can lead to [x <= v] to be processed *before* [x >= v - // y], meaning that these implied predicates should be replaced with their // reason - let reason = ConflictAnalysisContext::get_propagation_reason( + self.reason_buffer.clear(); + ConflictAnalysisContext::get_propagation_reason( predicate, context.assignments, CurrentNogood::new( @@ -150,23 +153,24 @@ impl ConflictResolver for ResolutionResolver { context.propagators, context.proof_log, context.unit_nogood_step_ids, + &mut self.reason_buffer, ); - if reason.is_empty() { + if self.reason_buffer.is_empty() { // In the case when the proof is being completed, it could be the case // that the reason for a root-level propagation is empty; this // predicate will be filtered out by the semantic minimisation pumpkin_assert_simple!(context.is_completing_proof); predicate } else { - pumpkin_assert_simple!(predicate.is_lower_bound_predicate() || predicate.is_not_equal_predicate(), "A non-decision predicate in the nogood should be either a lower-bound or a not-equals predicate but it was {predicate} with reason {reason:?}"); + pumpkin_assert_simple!(predicate.is_lower_bound_predicate() || predicate.is_not_equal_predicate(), "A non-decision predicate in the nogood should be either a lower-bound or a not-equals predicate but it was {predicate} with reason {:?}", self.reason_buffer); pumpkin_assert_simple!( - reason.len() == 1 && reason[0].is_lower_bound_predicate(), + self.reason_buffer.len() == 1 && self.reason_buffer[0].is_lower_bound_predicate(), "The reason for the only propagated predicates left on the trail should be lower-bound predicates, but the reason for {predicate} was {:?}", - reason + self.reason_buffer, ); - reason[0] + self.reason_buffer[0] } }; @@ -199,7 +203,9 @@ impl ConflictResolver for ResolutionResolver { .is_initial_bound(self.peek_predicate_from_conflict_nogood()) { let predicate = self.peek_predicate_from_conflict_nogood(); - let reason = ConflictAnalysisContext::get_propagation_reason( + + self.reason_buffer.clear(); + ConflictAnalysisContext::get_propagation_reason( predicate, context.assignments, CurrentNogood::new( @@ -211,13 +217,14 @@ impl ConflictResolver for ResolutionResolver { context.propagators, context.proof_log, context.unit_nogood_step_ids, + &mut self.reason_buffer, ); pumpkin_assert_simple!(predicate.is_lower_bound_predicate() || predicate.is_not_equal_predicate() , "If the final predicate in the conflict nogood is not a decision predicate then it should be either a lower-bound predicate or a not-equals predicate but was {predicate}"); pumpkin_assert_simple!( - reason.len() == 1 && reason[0].is_lower_bound_predicate(), - "The reason for the decision predicate should be a lower-bound predicate but was {}", reason[0] + self.reason_buffer.len() == 1 && self.reason_buffer[0].is_lower_bound_predicate(), + "The reason for the decision predicate should be a lower-bound predicate but was {}", self.reason_buffer[0] ); - self.replace_predicate_in_conflict_nogood(predicate, reason[0]); + self.replace_predicate_in_conflict_nogood(predicate, self.reason_buffer[0]); } // The final predicate in the heap will get pushed in `extract_final_nogood` @@ -226,7 +233,8 @@ impl ConflictResolver for ResolutionResolver { } // 2.b) Standard case, get the reason for the predicate and add it to the nogood. - let reason = ConflictAnalysisContext::get_propagation_reason( + self.reason_buffer.clear(); + ConflictAnalysisContext::get_propagation_reason( next_predicate, context.assignments, CurrentNogood::new( @@ -238,17 +246,22 @@ impl ConflictResolver for ResolutionResolver { context.propagators, context.proof_log, context.unit_nogood_step_ids, + &mut self.reason_buffer, ); - for predicate in reason.iter() { + // We do a little swapping of the ownership of the buffer, so we can call + // `self.add_predicate_to_conflict_nogood`. + let reason = std::mem::take(&mut self.reason_buffer); + for predicate in reason.iter().copied() { self.add_predicate_to_conflict_nogood( - *predicate, + predicate, context.assignments, context.brancher, self.mode, context.is_completing_proof, ); } + self.reason_buffer = reason; } Some(self.extract_final_nogood(context)) } diff --git a/pumpkin-solver/src/engine/constraint_satisfaction_solver.rs b/pumpkin-solver/src/engine/constraint_satisfaction_solver.rs index 34985844..4800c41a 100644 --- a/pumpkin-solver/src/engine/constraint_satisfaction_solver.rs +++ b/pumpkin-solver/src/engine/constraint_satisfaction_solver.rs @@ -1137,20 +1137,18 @@ impl ConstraintSatisfactionSolver { // Look up the reason for the bound that changed. // The reason for changing the bound cannot be a decision, so we can safely unwrap. - let reason_changing_bound = reason_store - .get_or_compute( - entry.reason.unwrap(), - ExplanationContext::from(&*assignments), - propagators, - ) - .unwrap(); - let mut empty_domain_reason: Vec = vec![ predicate!(conflict_domain >= entry.old_lower_bound), predicate!(conflict_domain <= entry.old_upper_bound), ]; - empty_domain_reason.append(&mut reason_changing_bound.to_vec()); + let _ = reason_store.get_or_compute( + entry.reason.unwrap(), + ExplanationContext::from(&*assignments), + propagators, + &mut empty_domain_reason, + ); + empty_domain_reason.into() } @@ -1269,19 +1267,18 @@ impl ConstraintSatisfactionSolver { ) { for trail_idx in start_trail_index..self.assignments.num_trail_entries() { let entry = self.assignments.get_trail_entry(trail_idx); - let reason = entry + let reason_ref = entry .reason .expect("Added by a propagator and must therefore have a reason"); // Get the conjunction of predicates explaining the propagation. - let reason = self - .reason_store - .get_or_compute( - reason, - ExplanationContext::new(&self.assignments, CurrentNogood::empty()), - &mut self.propagators, - ) - .expect("Reason ref is valid"); + let mut reason = vec![]; + let _ = self.reason_store.get_or_compute( + reason_ref, + ExplanationContext::new(&self.assignments, CurrentNogood::empty()), + &mut self.propagators, + &mut reason, + ); let propagated = entry.predicate; diff --git a/pumpkin-solver/src/engine/cp/propagation/contexts/propagation_context.rs b/pumpkin-solver/src/engine/cp/propagation/contexts/propagation_context.rs index 95c9ba69..fe97f1d9 100644 --- a/pumpkin-solver/src/engine/cp/propagation/contexts/propagation_context.rs +++ b/pumpkin-solver/src/engine/cp/propagation/contexts/propagation_context.rs @@ -98,7 +98,10 @@ impl<'a> PropagationContextMut<'a> { conjunction.add(reification_literal.get_true_predicate()); Reason::Eager(conjunction) } - Reason::DynamicLazy(_) => todo!(), + Reason::DynamicLazy(code) => Reason::ReifiedLazy(reification_literal, code), + Reason::ReifiedLazy(_, _) => { + unimplemented!("cannot reify an already reified reason") + } } } else { reason diff --git a/pumpkin-solver/src/engine/cp/reason.rs b/pumpkin-solver/src/engine/cp/reason.rs index 73ccfe1c..1d58c100 100644 --- a/pumpkin-solver/src/engine/cp/reason.rs +++ b/pumpkin-solver/src/engine/cp/reason.rs @@ -7,12 +7,12 @@ use crate::basic_types::PropositionalConjunction; use crate::basic_types::Trail; use crate::predicates::Predicate; use crate::pumpkin_assert_simple; +use crate::variables::Literal; /// The reason store holds a reason for each change made by a CP propagator on a trail. #[derive(Default, Debug)] pub(crate) struct ReasonStore { trail: Trail<(PropagatorId, Reason)>, - pub helper: PropositionalConjunction, } impl ReasonStore { @@ -27,15 +27,22 @@ impl ReasonStore { ReasonRef(index as u32) } - pub(crate) fn get_or_compute<'this>( - &'this self, + pub(crate) fn get_or_compute( + &self, reference: ReasonRef, context: ExplanationContext<'_>, - propagators: &'this mut PropagatorStore, - ) -> Option<&'this [Predicate]> { - self.trail - .get(reference.0 as usize) - .map(|reason| reason.1.compute(context, reason.0, propagators)) + propagators: &mut PropagatorStore, + destination_buffer: &mut impl Extend, + ) -> bool { + let Some(reason) = self.trail.get(reference.0 as usize) else { + return false; + }; + + reason + .1 + .compute(context, reason.0, propagators, destination_buffer); + + true } pub(crate) fn get_lazy_code(&self, reference: ReasonRef) -> Option<&u64> { @@ -43,6 +50,9 @@ impl ReasonStore { Some(reason) => match &reason.1 { Reason::Eager(_) => None, Reason::DynamicLazy(code) => Some(code), + Reason::ReifiedLazy(_, _) => { + unimplemented!("Getting the code of a reified lazy reason is unsupported.") + } }, None => None, } @@ -84,23 +94,38 @@ pub(crate) enum Reason { /// propagation the reason is for. The payload should be enough for the propagator to construct /// an explanation based on its internal state. DynamicLazy(u64), + /// A lazy explanation that has reified. + ReifiedLazy(Literal, u64), } impl Reason { - pub(crate) fn compute<'a>( - &'a self, + pub(crate) fn compute( + &self, context: ExplanationContext<'_>, propagator_id: PropagatorId, - propagators: &'a mut PropagatorStore, - ) -> &'a [Predicate] { + propagators: &mut PropagatorStore, + destination_buffer: &mut impl Extend, + ) { match self { // We do not replace the reason with an eager explanation for dynamic lazy explanations. // // Benchmarking will have to show whether this should change or not. - Reason::DynamicLazy(code) => { - propagators[propagator_id].lazy_explanation(*code, context) + Reason::DynamicLazy(code) => destination_buffer.extend( + propagators[propagator_id] + .lazy_explanation(*code, context) + .iter() + .copied(), + ), + Reason::Eager(result) => destination_buffer.extend(result.iter().copied()), + Reason::ReifiedLazy(literal, code) => { + destination_buffer.extend( + propagators[propagator_id] + .lazy_explanation(*code, context) + .iter() + .copied(), + ); + destination_buffer.extend(std::iter::once(literal.get_true_predicate())); } - Reason::Eager(result) => result.as_slice(), } } } @@ -115,8 +140,10 @@ impl From for Reason { mod tests { use super::*; use crate::conjunction; + use crate::engine::propagation::Propagator; use crate::engine::variables::DomainId; use crate::engine::Assignments; + use crate::predicate; #[test] fn computing_an_eager_reason_returns_a_reference_to_the_conjunction() { @@ -128,14 +155,15 @@ mod tests { let conjunction = conjunction!([x == 1] & [y == 2]); let reason = Reason::Eager(conjunction.clone()); - assert_eq!( - conjunction.as_slice(), - reason.compute( - ExplanationContext::from(&integers), - PropagatorId(0), - &mut PropagatorStore::default() - ) + let mut out_reason = vec![]; + reason.compute( + ExplanationContext::from(&integers), + PropagatorId(0), + &mut PropagatorStore::default(), + &mut out_reason, ); + + assert_eq!(conjunction.as_slice(), &out_reason); } #[test] @@ -151,13 +179,68 @@ mod tests { assert_eq!(ReasonRef(0), reason_ref); - assert_eq!( - Some(conjunction.as_slice()), - reason_store.get_or_compute( - reason_ref, - ExplanationContext::from(&integers), - &mut PropagatorStore::default() - ) + let mut out_reason = vec![]; + let _ = reason_store.get_or_compute( + reason_ref, + ExplanationContext::from(&integers), + &mut PropagatorStore::default(), + &mut out_reason, + ); + + assert_eq!(conjunction.as_slice(), &out_reason); + } + + #[test] + fn reified_lazy_explanation_has_reification_added_after_compute() { + let mut reason_store = ReasonStore::default(); + let mut integers = Assignments::default(); + + let x = integers.grow(1, 5); + let reif = Literal::new(integers.grow(0, 1)); + + struct TestPropagator(Vec); + + impl Propagator for TestPropagator { + fn name(&self) -> &str { + todo!() + } + + fn debug_propagate_from_scratch( + &self, + _: crate::engine::propagation::PropagationContextMut, + ) -> crate::basic_types::PropagationStatusCP { + todo!() + } + + fn initialise_at_root( + &mut self, + _: &mut crate::engine::propagation::PropagatorInitialisationContext, + ) -> Result<(), PropositionalConjunction> { + todo!() + } + + fn lazy_explanation(&mut self, code: u64, _: ExplanationContext) -> &[Predicate] { + assert_eq!(0, code); + + &self.0 + } + } + + let mut propagator_store = PropagatorStore::default(); + let propagator_id = + propagator_store.alloc(Box::new(TestPropagator(vec![predicate![x >= 2]])), None); + let reason_ref = reason_store.push(propagator_id, Reason::ReifiedLazy(reif, 0)); + + assert_eq!(ReasonRef(0), reason_ref); + + let mut reason = vec![]; + let _ = reason_store.get_or_compute( + reason_ref, + ExplanationContext::from(&integers), + &mut propagator_store, + &mut reason, ); + + assert_eq!(vec![predicate![x >= 2], reif.get_true_predicate()], reason); } } diff --git a/pumpkin-solver/src/engine/cp/test_solver.rs b/pumpkin-solver/src/engine/cp/test_solver.rs index 12bbc584..4dcc886a 100644 --- a/pumpkin-solver/src/engine/cp/test_solver.rs +++ b/pumpkin-solver/src/engine/cp/test_solver.rs @@ -244,14 +244,13 @@ impl TestSolver { let reason_ref = self .assignments .get_reason_for_predicate_brute_force(predicate); - let predicates = self - .reason_store - .get_or_compute( - reason_ref, - ExplanationContext::from(&self.assignments), - &mut self.propagator_store, - ) - .expect("reason_ref should not be stale"); + let mut predicates = vec![]; + let _ = self.reason_store.get_or_compute( + reason_ref, + ExplanationContext::from(&self.assignments), + &mut self.propagator_store, + &mut predicates, + ); PropositionalConjunction::from(predicates) } diff --git a/pumpkin-solver/src/engine/debug_helper.rs b/pumpkin-solver/src/engine/debug_helper.rs index 88f14ea7..99f0109f 100644 --- a/pumpkin-solver/src/engine/debug_helper.rs +++ b/pumpkin-solver/src/engine/debug_helper.rs @@ -162,16 +162,15 @@ impl DebugHelper { for trail_index in num_trail_entries_before..assignments.num_trail_entries() { let trail_entry = assignments.get_trail_entry(trail_index); - let reason = reason_store - .get_or_compute( - trail_entry - .reason - .expect("Expected checked propagation to have a reason"), - ExplanationContext::from(assignments), - propagators, - ) - .expect("reason should exist for this propagation") - .to_vec(); + let mut reason = vec![]; + let _ = reason_store.get_or_compute( + trail_entry + .reason + .expect("Expected checked propagation to have a reason"), + ExplanationContext::from(assignments), + propagators, + &mut reason, + ); result &= Self::debug_propagator_reason( trail_entry.predicate, diff --git a/pumpkin-solver/src/propagators/cumulative/time_table/propagation_handler.rs b/pumpkin-solver/src/propagators/cumulative/time_table/propagation_handler.rs index d7260e0f..9dca270f 100644 --- a/pumpkin-solver/src/propagators/cumulative/time_table/propagation_handler.rs +++ b/pumpkin-solver/src/propagators/cumulative/time_table/propagation_handler.rs @@ -714,16 +714,15 @@ pub(crate) mod test_propagation_handler { .assignments .get_reason_for_predicate_brute_force(predicate); let mut propagator_store = PropagatorStore::default(); - let reason = self - .reason_store - .get_or_compute( - reason_ref, - ExplanationContext::from(&self.assignments), - &mut propagator_store, - ) - .expect("reason_ref should not be stale"); + let mut reason = vec![]; + let _ = self.reason_store.get_or_compute( + reason_ref, + ExplanationContext::from(&self.assignments), + &mut propagator_store, + &mut reason, + ); - reason.iter().copied().collect() + reason.into() } } }