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 17ec8402..00b0c5b6 100644 --- a/pumpkin-solver/src/engine/conflict_analysis/resolvers/resolution_resolver.rs +++ b/pumpkin-solver/src/engine/conflict_analysis/resolvers/resolution_resolver.rs @@ -85,20 +85,32 @@ impl ConflictResolver for ResolutionResolver { { predicate } else { + // Note that we decompose [x == v] into the two predicates [x >= v] and [x + // <= v] and that these have distinct trail entries (where [x >= v] has a + // lower trail position than [x <= v]) + // + // 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 = ConflictAnalysisNogoodContext::get_propagation_reason_simple( predicate, context.assignments, context.reason_store, context.propagators, ); - // We expect only not equals predicates here, which just have one reason. - pumpkin_assert_simple!(reason.len() == 1); + pumpkin_assert_simple!( + reason.len() == 1 && reason[0].is_lower_bound_predicate(), + "The only non-decision predicates left should be unit reasons which consist of lower-bounds" + ); reason[0] }; + // We push to `predicates_lower_decision_level` since this structure will be + // used for creating the final nogood self.predicates_lower_decision_level .push(predicate_replacement); } + // The final predicate in the heap will get pushed in `extract_final_nogood` self.predicates_lower_decision_level.push(next_predicate); break; }