Skip to main content

pumpkin_core/propagation/
propagator.rs

1use downcast_rs::Downcast;
2use downcast_rs::impl_downcast;
3use dyn_clone::DynClone;
4use dyn_clone::clone_trait_object;
5
6use super::Domains;
7use super::ExplanationContext;
8use super::PropagationContext;
9use super::contexts::NotificationContext;
10use crate::basic_types::PredicateId;
11use crate::basic_types::PropagationStatusCP;
12use crate::basic_types::PropagatorConflict;
13#[cfg(doc)]
14use crate::create_statistics_struct;
15#[cfg(doc)]
16use crate::engine::ConstraintSatisfactionSolver;
17use crate::engine::notifications::OpaqueDomainEvent;
18use crate::predicates::Predicate;
19#[cfg(doc)]
20use crate::propagation::DomainEvent;
21#[cfg(doc)]
22use crate::propagation::PropagatorConstructor;
23#[cfg(doc)]
24use crate::propagation::PropagatorConstructorContext;
25#[cfg(doc)]
26use crate::propagation::ReadDomains;
27use crate::propagation::local_id::LocalId;
28#[cfg(doc)]
29use crate::pumpkin_asserts::PUMPKIN_ASSERT_ADVANCED;
30#[cfg(doc)]
31use crate::pumpkin_asserts::PUMPKIN_ASSERT_EXTREME;
32#[cfg(doc)]
33use crate::state::Conflict;
34use crate::statistics::statistic_logger::StatisticLogger;
35
36// We need to use this to cast from `Box<dyn Propagator>` to `NogoodPropagator`; rust inherently
37// does not allow downcasting from the trait definition to its concrete type.
38impl_downcast!(Propagator);
39
40// To allow the State object to be cloneable, we need to allow `Box<dyn Propagator>` to be cloned.
41clone_trait_object!(Propagator);
42
43/// A propagator removes values from domains which will never be in any solution, or raises
44/// explicit conflicts.
45///
46/// The only required functions are [`Propagator::name`],
47///  and [`Propagator::propagate_from_scratch`]; all other
48/// functions have default implementations. For initial development, the required functions are
49/// enough, but a more mature implementation considers all functions in most cases.
50///
51/// See the [`crate::propagation`] documentation for more details.
52pub trait Propagator: Downcast + DynClone {
53    /// Return the name of the propagator.
54    ///
55    /// This is a convenience method that is used for printing.
56    fn name(&self) -> &str;
57
58    /// Performs propagation from scratch (i.e., without relying on updating
59    /// internal data structures, as opposed to [`Propagator::propagate`]).
60    ///
61    /// The main aims of this method are to remove values from the domains of variables (using
62    /// [`PropagationContext::post`]) which cannot be part of any solution given the current
63    /// domains and to detect conflicts.
64    ///
65    /// In case no conflict has been detected this function should
66    /// return [`Result::Ok`], otherwise it should return a [`Result::Err`] with a [`Conflict`]
67    /// which contains the reason for the failure; either because a propagation caused an
68    /// an empty domain ([`Conflict::EmptyDomain`] as a result of [`PropagationContext::post`]) or
69    /// because the logic of the propagator found the current state to be inconsistent
70    /// ([`Conflict::Propagator`] ).
71    ///
72    /// It is usually best to implement this propagation method in the simplest
73    /// but correct way. When this crate is compiled with the `debug-checks` feature, this method
74    /// will be called to double check the reasons for failures and propagations that have been
75    /// reported by this propagator.
76    ///
77    /// Propagators are not required to propagate until a fixed point. It will be called again by
78    /// the solver until no further propagations happen.
79    fn propagate_from_scratch(&self, context: PropagationContext) -> PropagationStatusCP;
80
81    /// Performs propagation with state (i.e., with being able to mutate internal data structures,
82    /// as opposed to [`Propagator::propagate_from_scratch`]).
83    ///
84    /// The main aims of this method are to remove values from the domains of variables (using
85    /// [`PropagationContext::post`]) which cannot be part of any solution given the current
86    /// domains and to detect conflicts.
87    ///
88    /// In case no conflict has been detected this function should
89    /// return [`Result::Ok`], otherwise it should return a [`Result::Err`] with a [`Conflict`]
90    /// which contains the reason for the failure; either because a propagation caused an
91    /// an empty domain ([`Conflict::EmptyDomain`] as a result of [`PropagationContext::post`]) or
92    /// because the logic of the propagator found the current state to be inconsistent
93    /// ([`Conflict::Propagator`] ).
94    ///
95    /// Propagators are not required to propagate until a fixed point. It will be called
96    /// again by the solver until no further propagations happen.
97    ///
98    /// By default, this function calls [`Propagator::propagate_from_scratch`].
99    fn propagate(&mut self, context: PropagationContext) -> PropagationStatusCP {
100        self.propagate_from_scratch(context)
101    }
102
103    /// Returns whether the propagator should be enqueued for propagation when a [`DomainEvent`]
104    /// happens to one of the variables the propagator is subscribed to (as registered during
105    /// creation with [`PropagatorConstructor`] using [`PropagatorConstructorContext::register`]).
106    ///
107    /// This can be used to incrementally maintain data structures or perform propagations, and
108    /// should only be used for computationally cheap logic. Expensive computation should be
109    /// performed in the [`Propagator::propagate`] method.
110    ///
111    /// By default the propagator is always enqueued for every event it is subscribed to. Not all
112    /// propagators will benefit from implementing this, so it is not required to do so.
113    fn notify(
114        &mut self,
115        _context: NotificationContext,
116        _local_id: LocalId,
117        _event: OpaqueDomainEvent,
118    ) -> EnqueueDecision {
119        EnqueueDecision::Enqueue
120    }
121
122    /// This function is called when the effect of a [`DomainEvent`] is undone during backtracking
123    /// of one of the variables the propagator is subscribed to (as registered during creation with
124    /// [`PropagatorConstructor`] using [`PropagatorConstructorContext::register_backtrack`]).
125    ///
126    /// This can be used to incrementally maintain data structures or perform propagations, and
127    /// should only be used for computationally cheap logic. Expensive computation should be
128    /// performed in the [`Propagator::propagate`] method.
129    ///
130    /// *Note*: This method is only called for [`DomainEvent`]s for which [`Propagator::notify`]
131    /// was called. This means that if the propagator itself made a change, but was not notified of
132    /// it (e.g., due to a conflict being detected), then this method will also not be called for
133    /// that [`DomainEvent`].
134    ///
135    /// By default the propagator does nothing when this method is called. Not all propagators will
136    /// benefit from implementing this, so it is not required to do so.
137    fn notify_backtrack(
138        &mut self,
139        _context: Domains,
140        _local_id: LocalId,
141        _event: OpaqueDomainEvent,
142    ) {
143    }
144
145    /// Returns whether the propagator should be enqueued for propagation when a [`Predicate`] (with
146    /// corresponding [`PredicateId`]) which the propagator is subscribed to (as registered either
147    /// during using [`PropagationContext::register_predicate`] or during creation with
148    /// [`PropagatorConstructor`] using [`PropagatorConstructorContext::register_predicate`]).
149    ///
150    /// By default, the propagator will be enqueued.
151    fn notify_predicate_id_satisfied(
152        &mut self,
153        _context: NotificationContext,
154        _predicate_id: PredicateId,
155    ) -> EnqueueDecision {
156        EnqueueDecision::Enqueue
157    }
158
159    /// Called after backtracking, allowing the propagator to
160    /// update its internal data structures given the new variable domains.
161    ///
162    /// By default this function does nothing.
163    fn synchronise(&mut self, _context: NotificationContext<'_>) {}
164
165    /// Returns the [`Priority`] of the propagator, used for determining the order in which
166    /// propagators are called.
167    ///
168    /// See [`Priority`] documentation for more explanation.
169    ///
170    /// By default the priority is set to [`Priority::VeryLow`]. It is expected that
171    /// propagator implementations would set this value to some appropriate value.
172    fn priority(&self) -> Priority {
173        Priority::VeryLow
174    }
175
176    /// A function which returns [`Some`] with a [`PropagatorConflict`] when this propagator can
177    /// detect an inconsistency (and [`None`] otherwise).
178    ///
179    /// By implementing this function, if the propagator is reified, it can propagate the
180    /// reification literal based on the detected inconsistency. Yet, an implementation is not
181    /// needed for correctness, as [`Propagator::propagate`] should still check for
182    /// inconsistency as well.
183    fn detect_inconsistency(&self, _domains: Domains) -> Option<PropagatorConflict> {
184        None
185    }
186
187    /// Hook which is called when a propagated [`Predicate`] should be explained using a lazy
188    /// reason.
189    ///
190    /// The code which was attached to the propagation is given, as
191    /// well as a context object which defines what can be inspected from the solver to build the
192    /// explanation.
193    ///
194    /// *Note:* The context which is provided contains the _current_ state (i.e. the state when the
195    /// explanation is generated); the bounds at the time of the propagation can be retrieved using
196    /// methods such as [`ReadDomains::lower_bound_at_trail_position`] in combination
197    /// with [`ExplanationContext::get_trail_position`].
198    fn lazy_explanation(&mut self, _code: u64, _context: ExplanationContext) -> &[Predicate] {
199        panic!(
200            "{}",
201            format!(
202                "Propagator {} does not support lazy explanations.",
203                self.name()
204            )
205        );
206    }
207
208    /// Logs statistics of the propagator using the provided [`StatisticLogger`].
209    ///
210    /// It is recommended to create a struct through the [`create_statistics_struct!`] macro!
211    fn log_statistics(&self, _statistic_logger: StatisticLogger) {}
212}
213
214/// Indicator of what to do when a propagator is notified.
215#[derive(Clone, Copy, Debug, PartialEq, Eq)]
216pub enum EnqueueDecision {
217    /// The propagator should be enqueued.
218    Enqueue,
219    /// The propagator should not be enqueued.
220    Skip,
221}
222
223/// The priority of a propagator, used for determining the order in which propagators will be
224/// called.
225///
226/// Propagators with high priority are propagated before propagators with low(er) priority. If two
227/// propagators have the same priority, then the order in which they are propagated is unspecified.
228///
229/// Typically, propagators with low computational complexity should be assigned a high
230/// priority (i.e., should be propagated before computationally expensive propagators).
231#[derive(Default, Debug, Clone, Copy, Hash, PartialEq, Eq)]
232#[repr(u8)]
233pub enum Priority {
234    High = 0,
235    Medium = 1,
236    Low = 2,
237    #[default]
238    VeryLow = 3,
239}
240
241impl PartialOrd for Priority {
242    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
243        ((*self) as u8).partial_cmp(&((*other) as u8))
244    }
245}