From 7bdeaa62d8321940b4e35fc496b3fa989eabe11b Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Thu, 11 Dec 2025 19:20:06 +0100 Subject: [PATCH 1/8] refactor(pumpkin-core): Do not notify falsified predicates --- pumpkin-crates/core/src/engine/notifications/mod.rs | 13 ------------- .../predicate_notification/predicate_assignments.rs | 6 ------ .../predicate_notification/predicate_notifier.rs | 6 ------ 3 files changed, 25 deletions(-) diff --git a/pumpkin-crates/core/src/engine/notifications/mod.rs b/pumpkin-crates/core/src/engine/notifications/mod.rs index 3a851481e..b21216bf2 100644 --- a/pumpkin-crates/core/src/engine/notifications/mod.rs +++ b/pumpkin-crates/core/src/engine/notifications/mod.rs @@ -298,8 +298,6 @@ impl NotificationEngine { .get_propagator_mut(nogood_propagator_handle) .expect("nogood propagator handle refers to a nogood propagator"); self.notify_predicate_id_satisfied(nogood_propagator); - // At the moment this does nothing yet, but we call it to drain predicates. - self.notify_predicate_id_falsified(); self.last_notified_trail_index = assignments.num_trail_entries(); } @@ -334,15 +332,6 @@ impl NotificationEngine { true } - /// Notifies propagators that certain [`Predicate`]s have been falsified. - /// - /// Currently, no propagators are informed of this information. - fn notify_predicate_id_falsified(&mut self) { - for _predicate_id in self.predicate_notifier.drain_falsified_predicates() { - // At the moment this does nothing - } - } - /// Notifies the propagator that certain [`Predicate`]s have been satisfied. fn notify_predicate_id_satisfied(&mut self, propagator: &mut dyn Propagator) { for predicate_id in self.predicate_notifier.drain_satisfied_predicates() { @@ -486,8 +475,6 @@ impl NotificationEngine { .get_propagator_mut(handle) .expect("nogood propagator handle refers to a nogood propagator"); self.notify_predicate_id_satisfied(nogood_propagator); - // At the moment this does nothing yet, but we call it to drain predicates. - self.notify_predicate_id_falsified(); } self.last_notified_trail_index = assignments.num_trail_entries(); diff --git a/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_assignments.rs b/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_assignments.rs index b79e1f049..9274f597b 100644 --- a/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_assignments.rs +++ b/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_assignments.rs @@ -68,12 +68,6 @@ impl PredicateIdAssignments { self.predicate_values.keys() } - /// Returns the falsified predicates; note that this structure will be cleared once it is - /// dropped. - pub(crate) fn drain_falsified_predicates(&mut self) -> impl Iterator + '_ { - self.falsified_predicates.drain(..) - } - /// Returns the satisfied predicates; note that this structure will be cleared once it is /// dropped. pub(crate) fn drain_satisfied_predicates(&mut self) -> impl Iterator + '_ { diff --git a/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_notifier.rs b/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_notifier.rs index d695c472c..6fa6b29ca 100644 --- a/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_notifier.rs +++ b/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_notifier.rs @@ -46,12 +46,6 @@ impl PredicateNotifier { .debug_create_from_assignments(assignments, &mut self.predicate_to_id); } - /// Returns the falsified predicates; note that this structure will be cleared once it is - /// dropped. - pub(crate) fn drain_falsified_predicates(&mut self) -> impl Iterator + '_ { - self.predicate_id_assignments.drain_falsified_predicates() - } - /// Returns the satisfied predicates; note that this structure will be cleared once it is /// dropped. pub(crate) fn drain_satisfied_predicates(&mut self) -> impl Iterator + '_ { From caf252ebf1b63fc7988cc9320eb5d12c6825d5f6 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Thu, 11 Dec 2025 19:29:39 +0100 Subject: [PATCH 2/8] fix(pumpkin-core): Notify all registered propagators on predicate events --- .../core/src/engine/notifications/mod.rs | 35 +++++++++++-------- 1 file changed, 20 insertions(+), 15 deletions(-) diff --git a/pumpkin-crates/core/src/engine/notifications/mod.rs b/pumpkin-crates/core/src/engine/notifications/mod.rs index b21216bf2..02f5f5ac6 100644 --- a/pumpkin-crates/core/src/engine/notifications/mod.rs +++ b/pumpkin-crates/core/src/engine/notifications/mod.rs @@ -14,12 +14,12 @@ pub(crate) use predicate_notification::PredicateNotifier; use super::propagation::PropagationContext; use super::propagation::PropagatorVarId; use crate::basic_types::PredicateId; +use crate::containers::KeyedVec; use crate::engine::Assignments; use crate::engine::PropagatorQueue; use crate::engine::TrailedValues; use crate::engine::propagation::EnqueueDecision; use crate::engine::propagation::LocalId; -use crate::engine::propagation::Propagator; use crate::engine::propagation::PropagatorId; use crate::engine::propagation::contexts::PropagationContextWithTrailedValues; use crate::engine::propagation::store::PropagatorStore; @@ -39,6 +39,8 @@ pub(crate) struct NotificationEngine { /// Contains information on which propagator to notify upon /// integer events, e.g., lower or upper bound change of a variable. watch_list_domain_events: WatchListDomainEvents, + /// The watch list from predicates to propagators. + watch_list_predicate_id: KeyedVec>, /// Events which have occurred since the last round of notifications have taken place events: EventSink, /// Backtrack events which have occurred since the last of backtrack notifications have taken @@ -51,6 +53,7 @@ impl Default for NotificationEngine { fn default() -> Self { let mut result = Self { watch_list_domain_events: Default::default(), + watch_list_predicate_id: Default::default(), predicate_notifier: Default::default(), last_notified_trail_index: 0, events: Default::default(), @@ -73,6 +76,7 @@ impl Default for NotificationEngine { let mut result = Self { watch_list_domain_events, + watch_list_predicate_id: Default::default(), predicate_notifier: Default::default(), last_notified_trail_index: usize::MAX, events: Default::default(), @@ -292,12 +296,7 @@ impl NotificationEngine { self.events = events; // Then we notify the propagators that a predicate has been satisfied. - // - // Currently, only the nogood propagator is notified. - let nogood_propagator = propagators - .get_propagator_mut(nogood_propagator_handle) - .expect("nogood propagator handle refers to a nogood propagator"); - self.notify_predicate_id_satisfied(nogood_propagator); + self.notify_predicate_id_satisfied(nogood_propagator_handle, propagators); self.last_notified_trail_index = assignments.num_trail_entries(); } @@ -333,9 +332,20 @@ impl NotificationEngine { } /// Notifies the propagator that certain [`Predicate`]s have been satisfied. - fn notify_predicate_id_satisfied(&mut self, propagator: &mut dyn Propagator) { + fn notify_predicate_id_satisfied( + &mut self, + nogood_propagator_handle: PropagatorHandle, + propagators: &mut PropagatorStore, + ) { for predicate_id in self.predicate_notifier.drain_satisfied_predicates() { - propagator.notify_predicate_id_satisfied(predicate_id); + let propagators_to_notify = self.watch_list_predicate_id[predicate_id] + .iter() + .copied() + .chain(std::iter::once(nogood_propagator_handle.propagator_id())); + + for propagator_id in propagators_to_notify { + propagators[propagator_id].notify_predicate_id_satisfied(predicate_id); + } } } @@ -469,12 +479,7 @@ impl NotificationEngine { if let Some(handle) = nogood_propagator_handle { // Then we notify the propagators that a predicate has been satisfied. - // - // Currently, only the nogood propagator is notified. - let nogood_propagator = propagators - .get_propagator_mut(handle) - .expect("nogood propagator handle refers to a nogood propagator"); - self.notify_predicate_id_satisfied(nogood_propagator); + self.notify_predicate_id_satisfied(handle, propagators); } self.last_notified_trail_index = assignments.num_trail_entries(); From 524b5c1fe9ccb318983c2b6cd26a63ec2d0d27f1 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Thu, 11 Dec 2025 19:34:32 +0100 Subject: [PATCH 3/8] fix(pumpkin-core): Implement API for propagators to register predicates --- pumpkin-crates/core/src/containers/keyed_vec.rs | 4 ++++ .../core/src/engine/cp/propagation/constructor.rs | 9 +++++++++ pumpkin-crates/core/src/engine/notifications/mod.rs | 8 ++++++++ 3 files changed, 21 insertions(+) diff --git a/pumpkin-crates/core/src/containers/keyed_vec.rs b/pumpkin-crates/core/src/containers/keyed_vec.rs index b797a13f6..75d9a516f 100644 --- a/pumpkin-crates/core/src/containers/keyed_vec.rs +++ b/pumpkin-crates/core/src/containers/keyed_vec.rs @@ -117,6 +117,10 @@ impl KeyedVec { } impl KeyedVec { + pub(crate) fn accomodate(&mut self, key: Key, default_value: Value) { + self.elements.resize(key.index() + 1, default_value) + } + pub(crate) fn resize(&mut self, new_len: usize, value: Value) { self.elements.resize(new_len, value) } diff --git a/pumpkin-crates/core/src/engine/cp/propagation/constructor.rs b/pumpkin-crates/core/src/engine/cp/propagation/constructor.rs index bec94353b..9a79644a8 100644 --- a/pumpkin-crates/core/src/engine/cp/propagation/constructor.rs +++ b/pumpkin-crates/core/src/engine/cp/propagation/constructor.rs @@ -11,6 +11,7 @@ use crate::engine::DomainEvents; use crate::engine::State; use crate::engine::TrailedValues; use crate::engine::notifications::Watchers; +use crate::predicates::Predicate; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; use crate::proof::InferenceLabel; @@ -91,6 +92,14 @@ impl PropagatorConstructorContext<'_> { var.watch_all(&mut watchers, domain_events.get_int_events()); } + /// Register the propagator to be enqueued when the given [`Predicate`] becomes true. + #[allow(unused, reason = "will become public API")] + pub(crate) fn register_predicate(&mut self, predicate: Predicate) { + self.state + .notification_engine + .watch_predicate(predicate, self.propagator_id); + } + /// Subscribes the propagator to the given [`DomainEvents`] when they are undone during /// backtracking. This method is complementary to [`PropagatorConstructorContext::register`], /// the [`LocalId`]s provided to both of these method should be the same for the same variable. diff --git a/pumpkin-crates/core/src/engine/notifications/mod.rs b/pumpkin-crates/core/src/engine/notifications/mod.rs index 02f5f5ac6..85449ddb8 100644 --- a/pumpkin-crates/core/src/engine/notifications/mod.rs +++ b/pumpkin-crates/core/src/engine/notifications/mod.rs @@ -138,6 +138,14 @@ impl NotificationEngine { } } + pub(crate) fn watch_predicate(&mut self, predicate: Predicate, propagator_id: PropagatorId) { + let predicate_id = self.get_id(predicate); + + self.watch_list_predicate_id + .accomodate(predicate_id, vec![]); + self.watch_list_predicate_id[predicate_id].push(propagator_id); + } + pub(crate) fn watch_all_backtrack( &mut self, domain: DomainId, From e2b1f857332e6d9220b7b5e54527cc226ffeb29c Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Fri, 12 Dec 2025 10:06:20 +0100 Subject: [PATCH 4/8] refactor(pumpkin-core): Remove `falsified_predicates` from predicate ID assignments --- .../predicate_notification/predicate_assignments.rs | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_assignments.rs b/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_assignments.rs index 9274f597b..1cedb0fcb 100644 --- a/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_assignments.rs +++ b/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_assignments.rs @@ -24,11 +24,6 @@ pub(crate) struct PredicateIdAssignments { trail: Trail, /// The known value for each [`Predicate`] (represented by a [`PredicateId`]). predicate_values: KeyedVec, - /// The [`Predicate`]s which are currently known to be falsified used for notification. - /// - /// Note that this structure does not contain _all_ of the falsified [`Predicate`]s but rather - /// the one which have been falsified since the last round of notifications. - falsified_predicates: Vec, /// The [`Predicate`]s which are currently known to be satisfied used for notification. /// /// Note that this structure does not contain _all_ of the satisfied [`Predicate`]s but rather @@ -98,10 +93,8 @@ impl PredicateIdAssignments { if self.predicate_values[predicate_id] != value { // If it is not the same as what is already in the cache then we need to store it and // (potentially) update the predicates which should be notified - match value { - PredicateValue::AssignedTrue => self.satisfied_predicates.push(predicate_id), - PredicateValue::AssignedFalse => self.falsified_predicates.push(predicate_id), - _ => {} + if value == PredicateValue::AssignedTrue { + self.satisfied_predicates.push(predicate_id) } self.predicate_values[predicate_id] = value; self.trail.push(predicate_id) @@ -173,7 +166,6 @@ impl PredicateIdAssignments { // We also need to clear the stored updated predicates; if this is not done, then it can be // the case that a predicate is erroneously said to be satisfied/falsified while it is not self.satisfied_predicates.clear(); - self.falsified_predicates.clear(); self.trail .synchronise(new_checkpoint) From 00ae91dfee0aa05a7ce899d23498d8026517cc38 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Fri, 12 Dec 2025 10:10:33 +0100 Subject: [PATCH 5/8] fix(pumpkin-core): Check if a predicate ID is watched at all --- pumpkin-crates/core/src/containers/keyed_vec.rs | 4 ++++ .../core/src/engine/notifications/mod.rs | 14 ++++++++------ 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/pumpkin-crates/core/src/containers/keyed_vec.rs b/pumpkin-crates/core/src/containers/keyed_vec.rs index 75d9a516f..31ce60c94 100644 --- a/pumpkin-crates/core/src/containers/keyed_vec.rs +++ b/pumpkin-crates/core/src/containers/keyed_vec.rs @@ -42,6 +42,10 @@ impl KeyedVec { } impl KeyedVec { + pub(crate) fn get(&self, key: Key) -> Option<&Value> { + self.elements.get(key.index()) + } + pub(crate) fn len(&self) -> usize { self.elements.len() } diff --git a/pumpkin-crates/core/src/engine/notifications/mod.rs b/pumpkin-crates/core/src/engine/notifications/mod.rs index 85449ddb8..5b886af76 100644 --- a/pumpkin-crates/core/src/engine/notifications/mod.rs +++ b/pumpkin-crates/core/src/engine/notifications/mod.rs @@ -346,14 +346,16 @@ impl NotificationEngine { propagators: &mut PropagatorStore, ) { for predicate_id in self.predicate_notifier.drain_satisfied_predicates() { - let propagators_to_notify = self.watch_list_predicate_id[predicate_id] - .iter() - .copied() - .chain(std::iter::once(nogood_propagator_handle.propagator_id())); + if let Some(watch_list) = self.watch_list_predicate_id.get(predicate_id) { + let propagators_to_notify = watch_list.iter().copied(); - for propagator_id in propagators_to_notify { - propagators[propagator_id].notify_predicate_id_satisfied(predicate_id); + for propagator_id in propagators_to_notify { + propagators[propagator_id].notify_predicate_id_satisfied(predicate_id); + } } + + propagators[nogood_propagator_handle.propagator_id()] + .notify_predicate_id_satisfied(predicate_id); } } From 88ed25549693e86fe9b57772efc7b31d2d899a16 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Fri, 12 Dec 2025 10:13:57 +0100 Subject: [PATCH 6/8] fix(pumpkin-core): Fix KeyedVec::accomodate to not truncate --- pumpkin-crates/core/src/containers/keyed_vec.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/pumpkin-crates/core/src/containers/keyed_vec.rs b/pumpkin-crates/core/src/containers/keyed_vec.rs index 31ce60c94..84c34122b 100644 --- a/pumpkin-crates/core/src/containers/keyed_vec.rs +++ b/pumpkin-crates/core/src/containers/keyed_vec.rs @@ -122,7 +122,9 @@ impl KeyedVec { impl KeyedVec { pub(crate) fn accomodate(&mut self, key: Key, default_value: Value) { - self.elements.resize(key.index() + 1, default_value) + if key.index() >= self.elements.len() { + self.elements.resize(key.index() + 1, default_value) + } } pub(crate) fn resize(&mut self, new_len: usize, value: Value) { From 8424640e8f7462a7c6b8808ca5a2d11b3e7cb739 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Fri, 12 Dec 2025 10:15:13 +0100 Subject: [PATCH 7/8] fix(pumpkin-core): Remove unused propagator hook --- pumpkin-crates/core/src/engine/cp/propagation/propagator.rs | 6 ------ 1 file changed, 6 deletions(-) diff --git a/pumpkin-crates/core/src/engine/cp/propagation/propagator.rs b/pumpkin-crates/core/src/engine/cp/propagation/propagator.rs index 1e0d584ae..e7b6373bc 100644 --- a/pumpkin-crates/core/src/engine/cp/propagation/propagator.rs +++ b/pumpkin-crates/core/src/engine/cp/propagation/propagator.rs @@ -128,12 +128,6 @@ pub(crate) trait Propagator: Downcast + DynClone { /// By default, the propagator does nothing when this method is called. fn notify_predicate_id_satisfied(&mut self, _predicate_id: PredicateId) {} - /// Called when a [`PredicateId`] has been falsified. - /// - /// By default, the propagator does nothing when this method is called. - #[allow(dead_code, reason = "Will be part of the public API")] - fn notify_predicate_id_falsified(&mut self, _predicate_id: PredicateId) {} - /// Called each time the [`ConstraintSatisfactionSolver`] backtracks, the propagator can then /// update its internal data structures given the new variable domains. /// From 3342ff8a6003fe298aed43ae0543abebf16cbc36 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Fri, 12 Dec 2025 10:17:18 +0100 Subject: [PATCH 8/8] fix(pumpkin-core): Return PredicateId when registering predicate in constructor --- .../core/src/engine/cp/propagation/constructor.rs | 6 ++++-- pumpkin-crates/core/src/engine/notifications/mod.rs | 8 +++++++- 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/pumpkin-crates/core/src/engine/cp/propagation/constructor.rs b/pumpkin-crates/core/src/engine/cp/propagation/constructor.rs index 9a79644a8..37b9ec645 100644 --- a/pumpkin-crates/core/src/engine/cp/propagation/constructor.rs +++ b/pumpkin-crates/core/src/engine/cp/propagation/constructor.rs @@ -6,6 +6,7 @@ use super::PropagationContext; use super::Propagator; use super::PropagatorId; use super::PropagatorVarId; +use crate::basic_types::PredicateId; use crate::engine::Assignments; use crate::engine::DomainEvents; use crate::engine::State; @@ -93,11 +94,12 @@ impl PropagatorConstructorContext<'_> { } /// Register the propagator to be enqueued when the given [`Predicate`] becomes true. + /// Returns the [`PredicateId`] used by the solver to track the predicate. #[allow(unused, reason = "will become public API")] - pub(crate) fn register_predicate(&mut self, predicate: Predicate) { + pub(crate) fn register_predicate(&mut self, predicate: Predicate) -> PredicateId { self.state .notification_engine - .watch_predicate(predicate, self.propagator_id); + .watch_predicate(predicate, self.propagator_id) } /// Subscribes the propagator to the given [`DomainEvents`] when they are undone during diff --git a/pumpkin-crates/core/src/engine/notifications/mod.rs b/pumpkin-crates/core/src/engine/notifications/mod.rs index 5b886af76..533aa85d3 100644 --- a/pumpkin-crates/core/src/engine/notifications/mod.rs +++ b/pumpkin-crates/core/src/engine/notifications/mod.rs @@ -138,12 +138,18 @@ impl NotificationEngine { } } - pub(crate) fn watch_predicate(&mut self, predicate: Predicate, propagator_id: PropagatorId) { + pub(crate) fn watch_predicate( + &mut self, + predicate: Predicate, + propagator_id: PropagatorId, + ) -> PredicateId { let predicate_id = self.get_id(predicate); self.watch_list_predicate_id .accomodate(predicate_id, vec![]); self.watch_list_predicate_id[predicate_id].push(propagator_id); + + predicate_id } pub(crate) fn watch_all_backtrack(