From cae88322ee95de63b32fb0b3785be894b3763936 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Mon, 5 Oct 2026 12:03:27 +0200 Subject: [PATCH] chore: Update cached predicate when known to not be satisfied --- Cargo.lock | 30 ++ .../contexts/propagation_context.rs | 13 + .../propagators/nogoods/nogood_propagator.rs | 29 +- .../propagators/nogoods/propagation_mode.rs | 30 +- .../src/propagators/disjunctive/checker.rs | 314 +++++++++--------- 5 files changed, 233 insertions(+), 183 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 4bace134f..2faf97b89 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1464,6 +1464,36 @@ dependencies = [ "pin-project-lite", ] +[[package]] +name = "toml_datetime" +version = "1.1.1+spec-1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3165f65f62e28e0115a00b2ebdd37eb6f3b641855f9d636d3cd4103767159ad7" +dependencies = [ + "serde_core", +] + +[[package]] +name = "toml_edit" +version = "0.25.15+spec-1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1340ea94a5856333492c9064b02c778b191dd2c853778d9609debdcdfea3a614" +dependencies = [ + "indexmap", + "toml_datetime", + "toml_parser", + "winnow 1.0.4", +] + +[[package]] +name = "toml_parser" +version = "1.1.3+spec-1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1d38ac1cf9b95face32296c0a3ede1fdc270627c9d9c02a7274dd6d960dc4d56" +dependencies = [ + "winnow 1.0.4", +] + [[package]] name = "unicode-ident" version = "1.0.24" diff --git a/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs b/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs index f39d337b0..c39549aca 100644 --- a/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs +++ b/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs @@ -136,6 +136,19 @@ impl<'a> PropagationContext<'a> { ) } + /// Register the propagator to be enqueued when the predicate with the provided [`PredicateId`] + /// becomes true. + /// + /// Avoids looking up the [`PredicateId`] when it is already known. + pub(crate) fn register_predicate_id(&mut self, predicate_id: PredicateId) { + self.notification_engine.watch_predicate_id( + predicate_id, + self.propagator_id, + self.trailed_values, + self.assignments, + ) + } + /// Stop being enqueued for the given predicate. pub fn unregister_predicate(&mut self, predicate_id: PredicateId) { self.notification_engine diff --git a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs index 7a58596aa..6bf637e91 100644 --- a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs +++ b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs @@ -43,7 +43,6 @@ use crate::propagators::nogoods::WatcherProcessingStatus; use crate::propagators::nogoods::arena_allocator::ArenaAllocator; use crate::propagators::nogoods::arena_allocator::NogoodIndex; use crate::propagators::nogoods::semantic_minimiser::SemanticMinimiser; -use crate::pumpkin_assert_eq_simple; use crate::pumpkin_assert_extreme; use crate::pumpkin_assert_moderate; use crate::pumpkin_assert_simple; @@ -418,9 +417,16 @@ impl Propagator for NogoodPropagator { // Found another predicate that can be the watcher. found_new_watch = true; + // The old cached predicate is known to not be falsified (otherwise no + // new watcher would be searched for), so we set it to the other + // watcher. + let new_watcher = Watcher { + cached_predicate: nogood_predicates[0], + ..watcher + }; Self::replace_watcher( &mut context, - watcher, + new_watcher, nogood_predicates, i, 1, @@ -1107,23 +1113,24 @@ impl NogoodPropagator { .push(NogoodInfo::new_learned_nogood_info(lbd)); let _ = self.inference_codes.push(inference_code); - let watcher = Watcher { - nogood_id, - cached_predicate: self.nogood_predicates.get_nogood(nogood_id)[0], - }; - // Now we add two watchers to the first two predicates in the nogood; we are // guaranteed that these are different predicates NogoodPropagator::add_watcher( context, self.nogood_predicates.get_nogood(nogood_id)[0], - watcher, + Watcher { + nogood_id, + cached_predicate: self.nogood_predicates.get_nogood(nogood_id)[1], + }, &mut self.watch_lists, ); NogoodPropagator::add_watcher( context, self.nogood_predicates.get_nogood(nogood_id)[1], - watcher, + Watcher { + nogood_id, + cached_predicate: self.nogood_predicates.get_nogood(nogood_id)[0], + }, &mut self.watch_lists, ); @@ -1380,9 +1387,7 @@ impl NogoodPropagator { } if watch_lists[predicate].is_empty() { - let actual_predicate = context.get_predicate(predicate); - let other_id = context.register_predicate(actual_predicate); - pumpkin_assert_eq_simple!(predicate, other_id); + context.register_predicate_id(predicate); } watch_lists[predicate].push(watcher); diff --git a/pumpkin-crates/core/src/propagators/nogoods/propagation_mode.rs b/pumpkin-crates/core/src/propagators/nogoods/propagation_mode.rs index 650018542..22243f767 100644 --- a/pumpkin-crates/core/src/propagators/nogoods/propagation_mode.rs +++ b/pumpkin-crates/core/src/propagators/nogoods/propagation_mode.rs @@ -362,22 +362,23 @@ impl PropagationMode { let _ = nogood_info.push(NogoodInfo::new_permanent_nogood_info()); let _ = inference_codes.push(inference_code); - let watcher = Watcher { - nogood_id, - cached_predicate: nogood_predicates.get_nogood(nogood_id)[0], - }; - NogoodPropagator::add_watcher( context, nogood_predicates.get_nogood(nogood_id)[0], - watcher, + Watcher { + nogood_id, + cached_predicate: nogood_predicates.get_nogood(nogood_id)[1], + }, watch_lists, ); NogoodPropagator::add_watcher( context, nogood_predicates.get_nogood(nogood_id)[1], - watcher, + Watcher { + nogood_id, + cached_predicate: nogood_predicates.get_nogood(nogood_id)[0], + }, watch_lists, ); } else { @@ -394,21 +395,22 @@ impl PropagationMode { let _ = nogood_info.push(NogoodInfo::new_permanent_nogood_info()); let _ = inference_codes.push(inference_code); - let watcher = Watcher { - nogood_id, - cached_predicate: nogood_predicates.get_nogood(nogood_id)[0], - }; - NogoodPropagator::add_watcher( context, nogood_predicates.get_nogood(nogood_id)[0], - watcher, + Watcher { + nogood_id, + cached_predicate: nogood_predicates.get_nogood(nogood_id)[1], + }, watch_lists, ); NogoodPropagator::add_watcher( context, nogood_predicates.get_nogood(nogood_id)[1], - watcher, + Watcher { + nogood_id, + cached_predicate: nogood_predicates.get_nogood(nogood_id)[0], + }, watch_lists, ); } diff --git a/pumpkin-crates/propagators/src/propagators/disjunctive/checker.rs b/pumpkin-crates/propagators/src/propagators/disjunctive/checker.rs index f9d18f51f..2926b6bf0 100644 --- a/pumpkin-crates/propagators/src/propagators/disjunctive/checker.rs +++ b/pumpkin-crates/propagators/src/propagators/disjunctive/checker.rs @@ -122,6 +122,163 @@ where } } +#[derive(Debug, Clone)] +pub(super) struct CheckerThetaLambdaTree { + pub(super) nodes: Vec, + /// Then we keep track of a mapping from the [`LocalId`] to its position in the tree since the + /// methods take as input tasks with [`LocalId`]s. + mapping: KeyedVec, + /// The number of internal nodes in the tree; used to calculate the leaf node index based on + /// the index in the tree + number_of_internal_nodes: usize, + /// The tasks which are stored in the leaves of the tree. + /// + /// These tasks are sorted based on non-decreasing start time. + sorted_tasks: Vec>, + phantom_data: PhantomData, +} + +impl> CheckerThetaLambdaTree { + /// Initialises the theta-lambda tree. + /// + /// Note that [`Self::update`] should be called to actually create the tree itself. + pub(super) fn new(tasks: &[DisjunctiveTask]) -> Self { + // Calculate the number of internal nodes which are required to create the binary tree + let mut number_of_internal_nodes = 1; + while number_of_internal_nodes < tasks.len() { + number_of_internal_nodes <<= 1; + } + + CheckerThetaLambdaTree { + nodes: Default::default(), + mapping: KeyedVec::default(), + number_of_internal_nodes: number_of_internal_nodes - 1, + sorted_tasks: tasks.to_vec(), + phantom_data: PhantomData, + } + } + + /// Update the theta-lambda tree based on the provided `context`. + /// + /// It resets theta and lambda to be the empty set. + pub(super) fn update(&mut self, context: &VariableState) { + // First we sort the tasks by lower-bound/earliest start time. + self.sorted_tasks + .sort_by_key(|task| task.start_time.induced_lower_bound(context)); + + // Then we keep track of a mapping from the [`LocalId`] to its position in the tree and a + // reverse mapping + self.mapping.clear(); + for (index, task) in self.sorted_tasks.iter().enumerate() { + while self.mapping.len() <= task.id.index() { + let _ = self.mapping.push(usize::MAX); + } + self.mapping[task.id] = index; + } + + // Finally, we reset the entire tree to be empty + self.nodes.clear(); + for _ in 0..=2 * self.number_of_internal_nodes { + self.nodes.push(Node::empty()) + } + } + + /// Returns the earliest completion time of Theta + pub(super) fn ect(&self) -> i32 { + assert!(!self.nodes.is_empty()); + self.nodes[0].ect + } + + /// Add the provided task to Theta + pub(super) fn add_to_theta( + &mut self, + task: &DisjunctiveTask, + context: &VariableState, + ) { + // We need to find the leaf node index; note that there are |nodes| / 2 leaves + let position = self.nodes.len() / 2 + self.mapping[task.id]; + let ect = task.start_time.induced_lower_bound(context) + task.processing_time; + + self.nodes[position] = Node::new_white_node( + ect.try_into().expect("Should have bounds"), + task.processing_time, + ); + self.upheap(position) + } + + /// Returns the index of the left child of the provided index + fn get_left_child_index(index: usize) -> usize { + 2 * index + 1 + } + + /// Returns the index of the right child of the provided index + fn get_right_child_index(index: usize) -> usize { + 2 * index + 2 + } + + /// Returns the index of the parent of the provided index + fn get_parent(index: usize) -> usize { + assert!(index > 0); + (index - 1) / 2 + } + + /// Calculate the new values for the ancestors of the provided index + pub(super) fn upheap(&mut self, mut index: usize) { + while index != 0 { + let parent = Self::get_parent(index); + let left_child_of_parent = Self::get_left_child_index(parent); + let right_child_of_parent = Self::get_right_child_index(parent); + assert!(left_child_of_parent == index || right_child_of_parent == index); + + // The sum of processing times is the sum of processing times in the left child + the + // sum of processing times in right child + self.nodes[parent].sum_of_processing_times = self.nodes[left_child_of_parent] + .sum_of_processing_times + + self.nodes[right_child_of_parent].sum_of_processing_times; + + // The ECT is either the ECT of the left child node + the processing times of the right + // child or it is the ECT of the right child (we do not know whether the processing + // times of the left child influence the processing times of the right child) + let ect_left = self.nodes[left_child_of_parent].ect + + self.nodes[right_child_of_parent].sum_of_processing_times; + self.nodes[parent].ect = max(self.nodes[right_child_of_parent].ect, ect_left); + + // The sum of processing times (including one element of lambda) is either: + // 1) The sum of processing times of the right child + the sum of processing times of + // the left child including one element of lambda + // 2) The sum of processing times of the left child + the sum of processing times of the + // right child include one element of lambda + let sum_of_processing_times_left_child_lambda = self.nodes[left_child_of_parent] + .sum_of_processing_times_bar + + self.nodes[right_child_of_parent].sum_of_processing_times; + let sum_of_processing_times_right_child_lambda = self.nodes[left_child_of_parent] + .sum_of_processing_times + + self.nodes[right_child_of_parent].sum_of_processing_times_bar; + self.nodes[parent].sum_of_processing_times_bar = max( + sum_of_processing_times_left_child_lambda, + sum_of_processing_times_right_child_lambda, + ); + + // The earliest completion time (including one element of lambda) is either: + // 1) The earliest completion time including one element of lambda from the right child + // 2) The earliest completion time of the right child + the sum of processing times + // including one element of lambda of the right child + // 2) The earliest completion time of the left child + the sum of processing times + // including one element of lambda of the left child + let ect_right_child_lambda = self.nodes[left_child_of_parent].ect + + self.nodes[right_child_of_parent].sum_of_processing_times_bar; + let ect_left_child_lambda = self.nodes[left_child_of_parent].ect_bar + + self.nodes[right_child_of_parent].sum_of_processing_times; + self.nodes[parent].ect_bar = max( + self.nodes[right_child_of_parent].ect_bar, + max(ect_right_child_lambda, ect_left_child_lambda), + ); + + index = parent; + } + } +} + #[cfg(test)] mod tests { use pumpkin_checking::TestAtomic; @@ -337,160 +494,3 @@ mod tests { assert!(!checker.check(state, &premises, None)); } } - -#[derive(Debug, Clone)] -pub(super) struct CheckerThetaLambdaTree { - pub(super) nodes: Vec, - /// Then we keep track of a mapping from the [`LocalId`] to its position in the tree since the - /// methods take as input tasks with [`LocalId`]s. - mapping: KeyedVec, - /// The number of internal nodes in the tree; used to calculate the leaf node index based on - /// the index in the tree - number_of_internal_nodes: usize, - /// The tasks which are stored in the leaves of the tree. - /// - /// These tasks are sorted based on non-decreasing start time. - sorted_tasks: Vec>, - phantom_data: PhantomData, -} - -impl> CheckerThetaLambdaTree { - /// Initialises the theta-lambda tree. - /// - /// Note that [`Self::update`] should be called to actually create the tree itself. - pub(super) fn new(tasks: &[DisjunctiveTask]) -> Self { - // Calculate the number of internal nodes which are required to create the binary tree - let mut number_of_internal_nodes = 1; - while number_of_internal_nodes < tasks.len() { - number_of_internal_nodes <<= 1; - } - - CheckerThetaLambdaTree { - nodes: Default::default(), - mapping: KeyedVec::default(), - number_of_internal_nodes: number_of_internal_nodes - 1, - sorted_tasks: tasks.to_vec(), - phantom_data: PhantomData, - } - } - - /// Update the theta-lambda tree based on the provided `context`. - /// - /// It resets theta and lambda to be the empty set. - pub(super) fn update(&mut self, context: &VariableState) { - // First we sort the tasks by lower-bound/earliest start time. - self.sorted_tasks - .sort_by_key(|task| task.start_time.induced_lower_bound(context)); - - // Then we keep track of a mapping from the [`LocalId`] to its position in the tree and a - // reverse mapping - self.mapping.clear(); - for (index, task) in self.sorted_tasks.iter().enumerate() { - while self.mapping.len() <= task.id.index() { - let _ = self.mapping.push(usize::MAX); - } - self.mapping[task.id] = index; - } - - // Finally, we reset the entire tree to be empty - self.nodes.clear(); - for _ in 0..=2 * self.number_of_internal_nodes { - self.nodes.push(Node::empty()) - } - } - - /// Returns the earliest completion time of Theta - pub(super) fn ect(&self) -> i32 { - assert!(!self.nodes.is_empty()); - self.nodes[0].ect - } - - /// Add the provided task to Theta - pub(super) fn add_to_theta( - &mut self, - task: &DisjunctiveTask, - context: &VariableState, - ) { - // We need to find the leaf node index; note that there are |nodes| / 2 leaves - let position = self.nodes.len() / 2 + self.mapping[task.id]; - let ect = task.start_time.induced_lower_bound(context) + task.processing_time; - - self.nodes[position] = Node::new_white_node( - ect.try_into().expect("Should have bounds"), - task.processing_time, - ); - self.upheap(position) - } - - /// Returns the index of the left child of the provided index - fn get_left_child_index(index: usize) -> usize { - 2 * index + 1 - } - - /// Returns the index of the right child of the provided index - fn get_right_child_index(index: usize) -> usize { - 2 * index + 2 - } - - /// Returns the index of the parent of the provided index - fn get_parent(index: usize) -> usize { - assert!(index > 0); - (index - 1) / 2 - } - - /// Calculate the new values for the ancestors of the provided index - pub(super) fn upheap(&mut self, mut index: usize) { - while index != 0 { - let parent = Self::get_parent(index); - let left_child_of_parent = Self::get_left_child_index(parent); - let right_child_of_parent = Self::get_right_child_index(parent); - assert!(left_child_of_parent == index || right_child_of_parent == index); - - // The sum of processing times is the sum of processing times in the left child + the - // sum of processing times in right child - self.nodes[parent].sum_of_processing_times = self.nodes[left_child_of_parent] - .sum_of_processing_times - + self.nodes[right_child_of_parent].sum_of_processing_times; - - // The ECT is either the ECT of the left child node + the processing times of the right - // child or it is the ECT of the right child (we do not know whether the processing - // times of the left child influence the processing times of the right child) - let ect_left = self.nodes[left_child_of_parent].ect - + self.nodes[right_child_of_parent].sum_of_processing_times; - self.nodes[parent].ect = max(self.nodes[right_child_of_parent].ect, ect_left); - - // The sum of processing times (including one element of lambda) is either: - // 1) The sum of processing times of the right child + the sum of processing times of - // the left child including one element of lambda - // 2) The sum of processing times of the left child + the sum of processing times of the - // right child include one element of lambda - let sum_of_processing_times_left_child_lambda = self.nodes[left_child_of_parent] - .sum_of_processing_times_bar - + self.nodes[right_child_of_parent].sum_of_processing_times; - let sum_of_processing_times_right_child_lambda = self.nodes[left_child_of_parent] - .sum_of_processing_times - + self.nodes[right_child_of_parent].sum_of_processing_times_bar; - self.nodes[parent].sum_of_processing_times_bar = max( - sum_of_processing_times_left_child_lambda, - sum_of_processing_times_right_child_lambda, - ); - - // The earliest completion time (including one element of lambda) is either: - // 1) The earliest completion time including one element of lambda from the right child - // 2) The earliest completion time of the right child + the sum of processing times - // including one element of lambda of the right child - // 2) The earliest completion time of the left child + the sum of processing times - // including one element of lambda of the left child - let ect_right_child_lambda = self.nodes[left_child_of_parent].ect - + self.nodes[right_child_of_parent].sum_of_processing_times_bar; - let ect_left_child_lambda = self.nodes[left_child_of_parent].ect_bar - + self.nodes[right_child_of_parent].sum_of_processing_times; - self.nodes[parent].ect_bar = max( - self.nodes[right_child_of_parent].ect_bar, - max(ect_right_child_lambda, ect_left_child_lambda), - ); - - index = parent; - } - } -}