diff --git a/pumpkin-crates/core/src/basic_types/mod.rs b/pumpkin-crates/core/src/basic_types/mod.rs index b87c9a856..b1fd78c9c 100644 --- a/pumpkin-crates/core/src/basic_types/mod.rs +++ b/pumpkin-crates/core/src/basic_types/mod.rs @@ -4,7 +4,6 @@ mod function; mod predicate_id_generators; mod propositional_conjunction; mod random; -mod ref_or_owned; pub(crate) mod sequence_generators; mod solution; mod stored_conflict_info; @@ -19,7 +18,6 @@ pub use predicate_id_generators::PredicateId; pub use predicate_id_generators::PredicateIdGenerator; pub use propositional_conjunction::PropositionalConjunction; pub use random::*; -pub(crate) use ref_or_owned::*; pub use solution::ProblemSolution; pub use solution::Solution; pub use solution::SolutionReference; diff --git a/pumpkin-crates/core/src/basic_types/ref_or_owned.rs b/pumpkin-crates/core/src/basic_types/ref_or_owned.rs deleted file mode 100644 index f16f3d6c1..000000000 --- a/pumpkin-crates/core/src/basic_types/ref_or_owned.rs +++ /dev/null @@ -1,49 +0,0 @@ -use std::ops::Deref; -use std::ops::DerefMut; - -/// Either owns a value or has a mutable reference to a value. -/// -/// Used to store data in a reborrowed context that needs to be 'shared' with the original context -/// that was reborrowed from. For example, when dropping a reborrowed context, we want -/// [`PropagatorConstructorContext::get_next_local_id`] in the original context to 'know' about the -/// registered local ids in the reborrowed context. -#[derive(Debug)] -pub(crate) enum RefOrOwned<'a, T> { - Ref(&'a mut T), - Owned(T), -} - -impl RefOrOwned<'_, T> { - pub(crate) fn reborrow(&mut self) -> RefOrOwned<'_, T> { - match self { - RefOrOwned::Ref(ref_to_t) => RefOrOwned::Ref(ref_to_t), - RefOrOwned::Owned(value) => RefOrOwned::Ref(value), - } - } -} - -impl From for RefOrOwned<'_, T> { - fn from(value: T) -> Self { - RefOrOwned::Owned(value) - } -} - -impl Deref for RefOrOwned<'_, T> { - type Target = T; - - fn deref(&self) -> &Self::Target { - match self { - RefOrOwned::Ref(reference) => reference, - RefOrOwned::Owned(value) => value, - } - } -} - -impl DerefMut for RefOrOwned<'_, T> { - fn deref_mut(&mut self) -> &mut Self::Target { - match self { - RefOrOwned::Ref(reference) => reference, - RefOrOwned::Owned(value) => value, - } - } -} diff --git a/pumpkin-crates/core/src/engine/notifications/domain_event_notification/domain_event_watch_list.rs b/pumpkin-crates/core/src/engine/notifications/domain_event_notification/domain_event_watch_list.rs index 9d3220c2c..6646aecad 100644 --- a/pumpkin-crates/core/src/engine/notifications/domain_event_notification/domain_event_watch_list.rs +++ b/pumpkin-crates/core/src/engine/notifications/domain_event_notification/domain_event_watch_list.rs @@ -102,11 +102,6 @@ impl<'a> Watchers<'a> { } } - pub(crate) fn watch_all(&mut self, domain: DomainId, events: EnumSet) { - self.notification_engine - .watch_all(domain, events, self.propagator_var); - } - pub(crate) fn unwatch_all(&mut self, domain: DomainId) { self.notification_engine .unwatch_all(domain, self.propagator_var); diff --git a/pumpkin-crates/core/src/engine/notifications/mod.rs b/pumpkin-crates/core/src/engine/notifications/mod.rs index aca902f7c..335888bf4 100644 --- a/pumpkin-crates/core/src/engine/notifications/mod.rs +++ b/pumpkin-crates/core/src/engine/notifications/mod.rs @@ -109,7 +109,7 @@ impl NotificationEngine { self.predicate_notifier.get_predicate(predicate_id) } - pub(crate) fn watch_all( + pub(crate) fn register( &mut self, domain: DomainId, events: EnumSet, diff --git a/pumpkin-crates/core/src/engine/state.rs b/pumpkin-crates/core/src/engine/state.rs index 9e358fab6..177897111 100644 --- a/pumpkin-crates/core/src/engine/state.rs +++ b/pumpkin-crates/core/src/engine/state.rs @@ -36,6 +36,7 @@ use crate::propagation::Propagator; use crate::propagation::PropagatorConstructor; use crate::propagation::PropagatorConstructorContext; use crate::propagation::PropagatorId; +use crate::propagation::PropagatorVarId; use crate::propagation::store::PropagatorStore; use crate::pumpkin_assert_advanced; use crate::pumpkin_assert_eq_simple; @@ -341,7 +342,17 @@ impl State { let constructor_context = PropagatorConstructorContext::new(original_handle.propagator_id(), self); - let propagator = constructor.create(constructor_context); + let (registration, propagator) = constructor.create(constructor_context); + + for (domain_id, events, local_id) in registration.iter() { + let propagator_var = PropagatorVarId { + propagator: original_handle.propagator_id(), + variable: local_id, + }; + + self.notification_engine + .register(domain_id, events, propagator_var); + } pumpkin_assert_simple!( propagator.priority() as u8 <= 3, diff --git a/pumpkin-crates/core/src/engine/variables/affine_view.rs b/pumpkin-crates/core/src/engine/variables/affine_view.rs index 3ce96acfb..9142f0ba5 100644 --- a/pumpkin-crates/core/src/engine/variables/affine_view.rs +++ b/pumpkin-crates/core/src/engine/variables/affine_view.rs @@ -14,6 +14,9 @@ use crate::engine::predicates::predicate_constructor::PredicateConstructor; use crate::engine::variables::DomainId; use crate::engine::variables::IntegerVariable; use crate::math::num_ext::NumExt; +use crate::propagation::EventDispatcher; +use crate::propagation::EventTarget; +use crate::propagation::LocalId; /// Models the constraint `y = ax + b`, by expressing the domain of `y` as a transformation of the /// domain of `x`. @@ -54,6 +57,22 @@ impl AffineView { } } +impl EventTarget for AffineView { + fn register( + &self, + registration: &mut impl EventDispatcher, + mut events: EnumSet, + local_id: LocalId, + ) { + let bound = DomainEvent::LowerBound | DomainEvent::UpperBound; + let intersection = events.intersection(bound); + if intersection.len() == 1 && self.scale.is_negative() { + events = events.symmetric_difference(bound); + } + self.inner.register(registration, events, local_id); + } +} + impl CheckerVariable for AffineView { fn does_atomic_constrain_self(&self, atomic: &Predicate) -> bool { self.inner.does_atomic_constrain_self(atomic) @@ -265,15 +284,6 @@ where .map(|value| self.map(value)) } - fn watch_all(&self, watchers: &mut Watchers<'_>, mut events: EnumSet) { - let bound = DomainEvent::LowerBound | DomainEvent::UpperBound; - let intersection = events.intersection(bound); - if intersection.len() == 1 && self.scale.is_negative() { - events = events.symmetric_difference(bound); - } - self.inner.watch_all(watchers, events); - } - fn unwatch_all(&self, watchers: &mut Watchers<'_>) { self.inner.unwatch_all(watchers); } diff --git a/pumpkin-crates/core/src/engine/variables/constant.rs b/pumpkin-crates/core/src/engine/variables/constant.rs index 486ea28ab..af328ba3b 100644 --- a/pumpkin-crates/core/src/engine/variables/constant.rs +++ b/pumpkin-crates/core/src/engine/variables/constant.rs @@ -1,12 +1,21 @@ +use enumset::EnumSet; use pumpkin_checking::CheckerVariable; use pumpkin_checking::IntExt; use crate::engine::Assignments; use crate::predicates::Predicate; use crate::predicates::PredicateConstructor; +use crate::propagation::DomainEvent; +use crate::propagation::EventDispatcher; +use crate::propagation::EventTarget; +use crate::propagation::LocalId; use crate::variables::IntegerVariable; use crate::variables::TransformableVariable; +impl EventTarget for i32 { + fn register(&self, _: &mut impl EventDispatcher, _: EnumSet, _: LocalId) {} +} + impl IntegerVariable for i32 { type AffineView = i32; @@ -51,26 +60,16 @@ impl IntegerVariable for i32 { std::iter::once(*self) } - fn watch_all( - &self, - _watchers: &mut crate::engine::notifications::Watchers<'_>, - _events: enumset::EnumSet, - ) { - } - fn unwatch_all(&self, _watchers: &mut crate::engine::notifications::Watchers<'_>) {} fn watch_all_backtrack( &self, _watchers: &mut crate::engine::notifications::Watchers<'_>, - _events: enumset::EnumSet, + _events: EnumSet, ) { } - fn unpack_event( - &self, - _event: crate::propagation::OpaqueDomainEvent, - ) -> crate::propagation::DomainEvent { + fn unpack_event(&self, _event: crate::propagation::OpaqueDomainEvent) -> DomainEvent { unreachable!() } diff --git a/pumpkin-crates/core/src/engine/variables/domain_id.rs b/pumpkin-crates/core/src/engine/variables/domain_id.rs index 22ede3a40..0d1c42b62 100644 --- a/pumpkin-crates/core/src/engine/variables/domain_id.rs +++ b/pumpkin-crates/core/src/engine/variables/domain_id.rs @@ -12,6 +12,9 @@ use crate::engine::variables::IntegerVariable; use crate::predicates::Predicate; use crate::predicates::PredicateConstructor; use crate::predicates::PredicateType; +use crate::propagation::EventDispatcher; +use crate::propagation::EventTarget; +use crate::propagation::LocalId; use crate::pumpkin_assert_simple; /// A structure which represents the most basic [`IntegerVariable`]; it is simply the id which links @@ -32,6 +35,17 @@ impl DomainId { } } +impl EventTarget for DomainId { + fn register( + &self, + registration: &mut impl EventDispatcher, + events: EnumSet, + local_id: LocalId, + ) { + registration.register(*self, events, local_id); + } +} + impl CheckerVariable for DomainId { fn does_atomic_constrain_self(&self, atomic: &Predicate) -> bool { atomic.get_domain() == *self @@ -155,10 +169,6 @@ impl IntegerVariable for DomainId { assignment.get_domain_iterator(*self) } - fn watch_all(&self, watchers: &mut Watchers<'_>, events: EnumSet) { - watchers.watch_all(*self, events); - } - fn unwatch_all(&self, watchers: &mut Watchers<'_>) { watchers.unwatch_all(*self); } diff --git a/pumpkin-crates/core/src/engine/variables/integer_variable.rs b/pumpkin-crates/core/src/engine/variables/integer_variable.rs index 09badb92e..34083bbd5 100644 --- a/pumpkin-crates/core/src/engine/variables/integer_variable.rs +++ b/pumpkin-crates/core/src/engine/variables/integer_variable.rs @@ -10,6 +10,7 @@ use crate::engine::notifications::OpaqueDomainEvent; use crate::engine::notifications::Watchers; use crate::engine::predicates::predicate_constructor::PredicateConstructor; use crate::predicates::Predicate; +use crate::propagation::EventTarget; /// A trait specifying the required behaviour of an integer variable such as retrieving a /// lower-bound ([`IntegerVariable::lower_bound`]). @@ -19,6 +20,7 @@ pub trait IntegerVariable: + TransformableVariable + Debug + CheckerVariable + + EventTarget { type AffineView: IntegerVariable; @@ -50,9 +52,6 @@ pub trait IntegerVariable: /// Iterate over the values of the domain. fn iterate_domain(&self, assignment: &Assignments) -> impl Iterator; - /// Register a watch for this variable on the given domain events. - fn watch_all(&self, watchers: &mut Watchers<'_>, events: EnumSet); - /// Remove the watcher on this variable. fn unwatch_all(&self, watchers: &mut Watchers<'_>); diff --git a/pumpkin-crates/core/src/engine/variables/literal.rs b/pumpkin-crates/core/src/engine/variables/literal.rs index 980ffa737..3b358031f 100644 --- a/pumpkin-crates/core/src/engine/variables/literal.rs +++ b/pumpkin-crates/core/src/engine/variables/literal.rs @@ -15,6 +15,9 @@ use crate::engine::notifications::Watchers; use crate::engine::predicates::predicate::Predicate; use crate::engine::predicates::predicate_constructor::PredicateConstructor; use crate::engine::variables::AffineView; +use crate::propagation::EventDispatcher; +use crate::propagation::EventTarget; +use crate::propagation::LocalId; #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub struct Literal { @@ -73,6 +76,18 @@ macro_rules! forward { } } +impl EventTarget for Literal { + fn register( + &self, + registration: &mut impl EventDispatcher, + events: EnumSet, + local_id: LocalId, + ) { + self.integer_variable + .register(registration, events, local_id); + } +} + impl CheckerVariable for Literal { forward!(integer_variable, fn does_atomic_constrain_self(&self, atomic: &Predicate) -> bool); forward!(integer_variable, fn atomic_less_than(&self, value: i32) -> Predicate); @@ -164,10 +179,6 @@ impl IntegerVariable for Literal { self.integer_variable.iterate_domain(assignment) } - fn watch_all(&self, watchers: &mut Watchers<'_>, events: EnumSet) { - self.integer_variable.watch_all(watchers, events) - } - fn unwatch_all(&self, watchers: &mut Watchers<'_>) { self.integer_variable.unwatch_all(watchers) } diff --git a/pumpkin-crates/core/src/propagation/constructor.rs b/pumpkin-crates/core/src/propagation/constructor.rs index 791627880..6aa22776b 100644 --- a/pumpkin-crates/core/src/propagation/constructor.rs +++ b/pumpkin-crates/core/src/propagation/constructor.rs @@ -1,6 +1,3 @@ -use std::ops::Deref; -use std::ops::DerefMut; - use pumpkin_checking::InferenceChecker; use super::Domains; @@ -11,7 +8,6 @@ use super::PropagatorVarId; #[cfg(doc)] use crate::Solver; use crate::basic_types::PredicateId; -use crate::basic_types::RefOrOwned; use crate::engine::Assignments; use crate::engine::State; use crate::engine::TrailedValues; @@ -25,6 +21,7 @@ use crate::proof::InferenceCode; #[cfg(doc)] use crate::propagation::DomainEvent; use crate::propagation::DomainEvents; +use crate::propagation::EventsToRegister; use crate::propagators::reified_propagator::ReifiedChecker; use crate::variables::IntegerVariable; use crate::variables::Literal; @@ -48,7 +45,13 @@ pub trait PropagatorConstructor { fn add_inference_checkers(&self, _checkers: InferenceCheckers<'_>) {} /// Create the propagator instance from `Self`. - fn create(self, context: PropagatorConstructorContext) -> Self::PropagatorImpl; + /// + /// Alongside the propagator instance, this returns the events for which the propagator should + /// be enqueued. + fn create( + self, + context: PropagatorConstructorContext, + ) -> (EventsToRegister, Self::PropagatorImpl); } /// Interface used to add [`InferenceChecker`]s to the [`State`]. @@ -101,15 +104,6 @@ impl InferenceCheckers<'_> { pub struct PropagatorConstructorContext<'a> { state: &'a mut State, pub(crate) propagator_id: PropagatorId, - - /// A [`LocalId`] that is guaranteed not to be used to register any variables yet. This is - /// either a reference or an owned value, to support - /// [`PropagatorConstructorContext::reborrow`]. - next_local_id: RefOrOwned<'a, LocalId>, - - /// Marker to indicate whether the constructor registered for at least one domain event or - /// predicate becoming assigned. If not, the [`Drop`] implementation will cause a panic. - did_register: RefOrOwned<'a, bool>, } impl PropagatorConstructorContext<'_> { @@ -118,61 +112,19 @@ impl PropagatorConstructorContext<'_> { state: &'a mut State, ) -> PropagatorConstructorContext<'a> { PropagatorConstructorContext { - next_local_id: RefOrOwned::Owned(LocalId::from(0)), propagator_id, state, - did_register: RefOrOwned::Owned(false), } } - /// Indicate that the constructor is deliberately not registering the propagator to be enqueued - /// at any time. - /// - /// If this is called and later a registration happens, then the registration will still go - /// through. Calling this function only prevents the crash if no registration happens. - pub fn will_not_register_any_events(&mut self) { - *self.did_register = true; - } - /// Get domain information. pub fn domains(&mut self) -> Domains<'_> { Domains::new(&self.state.assignments, &mut self.state.trailed_values) } - /// Subscribes the propagator to the given [`DomainEvents`]. - /// - /// The domain events determine when [`Propagator::notify()`] will be called on the propagator. - /// The [`LocalId`] is internal information related to the propagator, - /// which is used when calling [`Propagator::notify()`] to identify the variable. - /// - /// Each variable *must* have a unique [`LocalId`]. Most often this would be its index of the - /// variable in the internal array of variables. - /// - /// Duplicate registrations are ignored. - pub fn register( - &mut self, - var: impl IntegerVariable, - domain_events: DomainEvents, - local_id: LocalId, - ) { - self.will_not_register_any_events(); - - let propagator_var = PropagatorVarId { - propagator: self.propagator_id, - variable: local_id, - }; - - self.update_next_local_id(local_id); - - let mut watchers = Watchers::new(propagator_var, &mut self.state.notification_engine); - var.watch_all(&mut watchers, domain_events.events()); - } - /// Register the propagator to be enqueued when the given [`Predicate`] becomes true. /// Returns the [`PredicateId`] used by the solver to track the predicate. pub fn register_predicate(&mut self, predicate: Predicate) -> PredicateId { - self.will_not_register_any_events(); - self.state.notification_engine.watch_predicate( predicate, self.propagator_id, @@ -182,8 +134,7 @@ impl PropagatorConstructorContext<'_> { } /// 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. + /// backtracking. The [`LocalId`]s used to register the variable should be the same here. /// /// The domain events determine when [`Propagator::notify_backtrack()`] will be called on the /// propagator. The [`LocalId`] is internal information related to the propagator, @@ -205,25 +156,16 @@ impl PropagatorConstructorContext<'_> { variable: local_id, }; - self.update_next_local_id(local_id); - let mut watchers = Watchers::new(propagator_var, &mut self.state.notification_engine); var.watch_all_backtrack(&mut watchers, domain_events.events()); } - /// Get a new [`LocalId`] which is guaranteed to be unused. - pub(crate) fn get_next_local_id(&self) -> LocalId { - *self.next_local_id.deref() - } - /// Reborrow the current context to a new value with a shorter lifetime. Should be used when /// passing `Self` to another function that takes ownership, but the value is still needed /// afterwards. pub fn reborrow(&mut self) -> PropagatorConstructorContext<'_> { PropagatorConstructorContext { propagator_id: self.propagator_id, - next_local_id: self.next_local_id.reborrow(), - did_register: self.did_register.reborrow(), state: self.state, } } @@ -239,35 +181,6 @@ impl PropagatorConstructorContext<'_> { ) { self.state.add_inference_checker(inference_code, checker); } - - /// Set the next local id to be at least one more than the largest encountered local id. - fn update_next_local_id(&mut self, local_id: LocalId) { - let next_local_id = (*self.next_local_id.deref()).max(LocalId::from(local_id.unpack() + 1)); - - *self.next_local_id.deref_mut() = next_local_id; - } -} - -impl Drop for PropagatorConstructorContext<'_> { - fn drop(&mut self) { - if std::thread::panicking() { - // If we are already unwinding due to a panic, we do not want to trigger another one. - return; - } - - let did_register = match self.did_register { - // If we are in a reborrowed context, we do not want to enforce registration. - RefOrOwned::Ref(_) => return, - - RefOrOwned::Owned(did_register) => did_register, - }; - - if !did_register { - panic!( - "Propagator did not register to be enqueued. If this is intentional, call PropagatorConstructorContext::will_not_register_any_events()." - ); - } - } } mod private { @@ -288,55 +201,3 @@ mod private { } } } - -#[cfg(test)] -mod tests { - - use super::*; - use crate::variables::DomainId; - - #[test] - #[should_panic] - fn panic_when_no_registration_happened() { - let mut state = State::default(); - state.notification_engine.grow(); - - let _c1 = PropagatorConstructorContext::new(PropagatorId(0), &mut state); - } - - #[test] - fn do_not_panic_if_told_no_registration_will_happen() { - let mut state = State::default(); - state.notification_engine.grow(); - - let mut ctx = PropagatorConstructorContext::new(PropagatorId(0), &mut state); - ctx.will_not_register_any_events(); - } - - #[test] - fn do_not_panic_if_no_registration_happens_in_reborrowed() { - let mut state = State::default(); - state.notification_engine.grow(); - - let mut ctx = PropagatorConstructorContext::new(PropagatorId(0), &mut state); - let ctx2 = ctx.reborrow(); - drop(ctx2); - - ctx.will_not_register_any_events(); - } - - #[test] - fn reborrowing_remembers_next_local_id() { - let mut state = State::default(); - state.notification_engine.grow(); - - let mut c1 = PropagatorConstructorContext::new(PropagatorId(0), &mut state); - c1.will_not_register_any_events(); - - let mut c2 = c1.reborrow(); - c2.register(DomainId::new(0), DomainEvents::ANY_INT, LocalId::from(1)); - drop(c2); - - assert_eq!(LocalId::from(2), c1.get_next_local_id()); - } -} diff --git a/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs b/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs index d84c33567..57187434c 100644 --- a/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs +++ b/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs @@ -1,3 +1,5 @@ +use enumset::EnumSet; + use crate::basic_types::PredicateId; use crate::engine::Assignments; use crate::engine::EmptyDomain; @@ -10,8 +12,10 @@ use crate::engine::reason::Reason; use crate::engine::reason::ReasonStore; use crate::engine::reason::StoredReason; use crate::engine::variables::Literal; +use crate::propagation::DomainEvent; use crate::propagation::DomainEvents; use crate::propagation::Domains; +use crate::propagation::EventDispatcher; use crate::propagation::HasAssignments; use crate::propagation::LocalId; #[cfg(doc)] @@ -23,6 +27,7 @@ use crate::propagation::PropagatorVarId; #[cfg(doc)] use crate::propagation::ReadDomains; use crate::pumpkin_assert_simple; +use crate::variables::DomainId; use crate::variables::IntegerVariable; /// Provided to the propagator when it is notified of a domain event. @@ -138,21 +143,20 @@ impl<'a> PropagationContext<'a> { } /// Subscribes the propagator to the given [`DomainEvents`]. - /// - /// See [`PropagatorConstructorContext::register`] for more information. pub fn register_domain_event( &mut self, var: impl IntegerVariable, domain_events: DomainEvents, local_id: LocalId, ) { - let propagator_var = PropagatorVarId { - propagator: self.propagator_id, - variable: local_id, - }; - - let mut watchers = Watchers::new(propagator_var, self.notification_engine); - var.watch_all(&mut watchers, domain_events.events()); + var.register( + &mut NotificationEngineWatchers { + notificaton_engine: self.notification_engine, + propagator_id: self.propagator_id, + }, + domain_events.events(), + local_id, + ); } /// Stop being enqueued for events on the given integer variable. @@ -295,3 +299,22 @@ pub(crate) fn build_reason( Reason::DynamicLazy(code) => StoredReason::DynamicLazy(code), } } + +/// A wrapper around the notification engine that implements [`EventDispatcher`]. +struct NotificationEngineWatchers<'a> { + propagator_id: PropagatorId, + notificaton_engine: &'a mut NotificationEngine, +} + +impl EventDispatcher for NotificationEngineWatchers<'_> { + fn register(&mut self, domain_id: DomainId, events: EnumSet, local_id: LocalId) { + self.notificaton_engine.register( + domain_id, + events, + PropagatorVarId { + propagator: self.propagator_id, + variable: local_id, + }, + ); + } +} diff --git a/pumpkin-crates/core/src/propagation/event_registration.rs b/pumpkin-crates/core/src/propagation/event_registration.rs new file mode 100644 index 000000000..13ca1af71 --- /dev/null +++ b/pumpkin-crates/core/src/propagation/event_registration.rs @@ -0,0 +1,149 @@ +use enumset::EnumSet; + +use crate::propagation::DomainEvent; +use crate::propagation::DomainEvents; +use crate::propagation::LocalId; +use crate::variables::DomainId; + +/// Anything that can subscribe to domain events. +/// +/// Typically these are variables. +pub trait EventTarget { + /// Indicate that `self` should be registered for the given domain events as the given local ID. + fn register( + &self, + registration: &mut impl EventDispatcher, + events: EnumSet, + local_id: LocalId, + ); +} + +/// The interface to a component that needs to know which variables care about which events. +pub trait EventDispatcher { + // This is a separate trait to isolate the event registration from the rest of the solver. + // That isolation is beneficial when writing tests, as individual components can easily be + // mocked without needing to set up an entire state/solver. + + /// Register the [`DomainId`] with the given [`LocalId`] on the given [`DomainEvents`]. + /// + /// It is possible to register the same [`DomainId`] with different [`LocalId`]s. This may + /// happen when the propagator uses multiple local IDs for different events for the same + /// variable. Or when different views over the same domain are used in a propagator. + fn register(&mut self, domain_id: DomainId, events: EnumSet, local_id: LocalId); +} + +/// Contains all the events and domains that a propagator needs to be enqueued for. +#[derive(Clone, Debug)] +pub struct EventsToRegister(Vec<(DomainId, EnumSet, LocalId)>); + +impl EventsToRegister { + /// Create an [`EventsToRegister`] without any variables. + /// + /// This is the uncommon case. Without registering for variable events, a propagator will never + /// be enqueued automatically. However, certain propagators like, e.g., compound propagators, + /// may not be able to register during construction in which case they will be enqueued + /// explicitly when a constraint is added to them. The nogood propagator is an example of such a + /// propagator. + pub fn empty() -> EventsToRegister { + EventsToRegister(vec![]) + } + + /// Create a new [`EventsToRegisterBuilder`]. + /// + /// If no event registrations will be made, use [`EventsToRegister::empty`] instead. + /// Calling [`EventsToRegisterBuilder::build`] without any registrations will cause a panic. + pub fn builder() -> EventsToRegisterBuilder { + EventsToRegisterBuilder { + registrations: EventsToRegister(vec![]), + } + } + + /// Add a new event registration to an existing instance of self. + /// + /// # Example + /// + /// ``` + /// use pumpkin_core::propagation::DomainEvents; + /// use pumpkin_core::propagation::EventsToRegister; + /// use pumpkin_core::propagation::LocalId; + /// use pumpkin_core::variables::DomainId; + /// + /// let v1 = DomainId::new(0); + /// let v2 = DomainId::new(0); + /// let mut registration = EventsToRegister::builder() + /// .add(&v1, DomainEvents::ANY_INT, LocalId::from(0)) + /// .build(); + /// + /// // Extend the events to register with another variable. + /// registration.add(&v2, DomainEvents::ANY_INT, LocalId::from(1)); + /// ``` + pub fn add( + &mut self, + target: &impl EventTarget, + domain_events: DomainEvents, + local_id: LocalId, + ) { + target.register(self, domain_events.events(), local_id); + } + + /// Iterate the registrations already made. + pub fn iter(&self) -> impl ExactSizeIterator, LocalId)> { + self.0.iter().copied() + } +} + +impl EventDispatcher for EventsToRegister { + fn register(&mut self, domain_id: DomainId, events: EnumSet, local_id: LocalId) { + self.0.push((domain_id, events, local_id)); + } +} + +/// Used to construct an [`EventsToRegister`] for heterogeneous [`EventTarget`] implementations. +/// +/// See [`EventsToRegister::builder`] for a usage example. +#[derive(Clone, Debug)] +pub struct EventsToRegisterBuilder { + registrations: EventsToRegister, +} + +impl EventsToRegisterBuilder { + /// Add a new event registration. + /// + /// # Example + /// + /// ``` + /// use pumpkin_core::propagation::DomainEvents; + /// use pumpkin_core::propagation::EventsToRegister; + /// use pumpkin_core::propagation::LocalId; + /// use pumpkin_core::variables::DomainId; + /// + /// let v1 = DomainId::new(0); + /// let v2 = DomainId::new(0); + /// let registration = EventsToRegister::builder() + /// .add(&v1, DomainEvents::ANY_INT, LocalId::from(0)) + /// .add(&v2, DomainEvents::ANY_INT, LocalId::from(1)) + /// .build(); + /// ``` + pub fn add( + mut self, + target: &impl EventTarget, + domain_events: DomainEvents, + local_id: LocalId, + ) -> Self { + self.registrations.add(target, domain_events, local_id); + self + } + + /// Finish constructing the [`EventsToRegister`]. + /// + /// If no variables are registered, then this panics. If no variables can be registered during + /// construction, use [`EventsToRegister::empty`]. + pub fn build(self) -> EventsToRegister { + assert!( + !self.registrations.0.is_empty(), + "did not register for any events" + ); + + self.registrations + } +} diff --git a/pumpkin-crates/core/src/propagation/local_id.rs b/pumpkin-crates/core/src/propagation/local_id.rs index b3a3334df..baff94a32 100644 --- a/pumpkin-crates/core/src/propagation/local_id.rs +++ b/pumpkin-crates/core/src/propagation/local_id.rs @@ -10,6 +10,11 @@ impl LocalId { LocalId(value) } + /// Get the next [`LocalId`]. + pub const fn successor(self) -> Self { + LocalId(self.0 + 1) + } + pub fn unpack(self) -> u32 { self.0 } diff --git a/pumpkin-crates/core/src/propagation/mod.rs b/pumpkin-crates/core/src/propagation/mod.rs index 7c4b5b02b..1646dda63 100644 --- a/pumpkin-crates/core/src/propagation/mod.rs +++ b/pumpkin-crates/core/src/propagation/mod.rs @@ -30,7 +30,7 @@ //! implement for this trait is [`Propagator::propagate`], which performs the domain reduction. //! //! A propagator is created by a [`PropagatorConstructor`]. The constructor is responsible for -//! registering to [`DomainEvents`] (using [`PropagatorConstructorContext::register`]), and setting +//! registering to [`DomainEvents`] and setting //! up the state of the propagator. The constructor is provided a [`PropagatorConstructorContext`], //! which has all the available functions allowing the propagator to hook into the solver state. //! @@ -69,6 +69,7 @@ mod constructor; mod contexts; mod domains; +mod event_registration; mod local_id; mod propagator; @@ -76,6 +77,8 @@ pub(crate) mod propagator_id; pub(crate) mod propagator_var_id; pub(crate) mod store; +pub use event_registration::*; + mod reexports { // Re-exports of types not in this module according to the file tree. // These will probably be be moved at some point, but for now they are simply re-exported here diff --git a/pumpkin-crates/core/src/propagation/propagator.rs b/pumpkin-crates/core/src/propagation/propagator.rs index 2ccffce40..9cb6690c6 100644 --- a/pumpkin-crates/core/src/propagation/propagator.rs +++ b/pumpkin-crates/core/src/propagation/propagator.rs @@ -113,7 +113,7 @@ pub trait Propagator: Downcast + DynClone { /// Returns whether the propagator should be enqueued for propagation when a [`DomainEvent`] /// happens to one of the variables the propagator is subscribed to (as registered during - /// creation with [`PropagatorConstructor`] using [`PropagatorConstructorContext::register`]). + /// creation with [`PropagatorConstructor`]. /// /// This can be used to incrementally maintain data structures or perform propagations, and /// should only be used for computationally cheap logic. Expensive computation should be diff --git a/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs b/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs index fc1e0a3f7..11b6fb604 100644 --- a/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs +++ b/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs @@ -7,6 +7,7 @@ use crate::predicates::PropositionalConjunction; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; use crate::propagation::DomainEvents; +use crate::propagation::EventsToRegister; use crate::propagation::InferenceCheckers; use crate::propagation::LocalId; use crate::propagation::PropagationContext; @@ -44,7 +45,10 @@ impl PropagatorConstructor for HypercubeLinearConstructor { ); } - fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + fn create( + self, + mut context: PropagatorConstructorContext, + ) -> (EventsToRegister, Self::PropagatorImpl) { let HypercubeLinearConstructor { hypercube, linear, @@ -65,13 +69,18 @@ impl PropagatorConstructor for HypercubeLinearConstructor { ] }; - HypercubeLinearPropagator { + let propagator = HypercubeLinearPropagator { linear, hypercube_predicates, watched_predicates, inference_code: InferenceCode::new(constraint_tag, HypercubeLinear), - } + }; + + // TODO: This will be expanded with registration of predicates. + let registration = EventsToRegister::empty(); + + (registration, propagator) } } diff --git a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs index a58cb7b27..82936e569 100644 --- a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs +++ b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs @@ -25,6 +25,7 @@ use crate::predicate; use crate::predicates::PredicateType; use crate::proof::InferenceCode; use crate::propagation::EnqueueDecision; +use crate::propagation::EventsToRegister; use crate::propagation::ExplanationContext; use crate::propagation::HasAssignments; use crate::propagation::LazyExplanation; @@ -169,10 +170,11 @@ impl NogoodPropagatorConstructor { impl PropagatorConstructor for NogoodPropagatorConstructor { type PropagatorImpl = NogoodPropagator; - fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { - context.will_not_register_any_events(); - - NogoodPropagator { + fn create( + self, + context: PropagatorConstructorContext, + ) -> (EventsToRegister, Self::PropagatorImpl) { + let propagator = NogoodPropagator { statistics: NogoodPropagatorStatistics::default(), handle: PropagatorHandle::new(context.propagator_id), parameters: self.parameters, @@ -189,7 +191,9 @@ impl PropagatorConstructor for NogoodPropagatorConstructor { propagation_mode: self.propagation_mode, semantic_minimiser: Default::default(), priority: self.priority, - } + }; + + (EventsToRegister::empty(), propagator) } } @@ -205,14 +209,6 @@ pub(crate) struct Watcher { pub(crate) cached_predicate: PredicateId, } -impl PropagatorConstructor for NogoodPropagator { - type PropagatorImpl = Self; - - fn create(self, _: PropagatorConstructorContext) -> Self::PropagatorImpl { - self - } -} - /// Keeps track of three tiers of nogoods: /// - "low" LBD nogoods /// - "mid" LBD nogoods diff --git a/pumpkin-crates/core/src/propagators/reified_propagator.rs b/pumpkin-crates/core/src/propagators/reified_propagator.rs index 0bb782495..d49059289 100644 --- a/pumpkin-crates/core/src/propagators/reified_propagator.rs +++ b/pumpkin-crates/core/src/propagators/reified_propagator.rs @@ -9,6 +9,7 @@ use crate::predicates::Predicate; use crate::propagation::DomainEvents; use crate::propagation::Domains; use crate::propagation::EnqueueDecision; +use crate::propagation::EventsToRegister; use crate::propagation::ExplanationContext; use crate::propagation::InferenceCheckers; use crate::propagation::LazyExplanation; @@ -38,30 +39,41 @@ where { type PropagatorImpl = ReifiedPropagator; - fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + fn create( + self, + mut context: PropagatorConstructorContext, + ) -> (EventsToRegister, Self::PropagatorImpl) { let ReifiedPropagatorArgs { propagator, reification_literal, } = self; - let propagator = propagator.create(context.reborrow()); - let reification_literal_id = context.get_next_local_id(); + let (mut registration, propagator) = propagator.create(context.reborrow()); - context.register( - self.reification_literal, + let reification_literal_id = registration + .iter() + .map(|(_, _, lid)| lid) + .max() + .expect("cannot reify propagators that do not register all variables immediately") + .successor(); + + registration.add( + &self.reification_literal, DomainEvents::BOUNDS, reification_literal_id, ); let name = format!("Reified({})", propagator.name()); - ReifiedPropagator { + let propagator = ReifiedPropagator { propagator, reification_literal, reification_literal_id, name, reason_buffer: vec![], - } + }; + + (registration, propagator) } fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { @@ -296,6 +308,7 @@ mod tests { let _ = solver .new_propagator(ReifiedPropagatorArgs { propagator: GenericPropagator::new( + vec![a, b], move |_: PropagationContext| { Err(PropagatorConflict { conjunction: t1.clone(), @@ -330,6 +343,7 @@ mod tests { let propagator = solver .new_propagator(ReifiedPropagatorArgs { propagator: GenericPropagator::new( + vec![var], move |mut ctx: PropagationContext| { ctx.post( predicate![var >= 3], @@ -373,6 +387,7 @@ mod tests { let inconsistency = solver .new_propagator(ReifiedPropagatorArgs { propagator: GenericPropagator::new( + vec![var], move |_: PropagationContext| { Err(PropagatorConflict { conjunction: conjunction!([var >= 1]), @@ -414,6 +429,7 @@ mod tests { let propagator = solver .new_propagator(ReifiedPropagatorArgs { propagator: GenericPropagator::new( + vec![var], |_: PropagationContext| Ok(()), move |context: Domains| { if context.is_fixed(&var) { @@ -450,16 +466,17 @@ mod tests { { type PropagatorImpl = Self; - fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + fn create( + self, + _: PropagatorConstructorContext, + ) -> (EventsToRegister, Self::PropagatorImpl) { + let mut registration = EventsToRegister::empty(); + for (index, variable) in self.variables_to_register.iter().enumerate() { - context.register( - *variable, - DomainEvents::ANY_INT, - LocalId::from(index as u32), - ); + registration.add(variable, DomainEvents::ANY_INT, LocalId::from(index as u32)); } - self + (registration, self) } } @@ -486,11 +503,15 @@ mod tests { Propagation: Fn(PropagationContext) -> PropagationStatusCP, ConsistencyCheck: Fn(Domains) -> Option, { - pub(crate) fn new(propagation: Propagation, consistency_check: ConsistencyCheck) -> Self { + pub(crate) fn new( + variables_to_register: Vec, + propagation: Propagation, + consistency_check: ConsistencyCheck, + ) -> Self { GenericPropagator { propagation, consistency_check, - variables_to_register: vec![], + variables_to_register, } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs index 2881dfa39..9934e6821 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs @@ -8,6 +8,7 @@ use pumpkin_core::predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; use pumpkin_core::propagation::DomainEvents; +use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::Priority; @@ -45,23 +46,27 @@ where ); } - fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + fn create(self, _: PropagatorConstructorContext) -> (EventsToRegister, Self::PropagatorImpl) { let AbsoluteValueArgs { signed, absolute, constraint_tag, } = self; - context.register(signed.clone(), DomainEvents::BOUNDS, LocalId::from(0)); - context.register(absolute.clone(), DomainEvents::BOUNDS, LocalId::from(1)); + let registration = EventsToRegister::builder() + .add(&signed, DomainEvents::BOUNDS, LocalId::from(0)) + .add(&absolute, DomainEvents::BOUNDS, LocalId::from(1)) + .build(); let inference_code = InferenceCode::new(constraint_tag, AbsoluteValue); - AbsoluteValuePropagator { + let propagator = AbsoluteValuePropagator { signed, absolute, inference_code, - } + }; + + (registration, propagator) } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs index b95b86b46..b43ccb585 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs @@ -20,6 +20,7 @@ use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EnqueueDecision; +use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::ExplanationContext; use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LazyExplanation; @@ -64,17 +65,19 @@ where ); } - fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + fn create(self, _: PropagatorConstructorContext) -> (EventsToRegister, Self::PropagatorImpl) { let BinaryEqualsPropagatorArgs { a, b, constraint_tag, } = self; - context.register(a.clone(), DomainEvents::ANY_INT, LocalId::from(0)); - context.register(b.clone(), DomainEvents::ANY_INT, LocalId::from(1)); + let registration = EventsToRegister::builder() + .add(&a, DomainEvents::ANY_INT, LocalId::from(0)) + .add(&b, DomainEvents::ANY_INT, LocalId::from(1)) + .build(); - BinaryEqualsPropagator { + let propagator = BinaryEqualsPropagator { a, b, @@ -86,7 +89,9 @@ where has_backtracked: false, first_propagation_loop: true, reason: Predicate::trivially_false(), - } + }; + + (registration, propagator) } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs index b33a98543..4ca2c4032 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs @@ -8,6 +8,7 @@ use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::Domains; +use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::Priority; @@ -47,7 +48,7 @@ where ); } - fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + fn create(self, _: PropagatorConstructorContext) -> (EventsToRegister, Self::PropagatorImpl) { let BinaryNotEqualsPropagatorArgs { a, b, @@ -55,15 +56,19 @@ where } = self; // We only care about the case where one of the two is assigned - context.register(a.clone(), DomainEvents::ASSIGN, LocalId::from(0)); - context.register(b.clone(), DomainEvents::ASSIGN, LocalId::from(1)); + let registration = EventsToRegister::builder() + .add(&a, DomainEvents::ASSIGN, LocalId::from(0)) + .add(&b, DomainEvents::ASSIGN, LocalId::from(1)) + .build(); - BinaryNotEqualsPropagator { + let propagator = BinaryNotEqualsPropagator { a, b, inference_code: InferenceCode::new(constraint_tag, BinaryNotEquals), - } + }; + + (registration, propagator) } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs index 882495a48..300b26e96 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs @@ -9,6 +9,7 @@ use pumpkin_core::predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; use pumpkin_core::propagation::DomainEvents; +use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::Priority; @@ -43,7 +44,10 @@ where { type PropagatorImpl = DivisionPropagator; - fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + fn create( + self, + context: PropagatorConstructorContext, + ) -> (EventsToRegister, Self::PropagatorImpl) { let DivisionArgs { numerator, denominator, @@ -56,18 +60,22 @@ where "Denominator cannot contain 0" ); - context.register(numerator.clone(), DomainEvents::BOUNDS, ID_NUMERATOR); - context.register(denominator.clone(), DomainEvents::BOUNDS, ID_DENOMINATOR); - context.register(rhs.clone(), DomainEvents::BOUNDS, ID_RHS); + let registration = EventsToRegister::builder() + .add(&numerator, DomainEvents::BOUNDS, ID_NUMERATOR) + .add(&denominator, DomainEvents::BOUNDS, ID_DENOMINATOR) + .add(&rhs, DomainEvents::BOUNDS, ID_RHS) + .build(); let inference_code = InferenceCode::new(constraint_tag, Division); - DivisionPropagator { + let propagator = DivisionPropagator { numerator, denominator, rhs, inference_code, - } + }; + + (registration, propagator) } fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs index 9e7d8d953..6811e17bc 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs @@ -8,6 +8,7 @@ use pumpkin_core::predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; use pumpkin_core::propagation::DomainEvents; +use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::Priority; @@ -50,7 +51,7 @@ where ); } - fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + fn create(self, _: PropagatorConstructorContext) -> (EventsToRegister, Self::PropagatorImpl) { let IntegerMultiplicationArgs { a, b, @@ -58,16 +59,20 @@ where constraint_tag, } = self; - context.register(a.clone(), DomainEvents::ANY_INT, ID_A); - context.register(b.clone(), DomainEvents::ANY_INT, ID_B); - context.register(c.clone(), DomainEvents::ANY_INT, ID_C); + let registration = EventsToRegister::builder() + .add(&a, DomainEvents::ANY_INT, ID_A) + .add(&b, DomainEvents::ANY_INT, ID_B) + .add(&c, DomainEvents::ANY_INT, ID_C) + .build(); - IntegerMultiplicationPropagator { + let propagator = IntegerMultiplicationPropagator { a, b, c, inference_code: InferenceCode::new(constraint_tag, IntegerMultiplication), - } + }; + + (registration, propagator) } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs index 075af43d9..a3a03be1c 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs @@ -13,6 +13,7 @@ use pumpkin_core::proof::InferenceCode; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EnqueueDecision; +use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::ExplanationContext; use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LazyExplanation; @@ -56,7 +57,10 @@ where ); } - fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + fn create( + self, + mut context: PropagatorConstructorContext, + ) -> (EventsToRegister, Self::PropagatorImpl) { let LinearLessOrEqualPropagatorArgs { x, c, @@ -66,26 +70,26 @@ where let mut lower_bound_left_hand_side = 0_i64; let mut current_bounds = vec![]; + let mut registration = EventsToRegister::builder(); for (i, x_i) in x.iter().enumerate() { - context.register( - x_i.clone(), - DomainEvents::LOWER_BOUND, - LocalId::from(i as u32), - ); + registration = + registration.add(x_i, DomainEvents::LOWER_BOUND, LocalId::from(i as u32)); lower_bound_left_hand_side += context.lower_bound(x_i) as i64; current_bounds.push(context.new_trailed_integer(context.lower_bound(x_i) as i64)); } let lower_bound_left_hand_side = context.new_trailed_integer(lower_bound_left_hand_side); - LinearLessOrEqualPropagator { + let propagator = LinearLessOrEqualPropagator { x, c, lower_bound_left_hand_side, current_bounds: current_bounds.into(), inference_code: InferenceCode::new(constraint_tag, LinearBounds), reason_buffer: Vec::default(), - } + }; + + (registration.build(), propagator) } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs index 130d2b2d8..d92290960 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs @@ -18,6 +18,7 @@ use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EnqueueDecision; +use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::NotificationContext; @@ -60,15 +61,19 @@ where ); } - fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + fn create( + self, + mut context: PropagatorConstructorContext, + ) -> (EventsToRegister, Self::PropagatorImpl) { let LinearNotEqualPropagatorArgs { terms, rhs, constraint_tag, } = self; + let mut registration = EventsToRegister::builder(); for (i, x_i) in terms.iter().enumerate() { - context.register(x_i.clone(), DomainEvents::ASSIGN, LocalId::from(i as u32)); + registration = registration.add(x_i, DomainEvents::ASSIGN, LocalId::from(i as u32)); context.register_backtrack( x_i.clone(), DomainEvents::new(enum_set!(DomainEvent::Assign | DomainEvent::Removal)), @@ -88,7 +93,7 @@ where propagator.recalculate_fixed_variables(context.domains()); - propagator + (registration.build(), propagator) } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs index 2a847bc4c..6f658ace3 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs @@ -9,6 +9,7 @@ use pumpkin_core::predicates::PropositionalConjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; use pumpkin_core::propagation::DomainEvents; +use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::Priority; @@ -46,30 +47,33 @@ where ); } - fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + fn create(self, _: PropagatorConstructorContext) -> (EventsToRegister, Self::PropagatorImpl) { let MaximumArgs { array, rhs, constraint_tag, } = self; + let mut registration = EventsToRegister::builder(); for (idx, var) in array.iter().enumerate() { - context.register(var.clone(), DomainEvents::BOUNDS, LocalId::from(idx as u32)); + registration = registration.add(var, DomainEvents::BOUNDS, LocalId::from(idx as u32)); } - context.register( - rhs.clone(), + registration = registration.add( + &rhs, DomainEvents::BOUNDS, LocalId::from(array.len() as u32), ); let inference_code = InferenceCode::new(constraint_tag, Maximum); - MaximumPropagator { + let propagator = MaximumPropagator { array, rhs, inference_code, - } + }; + + (registration.build(), propagator) } } diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs index fc5d108e4..ea2af2fda 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs @@ -11,6 +11,7 @@ use pumpkin_core::proof::InferenceCode; use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EnqueueDecision; +use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::NotificationContext; @@ -129,10 +130,13 @@ impl PropagatorConstruc ); } - fn create(mut self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + fn create( + mut self, + mut context: PropagatorConstructorContext, + ) -> (EventsToRegister, Self::PropagatorImpl) { // We only register for notifications of backtrack events if incremental backtracking is // enabled - register_tasks( + let registration = register_tasks( &self.parameters.tasks, context.reborrow(), self.parameters.options.incremental_backtracking, @@ -146,7 +150,7 @@ impl PropagatorConstruc self.inference_code = Some(InferenceCode::new(self.constraint_tag, TimeTable)); - self + (registration, self) } } diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs index 9b4ffa1e5..661df8e50 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs @@ -11,6 +11,7 @@ use pumpkin_core::proof::InferenceCode; use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EnqueueDecision; +use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::NotificationContext; @@ -126,8 +127,11 @@ impl Propagator ); } - fn create(mut self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { - register_tasks(&self.parameters.tasks, context.reborrow(), true); + fn create( + mut self, + mut context: PropagatorConstructorContext, + ) -> (EventsToRegister, Self::PropagatorImpl) { + let registration = register_tasks(&self.parameters.tasks, context.reborrow(), true); self.updatable_structures .reset_all_bounds_and_remove_fixed(context.domains(), &self.parameters); @@ -136,7 +140,7 @@ impl Propagator self.inference_code = Some(InferenceCode::new(self.constraint_tag, TimeTable)); - self + (registration, self) } } diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs index cb8b6926b..86b6adfef 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs @@ -9,6 +9,7 @@ use pumpkin_core::proof::InferenceCode; use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EnqueueDecision; +use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::NotificationContext; @@ -129,14 +130,17 @@ impl PropagatorConstructor ); } - fn create(mut self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + fn create( + mut self, + mut context: PropagatorConstructorContext, + ) -> (EventsToRegister, Self::PropagatorImpl) { self.updatable_structures .initialise_bounds_and_remove_fixed(context.domains(), &self.parameters); - register_tasks(&self.parameters.tasks, context.reborrow(), false); + let registration = register_tasks(&self.parameters.tasks, context.reborrow(), false); self.inference_code = Some(InferenceCode::new(self.constraint_tag, TimeTable)); - self + (registration, self) } } diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs index 5451cd01d..a8d11a955 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs @@ -11,6 +11,7 @@ use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::EnqueueDecision; +use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::NotificationContext; @@ -119,14 +120,17 @@ impl PropagatorConstructor for TimeTablePerPoint ); } - fn create(mut self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + fn create( + mut self, + mut context: PropagatorConstructorContext, + ) -> (EventsToRegister, Self::PropagatorImpl) { self.updatable_structures .initialise_bounds_and_remove_fixed(context.domains(), &self.parameters); - register_tasks(&self.parameters.tasks, context.reborrow(), false); + let registration = register_tasks(&self.parameters.tasks, context.reborrow(), false); self.inference_code = Some(InferenceCode::new(self.constraint_tag, TimeTable)); - self + (registration, self) } } diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/utils/util.rs b/pumpkin-crates/propagators/src/propagators/cumulative/utils/util.rs index 3b1d3f790..bd0f1c031 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/utils/util.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/utils/util.rs @@ -7,6 +7,7 @@ use enumset::enum_set; use pumpkin_core::propagation::DomainEvent; use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::Domains; +use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; @@ -52,15 +53,18 @@ pub(crate) fn register_tasks( tasks: &[Rc>], mut context: PropagatorConstructorContext<'_>, register_backtrack: bool, -) { - tasks.iter().for_each(|task| { - context.register( - task.start_variable.clone(), +) -> EventsToRegister { + let mut registration = EventsToRegister::builder(); + + for task in tasks.iter() { + registration = registration.add( + &task.start_variable, DomainEvents::new(enum_set!( DomainEvent::LowerBound | DomainEvent::UpperBound | DomainEvent::Assign )), task.id, ); + if register_backtrack { context.register_backtrack( task.start_variable.clone(), @@ -70,7 +74,9 @@ pub(crate) fn register_tasks( task.id, ); } - }); + } + + registration.build() } /// Updates the bounds of the provided [`Task`] to those stored in diff --git a/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs b/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs index 0d2da6002..753f71494 100644 --- a/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs +++ b/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs @@ -8,6 +8,7 @@ use pumpkin_core::predicates::PropositionalConjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; use pumpkin_core::propagation::DomainEvents; +use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::PropagationContext; @@ -79,7 +80,7 @@ impl DisjunctiveConstructor { impl PropagatorConstructor for DisjunctiveConstructor { type PropagatorImpl = DisjunctivePropagator; - fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + fn create(self, _: PropagatorConstructorContext) -> (EventsToRegister, Self::PropagatorImpl) { let tasks = self .tasks .into_iter() @@ -94,17 +95,20 @@ impl PropagatorConstructor for DisjunctiveConstr let inference_code = InferenceCode::new(self.constraint_tag, DisjunctiveEdgeFinding); - tasks.iter().for_each(|task| { - context.register(task.start_time.clone(), DomainEvents::BOUNDS, task.id); - }); + let mut registration = EventsToRegister::builder(); + for task in tasks.iter() { + registration = registration.add(&task.start_time, DomainEvents::BOUNDS, task.id); + } - DisjunctivePropagator { + let propagator = DisjunctivePropagator { tasks: tasks.clone().into_boxed_slice(), sorted_tasks: tasks, theta_lambda_tree, inference_code, - } + }; + + (registration.build(), propagator) } fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { diff --git a/pumpkin-crates/propagators/src/propagators/element.rs b/pumpkin-crates/propagators/src/propagators/element.rs index 8874a259c..3ce5516e1 100644 --- a/pumpkin-crates/propagators/src/propagators/element.rs +++ b/pumpkin-crates/propagators/src/propagators/element.rs @@ -17,6 +17,7 @@ use pumpkin_core::predicates::Predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; use pumpkin_core::propagation::DomainEvents; +use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::ExplanationContext; use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LazyExplanation; @@ -60,7 +61,7 @@ where ); } - fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + fn create(self, _: PropagatorConstructorContext) -> (EventsToRegister, Self::PropagatorImpl) { let ElementArgs { array, index, @@ -68,26 +69,29 @@ where constraint_tag, } = self; + let mut registration = EventsToRegister::builder(); for (i, x_i) in array.iter().enumerate() { - context.register( - x_i.clone(), + registration = registration.add( + x_i, DomainEvents::ANY_INT, LocalId::from(i as u32 + ID_X_OFFSET), ); } - context.register(index.clone(), DomainEvents::ANY_INT, ID_INDEX); - context.register(rhs.clone(), DomainEvents::ANY_INT, ID_RHS); + registration = registration.add(&index, DomainEvents::ANY_INT, ID_INDEX); + registration = registration.add(&rhs, DomainEvents::ANY_INT, ID_RHS); let inference_code = InferenceCode::new(constraint_tag, Element); - ElementPropagator { + let propagator = ElementPropagator { array, index, rhs, inference_code, rhs_reason_buffer: vec![], - } + }; + + (registration.build(), propagator) } } diff --git a/pumpkin-proof-processor/src/deduction_propagator.rs b/pumpkin-proof-processor/src/deduction_propagator.rs index bba962e49..26d6b86f3 100644 --- a/pumpkin-proof-processor/src/deduction_propagator.rs +++ b/pumpkin-proof-processor/src/deduction_propagator.rs @@ -2,6 +2,7 @@ use pumpkin_core::declare_inference_label; use pumpkin_core::predicates::PropositionalConjunction; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; +use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::PredicateId; use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; @@ -24,7 +25,10 @@ pub(crate) struct DeductionPropagatorConstructor { impl PropagatorConstructor for DeductionPropagatorConstructor { type PropagatorImpl = DeductionPropagator; - fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + fn create( + self, + mut context: PropagatorConstructorContext, + ) -> (EventsToRegister, Self::PropagatorImpl) { declare_inference_label!(Nogood); let DeductionPropagatorConstructor { @@ -37,12 +41,14 @@ impl PropagatorConstructor for DeductionPropagatorConstructor { .map(|&predicate| context.register_predicate(predicate)) .collect(); - DeductionPropagator { + let propagator = DeductionPropagator { nogood, ids, inference_code: InferenceCode::new(constraint_tag, Nogood), active: true, - } + }; + + (EventsToRegister::empty(), propagator) } }