Skip to content

fix: Time-table checker not detecting conflicts properly #405

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
ImkoMarijnissen merged 4 commits into from
Apr 1, 2026
Merged

fix: Time-table checker not detecting conflicts properly #405

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
a6cdcb4
fix: time-table checker not passing with holes
ImkoMarijnissen Mar 30, 2026
b99b962
fix: swapping around of values
ImkoMarijnissen Mar 30, 2026
2c70913
Revert "fix: swapping around of values"
ImkoMarijnissen Mar 31, 2026
a34897a
fix: remove instead of add
ImkoMarijnissen Mar 31, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
203 changes: 88 additions & 115 deletions pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<Var> {
pub tasks: Box<[CheckerTask<Var>]>,
Expand All @@ -21,66 +19,12 @@ pub struct CheckerTask<Var> {
pub processing_time: i32,
}

fn lower_bound_can_be_propagated_by_profile<
Var: CheckerVariable<Atomic>,
Atomic: AtomicConstraint,
>(
context: &VariableState<Atomic>,
lower_bound: i32,
fn can_be_propagated_by_profile<Var: CheckerVariable<Atomic>, Atomic: AtomicConstraint>(
task: &CheckerTask<Var>,
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>,
Atomic: AtomicConstraint,
>(
context: &VariableState<Atomic>,
upper_bound: i32,
task: &CheckerTask<Var>,
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<Var, Atomic> InferenceChecker<Atomic> for TimeTableChecker<Var>
Expand All @@ -90,7 +34,7 @@ where
{
fn check(
&self,
state: VariableState<Atomic>,
mut state: VariableState<Atomic>,
_: &[Atomic],
consequent: Option<&Atomic>,
) -> bool {
Expand All @@ -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| {
Expand All @@ -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
Expand Down Expand Up @@ -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()));
}
}
Loading