diff --git a/pumpkin-crates/core/src/containers/keyed_vec.rs b/pumpkin-crates/core/src/containers/keyed_vec.rs index b797a13f6..84c34122b 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() } @@ -117,6 +121,12 @@ impl KeyedVec { } impl KeyedVec { + pub(crate) fn accomodate(&mut self, key: Key, default_value: 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) { 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..37b9ec645 100644 --- a/pumpkin-crates/core/src/engine/cp/propagation/constructor.rs +++ b/pumpkin-crates/core/src/engine/cp/propagation/constructor.rs @@ -6,11 +6,13 @@ 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; 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 +93,15 @@ impl PropagatorConstructorContext<'_> { var.watch_all(&mut watchers, domain_events.get_int_events()); } + /// 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) -> PredicateId { + 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/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. /// diff --git a/pumpkin-crates/core/src/engine/notifications/mod.rs b/pumpkin-crates/core/src/engine/notifications/mod.rs index 3a851481e..533aa85d3 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(), @@ -134,6 +138,20 @@ impl NotificationEngine { } } + 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( &mut self, domain: DomainId, @@ -292,14 +310,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); - // At the moment this does nothing yet, but we call it to drain predicates. - self.notify_predicate_id_falsified(); + self.notify_predicate_id_satisfied(nogood_propagator_handle, propagators); self.last_notified_trail_index = assignments.num_trail_entries(); } @@ -334,19 +345,23 @@ 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) { + 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); + 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); + } + } + + propagators[nogood_propagator_handle.propagator_id()] + .notify_predicate_id_satisfied(predicate_id); } } @@ -480,14 +495,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); - // At the moment this does nothing yet, but we call it to drain predicates. - self.notify_predicate_id_falsified(); + self.notify_predicate_id_satisfied(handle, propagators); } 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..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 @@ -68,12 +63,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 + '_ { @@ -104,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) @@ -179,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) 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 + '_ {