fix(pumpkin-core): Allow propagators to register for predicates becoming true (#331)

Predicate notification only happened for the `NogoodPropagator`. Now
that we are moving toward a more flexible API, we need arbitrary
propagators to be able to register for predicates becoming true.

This patch does _not_ remove the special status of the
`NogoodPropagator`, it merely enables other propagators to register for
specific events.

Author: maartenflippo

pumpkin-crates/core/src/containers/keyed_vec.rs

@@ -42,6 +42,10 @@ impl<Key, Value> KeyedVec<Key, Value> {
 }
 
 impl<Key: StorageKey, Value> KeyedVec<Key, Value> {
+    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<Key: StorageKey, Value> KeyedVec<Key, Value> {
 }
 
 impl<Key: StorageKey, Value: Clone> KeyedVec<Key, Value> {
+    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)
     }

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.

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.
     ///

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<PredicateId, Vec<PropagatorId>>,
     /// 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<NogoodPropagator>,
+        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();

pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_assignments.rs

@@ -24,11 +24,6 @@ pub(crate) struct PredicateIdAssignments {
     trail: Trail<PredicateId>,
     /// The known value for each [`Predicate`] (represented by a [`PredicateId`]).
     predicate_values: KeyedVec<PredicateId, PredicateValue>,
-    /// 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<PredicateId>,
     /// 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<Item = PredicateId> + '_ {
-        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<Item = PredicateId> + '_ {
@@ -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)

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<Item = PredicateId> + '_ {
-        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<Item = PredicateId> + '_ {