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}