refactor(pumpkin-core): Empty domain conflict is a predicate and reason

pumpkin-crates/core/src/basic_types/mod.rs

@@ -23,5 +23,5 @@ pub use random::*;
 pub use solution::ProblemSolution;
 pub use solution::Solution;
 pub use solution::SolutionReference;
-pub(crate) use stored_conflict_info::StoredConflictInfo;
+pub(crate) use stored_conflict_info::*;
 pub(crate) use trail::Trail;

pumpkin-crates/core/src/basic_types/stored_conflict_info.rs

@@ -1,10 +1,13 @@
-use super::PropositionalConjunction;
 use super::propagation_status_cp::PropagatorConflict;
 use crate::ConstraintOperationError;
 #[cfg(doc)]
 use crate::engine::ConstraintSatisfactionSolver;
 #[cfg(doc)]
 use crate::engine::propagation::Propagator;
+use crate::engine::reason::ReasonRef;
+use crate::predicates::Predicate;
+use crate::proof::InferenceCode;
+use crate::variables::DomainId;
 
 /// A conflict info which can be stored in the solver.
 /// Two (related) conflicts can happen:
@@ -13,8 +16,28 @@ use crate::engine::propagation::Propagator;
 #[derive(Debug, PartialEq, Eq, Clone)]
 pub(crate) enum StoredConflictInfo {
     Propagator(PropagatorConflict),
-    EmptyDomain {
-        conflict_nogood: PropositionalConjunction,
-    },
+    EmptyDomain(EmptyDomainConflict),
+    /// The conflict is due to inconsistent assumptions.
+    ///
+    /// The provided predicate and its negation are both assumptions.
+    InconsistentAssumptions(Predicate),
     RootLevelConflict(ConstraintOperationError),
 }
+
+/// A conflict because a domain became empty.
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub(crate) struct EmptyDomainConflict {
+    /// The predicate that caused a domain to become empty.
+    pub(crate) trigger_predicate: Predicate,
+    /// The reason for [`EmptyDomainConflict::trigger_predicate`] to be true.
+    pub(crate) trigger_reason: ReasonRef,
+    /// The [`InferenceCode`] that accompanies [`EmptyDomainConflict::trigger_reason`].
+    pub(crate) trigger_inference_code: InferenceCode,
+}
+
+impl EmptyDomainConflict {
+    /// The domain that became empty.
+    pub(crate) fn domain(&self) -> DomainId {
+        self.trigger_predicate.get_domain()
+    }
+}

pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs

@@ -2,6 +2,7 @@ use std::fmt::Debug;
 
 use super::minimisers::SemanticMinimiser;
 use crate::Random;
+use crate::basic_types::EmptyDomainConflict;
 use crate::basic_types::StoredConflictInfo;
 use crate::branching::Brancher;
 use crate::containers::HashMap;
@@ -23,11 +24,13 @@ use crate::engine::reason::ReasonRef;
 use crate::engine::reason::ReasonStore;
 use crate::engine::solver_statistics::SolverStatistics;
 use crate::predicate;
+use crate::predicates::PropositionalConjunction;
 use crate::proof::InferenceCode;
 use crate::proof::ProofLog;
 use crate::proof::RootExplanationContext;
 use crate::proof::explain_root_assignment;
 use crate::propagators::nogoods::NogoodPropagator;
+use crate::pumpkin_assert_eq_simple;
 use crate::pumpkin_assert_simple;
 
 /// Used during conflict analysis to provide the necessary information.
@@ -120,19 +123,22 @@ impl ConflictAnalysisContext<'_> {
 
                 conflict.conjunction
             }
-            StoredConflictInfo::EmptyDomain { conflict_nogood } => conflict_nogood,
+            StoredConflictInfo::EmptyDomain(conflict) => self.compute_conflict_nogood(conflict),
             StoredConflictInfo::RootLevelConflict(_) => {
                 unreachable!("Should never attempt to learn a nogood from a root level conflict")
             }
+            StoredConflictInfo::InconsistentAssumptions(predicate) => {
+                vec![predicate, !predicate].into()
+            }
         };
 
         for &predicate in conflict_nogood.iter() {
-            if self
+            let predicate_dl = self
                 .assignments
                 .get_decision_level_for_predicate(&predicate)
-                .unwrap()
-                == 0
-            {
+                .expect("all predicates in the conflict nogood should be assigned to true");
+
+            if predicate_dl == 0 {
                 explain_root_assignment(
                     &mut RootExplanationContext {
                         propagators: self.propagators,
@@ -495,4 +501,93 @@ impl ConflictAnalysisContext<'_> {
             };
         }
     }
+
+    fn compute_conflict_nogood(
+        &mut self,
+        conflict: EmptyDomainConflict,
+    ) -> PropositionalConjunction {
+        let conflict_domain = conflict.domain();
+
+        // 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 mut empty_domain_reason: Vec<Predicate> = vec![];
+        let _ = self.reason_store.get_or_compute(
+            conflict.trigger_reason,
+            ExplanationContext::without_working_nogood(
+                self.assignments,
+                self.assignments.num_trail_entries() - 1,
+                self.notification_engine,
+            ),
+            self.propagators,
+            &mut empty_domain_reason,
+        );
+
+        // We also need to log this last propagation to the proof log as an inference.
+        let _ = self.proof_log.log_inference(
+            conflict.trigger_inference_code,
+            empty_domain_reason.iter().copied(),
+            Some(conflict.trigger_predicate),
+            self.variable_names,
+        );
+
+        let old_lower_bound = self.assignments.get_lower_bound(conflict_domain);
+        let old_upper_bound = self.assignments.get_upper_bound(conflict_domain);
+
+        match conflict.trigger_predicate.get_predicate_type() {
+            PredicateType::LowerBound => {
+                // The last trail entry was a lower-bound propagation meaning that the empty domain
+                // was caused by the upper-bound
+                //
+                // We lift so that it is the most general upper-bound possible while still causing
+                // the empty domain
+                empty_domain_reason.push(predicate!(
+                    conflict_domain <= conflict.trigger_predicate.get_right_hand_side() - 1
+                ));
+            }
+            PredicateType::UpperBound => {
+                // The last trail entry was an upper-bound propagation meaning that the empty domain
+                // was caused by the lower-bound
+                //
+                // We lift so that it is the most general lower-bound possible while still causing
+                // the empty domain
+                empty_domain_reason.push(predicate!(
+                    conflict_domain >= conflict.trigger_predicate.get_right_hand_side() + 1
+                ));
+            }
+            PredicateType::NotEqual => {
+                // The last trail entry was a not equals propagation meaning that the empty domain
+                // was due to the domain being assigned to the removed value
+                pumpkin_assert_eq_simple!(old_upper_bound, old_lower_bound);
+
+                empty_domain_reason.push(predicate!(conflict_domain == old_lower_bound));
+            }
+            PredicateType::Equal => {
+                // The last trail entry was an equality propagation; we split into three cases.
+                if conflict.trigger_predicate.get_right_hand_side() < old_lower_bound {
+                    // 1) The assigned value was lower than the lower-bound
+                    //
+                    // We lift so that it is the most general lower-bound possible while still
+                    // causing the empty domain
+                    empty_domain_reason.push(predicate!(
+                        conflict_domain >= conflict.trigger_predicate.get_right_hand_side() + 1
+                    ));
+                } else if conflict.trigger_predicate.get_right_hand_side() > old_upper_bound {
+                    // 2) The assigned value was larger than the upper-bound
+                    //
+                    // We lift so that it is the most general upper-bound possible while still
+                    // causing the empty domain
+                    empty_domain_reason.push(predicate!(
+                        conflict_domain <= conflict.trigger_predicate.get_right_hand_side() - 1
+                    ));
+                } else {
+                    // 3) The assigned value was equal to a hole in the domain
+                    empty_domain_reason.push(predicate!(
+                        conflict_domain != conflict.trigger_predicate.get_right_hand_side()
+                    ))
+                }
+            }
+        }
+
+        empty_domain_reason.into()
+    }
 }