pumpkin_core/engine/
conflict.rs

1use crate::engine::reason::ReasonRef;
2use crate::predicates::Predicate;
3use crate::predicates::PropositionalConjunction;
4use crate::proof::InferenceCode;
5use crate::propagation::ExplanationContext;
6use crate::state::CurrentNogood;
7use crate::state::State;
8use crate::variables::DomainId;
9
10/// The result of invoking a constraint programming propagator. The propagation can either succeed
11/// or identify a conflict. The necessary conditions for the conflict must be captured in the error
12/// variant, i.e. a propositional conjunction.
13pub type PropagationStatusCP = Result<(), Conflict>;
14
15/// Convenience function to create [`PropagationStatusCP`] with a [`PropagatorConflict`].
16pub fn propagator_conflict(
17    conjunction: PropositionalConjunction,
18    inference_code: &InferenceCode,
19) -> PropagationStatusCP {
20    Err(Conflict::Propagator(PropagatorConflict {
21        conjunction,
22        inference_code: inference_code.clone(),
23    }))
24}
25
26/// Information concerning the conflict returned by [`State::propagate_to_fixed_point`].
27///
28/// Two (related) conflicts can happen:
29/// 1) a propagator explicitly detects a conflict.
30/// 2) a propagator post a domain change that results in a variable having an empty domain.
31#[derive(Debug, Clone, PartialEq, Eq)]
32pub enum Conflict {
33    /// A conflict raised explicitly by a propagator.
34    Propagator(PropagatorConflict),
35    /// A conflict caused by an empty domain for a variable occurring.
36    EmptyDomain(EmptyDomainConflict),
37}
38
39impl From<EmptyDomainConflict> for Conflict {
40    fn from(value: EmptyDomainConflict) -> Self {
41        Conflict::EmptyDomain(value)
42    }
43}
44
45impl From<PropagatorConflict> for Conflict {
46    fn from(value: PropagatorConflict) -> Self {
47        Conflict::Propagator(value)
48    }
49}
50
51/// A conflict because a domain became empty.
52#[derive(Clone, Copy, Debug, PartialEq, Eq)]
53pub struct EmptyDomainConflict {
54    /// The predicate that caused a domain to become empty.
55    pub trigger_predicate: Predicate,
56    /// The reason for [`EmptyDomainConflict::trigger_predicate`] to be true.
57    ///
58    /// If the empty domain is not triggered by a propagation, this is [`None`].
59    pub(crate) trigger_reason: Option<ReasonRef>,
60}
61
62impl EmptyDomainConflict {
63    /// The domain that became empty.
64    pub fn domain(&self) -> DomainId {
65        self.trigger_predicate.get_domain()
66    }
67
68    /// Returns the reason for the [`EmptyDomainConflict::trigger_predicate`] being propagated to
69    /// true while it is already false in the [`State`].
70    pub fn get_reason(
71        &self,
72        state: &mut State,
73        reason_buffer: &mut (impl Extend<Predicate> + AsRef<[Predicate]>),
74        current_nogood: CurrentNogood,
75    ) -> Option<InferenceCode> {
76        self.trigger_reason.map(|reason_ref| {
77            state.reason_store.get_or_compute(
78                reason_ref,
79                ExplanationContext::new(
80                    &state.assignments,
81                    current_nogood,
82                    state.trail_len(),
83                    &mut state.notification_engine,
84                ),
85                &mut state.propagators,
86                reason_buffer,
87            )
88        })
89    }
90}
91
92/// A conflict stated by a propagator. A propagator that identifies a conflict that is _not_ an
93/// empty domain, describes that conflict with this type.
94#[derive(Clone, Debug, PartialEq, Eq)]
95pub struct PropagatorConflict {
96    /// The conjunction that describes the infeasible partial assignment.
97    pub conjunction: PropositionalConjunction,
98    /// The inference code that identified the conflict.
99    pub inference_code: InferenceCode,
100}
pumpkin_core/engine/conflict.rs

pumpkin_core/engine/
conflict.rs
