From a6cdcb4ff44cf255aad38dfa2fccbf013382984c Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Mon, 30 Mar 2026 15:19:05 +0200 Subject: [PATCH 1/4] fix: time-table checker not passing with holes --- .../cumulative/time_table/checker.rs | 203 ++++++++---------- 1 file changed, 88 insertions(+), 115 deletions(-) diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs index 83790b842..6a33ddbb9 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs @@ -6,8 +6,6 @@ use pumpkin_checking::InferenceChecker; use pumpkin_checking::IntExt; use pumpkin_checking::VariableState; -use crate::cumulative::time_table::time_table_util::has_overlap_with_interval; - #[derive(Clone, Debug)] pub struct TimeTableChecker { pub tasks: Box<[CheckerTask]>, @@ -21,66 +19,12 @@ pub struct CheckerTask { pub processing_time: i32, } -fn lower_bound_can_be_propagated_by_profile< - Var: CheckerVariable, - Atomic: AtomicConstraint, ->( - context: &VariableState, - lower_bound: i32, +fn can_be_propagated_by_profile, Atomic: AtomicConstraint>( task: &CheckerTask, - start: i32, - end: i32, height: i32, capacity: i32, ) -> bool { - let upper_bound = task - .start_time - .induced_upper_bound(context) - .try_into() - .unwrap(); - height + task.resource_usage > capacity - && !(upper_bound < (lower_bound + task.processing_time) - && has_overlap_with_interval( - upper_bound, - lower_bound + task.processing_time, - start, - end, - )) - && has_overlap_with_interval(lower_bound, upper_bound + task.processing_time, start, end) - && (lower_bound + task.processing_time) > start - && lower_bound <= end -} - -fn upper_bound_can_be_propagated_by_profile< - Var: CheckerVariable, - Atomic: AtomicConstraint, ->( - context: &VariableState, - upper_bound: i32, - task: &CheckerTask, - start: i32, - end: i32, - height: i32, - capacity: i32, -) -> bool { - let lower_bound = task - .start_time - .induced_lower_bound(context) - .try_into() - .unwrap(); - - height + task.resource_usage > capacity - && !(upper_bound < (lower_bound + task.processing_time) - && has_overlap_with_interval( - upper_bound, - lower_bound + task.processing_time, - start, - end, - )) - && has_overlap_with_interval(lower_bound, upper_bound + task.processing_time, start, end) - && (upper_bound + task.processing_time) > end - && upper_bound <= end } impl InferenceChecker for TimeTableChecker @@ -90,7 +34,7 @@ where { fn check( &self, - state: VariableState, + mut state: VariableState, _: &[Atomic], consequent: Option<&Atomic>, ) -> bool { @@ -117,30 +61,12 @@ where .try_into() .unwrap(); - if lst < est + task.processing_time { - *profile.entry(lst).or_insert(0) += task.resource_usage; - *profile.entry(est + task.processing_time).or_insert(0) -= task.resource_usage; - } - } - - let mut profiles = Vec::new(); - let mut current_usage = 0; - let mut previous_time_point = *profile - .first_key_value() - .expect("Expected at least one mandatory part") - .0; - for (time_point, usage) in profile.iter() { - if current_usage > 0 && *time_point != previous_time_point { - profiles.push((previous_time_point, *time_point - 1, current_usage)) - } - - current_usage += *usage; - - if current_usage > self.capacity { - return true; + for t in lst..est + task.processing_time { + *profile.entry(t).or_insert(0) += task.resource_usage; + if *profile.get(&t).unwrap() > self.capacity { + return true; + } } - - previous_time_point = *time_point; } if let Some(propagating_task) = consequent.map(|consequent| { @@ -149,48 +75,32 @@ where .find(|task| task.start_time.does_atomic_constrain_self(consequent)) .expect("If there is a consequent, then there should be a propagating task") }) { - let mut lower_bound: i32 = propagating_task + let lst: i32 = propagating_task .start_time - .induced_lower_bound(&state) + .induced_upper_bound(&state) .try_into() .unwrap(); - for (start, end_inclusive, height) in profiles.iter() { - if lower_bound_can_be_propagated_by_profile( - &state, - lower_bound, - propagating_task, - *start, - *end_inclusive, - *height, - self.capacity, - ) { - lower_bound = end_inclusive + 1; - } - } - if lower_bound > propagating_task.start_time.induced_upper_bound(&state) { - return true; - } - - let mut upper_bound: i32 = propagating_task + let est: i32 = propagating_task .start_time - .induced_upper_bound(&state) + .induced_lower_bound(&state) .try_into() .unwrap(); - for (start, end_inclusive, height) in profiles.iter().rev() { - if upper_bound_can_be_propagated_by_profile( - &state, - upper_bound, - propagating_task, - *start, - *end_inclusive, - *height, - self.capacity, - ) { - upper_bound = start - propagating_task.processing_time; + + for t in lst..est + propagating_task.processing_time { + *profile.entry(t).or_insert(0) += propagating_task.resource_usage; + if *profile.get(&t).unwrap() > self.capacity { + return true; } } - if upper_bound < propagating_task.start_time.induced_lower_bound(&state) { - return true; + + for (t, height) in profile.iter() { + if can_be_propagated_by_profile(propagating_task, *height, self.capacity) { + for t in (t - propagating_task.processing_time + 1)..=*t { + if !state.apply(&propagating_task.start_time.atomic_not_equal(t)) { + return true; + } + } + } } } false @@ -573,4 +483,67 @@ mod tests { assert!(checker.check(state, &premises, consequent.as_ref())); } + + #[test] + fn test_holes_in_domain() { + let premises = [ + TestAtomic { + name: "x3", + comparison: pumpkin_checking::Comparison::GreaterEqual, + value: 1, + }, + TestAtomic { + name: "x3", + comparison: pumpkin_checking::Comparison::LessEqual, + value: 3, + }, + TestAtomic { + name: "x1", + comparison: pumpkin_checking::Comparison::GreaterEqual, + value: 4, + }, + TestAtomic { + name: "x1", + comparison: pumpkin_checking::Comparison::LessEqual, + value: 4, + }, + TestAtomic { + name: "x2", + comparison: pumpkin_checking::Comparison::GreaterEqual, + value: 2, + }, + ]; + + let consequent = Some(TestAtomic { + name: "x2", + comparison: pumpkin_checking::Comparison::GreaterEqual, + value: 5, + }); + let state = VariableState::prepare_for_conflict_check(premises, consequent) + .expect("no conflicting atomics"); + + let checker = TimeTableChecker { + tasks: vec![ + CheckerTask { + start_time: "x3", + resource_usage: 1, + processing_time: 3, + }, + CheckerTask { + start_time: "x2", + resource_usage: 2, + processing_time: 2, + }, + CheckerTask { + start_time: "x1", + resource_usage: 1, + processing_time: 1, + }, + ] + .into(), + capacity: 2, + }; + + assert!(checker.check(state, &premises, consequent.as_ref())); + } } From b99b962e26b066ffb44efa7f808f23216690d6ab Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Mon, 30 Mar 2026 16:03:58 +0200 Subject: [PATCH 2/4] fix: swapping around of values --- .../src/propagators/cumulative/time_table/checker.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs index 6a33ddbb9..31d08cb28 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs @@ -61,7 +61,7 @@ where .try_into() .unwrap(); - for t in lst..est + task.processing_time { + for t in est + task.processing_time..lst { *profile.entry(t).or_insert(0) += task.resource_usage; if *profile.get(&t).unwrap() > self.capacity { return true; @@ -86,7 +86,7 @@ where .try_into() .unwrap(); - for t in lst..est + propagating_task.processing_time { + for t in est + propagating_task.processing_time..lst { *profile.entry(t).or_insert(0) += propagating_task.resource_usage; if *profile.get(&t).unwrap() > self.capacity { return true; From 2c70913794b52b4e5f3827c834117313bbd23b77 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Tue, 31 Mar 2026 08:42:16 +0200 Subject: [PATCH 3/4] Revert "fix: swapping around of values" This reverts commit b99b962e26b066ffb44efa7f808f23216690d6ab. --- .../src/propagators/cumulative/time_table/checker.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs index 31d08cb28..6a33ddbb9 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs @@ -61,7 +61,7 @@ where .try_into() .unwrap(); - for t in est + task.processing_time..lst { + for t in lst..est + task.processing_time { *profile.entry(t).or_insert(0) += task.resource_usage; if *profile.get(&t).unwrap() > self.capacity { return true; @@ -86,7 +86,7 @@ where .try_into() .unwrap(); - for t in est + propagating_task.processing_time..lst { + for t in lst..est + propagating_task.processing_time { *profile.entry(t).or_insert(0) += propagating_task.resource_usage; if *profile.get(&t).unwrap() > self.capacity { return true; From a34897a36623598f62b27fcec8e2ccc979706ac5 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Tue, 31 Mar 2026 08:47:07 +0200 Subject: [PATCH 4/4] fix: remove instead of add --- .../src/propagators/cumulative/time_table/checker.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs index 6a33ddbb9..d475463d6 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs @@ -87,7 +87,7 @@ where .unwrap(); for t in lst..est + propagating_task.processing_time { - *profile.entry(t).or_insert(0) += propagating_task.resource_usage; + *profile.entry(t).or_insert(0) -= propagating_task.resource_usage; if *profile.get(&t).unwrap() > self.capacity { return true; }