diff --git a/minizinc/lib/fzn_cumulative.mzn b/minizinc/lib/fzn_cumulative.mzn index f51922d27..896015dbf 100644 --- a/minizinc/lib/fzn_cumulative.mzn +++ b/minizinc/lib/fzn_cumulative.mzn @@ -13,93 +13,9 @@ predicate fzn_cumulative(array[int] of var int: s, /\ if is_fixed(d) /\ is_fixed(r) /\ is_fixed(b) then pumpkin_cumulative(s, fix(d), fix(r), fix(b)) else - fzn_decomposition_cumulative(s, d, r, b) + pumpkin_cumulative_vars(s, d, r, b) endif ); -% The following predicate is taken from https://github.com/MiniZinc/libminizinc/blob/2.5.5/share/minizinc/std/cumulative.mzn -predicate fzn_decomposition_cumulative(array[int] of var int: s, - array[int] of var int: d, - array[int] of var int: r, - var int: b) = - assert(index_set(s) == index_set(d) /\ index_set(s) == index_set(r), - "cumulative: the 3 array arguments must have identical index sets", - if length(s) >= 1 then - assert(lb_array(d) >= 0 /\ lb_array(r) >= 0, - "cumulative: durations and resource usages must be non-negative", - if - %% the previous test will not work for resources usages like [2,3,3,4,4] with a bound of 4 since the 2 appears exactly once - let { int: mr = lb_array(r); - int: mri = arg_min([ lb(r[i]) | i in index_set(r) ]) } in - forall(i in index_set(r)) - (is_fixed(r[i]) /\ (fix(r[i]) + mr > ub(b) \/ i = mri)) - then - if forall(i in index_set(d))(is_fixed(d[i]) /\ fix(d[i]) == 1) - then - all_different(s) - else - disjunctive(s, d) - endif - else - decomposition_cumulative(s, d, r, b) - endif - ) - endif); - -% The following predicate is taken from https://github.com/MiniZinc/libminizinc/blob/2.5.5/share/minizinc/std/fzn_cumulative.mzn -predicate decomposition_cumulative(array[int] of var int: s, - array[int] of var int: d, - array[int] of var int: r, var int: b) = - let { - set of int: Tasks = - {i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 } - } in - if 0==card(Tasks) then /*true*/ 0==card(index_set(s)) \/ b>=0 - else - let { - int: early = min([ lb(s[i]) | i in Tasks ]), - int: late = max([ ub(s[i]) + ub(d[i]) | i in Tasks ]) - } in ( - if late - early > 5000 then - fzn_cumulative_task(s, d, r, b) - else - fzn_cumulative_time(s, d, r, b) - endif - ) - endif - ; - -% The following predicate is taken from https://github.com/MiniZinc/libminizinc/blob/2.5.5/share/minizinc/std/fzn_cumulative.mzn -predicate fzn_cumulative_time(array[int] of var int: s, - array[int] of var int: d, - array[int] of var int: r, var int: b) = - let { - set of int: Tasks = - {i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 }, - int: early = min([ lb(s[i]) | i in Tasks ]), - int: late = max([ ub(s[i]) + ub(d[i]) | i in Tasks ]) - } in ( - forall( t in early..late ) ( - b >= sum( i in Tasks ) ( - bool2int(s[i] <= t /\ t < s[i] + d[i]) * r[i] - ) - ) - ); - -% The following predicate is taken from https://github.com/MiniZinc/libminizinc/blob/2.5.5/share/minizinc/std/fzn_cumulative.mzn -predicate fzn_cumulative_task(array[int] of var int: s, - array[int] of var int: d, - array[int] of var int: r, var int: b) = - let { - set of int: Tasks = - {i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 } - } in ( - forall( j in Tasks ) ( - b >= r[j] + sum( i in Tasks where i != j ) ( - bool2int(s[i] <= s[j] /\ s[j] < s[i] + d[i] ) * r[i] - ) - ) - ); - predicate pumpkin_cumulative(array[int] of var int: s, array[int] of int: d, array[int] of int: r, int: b); -predicate pumpkin_cumulative_vars(array[int] of var int: s, array[int] of var int: d, array[int] of var int: r, var int: b); \ No newline at end of file +predicate pumpkin_cumulative_vars(array[int] of var int: s, array[int] of var int: d, array[int] of var int: r, var int: b); diff --git a/pumpkin-crates/core/src/api/mod.rs b/pumpkin-crates/core/src/api/mod.rs index aeb8de03f..89cb45a08 100644 --- a/pumpkin-crates/core/src/api/mod.rs +++ b/pumpkin-crates/core/src/api/mod.rs @@ -59,6 +59,7 @@ pub mod constraint_arguments { //! Contains inputs to constraints. pub use crate::propagators::ArgDisjunctiveTask; + pub use crate::propagators::ArgTask; pub use crate::propagators::CumulativeExplanationType; pub use crate::propagators::CumulativeOptions; pub use crate::propagators::CumulativePropagationMethod; diff --git a/pumpkin-crates/core/src/api/solver.rs b/pumpkin-crates/core/src/api/solver.rs index 95f01a5fe..9d71bea61 100644 --- a/pumpkin-crates/core/src/api/solver.rs +++ b/pumpkin-crates/core/src/api/solver.rs @@ -165,6 +165,10 @@ impl Solver { pub fn upper_bound(&self, variable: &impl IntegerVariable) -> i32 { self.satisfaction_solver.get_upper_bound(variable) } + + pub(crate) fn is_fixed(&self, variable: &impl IntegerVariable) -> bool { + self.lower_bound(variable) == self.upper_bound(variable) + } } /// Functions to create and retrieve integer and propositional variables. diff --git a/pumpkin-crates/core/src/constraints/cumulative.rs b/pumpkin-crates/core/src/constraints/cumulative.rs index 519fd5cbc..ddcbba9a5 100644 --- a/pumpkin-crates/core/src/constraints/cumulative.rs +++ b/pumpkin-crates/core/src/constraints/cumulative.rs @@ -1,4 +1,4 @@ -use std::fmt::Debug; +use log::info; use super::Constraint; use crate::ConstraintOperationError; @@ -7,11 +7,10 @@ use crate::constraint_arguments::CumulativePropagationMethod; use crate::proof::ConstraintTag; use crate::propagators::ArgTask; use crate::propagators::CumulativeOptions; -use crate::propagators::TimeTableOverIntervalIncrementalPropagator; -use crate::propagators::TimeTableOverIntervalPropagator; -use crate::propagators::TimeTablePerPointIncrementalPropagator; -use crate::propagators::TimeTablePerPointPropagator; -use crate::pumpkin_assert_simple; +use crate::propagators::TimeTableOverIntervalConstructor; +use crate::propagators::TimeTableOverIntervalIncrementalConstructor; +use crate::propagators::TimeTablePerPointConstructor; +use crate::propagators::TimeTablePerPointIncrementalConstructor; use crate::variables::IntegerVariable; use crate::variables::Literal; @@ -44,6 +43,7 @@ use crate::variables::Literal; /// # use pumpkin_core::constraints; /// # use pumpkin_core::constraints::Constraint; /// # use crate::pumpkin_core::results::ProblemSolution; +/// # use pumpkin_core::constraint_arguments::ArgTask; /// let solver = Solver::default(); /// /// let mut solver = Solver::default(); @@ -61,9 +61,23 @@ use crate::variables::Literal; /// /// solver /// .add_constraint(constraints::cumulative( -/// start_times.clone(), -/// durations.clone(), -/// resource_requirements.clone(), +/// [ +/// ArgTask { +/// start_time: start_0, +/// processing_time: 5, +/// resource_usage: 1, +/// }, +/// ArgTask { +/// start_time: start_1, +/// processing_time: 2, +/// resource_usage: 1, +/// }, +/// ArgTask { +/// start_time: start_2, +/// processing_time: 5, +/// resource_usage: 2, +/// }, +/// ], /// resource_capacity, /// constraint_tag, /// )) @@ -123,26 +137,18 @@ use crate::variables::Literal; /// cumulative constraint’, in Principles and Practice of Constraint Programming: 21st /// International Conference, CP 2015, Cork, Ireland, August 31--September 4, 2015, Proceedings /// 21, 2015, pp. 149–157. -pub fn cumulative( - start_times: StartTimes, - durations: Durations, - resource_requirements: ResourceRequirements, - resource_capacity: i32, +pub fn cumulative< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( + tasks: impl IntoIterator>, + resource_capacity: CVar, constraint_tag: ConstraintTag, -) -> impl Constraint -where - StartTimes: IntoIterator, - StartTimes::Item: IntegerVariable + Debug + 'static, - StartTimes::IntoIter: ExactSizeIterator, - Durations: IntoIterator, - Durations::IntoIter: ExactSizeIterator, - ResourceRequirements: IntoIterator, - ResourceRequirements::IntoIter: ExactSizeIterator, -{ +) -> impl Constraint { cumulative_with_options( - start_times, - durations, - resource_requirements, + tasks, resource_capacity, CumulativeOptions::default(), constraint_tag, @@ -153,59 +159,42 @@ where /// with the provided [`CumulativeOptions`]. /// /// See the documentation of [`cumulative`] for more information about the constraint. -pub fn cumulative_with_options( - start_times: StartTimes, - durations: Durations, - resource_requirements: ResourceRequirements, - resource_capacity: i32, +pub fn cumulative_with_options< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( + tasks: impl IntoIterator>, + resource_capacity: CVar, options: CumulativeOptions, constraint_tag: ConstraintTag, -) -> impl Constraint -where - StartTimes: IntoIterator, - StartTimes::Item: IntegerVariable + Debug + 'static, - StartTimes::IntoIter: ExactSizeIterator, - Durations: IntoIterator, - Durations::IntoIter: ExactSizeIterator, - ResourceRequirements: IntoIterator, - ResourceRequirements::IntoIter: ExactSizeIterator, -{ - let start_times = start_times.into_iter(); - let durations = durations.into_iter(); - let resource_requirements = resource_requirements.into_iter(); - - pumpkin_assert_simple!( - start_times.len() == durations.len() && durations.len() == resource_requirements.len(), - "The number of start variables, durations and resource requirements should be the same!" - ); - - CumulativeConstraint::new( - &start_times - .zip(durations) - .zip(resource_requirements) - .map(|((start_time, duration), resource_requirement)| ArgTask { - start_time, - processing_time: duration, - resource_usage: resource_requirement, - }) - .collect::>(), +) -> impl Constraint { + CumulativeConstraint::::new( + &tasks.into_iter().collect::>(), resource_capacity, options, constraint_tag, ) } -struct CumulativeConstraint { - tasks: Vec>, - resource_capacity: i32, +struct CumulativeConstraint { + tasks: Vec>, + resource_capacity: CVar, options: CumulativeOptions, constraint_tag: ConstraintTag, } -impl CumulativeConstraint { +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +> CumulativeConstraint +{ fn new( - tasks: &[ArgTask], - resource_capacity: i32, + tasks: &[ArgTask], + resource_capacity: CVar, options: CumulativeOptions, constraint_tag: ConstraintTag, ) -> Self { @@ -217,13 +206,67 @@ impl CumulativeConstraint { constraint_tag, } } + + fn swap_if_variable(&mut self, solver: &Solver, capacity: CVar) { + let mut resource_usage_constant = true; + let mut duration_constant = true; + let capacity_constant = solver.is_fixed(&capacity); + + for task in self.tasks.iter() { + if !solver.is_fixed(&task.resource_usage) { + resource_usage_constant = false; + } + + if !solver.is_fixed(&task.processing_time) { + duration_constant = false; + } + } + + let is_variable = !resource_usage_constant || !duration_constant || !capacity_constant; + let result = match self.options.propagation_method { + CumulativePropagationMethod::TimeTablePerPointIncremental if is_variable => { + info!( + "Could not use incremental version when having either variable resource usage or duration, switching to non-incremental version" + ); + CumulativePropagationMethod::TimeTablePerPoint + } + CumulativePropagationMethod::TimeTablePerPointIncrementalSynchronised => { + info!( + "Could not use incremental version when having either variable resource usage or duration, switching to non-incremental version" + ); + CumulativePropagationMethod::TimeTablePerPoint + } + CumulativePropagationMethod::TimeTableOverIntervalIncremental => { + info!( + "Could not use incremental version when having either variable resource usage or duration, switching to non-incremental version" + ); + CumulativePropagationMethod::TimeTableOverInterval + } + CumulativePropagationMethod::TimeTableOverIntervalIncrementalSynchronised => { + info!( + "Could not use incremental version when having either variable resource usage or duration, switching to non-incremental version" + ); + CumulativePropagationMethod::TimeTableOverInterval + } + other => other, + }; + + self.options.propagation_method = result; + } } -impl Constraint for CumulativeConstraint { - fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> { +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +> Constraint for CumulativeConstraint +{ + fn post(mut self, solver: &mut Solver) -> Result<(), ConstraintOperationError> { + self.swap_if_variable(solver, self.resource_capacity.clone()); match self.options.propagation_method { - CumulativePropagationMethod::TimeTablePerPoint => TimeTablePerPointPropagator::new( - &self.tasks, + CumulativePropagationMethod::TimeTablePerPoint => TimeTablePerPointConstructor::new( + self.tasks, self.resource_capacity, self.options.propagator_options, self.constraint_tag, @@ -231,8 +274,8 @@ impl Constraint for CumulativeConstraint .post(solver), CumulativePropagationMethod::TimeTablePerPointIncremental => { - TimeTablePerPointIncrementalPropagator::::new( - &self.tasks, + TimeTablePerPointIncrementalConstructor::::new( + self.tasks, self.resource_capacity, self.options.propagator_options, self.constraint_tag, @@ -240,8 +283,8 @@ impl Constraint for CumulativeConstraint .post(solver) } CumulativePropagationMethod::TimeTablePerPointIncrementalSynchronised => { - TimeTablePerPointIncrementalPropagator::::new( - &self.tasks, + TimeTablePerPointIncrementalConstructor::::new( + self.tasks, self.resource_capacity, self.options.propagator_options, self.constraint_tag, @@ -249,8 +292,8 @@ impl Constraint for CumulativeConstraint .post(solver) } CumulativePropagationMethod::TimeTableOverInterval => { - TimeTableOverIntervalPropagator::new( - &self.tasks, + TimeTableOverIntervalConstructor::new( + self.tasks, self.resource_capacity, self.options.propagator_options, self.constraint_tag, @@ -258,8 +301,8 @@ impl Constraint for CumulativeConstraint .post(solver) } CumulativePropagationMethod::TimeTableOverIntervalIncremental => { - TimeTableOverIntervalIncrementalPropagator::::new( - &self.tasks, + TimeTableOverIntervalIncrementalConstructor::::new( + self.tasks, self.resource_capacity, self.options.propagator_options, self.constraint_tag, @@ -267,8 +310,8 @@ impl Constraint for CumulativeConstraint .post(solver) } CumulativePropagationMethod::TimeTableOverIntervalIncrementalSynchronised => { - TimeTableOverIntervalIncrementalPropagator::::new( - &self.tasks, + TimeTableOverIntervalIncrementalConstructor::::new( + self.tasks, self.resource_capacity, self.options.propagator_options, self.constraint_tag, @@ -279,21 +322,22 @@ impl Constraint for CumulativeConstraint } fn implied_by( - self, + mut self, solver: &mut Solver, reification_literal: Literal, ) -> Result<(), ConstraintOperationError> { + self.swap_if_variable(solver, self.resource_capacity.clone()); match self.options.propagation_method { - CumulativePropagationMethod::TimeTablePerPoint => TimeTablePerPointPropagator::new( - &self.tasks, + CumulativePropagationMethod::TimeTablePerPoint => TimeTablePerPointConstructor::new( + self.tasks, self.resource_capacity, self.options.propagator_options, self.constraint_tag, ) .implied_by(solver, reification_literal), CumulativePropagationMethod::TimeTablePerPointIncremental => { - TimeTablePerPointIncrementalPropagator::::new( - &self.tasks, + TimeTablePerPointIncrementalConstructor::::new( + self.tasks, self.resource_capacity, self.options.propagator_options, self.constraint_tag, @@ -301,8 +345,8 @@ impl Constraint for CumulativeConstraint .implied_by(solver, reification_literal) } CumulativePropagationMethod::TimeTablePerPointIncrementalSynchronised => { - TimeTablePerPointIncrementalPropagator::::new( - &self.tasks, + TimeTablePerPointIncrementalConstructor::::new( + self.tasks, self.resource_capacity, self.options.propagator_options, self.constraint_tag, @@ -310,8 +354,8 @@ impl Constraint for CumulativeConstraint .implied_by(solver, reification_literal) } CumulativePropagationMethod::TimeTableOverInterval => { - TimeTableOverIntervalPropagator::new( - &self.tasks, + TimeTableOverIntervalConstructor::new( + self.tasks, self.resource_capacity, self.options.propagator_options, self.constraint_tag, @@ -319,8 +363,8 @@ impl Constraint for CumulativeConstraint .implied_by(solver, reification_literal) } CumulativePropagationMethod::TimeTableOverIntervalIncremental => { - TimeTableOverIntervalIncrementalPropagator::::new( - &self.tasks, + TimeTableOverIntervalIncrementalConstructor::::new( + self.tasks, self.resource_capacity, self.options.propagator_options, self.constraint_tag, @@ -328,8 +372,8 @@ impl Constraint for CumulativeConstraint .implied_by(solver, reification_literal) } CumulativePropagationMethod::TimeTableOverIntervalIncrementalSynchronised => { - TimeTableOverIntervalIncrementalPropagator::::new( - &self.tasks, + TimeTableOverIntervalIncrementalConstructor::::new( + self.tasks, self.resource_capacity, self.options.propagator_options, self.constraint_tag, diff --git a/pumpkin-crates/core/src/engine/cp/test_solver.rs b/pumpkin-crates/core/src/engine/cp/test_solver.rs index 92053c1ee..9bd21c2a7 100644 --- a/pumpkin-crates/core/src/engine/cp/test_solver.rs +++ b/pumpkin-crates/core/src/engine/cp/test_solver.rs @@ -318,6 +318,23 @@ impl TestSolver { ); } + pub(crate) fn get_reason_empty_domain(&mut self) -> Vec { + let entry_reason = self.assignments.remove_last_trail_element().1; + let mut reason_scratch = vec![]; + let _ = self.reason_store.get_or_compute( + entry_reason, + ExplanationContext::without_working_nogood( + &self.assignments, + self.assignments.num_trail_entries() - 1, + &mut self.notification_engine, + ), + &mut self.propagator_store, + &mut reason_scratch, + ); + + reason_scratch + } + pub(crate) fn get_reason_int(&mut self, predicate: Predicate) -> PropositionalConjunction { let reason_ref = self .assignments diff --git a/pumpkin-crates/core/src/engine/variables/constant.rs b/pumpkin-crates/core/src/engine/variables/constant.rs new file mode 100644 index 000000000..bae0afffd --- /dev/null +++ b/pumpkin-crates/core/src/engine/variables/constant.rs @@ -0,0 +1,127 @@ +use crate::engine::Assignments; +use crate::engine::notifications::DomainEvent; +use crate::engine::notifications::OpaqueDomainEvent; +use crate::predicates::Predicate; +use crate::predicates::PredicateConstructor; +use crate::variables::IntegerVariable; +use crate::variables::TransformableVariable; + +impl IntegerVariable for i32 { + type AffineView = i32; + + fn lower_bound(&self, _assignment: &Assignments) -> i32 { + *self + } + + fn lower_bound_at_trail_position( + &self, + _assignment: &Assignments, + _trail_position: usize, + ) -> i32 { + *self + } + + fn upper_bound(&self, _assignment: &Assignments) -> i32 { + *self + } + + fn upper_bound_at_trail_position( + &self, + _assignment: &Assignments, + _trail_position: usize, + ) -> i32 { + *self + } + + fn contains(&self, _assignment: &Assignments, value: i32) -> bool { + value == *self + } + + fn contains_at_trail_position( + &self, + assignment: &Assignments, + value: i32, + _trail_position: usize, + ) -> bool { + self.contains(assignment, value) + } + + fn iterate_domain(&self, _assignment: &Assignments) -> impl Iterator { + std::iter::once(*self) + } + + fn watch_all( + &self, + _watchers: &mut crate::engine::notifications::Watchers<'_>, + _events: enumset::EnumSet, + ) { + } + + fn watch_all_backtrack( + &self, + _watchers: &mut crate::engine::notifications::Watchers<'_>, + _events: enumset::EnumSet, + ) { + } + + fn unpack_event(&self, _event: OpaqueDomainEvent) -> DomainEvent { + unreachable!("A constant should never be able to notify of an event") + } + + fn get_holes_on_current_decision_level( + &self, + _assignments: &Assignments, + ) -> impl Iterator { + std::iter::empty() + } + + fn get_holes(&self, _assignments: &Assignments) -> impl Iterator { + std::iter::empty() + } +} + +impl PredicateConstructor for i32 { + type Value = i32; + + fn lower_bound_predicate(&self, bound: Self::Value) -> Predicate { + if bound <= *self { + Predicate::trivially_true() + } else { + Predicate::trivially_false() + } + } + + fn upper_bound_predicate(&self, bound: Self::Value) -> Predicate { + if bound >= *self { + Predicate::trivially_true() + } else { + Predicate::trivially_false() + } + } + + fn equality_predicate(&self, bound: Self::Value) -> Predicate { + if bound == *self { + Predicate::trivially_true() + } else { + Predicate::trivially_false() + } + } + + fn disequality_predicate(&self, bound: Self::Value) -> Predicate { + if bound != *self { + Predicate::trivially_true() + } else { + Predicate::trivially_false() + } + } +} + +impl TransformableVariable for i32 { + fn scaled(&self, scale: i32) -> i32 { + *self * scale + } + + fn offset(&self, offset: i32) -> i32 { + *self + offset + } +} diff --git a/pumpkin-crates/core/src/engine/variables/mod.rs b/pumpkin-crates/core/src/engine/variables/mod.rs index 3c5b00bcd..42837e402 100644 --- a/pumpkin-crates/core/src/engine/variables/mod.rs +++ b/pumpkin-crates/core/src/engine/variables/mod.rs @@ -3,6 +3,7 @@ //! constraints. mod affine_view; +mod constant; mod domain_generator_iterator; mod domain_id; mod integer_variable; diff --git a/pumpkin-crates/core/src/propagators/cumulative/mod.rs b/pumpkin-crates/core/src/propagators/cumulative/mod.rs index 8f1ce41d6..f9e4c216a 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/mod.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/mod.rs @@ -43,26 +43,41 @@ //! # use pumpkin_core::results::SatisfactionResult; //! # use pumpkin_core::constraints; //! # use pumpkin_core::constraints::Constraint; -//! # use crate::pumpkin_core::results::ProblemSolution; +//! # use pumpkin_core::results::ProblemSolution; +//! # use pumpkin_core::constraint_arguments::ArgTask; //! let mut solver = Solver::default(); //! -//! let start_0 = solver.new_bounded_integer(0, 4); -//! let start_1 = solver.new_bounded_integer(0, 4); -//! let start_2 = solver.new_bounded_integer(0, 5); +//! let constraint_tag = solver.new_constraint_tag(); //! -//! let start_times = [start_0, start_1, start_2]; +//! let resource_capacity = 2; //! let durations = [5, 2, 5]; //! let resource_requirements = [1, 1, 2]; -//! let resource_capacity = 2; //! -//! let c1 = solver.new_constraint_tag(); +//! let start_0 = solver.new_bounded_integer(0, 4); +//! let start_1 = solver.new_bounded_integer(0, 4); +//! let start_2 = solver.new_bounded_integer(0, 5); +//! //! solver //! .add_constraint(constraints::cumulative( -//! start_times.clone(), -//! durations.clone(), -//! resource_requirements.clone(), +//! [ +//! ArgTask { +//! start_time: start_0, +//! processing_time: durations[0], +//! resource_usage: resource_requirements[0], +//! }, +//! ArgTask { +//! start_time: start_1, +//! processing_time: durations[1], +//! resource_usage: resource_requirements[1], +//! }, +//! ArgTask { +//! start_time: start_2, +//! processing_time: durations[2], +//! resource_usage: resource_requirements[2], +//! }, +//! ], //! resource_capacity, -//! c1, +//! constraint_tag, //! )) //! .post(); //! @@ -122,4 +137,5 @@ mod options; pub use options::*; mod utils; +pub use utils::ArgTask; pub(crate) use utils::*; diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/big_step.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/big_step.rs index 33b04df36..904e2e0be 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/big_step.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/big_step.rs @@ -12,8 +12,15 @@ use crate::variables::IntegerVariable; /// Creates the propagation explanation using the big-step approach (see /// [`CumulativeExplanationType::BigStep`]) -pub(crate) fn create_big_step_propagation_explanation( - profile: &ResourceProfile, +pub(crate) fn create_big_step_propagation_explanation< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( + context: PropagationContext, + profile: &ResourceProfile, + capacity: CVar, ) -> PropositionalConjunction { profile .profile_tasks @@ -21,18 +28,36 @@ pub(crate) fn create_big_step_propagation_explanation= profile.end - profile_task.processing_time + 1 + profile_task.start_variable + >= profile.end - context.lower_bound(&profile_task.processing_time) + 1 ), predicate!(profile_task.start_variable <= profile.start), + predicate!( + profile_task.processing_time + >= context.lower_bound(&profile_task.processing_time) + ), + predicate!( + profile_task.resource_usage + >= context.lower_bound(&profile_task.resource_usage) + ), ] }) + .chain(std::iter::once(predicate!( + capacity <= context.upper_bound(&capacity) + ))) + .filter(|&predicate| predicate != Predicate::trivially_true()) .collect() } /// Creates the conflict explanation using the big-step approach (see /// [`CumulativeExplanationType::BigStep`]) -pub(crate) fn create_big_step_conflict_explanation( - conflict_profile: &ResourceProfile, +pub(crate) fn create_big_step_conflict_explanation< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + context: PropagationContext, + conflict_profile: &ResourceProfile, ) -> PropositionalConjunction { conflict_profile .profile_tasks @@ -41,40 +66,74 @@ pub(crate) fn create_big_step_conflict_explanation= conflict_profile.end - profile_task.processing_time + 1 + >= conflict_profile.end + - context.lower_bound(&profile_task.processing_time) + + 1 ), predicate!(profile_task.start_variable <= conflict_profile.start), + predicate!( + profile_task.processing_time + >= context.lower_bound(&profile_task.processing_time) + ), + predicate!( + profile_task.resource_usage + >= context.lower_bound(&profile_task.resource_usage) + ), ] }) + .filter(|&predicate| predicate != Predicate::trivially_true()) .collect() } -pub(crate) fn create_big_step_predicate_propagating_task_lower_bound_propagation( - task: &Rc>, - profile: &ResourceProfile, -) -> Predicate +pub(crate) fn create_big_step_predicate_propagating_task_lower_bound_propagation( + context: PropagationContext, + task: &Rc>, + profile: &ResourceProfile, +) -> PropositionalConjunction where Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, { - predicate!(task.start_variable >= profile.start + 1 - task.processing_time) + [ + predicate!( + task.start_variable >= profile.start + 1 - context.lower_bound(&task.processing_time) + ), + predicate!(task.processing_time >= context.lower_bound(&task.processing_time)), + predicate!(task.resource_usage >= context.lower_bound(&task.resource_usage)), + ] + .into_iter() + .filter(|&predicate| predicate != Predicate::trivially_true()) + .collect() } -pub(crate) fn create_big_step_predicate_propagating_task_upper_bound_propagation( - task: &Rc>, - profile: &ResourceProfile, +pub(crate) fn create_big_step_predicate_propagating_task_upper_bound_propagation( + task: &Rc>, + profile: &ResourceProfile, context: PropagationContext, -) -> Predicate +) -> PropositionalConjunction where Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, { - predicate!(task.start_variable <= max(context.upper_bound(&task.start_variable), profile.end)) + [ + predicate!( + task.start_variable <= max(context.upper_bound(&task.start_variable), profile.end) + ), + predicate!(task.processing_time >= context.lower_bound(&task.processing_time)), + predicate!(task.resource_usage >= context.lower_bound(&task.resource_usage)), + ] + .into_iter() + .filter(|&predicate| predicate != Predicate::trivially_true()) + .collect() } #[cfg(test)] mod tests { + use crate::constraint_arguments::CumulativeExplanationType; use crate::predicate; use crate::predicates::PropositionalConjunction; - use crate::propagators::CumulativeExplanationType; use crate::propagators::cumulative::time_table::propagation_handler::test_propagation_handler::TestPropagationHandler; #[test] diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/mod.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/mod.rs index be2b113e2..7273fb8cd 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/mod.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/mod.rs @@ -12,7 +12,6 @@ use pointwise::create_pointwise_predicate_propagating_task_lower_bound_propagati use pointwise::create_pointwise_predicate_propagating_task_upper_bound_propagation; use crate::engine::propagation::PropagationContext; -use crate::predicates::Predicate; use crate::predicates::PropositionalConjunction; use crate::propagators::ResourceProfile; use crate::propagators::Task; @@ -71,36 +70,46 @@ impl Display for CumulativeExplanationType { /// Creates the lower-bound [`Predicate`] of the `propagating_task` based on the `explanation_type`. pub(crate) fn create_predicate_propagating_task_lower_bound_propagation< Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, >( explanation_type: CumulativeExplanationType, context: PropagationContext, - task: &Rc>, - profile: &ResourceProfile, + task: &Rc>, + profile: &ResourceProfile, time_point: Option, -) -> Predicate { +) -> PropositionalConjunction { match explanation_type { CumulativeExplanationType::Naive => { create_naive_predicate_propagating_task_lower_bound_propagation(context, task) } CumulativeExplanationType::BigStep => { - create_big_step_predicate_propagating_task_lower_bound_propagation(task, profile) + create_big_step_predicate_propagating_task_lower_bound_propagation( + context, task, profile, + ) } CumulativeExplanationType::Pointwise => { - create_pointwise_predicate_propagating_task_lower_bound_propagation(task, time_point) + create_pointwise_predicate_propagating_task_lower_bound_propagation( + context, task, time_point, + ) } } } /// Adds the lower-bound predicate of the propagating task to the provided `explanation`. -pub(crate) fn add_propagating_task_predicate_lower_bound( +pub(crate) fn add_propagating_task_predicate_lower_bound< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( mut explanation: PropositionalConjunction, explanation_type: CumulativeExplanationType, context: PropagationContext, - task: &Rc>, - profile: &ResourceProfile, + task: &Rc>, + profile: &ResourceProfile, time_point: Option, ) -> PropositionalConjunction { - explanation.add(create_predicate_propagating_task_lower_bound_propagation( + explanation.extend(create_predicate_propagating_task_lower_bound_propagation( explanation_type, context, task, @@ -113,13 +122,15 @@ pub(crate) fn add_propagating_task_predicate_lower_bound( explanation_type: CumulativeExplanationType, context: PropagationContext, - task: &Rc>, - profile: &ResourceProfile, + task: &Rc>, + profile: &ResourceProfile, time_point: Option, -) -> Predicate { +) -> PropositionalConjunction { match explanation_type { CumulativeExplanationType::Naive => { create_naive_predicate_propagating_task_upper_bound_propagation(context, task) @@ -130,21 +141,27 @@ pub(crate) fn create_predicate_propagating_task_upper_bound_propagation< ) } CumulativeExplanationType::Pointwise => { - create_pointwise_predicate_propagating_task_upper_bound_propagation(task, time_point) + create_pointwise_predicate_propagating_task_upper_bound_propagation( + context, task, time_point, + ) } } } /// Adds the upper-bound predicate of the propagating task to the provided `explanation`. -pub(crate) fn add_propagating_task_predicate_upper_bound( +pub(crate) fn add_propagating_task_predicate_upper_bound< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( mut explanation: PropositionalConjunction, explanation_type: CumulativeExplanationType, context: PropagationContext, - task: &Rc>, - profile: &ResourceProfile, + task: &Rc>, + profile: &ResourceProfile, time_point: Option, ) -> PropositionalConjunction { - explanation.add(create_predicate_propagating_task_upper_bound_propagation( + explanation.extend(create_predicate_propagating_task_upper_bound_propagation( explanation_type, context, task, diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/naive.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/naive.rs index 4c1f1270b..a8e8b2468 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/naive.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/naive.rs @@ -11,9 +11,15 @@ use crate::variables::IntegerVariable; /// Creates the propagation explanation using the naive approach (see /// [`CumulativeExplanationType::Naive`]) -pub(crate) fn create_naive_propagation_explanation( - profile: &ResourceProfile, +pub(crate) fn create_naive_propagation_explanation< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( + profile: &ResourceProfile, context: PropagationContext, + capacity: CVar, ) -> PropositionalConjunction { profile .profile_tasks @@ -28,20 +34,34 @@ pub(crate) fn create_naive_propagation_explanation= context.lower_bound(&profile_task.processing_time) + ), + predicate!( + profile_task.resource_usage + >= context.lower_bound(&profile_task.resource_usage) + ), ] }) + .chain(std::iter::once(predicate!( + capacity <= context.upper_bound(&capacity) + ))) + .filter(|&predicate| predicate != Predicate::trivially_true()) .collect() } /// Creates the conflict explanation using the naive approach (see /// [`CumulativeExplanationType::Naive`]) -pub(crate) fn create_naive_conflict_explanation( - conflict_profile: &ResourceProfile, - context: Context, -) -> PropositionalConjunction -where +pub(crate) fn create_naive_conflict_explanation< Var: IntegerVariable + 'static, -{ + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + Context: ReadDomains + Copy, +>( + conflict_profile: &ResourceProfile, + context: Context, +) -> PropositionalConjunction { conflict_profile .profile_tasks .iter() @@ -55,36 +75,63 @@ where profile_task.start_variable <= context.upper_bound(&profile_task.start_variable) ), + predicate!( + profile_task.processing_time + >= context.lower_bound(&profile_task.processing_time) + ), + predicate!( + profile_task.resource_usage + >= context.lower_bound(&profile_task.resource_usage) + ), ] }) + .filter(|&predicate| predicate != Predicate::trivially_true()) .collect() } -pub(crate) fn create_naive_predicate_propagating_task_lower_bound_propagation( +pub(crate) fn create_naive_predicate_propagating_task_lower_bound_propagation( context: PropagationContext, - task: &Rc>, -) -> Predicate + task: &Rc>, +) -> PropositionalConjunction where Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, { - predicate!(task.start_variable >= context.lower_bound(&task.start_variable)) + [ + predicate!(task.start_variable >= context.lower_bound(&task.start_variable)), + predicate!(task.processing_time >= context.lower_bound(&task.processing_time)), + predicate!(task.resource_usage >= context.lower_bound(&task.resource_usage)), + ] + .into_iter() + .filter(|&predicate| predicate != Predicate::trivially_true()) + .collect() } -pub(crate) fn create_naive_predicate_propagating_task_upper_bound_propagation( +pub(crate) fn create_naive_predicate_propagating_task_upper_bound_propagation( context: PropagationContext, - task: &Rc>, -) -> Predicate + task: &Rc>, +) -> PropositionalConjunction where Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, { - predicate!(task.start_variable <= context.upper_bound(&task.start_variable)) + [ + predicate!(task.start_variable <= context.upper_bound(&task.start_variable)), + predicate!(task.processing_time >= context.lower_bound(&task.processing_time)), + predicate!(task.resource_usage >= context.lower_bound(&task.resource_usage)), + ] + .into_iter() + .filter(|&predicate| predicate != Predicate::trivially_true()) + .collect() } #[cfg(test)] mod tests { + use crate::constraint_arguments::CumulativeExplanationType; use crate::predicate; use crate::predicates::PropositionalConjunction; - use crate::propagators::CumulativeExplanationType; use crate::propagators::cumulative::time_table::propagation_handler::test_propagation_handler::TestPropagationHandler; #[test] diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/pointwise.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/pointwise.rs index 2348a9117..cfab161d1 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/pointwise.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/pointwise.rs @@ -2,6 +2,7 @@ use std::rc::Rc; use crate::constraint_arguments::CumulativeExplanationType; use crate::engine::EmptyDomain; +use crate::engine::propagation::PropagationContext; use crate::engine::propagation::PropagationContextMut; use crate::engine::propagation::ReadDomains; use crate::engine::propagation::contexts::propagation_context::HasAssignments; @@ -17,10 +18,16 @@ use crate::pumpkin_assert_extreme; use crate::pumpkin_assert_simple; use crate::variables::IntegerVariable; -pub(crate) fn propagate_lower_bounds_with_pointwise_explanations( +pub(crate) fn propagate_lower_bounds_with_pointwise_explanations< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( context: &mut PropagationContextMut, - profiles: &[&ResourceProfile], - propagating_task: &Rc>, + profiles: &[&ResourceProfile], + propagating_task: &Rc>, + capacity: CVar, inference_code: InferenceCode, ) -> Result<(), EmptyDomain> { // The time points should follow the following properties (based on `Improving @@ -43,7 +50,8 @@ pub(crate) fn propagate_lower_bounds_with_pointwise_explanations= t_l + 1 - p]`, and this predicate holds only if the -1 is added) let mut time_point = profiles[current_profile_index].end.min( - context.lower_bound(&propagating_task.start_variable) + propagating_task.processing_time + context.lower_bound(&propagating_task.start_variable) + + context.lower_bound(&propagating_task.processing_time) - 1, ); let mut should_exit = false; @@ -60,8 +68,10 @@ pub(crate) fn propagate_lower_bounds_with_pointwise_explanations= context.lower_bound(&propagating_task.start_variable) { let explanation = add_propagating_task_predicate_lower_bound( create_pointwise_propagation_explanation( + context.as_readonly(), time_point, profiles[current_profile_index], + capacity.clone(), ), CumulativeExplanationType::Pointwise, context.as_readonly(), @@ -87,7 +97,7 @@ pub(crate) fn propagate_lower_bounds_with_pointwise_explanations profiles[current_profile_index].end { @@ -126,10 +136,16 @@ pub(crate) fn propagate_lower_bounds_with_pointwise_explanations( +pub(crate) fn propagate_upper_bounds_with_pointwise_explanations< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( context: &mut PropagationContextMut, - profiles: &[&ResourceProfile], - propagating_task: &Rc>, + profiles: &[&ResourceProfile], + propagating_task: &Rc>, + capacity: CVar, inference_code: InferenceCode, ) -> Result<(), EmptyDomain> { // The time points should follow the following properties (based on `Improving @@ -164,13 +180,15 @@ pub(crate) fn propagate_upper_bounds_with_pointwise_explanations( +pub(crate) fn create_pointwise_propagation_explanation< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( + context: PropagationContext, time_point: i32, - profile: &ResourceProfile, + profile: &ResourceProfile, + capacity: CVar, ) -> PropositionalConjunction { profile .profile_tasks @@ -245,18 +270,36 @@ pub(crate) fn create_pointwise_propagation_explanation= time_point + 1 - profile_task.processing_time + profile_task.start_variable + >= time_point + 1 - context.lower_bound(&profile_task.processing_time) ), predicate!(profile_task.start_variable <= time_point), + predicate!( + profile_task.processing_time + >= context.lower_bound(&profile_task.processing_time) + ), + predicate!( + profile_task.resource_usage + >= context.lower_bound(&profile_task.resource_usage) + ), ] }) + .chain(std::iter::once(predicate!( + capacity <= context.upper_bound(&capacity) + ))) + .filter(|&predicate| predicate != Predicate::trivially_true()) .collect() } /// Creates the conflict explanation using the point-wise approach (see /// [`CumulativeExplanationType::PointWise`]) -pub(crate) fn create_pointwise_conflict_explanation( - conflict_profile: &ResourceProfile, +pub(crate) fn create_pointwise_conflict_explanation< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + context: PropagationContext, + conflict_profile: &ResourceProfile, ) -> PropositionalConjunction { // As stated in improving scheduling by learning, we choose the middle point; this // could potentially be improved @@ -271,49 +314,79 @@ pub(crate) fn create_pointwise_conflict_explanation= middle_point + 1 - profile_task.processing_time + profile_task.start_variable + >= middle_point + 1 - context.lower_bound(&profile_task.processing_time) ), predicate!(profile_task.start_variable <= middle_point), + predicate!( + profile_task.processing_time + >= context.lower_bound(&profile_task.processing_time) + ), + predicate!( + profile_task.resource_usage + >= context.lower_bound(&profile_task.resource_usage) + ), ] }) + .filter(|&predicate| predicate != Predicate::trivially_true()) .collect() } -pub(crate) fn create_pointwise_predicate_propagating_task_lower_bound_propagation( - task: &Rc>, +pub(crate) fn create_pointwise_predicate_propagating_task_lower_bound_propagation( + context: PropagationContext, + task: &Rc>, time_point: Option, -) -> Predicate +) -> PropositionalConjunction where Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, { - predicate!( - task.start_variable - >= time_point - .expect("Expected time-point to be provided to pointwise explanation creation") - + 1 - - task.processing_time - ) + [ + predicate!( + task.start_variable + >= time_point + .expect("Expected time-point to be provided to pointwise explanation creation") + + 1 + - context.lower_bound(&task.processing_time) + ), + predicate!(task.processing_time >= context.lower_bound(&task.processing_time)), + predicate!(task.resource_usage >= context.lower_bound(&task.resource_usage)), + ] + .into_iter() + .filter(|&predicate| predicate != Predicate::trivially_true()) + .collect() } -pub(crate) fn create_pointwise_predicate_propagating_task_upper_bound_propagation( - task: &Rc>, +pub(crate) fn create_pointwise_predicate_propagating_task_upper_bound_propagation( + context: PropagationContext, + task: &Rc>, time_point: Option, -) -> Predicate +) -> PropositionalConjunction where Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, { - predicate!( - task.start_variable - <= time_point - .expect("Expected time-point to be provided to pointwise explanation creation") - ) + [ + predicate!( + task.start_variable + <= time_point + .expect("Expected time-point to be provided to pointwise explanation creation") + ), + predicate!(task.processing_time >= context.lower_bound(&task.processing_time)), + predicate!(task.resource_usage >= context.lower_bound(&task.resource_usage)), + ] + .into_iter() + .filter(|&predicate| predicate != Predicate::trivially_true()) + .collect() } #[cfg(test)] mod tests { + use crate::constraint_arguments::CumulativeExplanationType; use crate::predicate; use crate::predicates::PropositionalConjunction; - use crate::propagators::CumulativeExplanationType; use crate::propagators::cumulative::time_table::propagation_handler::test_propagation_handler::TestPropagationHandler; #[test] diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/checks.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/checks.rs index 59ff17cc0..739d4bbc4 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/checks.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/checks.rs @@ -5,6 +5,8 @@ use std::cmp::min; use std::ops::Range; use std::rc::Rc; +use crate::engine::cp::propagation::contexts::propagation_context::ReadDomains; +use crate::engine::propagation::PropagationContext; use crate::propagators::OverIntervalTimeTableType; use crate::propagators::ResourceProfile; use crate::propagators::Task; @@ -12,13 +14,18 @@ use crate::variables::IntegerVariable; /// Determines whether the added mandatory part causes a new profile before the first overapping /// profile. -pub(crate) fn new_profile_before_first_profile( +pub(crate) fn new_profile_before_first_profile< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + context: PropagationContext, current_index: usize, start_index: usize, update_range: &Range, - profile: &ResourceProfile, - to_add: &mut Vec>, - task: &Rc>, + profile: &ResourceProfile, + to_add: &mut Vec>, + task: &Rc>, ) { if current_index == start_index && update_range.start < profile.start { // We are considering the first overlapping profile and there is @@ -30,21 +37,27 @@ pub(crate) fn new_profile_before_first_profile( end: profile.start - 1, /* Note that this profile needs to end before the start * of the current profile, hence the -1 */ profile_tasks: vec![Rc::clone(task)], - height: task.resource_usage, + height: context.lower_bound(&task.resource_usage), }) } } /// Determines whether a new profile should be inserted between the current profile (pointed to /// by `current_index`) and the previous profile. -pub(crate) fn new_profile_between_profiles( - time_table: &OverIntervalTimeTableType, +#[allow(clippy::too_many_arguments, reason = "Should be refactored")] +pub(crate) fn new_profile_between_profiles< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + context: PropagationContext, + time_table: &OverIntervalTimeTableType, current_index: usize, start_index: usize, update_range: &Range, - profile: &ResourceProfile, - to_add: &mut Vec>, - task: &Rc>, + profile: &ResourceProfile, + to_add: &mut Vec>, + task: &Rc>, ) { if current_index != start_index && current_index != 0 { // We are not considering the first profile and there could be a @@ -66,7 +79,7 @@ pub(crate) fn new_profile_between_profiles( start: previous_profile.end + 1, end: profile.start - 1, profile_tasks: vec![Rc::clone(task)], - height: task.resource_usage, + height: context.lower_bound(&task.resource_usage), }) } } @@ -80,10 +93,12 @@ pub(crate) fn new_profile_between_profiles( /// is added in [`overlap_updated_profile`]. pub(crate) fn split_profile_added_part_starts_after_profile_start< Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, >( update_range: &Range, - profile: &ResourceProfile, - to_add: &mut Vec>, + profile: &ResourceProfile, + to_add: &mut Vec>, ) { if update_range.start > profile.start { // We are splitting the current profile into one or more parts @@ -106,13 +121,19 @@ pub(crate) fn split_profile_added_part_starts_after_profile_start< /// Determines whether a new profile which contains the overlap between `profile` and the added /// mandatory part should be added. -pub(crate) fn overlap_updated_profile( +pub(crate) fn overlap_updated_profile< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( + context: PropagationContext, update_range: &Range, - profile: &ResourceProfile, - to_add: &mut Vec>, - task: &Rc>, - capacity: i32, -) -> Result<(), ResourceProfile> { + profile: &ResourceProfile, + to_add: &mut Vec>, + task: &Rc>, + capacity: CVar, +) -> Result<(), ResourceProfile> { // Now we create a new profile which consists of the part of the // profile covered by the update range // This means that we are adding the contribution of the updated @@ -139,7 +160,7 @@ pub(crate) fn overlap_updated_profile( start: new_profile_lower_bound, end: new_profile_upper_bound, profile_tasks: new_profile_tasks.clone(), - height: profile.height + task.resource_usage, + height: profile.height + context.lower_bound(&task.resource_usage), }; // We thus create a new profile consisting of the combination of @@ -148,14 +169,16 @@ pub(crate) fn overlap_updated_profile( // A sanity check, there is a new profile to create consisting // of a combination of the previous profile and the updated task - if profile.height + task.resource_usage > capacity { + if profile.height + context.lower_bound(&task.resource_usage) + > context.upper_bound(&capacity) + { // The addition of the new mandatory part to the profile // caused an overflow of the resource return Err(ResourceProfile { start: new_profile_lower_bound, end: new_profile_upper_bound, profile_tasks: new_profile_tasks, - height: profile.height + task.resource_usage, + height: profile.height + context.lower_bound(&task.resource_usage), }); } } @@ -168,10 +191,14 @@ pub(crate) fn overlap_updated_profile( /// Note that this function adds the unchanged part only (i.e. the part of the profile with /// which the added mandatory part does **not** overlap), the updated part of this profile /// is added in [`overlap_updated_profile`]. -pub(crate) fn split_profile_added_part_ends_before_profile_end( +pub(crate) fn split_profile_added_part_ends_before_profile_end< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( update_range: &Range, - profile: &ResourceProfile, - to_add: &mut Vec>, + profile: &ResourceProfile, + to_add: &mut Vec>, ) { if profile.end >= update_range.end { // We are splitting the current profile into one or more parts @@ -190,13 +217,18 @@ pub(crate) fn split_profile_added_part_ends_before_profile_end( +pub(crate) fn new_part_after_last_profile< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + context: PropagationContext, current_index: usize, end_index: usize, update_range: &Range, - profile: &ResourceProfile, - to_add: &mut Vec>, - task: &Rc>, + profile: &ResourceProfile, + to_add: &mut Vec>, + task: &Rc>, ) { if current_index == end_index && update_range.end > profile.end + 1 { // We are considering the last overlapping profile and there is @@ -207,7 +239,7 @@ pub(crate) fn new_part_after_last_profile( start: profile.end + 1, end: update_range.end - 1, profile_tasks: vec![Rc::clone(task)], - height: task.resource_usage, + height: context.lower_bound(&task.resource_usage), }) } } diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/debug.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/debug.rs index 7404ac45f..82cfe34a8 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/debug.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/debug.rs @@ -2,7 +2,7 @@ use std::ops::Range; use crate::containers::HashSet; -use crate::engine::propagation::PropagationContext; +use crate::engine::propagation::PropagationContextMut; use crate::proof::InferenceCode; use crate::propagators::CumulativeParameters; use crate::propagators::OverIntervalTimeTableType; @@ -12,7 +12,7 @@ use crate::pumpkin_assert_extreme; use crate::pumpkin_assert_simple; use crate::variables::IntegerVariable; -/// Determines whether the provided `time_table` is the same as the one creatd from scratch +/// Determines whether the provided `time_table` is the same as the one created from scratch /// using the following checks: /// - The time-tables should contain the same number of profiles /// - For each profile it should hold that @@ -23,12 +23,15 @@ use crate::variables::IntegerVariable; /// same! pub(crate) fn time_tables_are_the_same_interval< Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, const SYNCHRONISE: bool, >( - context: PropagationContext, + context: &mut PropagationContextMut, inference_code: InferenceCode, - time_table: &OverIntervalTimeTableType, - parameters: &CumulativeParameters, + time_table: &OverIntervalTimeTableType, + parameters: &CumulativeParameters, ) -> bool { let time_table_scratch = create_time_table_over_interval_from_scratch(context, parameters, inference_code) @@ -79,8 +82,12 @@ pub(crate) fn time_tables_are_the_same_interval< /// Merge all mergeable profiles (see [`are_mergeable`]) going from `[start_index, end_index]` /// in the provided `time_table`. -pub(crate) fn merge_profiles( - time_table: &mut OverIntervalTimeTableType, +pub(crate) fn merge_profiles< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + time_table: &mut OverIntervalTimeTableType, start_index: usize, end_index: usize, ) { @@ -96,7 +103,7 @@ pub(crate) fn merge_profiles( // To avoid needless splicing, we keep track of the range at which insertions will take place let mut insertion_range: Option> = None; // And the profiles which need to be added - let mut to_add: Option>> = None; + let mut to_add: Option>> = None; // We go over all pairs of profiles, starting from start index until end index while current_index < end { @@ -178,9 +185,13 @@ pub(crate) fn merge_profiles( /// time-table created from scratch. /// /// It is assumed that the profile tasks of both profiles do not contain duplicates -pub(crate) fn are_mergeable( - first_profile: &ResourceProfile, - second_profile: &ResourceProfile, +pub(crate) fn are_mergeable< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + first_profile: &ResourceProfile, + second_profile: &ResourceProfile, ) -> bool { pumpkin_assert_extreme!( first_profile diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/insertion.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/insertion.rs index 0347256a8..7c1d35d12 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/insertion.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/insertion.rs @@ -3,6 +3,8 @@ use std::ops::Range; use std::rc::Rc; +use crate::engine::cp::propagation::contexts::propagation_context::ReadDomains; +use crate::engine::propagation::PropagationContext; use crate::propagators::OverIntervalTimeTableType; use crate::propagators::ResourceProfile; use crate::propagators::Task; @@ -16,14 +18,18 @@ use crate::variables::IntegerVariable; /// profiles and adds them to the `time-table` at the correct position. pub(crate) fn insert_profiles_overlapping_with_added_mandatory_part< Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, >( - time_table: &mut OverIntervalTimeTableType, + context: PropagationContext, + time_table: &mut OverIntervalTimeTableType, start_index: usize, end_index: usize, update_range: &Range, - updated_task: &Rc>, - capacity: i32, -) -> Result<(), ResourceProfile> { + updated_task: &Rc>, + capacity: CVar, +) -> Result<(), ResourceProfile> { let mut to_add = Vec::new(); // We keep track of whether a conflict has been found @@ -39,6 +45,7 @@ pub(crate) fn insert_profiles_overlapping_with_added_mandatory_part< // Check whether there is a new profile before the first overlapping // profile checks::new_profile_before_first_profile( + context, current_index, start_index, update_range, @@ -50,6 +57,7 @@ pub(crate) fn insert_profiles_overlapping_with_added_mandatory_part< // Check whether there is a new profile between the current profile // and the previous profile (beginning of profile remains unchanged) checks::new_profile_between_profiles( + context, time_table, current_index, start_index, @@ -72,11 +80,12 @@ pub(crate) fn insert_profiles_overlapping_with_added_mandatory_part< // // The addition of the mandatory part can lead to an overflow let result = checks::overlap_updated_profile( + context, update_range, profile, &mut to_add, updated_task, - capacity, + capacity.clone(), ); if result.is_err() && conflict.is_none() { conflict = Some(result) @@ -93,6 +102,7 @@ pub(crate) fn insert_profiles_overlapping_with_added_mandatory_part< // Check whether there is a new profile before the last overlapping // profile checks::new_part_after_last_profile( + context, current_index, end_index, update_range, @@ -115,11 +125,16 @@ pub(crate) fn insert_profiles_overlapping_with_added_mandatory_part< /// The new mandatory part added by `updated_task` (spanning `update_range`) does not overlap /// with any existing profile. This method inserts it at the position of `index_to_insert` /// in the `time-table`. -pub(crate) fn insert_profile_new_mandatory_part( - time_table: &mut OverIntervalTimeTableType, +pub(crate) fn insert_profile_new_mandatory_part< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + context: PropagationContext, + time_table: &mut OverIntervalTimeTableType, index_to_insert: usize, update_range: &Range, - updated_task: &Rc>, + updated_task: &Rc>, ) { pumpkin_assert_moderate!( index_to_insert <= time_table.len() @@ -135,7 +150,7 @@ pub(crate) fn insert_profile_new_mandatory_part( start: update_range.start, end: update_range.end - 1, profile_tasks: vec![Rc::clone(updated_task)], - height: updated_task.resource_usage, + height: context.lower_bound(&updated_task.resource_usage), }, ); } diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/removal.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/removal.rs index dc9dfa4af..64802b45d 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/removal.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/removal.rs @@ -5,6 +5,8 @@ use std::cmp::min; use std::ops::Range; use std::rc::Rc; +use crate::engine::cp::propagation::contexts::propagation_context::ReadDomains; +use crate::engine::propagation::PropagationContext; use crate::propagators::OverIntervalTimeTableType; use crate::propagators::ResourceProfile; use crate::propagators::Task; @@ -15,12 +17,15 @@ use crate::variables::IntegerVariable; /// profiles and adds them to the `time-table` at the correct position. pub(crate) fn reduce_profiles_overlapping_with_added_mandatory_part< Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, >( - time_table: &mut OverIntervalTimeTableType, + context: PropagationContext, + time_table: &mut OverIntervalTimeTableType, start_index: usize, end_index: usize, update_range: &Range, - updated_task: &Rc>, + updated_task: &Rc>, ) { let mut to_add = vec![]; @@ -37,7 +42,7 @@ pub(crate) fn reduce_profiles_overlapping_with_added_mandatory_part< // Then we need to add the updated profile due to the overlap between `profile` and // `updated_task` - overlap_updated_profile(update_range, profile, &mut to_add, updated_task); + overlap_updated_profile(context, update_range, profile, &mut to_add, updated_task); // We need to check whether the last overlapping profile was split if index == end_index { @@ -51,12 +56,17 @@ pub(crate) fn reduce_profiles_overlapping_with_added_mandatory_part< } /// Returns the provided `profile` with the provided `updated_task` removed. -fn remove_task_from_profile( - updated_task: &Rc>, +fn remove_task_from_profile< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + context: PropagationContext, + updated_task: &Rc>, start: i32, end: i32, - profile: &ResourceProfile, -) -> ResourceProfile { + profile: &ResourceProfile, +) -> ResourceProfile { let mut updated_profile_tasks = profile.profile_tasks.clone(); let _ = updated_profile_tasks.swap_remove( updated_profile_tasks @@ -69,16 +79,20 @@ fn remove_task_from_profile( start, end, profile_tasks: updated_profile_tasks, - height: profile.height - updated_task.resource_usage, + height: profile.height - context.lower_bound(&updated_task.resource_usage), } } /// If there is a partial overlap, this method creates a profile consisting of the original /// profile before the overlap. -pub(crate) fn split_first_profile( - to_add: &mut Vec>, +pub(crate) fn split_first_profile< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + to_add: &mut Vec>, update_range: &Range, - first_profile: &ResourceProfile, + first_profile: &ResourceProfile, ) { if update_range.start > first_profile.start { to_add.push(ResourceProfile { @@ -90,10 +104,14 @@ pub(crate) fn split_first_profile( } } -pub(crate) fn split_last_profile( - to_add: &mut Vec>, +pub(crate) fn split_last_profile< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + to_add: &mut Vec>, update_range: &Range, - last_profile: &ResourceProfile, + last_profile: &ResourceProfile, ) { if last_profile.end >= update_range.end { // We are splitting the current profile into one or more parts @@ -111,13 +129,18 @@ pub(crate) fn split_last_profile( } /// This method creates a new profile based on the overlap with the provided `profile`. -pub(crate) fn overlap_updated_profile( +pub(crate) fn overlap_updated_profile< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + context: PropagationContext, update_range: &Range, - profile: &ResourceProfile, - to_add: &mut Vec>, - updated_task: &Rc>, + profile: &ResourceProfile, + to_add: &mut Vec>, + updated_task: &Rc>, ) { - if profile.height - updated_task.resource_usage == 0 { + if profile.height - context.lower_bound(&updated_task.resource_usage) == 0 { // If the removal of this task results in an empty profile then we simply do not add it return; } @@ -147,6 +170,7 @@ pub(crate) fn overlap_updated_profile( // We thus create a new profile consisting of the combination of // the previous profile and the updated task under consideration to_add.push(remove_task_from_profile( + context, updated_task, new_profile_lower_bound, new_profile_upper_bound, diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/synchronisation.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/synchronisation.rs index fa7dd3aa6..57e0581f7 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/synchronisation.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/synchronisation.rs @@ -5,6 +5,7 @@ use super::debug::merge_profiles; use crate::basic_types::Inconsistency; use crate::basic_types::PropagationStatusCP; use crate::engine::propagation::PropagationContext; +use crate::engine::propagation::PropagationContextMut; use crate::engine::propagation::ReadDomains; use crate::proof::InferenceCode; use crate::propagators::CumulativeParameters; @@ -13,24 +14,30 @@ use crate::propagators::ResourceProfile; #[cfg(doc)] use crate::propagators::TimeTableOverIntervalPropagator; use crate::propagators::create_time_table_over_interval_from_scratch; -use crate::propagators::cumulative::time_table::propagation_handler::create_conflict_explanation; +use crate::propagators::cumulative::time_table::propagation_handler::create_explanation_profile_height; use crate::variables::IntegerVariable; /// Finds the conflicting profile which would have been found by the /// [`TimeTableOverIntervalPropagator`]; this is the first conflicting profile in terms of start /// time, however, the returned profile should be merged with adjacent profiles to create the /// returned conflict profile. -pub(crate) fn find_synchronised_conflict( - time_table: &mut OverIntervalTimeTableType, - parameters: &CumulativeParameters, -) -> Option> { +pub(crate) fn find_synchronised_conflict< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( + context: PropagationContext, + time_table: &mut OverIntervalTimeTableType, + parameters: &CumulativeParameters, +) -> Option> { if time_table.is_empty() { return None; } let first_conflict_profile_index = time_table .iter() - .position(|profile| profile.height > parameters.capacity); + .position(|profile| profile.height > context.upper_bound(¶meters.capacity)); if let Some(mut first_conflict_profile_index) = first_conflict_profile_index { let mut new_profile = time_table[first_conflict_profile_index].clone(); @@ -55,15 +62,18 @@ pub(crate) fn find_synchronised_conflict( /// [`TimeTableOverIntervalPropagator`]. pub(crate) fn check_synchronisation_conflict_explanation_over_interval< Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, >( synchronised_conflict_explanation: &PropagationStatusCP, - context: PropagationContext, - parameters: &CumulativeParameters, + context: &mut PropagationContextMut, + parameters: &CumulativeParameters, inference_code: InferenceCode, ) -> bool { let error_from_scratch = create_time_table_over_interval_from_scratch(context, parameters, inference_code); - if let Err(explanation_scratch) = error_from_scratch { + if let Err(Inconsistency::Conflict(explanation_scratch)) = error_from_scratch { if let Err(Inconsistency::Conflict(explanation)) = &synchronised_conflict_explanation { // We check whether both inconsistencies are of the same type and then we check their // corresponding explanations @@ -80,11 +90,16 @@ pub(crate) fn check_synchronisation_conflict_explanation_over_interval< /// by [`TimeTableOverIntervalPropagator`]), this function calculates the error which would have /// been reported by [`TimeTableOverIntervalPropagator`] by finding the tasks which should be /// included in the profile and sorting them in the same order. -pub(crate) fn create_synchronised_conflict_explanation( +pub(crate) fn create_synchronised_conflict_explanation< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( context: PropagationContext, inference_code: InferenceCode, - conflicting_profile: &mut ResourceProfile, - parameters: &CumulativeParameters, + conflicting_profile: &mut ResourceProfile, + parameters: &CumulativeParameters, ) -> PropagationStatusCP { // If we need to synchronise then we need to find the conflict profile which // would have been found by the non-incremental propagator; we thus first sort based on @@ -100,14 +115,14 @@ pub(crate) fn create_synchronised_conflict_explanation( - time_table: &mut OverIntervalTimeTableType, +pub(crate) fn synchronise_time_table< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + time_table: &mut OverIntervalTimeTableType, context: PropagationContext, ) { if !time_table.is_empty() { @@ -143,8 +162,12 @@ pub(crate) fn synchronise_time_table( /// Sorts the provided `profile` on non-decreasing order of upper-bound while tie-breaking in /// non-decreasing order of ID -fn sort_profile_based_on_upper_bound_and_id( - profile: &mut ResourceProfile, +fn sort_profile_based_on_upper_bound_and_id< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + profile: &mut ResourceProfile, context: PropagationContext, ) { profile.profile_tasks.sort_by(|a, b| { diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs index 671f56de6..44235cd6d 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs @@ -1,3 +1,4 @@ +use crate::engine::cp::propagation::contexts::propagation_context::ReadDomains; use std::fmt::Debug; use std::ops::Range; use std::rc::Rc; @@ -27,7 +28,7 @@ use crate::propagators::cumulative::time_table::over_interval_incremental_propag use crate::propagators::cumulative::time_table::over_interval_incremental_propagator::synchronisation::create_synchronised_conflict_explanation; use crate::propagators::cumulative::time_table::over_interval_incremental_propagator::synchronisation::find_synchronised_conflict; use crate::propagators::cumulative::time_table::over_interval_incremental_propagator::synchronisation::synchronise_time_table; -use crate::propagators::cumulative::time_table::propagation_handler::create_conflict_explanation; +use crate::propagators::cumulative::time_table::propagation_handler::create_explanation_profile_height; use crate::propagators::cumulative::time_table::time_table_util::backtrack_update; use crate::propagators::cumulative::time_table::time_table_util::has_overlap_with_interval; use crate::propagators::cumulative::time_table::time_table_util::insert_update; @@ -74,16 +75,22 @@ use crate::pumpkin_assert_simple; /// \[1\] A. Schutt, Improving scheduling by learning. University of Melbourne, Department of /// Computer Science and Software Engineering, 2011. #[derive(Clone, Debug)] -pub(crate) struct TimeTableOverIntervalIncrementalPropagator { +pub(crate) struct TimeTableOverIntervalIncrementalPropagator< + Var, + PVar, + RVar, + CVar, + const SYNCHRONISE: bool, +> { /// The key `t` (representing a time-point) holds the mandatory resource consumption of /// [`Task`]s at that time (stored in a [`ResourceProfile`]); the [`ResourceProfile`]s are /// sorted based on start time and they are assumed to be non-overlapping - time_table: OverIntervalTimeTableType, + time_table: OverIntervalTimeTableType, /// Stores the input parameters to the cumulative constraint - parameters: CumulativeParameters, + parameters: CumulativeParameters, /// Stores structures which change during the search; either to store bounds or when applying /// incrementality - updatable_structures: UpdatableStructures, + updatable_structures: UpdatableStructures, /// Stores whether the propagator found a conflict in the previous call /// /// This is stored to deal with the case where the same conflict can be created via two @@ -96,58 +103,101 @@ pub(crate) struct TimeTableOverIntervalIncrementalPropagator { + tasks: Vec>, + capacity: CVar, + cumulative_options: CumulativePropagatorOptions, constraint_tag: ConstraintTag, - inference_code: Option, } -impl PropagatorConstructor - for TimeTableOverIntervalIncrementalPropagator +impl + TimeTableOverIntervalIncrementalConstructor { - type PropagatorImpl = Self; - - fn create(mut self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { - // We only register for notifications of backtrack events if incremental backtracking is - // enabled - register_tasks( - &self.parameters.tasks, - context.reborrow(), - self.parameters.options.incremental_backtracking, - ); - - // First we store the bounds in the parameters - self.updatable_structures - .reset_all_bounds_and_remove_fixed(context.as_readonly(), &self.parameters); + pub(crate) fn new( + arg_tasks: Vec>, + capacity: CVar, + cumulative_options: CumulativePropagatorOptions, + constraint_tag: ConstraintTag, + ) -> Self { + Self { + tasks: arg_tasks, + capacity, + cumulative_options, + constraint_tag, + } + } +} - self.is_time_table_outdated = true; +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, + const SYNCHRONISE: bool, +> PropagatorConstructor + for TimeTableOverIntervalIncrementalConstructor +{ + type PropagatorImpl = + TimeTableOverIntervalIncrementalPropagator; - self.inference_code = Some(context.create_inference_code(self.constraint_tag, TimeTable)); + fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + let inference_code = context.create_inference_code(self.constraint_tag, TimeTable); - self + TimeTableOverIntervalIncrementalPropagator::new( + context, + &self.tasks, + self.capacity, + self.cumulative_options, + inference_code, + ) } } -impl - TimeTableOverIntervalIncrementalPropagator +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, + const SYNCHRONISE: bool, +> TimeTableOverIntervalIncrementalPropagator { - pub(crate) fn new( - arg_tasks: &[ArgTask], - capacity: i32, + fn new( + mut context: PropagatorConstructorContext, + arg_tasks: &[ArgTask], + capacity: CVar, cumulative_options: CumulativePropagatorOptions, - constraint_tag: ConstraintTag, - ) -> TimeTableOverIntervalIncrementalPropagator { - let tasks = create_tasks(arg_tasks); - let parameters = CumulativeParameters::new(tasks, capacity, cumulative_options); - let updatable_structures = UpdatableStructures::new(¶meters); + inference_code: InferenceCode, + ) -> TimeTableOverIntervalIncrementalPropagator { + let tasks = create_tasks(context.as_readonly(), arg_tasks); + + let parameters = + CumulativeParameters::new(context.as_readonly(), tasks, capacity, cumulative_options); + register_tasks( + ¶meters.tasks, + ¶meters.capacity, + context.reborrow(), + cumulative_options.incremental_backtracking, + ); + + let mut updatable_structures = UpdatableStructures::new(¶meters); + updatable_structures.initialise_bounds_and_remove_fixed(context.as_readonly(), ¶meters); TimeTableOverIntervalIncrementalPropagator { time_table: Default::default(), parameters, updatable_structures, found_previous_conflict: false, - is_time_table_outdated: false, - constraint_tag, - inference_code: None, + is_time_table_outdated: true, + inference_code, } } @@ -157,7 +207,7 @@ impl &mut self, context: PropagationContext, mandatory_part_adjustments: &MandatoryPartAdjustments, - task: &Rc>, + task: &Rc>, ) -> PropagationStatusCP { let mut conflict = None; // We consider both of the possible update ranges @@ -168,19 +218,20 @@ impl match determine_profiles_to_update(&self.time_table, &update_range) { Ok((start_index, end_index)) => { let result = insertion::insert_profiles_overlapping_with_added_mandatory_part( + context, &mut self.time_table, start_index, end_index, &update_range, task, - self.parameters.capacity, + self.parameters.capacity.clone(), ); if let Err(conflict_tasks) = result && conflict.is_none() { - conflict = Some(Err(create_conflict_explanation( + conflict = Some(Err(create_explanation_profile_height( context, - self.inference_code.unwrap(), + self.inference_code, &conflict_tasks, self.parameters.options.explanation_type, ) @@ -188,6 +239,7 @@ impl } } Err(index_to_insert) => insertion::insert_profile_new_mandatory_part( + context, &mut self.time_table, index_to_insert, &update_range, @@ -205,8 +257,9 @@ impl /// Removes the removed parts in the provided [`MandatoryPartAdjustments`] from the time-table fn remove_from_time_table( &mut self, + context: PropagationContext, mandatory_part_adjustments: &MandatoryPartAdjustments, - task: &Rc>, + task: &Rc>, ) { // We consider both of the possible update ranges // Note that the upper update range is first considered to avoid any issues with the @@ -216,6 +269,7 @@ impl match determine_profiles_to_update(&self.time_table, &update_range) { Ok((start_index, end_index)) => { removal::reduce_profiles_overlapping_with_added_mandatory_part( + context, &mut self.time_table, start_index, end_index, @@ -239,9 +293,9 @@ impl if self.is_time_table_outdated { // We create the time-table from scratch (and return an error if it overflows) self.time_table = create_time_table_over_interval_from_scratch( - context.as_readonly(), + context, &self.parameters, - self.inference_code.unwrap(), + self.inference_code, )?; // Then we note that the time-table is not outdated anymore @@ -262,13 +316,18 @@ impl let element = self.updatable_structures.get_update_for_task(&updated_task); // We get the adjustments based on the stored updated - let mandatory_part_adjustments = element.get_mandatory_part_adjustments(); + let mandatory_part_adjustments = + element.get_mandatory_part_adjustments(context.as_readonly()); // Then we first remove from the time-table (if necessary) // // This order ensures that there is less of a chance of incorrect overflows being // reported - self.remove_from_time_table(&mandatory_part_adjustments, &updated_task); + self.remove_from_time_table( + context.as_readonly(), + &mandatory_part_adjustments, + &updated_task, + ); // Then we add to the time-table (if necessary) // @@ -294,24 +353,27 @@ impl if SYNCHRONISE { // If we are synchronising then we need to search for the conflict which would have // been found by the non-incremental propagator - let conflicting_profile = - find_synchronised_conflict(&mut self.time_table, &self.parameters); + let conflicting_profile = find_synchronised_conflict( + context.as_readonly(), + &mut self.time_table, + &self.parameters, + ); // Now we need to find the same explanation as would have been found by // the non-incremental propagator if let Some(mut conflicting_profile) = conflicting_profile { let synchronised_conflict_explanation = create_synchronised_conflict_explanation( context.as_readonly(), - self.inference_code.unwrap(), + self.inference_code, &mut conflicting_profile, &self.parameters, ); pumpkin_assert_extreme!( check_synchronisation_conflict_explanation_over_interval( &synchronised_conflict_explanation, - context.as_readonly(), + context, &self.parameters, - self.inference_code.unwrap(), + self.inference_code, ), "The conflict explanation was not the same as the conflict explanation from scratch!" ); @@ -322,18 +384,17 @@ impl self.found_previous_conflict = false; } else { // We linearly scan the profiles and find the first one which exceeds the capacity - let conflicting_profile = self - .time_table - .iter_mut() - .find(|profile| profile.height > self.parameters.capacity); + let conflicting_profile = self.time_table.iter_mut().find(|profile| { + profile.height > context.upper_bound(&self.parameters.capacity) + }); // If we have found such a conflict then we return it if let Some(conflicting_profile) = conflicting_profile { pumpkin_assert_extreme!( create_time_table_over_interval_from_scratch( - context.as_readonly(), + context, &self.parameters, - self.inference_code.unwrap(), + self.inference_code, ) .is_err(), "Time-table from scratch could not find conflict" @@ -341,9 +402,9 @@ impl // We have found the previous conflict self.found_previous_conflict = true; - return Err(create_conflict_explanation( + return Err(create_explanation_profile_height( context.as_readonly(), - self.inference_code.unwrap(), + self.inference_code, conflicting_profile, self.parameters.options.explanation_type, ) @@ -366,14 +427,19 @@ impl pumpkin_assert_extreme!( self.time_table .iter() - .all(|profile| profile.height <= self.parameters.capacity) + .all(|profile| profile.height <= context.upper_bound(&self.parameters.capacity)) ); Ok(()) } } -impl Propagator - for TimeTableOverIntervalIncrementalPropagator +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, + const SYNCHRONISE: bool, +> Propagator for TimeTableOverIntervalIncrementalPropagator { fn propagate(&mut self, mut context: PropagationContextMut) -> PropagationStatusCP { pumpkin_assert_advanced!( @@ -388,16 +454,16 @@ impl Propagator if self.parameters.is_infeasible { return Err(Inconsistency::Conflict(PropagatorConflict { conjunction: conjunction!(), - inference_code: self.inference_code.unwrap(), + inference_code: self.inference_code, })); } self.update_time_table(&mut context)?; pumpkin_assert_extreme!( - debug::time_tables_are_the_same_interval::( - context.as_readonly(), - self.inference_code.unwrap(), + debug::time_tables_are_the_same_interval::( + &mut context, + self.inference_code, &self.time_table, &self.parameters, ), @@ -410,7 +476,7 @@ impl Propagator // could cause another propagation by a profile which has not been updated propagate_based_on_timetable( &mut context, - self.inference_code.unwrap(), + self.inference_code, self.time_table.iter(), &self.parameters, &mut self.updatable_structures, @@ -421,7 +487,7 @@ impl Propagator &mut self, context: PropagationContextWithTrailedValues, local_id: LocalId, - event: OpaqueDomainEvent, + _event: OpaqueDomainEvent, ) -> EnqueueDecision { let updated_task = Rc::clone(&self.parameters.tasks[local_id.unpack() as usize]); // Note that we do not take into account the fact that the time-table could be outdated @@ -449,10 +515,10 @@ impl Propagator &updated_task, ); - if matches!( - updated_task.start_variable.unpack_event(event), - DomainEvent::Assign - ) { + if context.is_fixed(&updated_task.start_variable) + && context.is_fixed(&updated_task.processing_time) + && context.is_fixed(&updated_task.resource_usage) + { self.updatable_structures.fix_task(&updated_task) } @@ -520,7 +586,7 @@ impl Propagator &mut context, &self.parameters, &self.updatable_structures, - self.inference_code.unwrap(), + self.inference_code, ) } } @@ -534,8 +600,12 @@ impl Propagator /// if there are no overlapping profiles /// /// Note that the lower-bound of the range is inclusive and the upper-bound is exclusive -fn determine_profiles_to_update( - time_table: &OverIntervalTimeTableType, +fn determine_profiles_to_update< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + time_table: &OverIntervalTimeTableType, update_range: &Range, ) -> Result<(usize, usize), usize> { let overlapping_profile = find_overlapping_profile(time_table, update_range); @@ -603,8 +673,12 @@ fn determine_profiles_to_update( /// [Ok] containing the index of the overlapping profile. If no such element could be found, /// it returns [Err] containing the index at which the element should be inserted to /// preserve the ordering -fn find_overlapping_profile( - time_table: &OverIntervalTimeTableType, +fn find_overlapping_profile< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + time_table: &OverIntervalTimeTableType, update_range: &Range, ) -> Result { time_table.binary_search_by(|profile| { @@ -624,16 +698,15 @@ fn find_overlapping_profile( #[cfg(test)] mod tests { - use crate::basic_types::Inconsistency; use crate::conjunction; + use crate::constraint_arguments::CumulativeExplanationType; use crate::engine::predicates::predicate::Predicate; use crate::engine::propagation::EnqueueDecision; use crate::engine::test_solver::TestSolver; use crate::predicate; use crate::propagators::ArgTask; - use crate::propagators::CumulativeExplanationType; use crate::propagators::CumulativePropagatorOptions; - use crate::propagators::TimeTableOverIntervalIncrementalPropagator; + use crate::propagators::TimeTableOverIntervalIncrementalConstructor; use crate::variables::DomainId; #[test] @@ -644,27 +717,31 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator( - TimeTableOverIntervalIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 4, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 3, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions::default(), - constraint_tag, - ), - ) + .new_propagator(TimeTableOverIntervalIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 4, + resource_usage: 1, + }, + ArgTask { + start_time: s2, + processing_time: 3, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions::default(), + constraint_tag, + )) .expect("No conflict"); assert_eq!(solver.lower_bound(s2), 5); assert_eq!(solver.upper_bound(s2), 8); @@ -679,11 +756,14 @@ mod tests { let s2 = solver.new_variable(1, 1); let constraint_tag = solver.new_constraint_tag(); - let result = solver.new_propagator(TimeTableOverIntervalIncrementalPropagator::< + let result = solver.new_propagator(TimeTableOverIntervalIncrementalConstructor::< DomainId, + i32, + i32, + i32, false, >::new( - &[ + [ ArgTask { start_time: s1, processing_time: 4, @@ -705,25 +785,20 @@ mod tests { constraint_tag, )); - assert!(matches!(result, Err(Inconsistency::Conflict(_)))); - assert!(match result { - Err(Inconsistency::Conflict(conflict)) => { - let expected = [ - predicate!(s1 <= 1), - predicate!(s1 >= 1), - predicate!(s2 >= 1), - predicate!(s2 <= 1), - ]; - expected.iter().all(|y| { - conflict - .conjunction - .iter() - .collect::>() - .contains(&y) - }) && conflict.conjunction.iter().all(|y| expected.contains(y)) - } - _ => false, - }); + assert!(result.is_err()); + let reason = solver.get_reason_int(Predicate::trivially_false()); + let expected = [ + predicate!(s1 <= 1), + predicate!(s1 >= 1), + predicate!(s2 >= 1), + predicate!(s2 <= 1), + ]; + assert!( + expected + .iter() + .all(|y| { reason.iter().collect::>().contains(&y) }) + && reason.iter().all(|y| expected.contains(y)) + ); } #[test] @@ -734,27 +809,31 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator( - TimeTableOverIntervalIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 4, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 3, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions::default(), - constraint_tag, - ), - ) + .new_propagator(TimeTableOverIntervalIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 4, + resource_usage: 1, + }, + ArgTask { + start_time: s2, + processing_time: 3, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions::default(), + constraint_tag, + )) .expect("No conflict"); assert_eq!(solver.lower_bound(s2), 0); assert_eq!(solver.upper_bound(s2), 6); @@ -774,47 +853,51 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator( - TimeTableOverIntervalIncrementalPropagator::::new( - &[ - ArgTask { - start_time: a, - processing_time: 2, - resource_usage: 1, - }, - ArgTask { - start_time: b, - processing_time: 6, - resource_usage: 2, - }, - ArgTask { - start_time: c, - processing_time: 2, - resource_usage: 4, - }, - ArgTask { - start_time: d, - processing_time: 2, - resource_usage: 2, - }, - ArgTask { - start_time: e, - processing_time: 5, - resource_usage: 2, - }, - ArgTask { - start_time: f, - processing_time: 6, - resource_usage: 2, - }, - ] - .into_iter() - .collect::>(), - 5, - CumulativePropagatorOptions::default(), - constraint_tag, - ), - ) + .new_propagator(TimeTableOverIntervalIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: a, + processing_time: 2, + resource_usage: 1, + }, + ArgTask { + start_time: b, + processing_time: 6, + resource_usage: 2, + }, + ArgTask { + start_time: c, + processing_time: 2, + resource_usage: 4, + }, + ArgTask { + start_time: d, + processing_time: 2, + resource_usage: 2, + }, + ArgTask { + start_time: e, + processing_time: 5, + resource_usage: 2, + }, + ArgTask { + start_time: f, + processing_time: 6, + resource_usage: 2, + }, + ] + .into_iter() + .collect::>(), + 5, + CumulativePropagatorOptions::default(), + constraint_tag, + )) .expect("No conflict"); assert_eq!(solver.lower_bound(f), 10); } @@ -827,27 +910,31 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator( - TimeTableOverIntervalIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 2, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 3, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions::default(), - constraint_tag, - ), - ) + .new_propagator(TimeTableOverIntervalIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 2, + resource_usage: 1, + }, + ArgTask { + start_time: s2, + processing_time: 3, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions::default(), + constraint_tag, + )) .expect("No conflict"); assert_eq!(solver.lower_bound(s2), 6); assert_eq!(solver.upper_bound(s2), 10); @@ -875,30 +962,34 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator( - TimeTableOverIntervalIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 4, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 3, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions { - explanation_type: CumulativeExplanationType::Naive, - ..Default::default() + .new_propagator(TimeTableOverIntervalIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 4, + resource_usage: 1, }, - constraint_tag, - ), - ) + ArgTask { + start_time: s2, + processing_time: 3, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions { + explanation_type: CumulativeExplanationType::Naive, + ..Default::default() + }, + constraint_tag, + )) .expect("No conflict"); assert_eq!(solver.lower_bound(s2), 1); assert_eq!(solver.upper_bound(s2), 3); @@ -921,47 +1012,51 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator( - TimeTableOverIntervalIncrementalPropagator::::new( - &[ - ArgTask { - start_time: a, - processing_time: 2, - resource_usage: 1, - }, - ArgTask { - start_time: b, - processing_time: 6, - resource_usage: 2, - }, - ArgTask { - start_time: c, - processing_time: 2, - resource_usage: 4, - }, - ArgTask { - start_time: d, - processing_time: 2, - resource_usage: 2, - }, - ArgTask { - start_time: e, - processing_time: 4, - resource_usage: 2, - }, - ArgTask { - start_time: f, - processing_time: 6, - resource_usage: 2, - }, - ] - .into_iter() - .collect::>(), - 5, - CumulativePropagatorOptions::default(), - constraint_tag, - ), - ) + .new_propagator(TimeTableOverIntervalIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: a, + processing_time: 2, + resource_usage: 1, + }, + ArgTask { + start_time: b, + processing_time: 6, + resource_usage: 2, + }, + ArgTask { + start_time: c, + processing_time: 2, + resource_usage: 4, + }, + ArgTask { + start_time: d, + processing_time: 2, + resource_usage: 2, + }, + ArgTask { + start_time: e, + processing_time: 4, + resource_usage: 2, + }, + ArgTask { + start_time: f, + processing_time: 6, + resource_usage: 2, + }, + ] + .into_iter() + .collect::>(), + 5, + CumulativePropagatorOptions::default(), + constraint_tag, + )) .expect("No conflict"); assert_eq!(solver.lower_bound(a), 0); assert_eq!(solver.upper_bound(a), 1); @@ -999,52 +1094,56 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator( - TimeTableOverIntervalIncrementalPropagator::::new( - &[ - ArgTask { - start_time: a, - processing_time: 2, - resource_usage: 1, - }, - ArgTask { - start_time: b1, - processing_time: 2, - resource_usage: 2, - }, - ArgTask { - start_time: b2, - processing_time: 3, - resource_usage: 2, - }, - ArgTask { - start_time: c, - processing_time: 2, - resource_usage: 4, - }, - ArgTask { - start_time: d, - processing_time: 2, - resource_usage: 2, - }, - ArgTask { - start_time: e, - processing_time: 4, - resource_usage: 2, - }, - ArgTask { - start_time: f, - processing_time: 6, - resource_usage: 2, - }, - ] - .into_iter() - .collect::>(), - 5, - CumulativePropagatorOptions::default(), - constraint_tag, - ), - ) + .new_propagator(TimeTableOverIntervalIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: a, + processing_time: 2, + resource_usage: 1, + }, + ArgTask { + start_time: b1, + processing_time: 2, + resource_usage: 2, + }, + ArgTask { + start_time: b2, + processing_time: 3, + resource_usage: 2, + }, + ArgTask { + start_time: c, + processing_time: 2, + resource_usage: 4, + }, + ArgTask { + start_time: d, + processing_time: 2, + resource_usage: 2, + }, + ArgTask { + start_time: e, + processing_time: 4, + resource_usage: 2, + }, + ArgTask { + start_time: f, + processing_time: 6, + resource_usage: 2, + }, + ] + .into_iter() + .collect::>(), + 5, + CumulativePropagatorOptions::default(), + constraint_tag, + )) .expect("No conflict"); assert_eq!(solver.lower_bound(a), 0); assert_eq!(solver.upper_bound(a), 1); @@ -1075,30 +1174,34 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator( - TimeTableOverIntervalIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 4, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 3, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions { - explanation_type: CumulativeExplanationType::Naive, - ..Default::default() + .new_propagator(TimeTableOverIntervalIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 4, + resource_usage: 1, }, - constraint_tag, - ), - ) + ArgTask { + start_time: s2, + processing_time: 3, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions { + explanation_type: CumulativeExplanationType::Naive, + ..Default::default() + }, + constraint_tag, + )) .expect("No conflict"); assert_eq!(solver.lower_bound(s2), 5); assert_eq!(solver.upper_bound(s2), 8); @@ -1118,35 +1221,39 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator( - TimeTableOverIntervalIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 2, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 2, - resource_usage: 1, - }, - ArgTask { - start_time: s3, - processing_time: 4, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions { - explanation_type: CumulativeExplanationType::Naive, - ..Default::default() + .new_propagator(TimeTableOverIntervalIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 2, + resource_usage: 1, }, - constraint_tag, - ), - ) + ArgTask { + start_time: s2, + processing_time: 2, + resource_usage: 1, + }, + ArgTask { + start_time: s3, + processing_time: 4, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions { + explanation_type: CumulativeExplanationType::Naive, + ..Default::default() + }, + constraint_tag, + )) .expect("No conflict"); assert_eq!(solver.lower_bound(s3), 7); assert_eq!(solver.upper_bound(s3), 15); @@ -1167,31 +1274,35 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator( - TimeTableOverIntervalIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 4, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 3, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions { - explanation_type: CumulativeExplanationType::Naive, - allow_holes_in_domain: true, - ..Default::default() + .new_propagator(TimeTableOverIntervalIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 4, + resource_usage: 1, }, - constraint_tag, - ), - ) + ArgTask { + start_time: s2, + processing_time: 3, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions { + explanation_type: CumulativeExplanationType::Naive, + allow_holes_in_domain: true, + ..Default::default() + }, + constraint_tag, + )) .expect("No conflict"); assert_eq!(solver.lower_bound(s2), 0); assert_eq!(solver.upper_bound(s2), 8); diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs index 5dd863117..1e2cb0c35 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs @@ -1,57 +1,36 @@ use std::rc::Rc; -use crate::basic_types::Inconsistency; use crate::basic_types::PropagationStatusCP; +use crate::engine::cp::propagation::contexts::propagation_context::ReadDomains; use crate::engine::propagation::PropagationContext; use crate::proof::InferenceCode; use crate::propagators::CumulativeParameters; use crate::propagators::PerPointTimeTableType; use crate::propagators::ResourceProfile; use crate::propagators::Task; -use crate::propagators::create_time_table_per_point_from_scratch; -use crate::propagators::cumulative::time_table::propagation_handler::create_conflict_explanation; +use crate::propagators::cumulative::time_table::propagation_handler::create_explanation_profile_height; use crate::pumpkin_assert_moderate; use crate::variables::IntegerVariable; -/// Returns whether the synchronised conflict explanation created by -/// [`TimeTablePerPointIncrementalPropgator`] is the same as that created by -/// [`TimeTablePerPointPropagator`]. -pub(crate) fn check_synchronisation_conflict_explanation_per_point< - Var: IntegerVariable + 'static, ->( - synchronised_conflict_explanation: &PropagationStatusCP, - context: PropagationContext, - inference_code: InferenceCode, - parameters: &CumulativeParameters, -) -> bool { - let error_from_scratch = - create_time_table_per_point_from_scratch(context, inference_code, parameters); - if let Err(explanation_scratch) = error_from_scratch { - if let Err(Inconsistency::Conflict(conflict)) = &synchronised_conflict_explanation { - // We check whether both inconsistencies are of the same type and then we check their - // corresponding explanations - conflict.conjunction == explanation_scratch.conjunction - } else { - false - } - } else { - false - } -} - /// Finds the conflicting profile which would have been found by the /// [`TimeTablePerPointPropagator`]; this is the conflicting profile which has the minimum maximum /// ID in set of the first `n` profile tasks (when sorted on ID) which overflow the capacity -pub(crate) fn find_synchronised_conflict( - time_table: &mut PerPointTimeTableType, - parameters: &CumulativeParameters, +pub(crate) fn find_synchronised_conflict< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( + context: PropagationContext, + time_table: &mut PerPointTimeTableType, + parameters: &CumulativeParameters, ) -> Option { let mut profile_time_point = None; let mut minimum_maximum_id = u32::MAX; // We go over every profile for (time_point, profile) in time_table.iter_mut() { - if profile.height <= parameters.capacity { + if profile.height <= context.upper_bound(¶meters.capacity) { // If the profile cannot overflow the resource capacity then we move onto the next // profile continue; @@ -61,10 +40,14 @@ pub(crate) fn find_synchronised_conflict( // is overflown and we get the last element in this set (which has the one with the maximum // ID since the profile is sorted in the method based on ID) let mut new_height = 0; - let conflicting_tasks = - get_minimum_set_of_tasks_which_overflow_capacity(profile, parameters, &mut new_height); + let conflicting_tasks = get_minimum_set_of_tasks_which_overflow_capacity( + context, + profile, + parameters, + &mut new_height, + ); if let Some(task_with_maximum_id) = conflicting_tasks.last() { - pumpkin_assert_moderate!(new_height > parameters.capacity); + pumpkin_assert_moderate!(new_height > context.upper_bound(¶meters.capacity)); if task_with_maximum_id.id.unpack() < minimum_maximum_id { minimum_maximum_id = task_with_maximum_id.id.unpack(); profile_time_point = Some(*time_point); @@ -79,11 +62,18 @@ pub(crate) fn find_synchronised_conflict( /// /// The sum of the heights of the tasks is stored in the provided `output_height`; note that this /// means that the iterator should be consumed before reading the `output_height` -fn get_minimum_set_of_tasks_which_overflow_capacity<'a, Var: IntegerVariable + 'static>( - profile: &'a mut ResourceProfile, - parameters: &'a CumulativeParameters, +fn get_minimum_set_of_tasks_which_overflow_capacity< + 'a, + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( + context: PropagationContext<'a>, + profile: &'a mut ResourceProfile, + parameters: &'a CumulativeParameters, output_height: &'a mut i32, -) -> impl Iterator>> + 'a { +) -> impl Iterator>> + 'a { // First we sort the profile based on the ID sort_profile_based_on_id(profile); @@ -94,10 +84,10 @@ fn get_minimum_set_of_tasks_which_overflow_capacity<'a, Var: IntegerVariable + ' .profile_tasks .iter() .take_while(move |task| { - if *resource_usage > parameters.capacity { + if *resource_usage > context.upper_bound(¶meters.capacity) { return false; } - *resource_usage += task.resource_usage; + *resource_usage += context.lower_bound(&task.resource_usage); true }) .cloned() @@ -109,11 +99,16 @@ fn get_minimum_set_of_tasks_which_overflow_capacity<'a, Var: IntegerVariable + ' /// by [`TimeTablePerPointPropagator`]), this function calculates the error which would have been /// reported by [`TimeTablePerPointPropagator`] by finding the tasks which should be included in the /// profile and sorting them in the same order. -pub(crate) fn create_synchronised_conflict_explanation( +pub(crate) fn create_synchronised_conflict_explanation< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( context: PropagationContext, inference_code: InferenceCode, - conflicting_profile: &mut ResourceProfile, - parameters: &CumulativeParameters, + conflicting_profile: &mut ResourceProfile, + parameters: &CumulativeParameters, ) -> PropagationStatusCP { // Store because we are mutably borrowing the conflicting profile let new_profile_start = conflicting_profile.start; @@ -124,13 +119,14 @@ pub(crate) fn create_synchronised_conflict_explanation( - time_table: impl Iterator>, +pub(crate) fn synchronise_time_table< + 'a, + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + time_table: impl Iterator>, ) { time_table.for_each(|profile| sort_profile_based_on_id(profile)) } /// Sorts the provided `profile` on non-decreasing order of ID -fn sort_profile_based_on_id(profile: &mut ResourceProfile) { +fn sort_profile_based_on_id< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + profile: &mut ResourceProfile, +) { profile .profile_tasks .sort_by(|a, b| a.id.unpack().cmp(&b.id.unpack())); @@ -166,6 +173,7 @@ mod tests { use super::find_synchronised_conflict; use crate::engine::propagation::LocalId; + use crate::engine::propagation::PropagationContext; use crate::engine::test_solver::TestSolver; use crate::propagators::CumulativeParameters; use crate::propagators::CumulativePropagatorOptions; @@ -202,8 +210,14 @@ mod tests { }, ]; - let parameters = - CumulativeParameters::new(tasks, 1, CumulativePropagatorOptions::default()); + let parameters = CumulativeParameters::new( + PropagationContext { + assignments: &solver.assignments, + }, + tasks, + 1, + CumulativePropagatorOptions::default(), + ); let mut time_table = PerPointTimeTableType::default(); let _ = time_table.insert( @@ -228,7 +242,13 @@ mod tests { }, ); - let result = find_synchronised_conflict(&mut time_table, ¶meters); + let result = find_synchronised_conflict( + PropagationContext { + assignments: &solver.assignments, + }, + &mut time_table, + ¶meters, + ); assert!(matches!(result, Some(4))); } } diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs index 183ced768..15aa8f492 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs @@ -7,6 +7,7 @@ use crate::basic_types::Inconsistency; use crate::basic_types::PropagationStatusCP; use crate::basic_types::PropagatorConflict; use crate::conjunction; +use crate::engine::cp::propagation::contexts::propagation_context::ReadDomains; use crate::engine::notifications::DomainEvent; use crate::engine::notifications::OpaqueDomainEvent; use crate::engine::propagation::EnqueueDecision; @@ -32,11 +33,10 @@ use crate::propagators::TimeTablePerPointPropagator; use crate::propagators::UpdatableStructures; use crate::propagators::create_time_table_per_point_from_scratch; use crate::propagators::cumulative::time_table::TimeTable; -use crate::propagators::cumulative::time_table::per_point_incremental_propagator::synchronisation::check_synchronisation_conflict_explanation_per_point; use crate::propagators::cumulative::time_table::per_point_incremental_propagator::synchronisation::create_synchronised_conflict_explanation; use crate::propagators::cumulative::time_table::per_point_incremental_propagator::synchronisation::find_synchronised_conflict; use crate::propagators::cumulative::time_table::per_point_incremental_propagator::synchronisation::synchronise_time_table; -use crate::propagators::cumulative::time_table::propagation_handler::create_conflict_explanation; +use crate::propagators::cumulative::time_table::propagation_handler::create_explanation_profile_height; use crate::propagators::cumulative::time_table::time_table_util::backtrack_update; use crate::propagators::cumulative::time_table::time_table_util::insert_update; use crate::propagators::cumulative::time_table::time_table_util::propagate_based_on_timetable; @@ -70,16 +70,22 @@ use crate::pumpkin_assert_extreme; /// Computer Science and Software Engineering, 2011. #[derive(Debug)] -pub(crate) struct TimeTablePerPointIncrementalPropagator { +pub(crate) struct TimeTablePerPointIncrementalPropagator< + Var, + PVar, + RVar, + CVar, + const SYNCHRONISE: bool, +> { /// The key `t` (representing a time-point) holds the mandatory resource consumption of /// [`Task`]s at that time (stored in a [`ResourceProfile`]); the [`ResourceProfile`]s are /// sorted based on start time and they are assumed to be non-overlapping - time_table: PerPointTimeTableType, + time_table: PerPointTimeTableType, /// Stores the input parameters to the cumulative constraint - parameters: CumulativeParameters, + parameters: CumulativeParameters, /// Stores structures which change during the search; either to store bounds or when applying /// incrementality - updatable_structures: UpdatableStructures, + updatable_structures: UpdatableStructures, /// Stores whether the propagator found a conflict in the previous call /// /// This is stored to deal with the case where the same conflict can be created via two @@ -92,51 +98,101 @@ pub(crate) struct TimeTablePerPointIncrementalPropagator { + tasks: Vec>, + capacity: CVar, + cumulative_options: CumulativePropagatorOptions, constraint_tag: ConstraintTag, - inference_code: Option, } -impl PropagatorConstructor - for TimeTablePerPointIncrementalPropagator +impl + TimeTablePerPointIncrementalConstructor { - type PropagatorImpl = Self; - - fn create(mut self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { - register_tasks(&self.parameters.tasks, context.reborrow(), true); - self.updatable_structures - .reset_all_bounds_and_remove_fixed(context.as_readonly(), &self.parameters); + pub(crate) fn new( + arg_tasks: Vec>, + capacity: CVar, + cumulative_options: CumulativePropagatorOptions, + constraint_tag: ConstraintTag, + ) -> Self { + Self { + tasks: arg_tasks, + capacity, + cumulative_options, + constraint_tag, + } + } +} - // Then we do normal propagation - self.is_time_table_outdated = true; +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, + const SYNCHRONISE: bool, +> PropagatorConstructor + for TimeTablePerPointIncrementalConstructor +{ + type PropagatorImpl = + TimeTablePerPointIncrementalPropagator; - self.inference_code = Some(context.create_inference_code(self.constraint_tag, TimeTable)); + fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + let inference_code = context.create_inference_code(self.constraint_tag, TimeTable); - self + TimeTablePerPointIncrementalPropagator::new( + context, + &self.tasks, + self.capacity, + self.cumulative_options, + inference_code, + ) } } -impl - TimeTablePerPointIncrementalPropagator +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, + const SYNCHRONISE: bool, +> TimeTablePerPointIncrementalPropagator { - pub(crate) fn new( - arg_tasks: &[ArgTask], - capacity: i32, + fn new( + mut context: PropagatorConstructorContext, + arg_tasks: &[ArgTask], + capacity: CVar, cumulative_options: CumulativePropagatorOptions, - constraint_tag: ConstraintTag, - ) -> TimeTablePerPointIncrementalPropagator { - let tasks = create_tasks(arg_tasks); - let parameters = CumulativeParameters::new(tasks, capacity, cumulative_options); - let updatable_structures = UpdatableStructures::new(¶meters); + inference_code: InferenceCode, + ) -> TimeTablePerPointIncrementalPropagator { + let tasks = create_tasks(context.as_readonly(), arg_tasks); + + let parameters = + CumulativeParameters::new(context.as_readonly(), tasks, capacity, cumulative_options); + register_tasks( + ¶meters.tasks, + ¶meters.capacity, + context.reborrow(), + cumulative_options.incremental_backtracking, + ); + + let mut updatable_structures = UpdatableStructures::new(¶meters); + updatable_structures.initialise_bounds_and_remove_fixed(context.as_readonly(), ¶meters); + TimeTablePerPointIncrementalPropagator { time_table: BTreeMap::new(), parameters, updatable_structures, found_previous_conflict: false, - is_time_table_outdated: false, - constraint_tag, - inference_code: None, + is_time_table_outdated: true, + inference_code, } } @@ -146,7 +202,7 @@ impl &mut self, context: PropagationContext, mandatory_part_adjustments: &MandatoryPartAdjustments, - task: &Rc>, + task: &Rc>, ) -> PropagationStatusCP { // Go over all of the updated tasks and calculate the added mandatory part (we know // that for each of these tasks, a mandatory part exists, otherwise it would not @@ -169,19 +225,21 @@ impl ); // Add the updated profile to the ResourceProfile at time t - let current_profile: &mut ResourceProfile = self + let current_profile: &mut ResourceProfile = self .time_table .entry(time_point as u32) .or_insert(ResourceProfile::default(time_point)); - current_profile.height += task.resource_usage; + current_profile.height += context.lower_bound(&task.resource_usage); current_profile.profile_tasks.push(Rc::clone(task)); - if current_profile.height > self.parameters.capacity && conflict.is_none() { + if current_profile.height > context.upper_bound(&self.parameters.capacity) + && conflict.is_none() + { // The newly introduced mandatory part(s) caused an overflow of the resource - conflict = Some(Err(create_conflict_explanation( + conflict = Some(Err(create_explanation_profile_height( context, - self.inference_code.unwrap(), + self.inference_code, current_profile, self.parameters.options.explanation_type, ) @@ -200,8 +258,9 @@ impl /// Removes the removed parts in the provided [`MandatoryPartAdjustments`] from the time-table fn remove_from_time_table( &mut self, + context: PropagationContext, mandatory_part_adjustments: &MandatoryPartAdjustments, - task: &Rc>, + task: &Rc>, ) { for time_point in mandatory_part_adjustments.get_removed_parts().flatten() { pumpkin_assert_extreme!( @@ -224,7 +283,7 @@ impl .entry(time_point as u32) .and_modify(|profile| { // We remove the resource usage of the task from the height of the profile - profile.height -= task.resource_usage; + profile.height -= context.lower_bound(&task.resource_usage); // If the height of the profile is not equal to 0 then we remove the task // from the profile tasks @@ -257,8 +316,8 @@ impl if self.is_time_table_outdated { // We create the time-table from scratch (and return an error if it overflows) self.time_table = create_time_table_per_point_from_scratch( - context.as_readonly(), - self.inference_code.unwrap(), + context, + self.inference_code, &self.parameters, )?; @@ -280,13 +339,18 @@ impl let element = self.updatable_structures.get_update_for_task(&updated_task); // We get the adjustments based on the stored updated - let mandatory_part_adjustments = element.get_mandatory_part_adjustments(); + let mandatory_part_adjustments = + element.get_mandatory_part_adjustments(context.as_readonly()); // Then we first remove from the time-table (if necessary) // // This order ensures that there is less of a chance of incorrect overflows being // reported - self.remove_from_time_table(&mandatory_part_adjustments, &updated_task); + self.remove_from_time_table( + context.as_readonly(), + &mandatory_part_adjustments, + &updated_task, + ); // Then we add to the time-table (if necessary) // @@ -312,8 +376,11 @@ impl if SYNCHRONISE { // If we are synchronising then we need to search for the conflict which would have // been found by the non-incremental propagator - let synchronised_conflict = - find_synchronised_conflict(&mut self.time_table, &self.parameters); + let synchronised_conflict = find_synchronised_conflict( + context.as_readonly(), + &mut self.time_table, + &self.parameters, + ); // After finding the profile which would have been found by the non-incremental // propagator, we also need to find the profile explanation which would have been @@ -326,21 +393,11 @@ impl let synchronised_conflict_explanation = create_synchronised_conflict_explanation( context.as_readonly(), - self.inference_code.unwrap(), + self.inference_code, conflicting_profile, &self.parameters, ); - pumpkin_assert_extreme!( - check_synchronisation_conflict_explanation_per_point( - &synchronised_conflict_explanation, - context.as_readonly(), - self.inference_code.unwrap(), - &self.parameters, - ), - "The conflict explanation was not the same as the conflict explanation from scratch!" - ); - // We have found the previous conflict self.found_previous_conflict = true; @@ -351,17 +408,16 @@ impl self.found_previous_conflict = false; } else { // We linearly scan the profiles and find the first one which exceeds the capacity - let conflicting_profile = self - .time_table - .values_mut() - .find(|profile| profile.height > self.parameters.capacity); + let conflicting_profile = self.time_table.values_mut().find(|profile| { + profile.height > context.upper_bound(&self.parameters.capacity) + }); // If we have found such a conflict then we return it if let Some(conflicting_profile) = conflicting_profile { pumpkin_assert_extreme!( create_time_table_per_point_from_scratch( - context.as_readonly(), - self.inference_code.unwrap(), + context, + self.inference_code, &self.parameters ) .is_err(), @@ -370,9 +426,9 @@ impl // We have found the previous conflict self.found_previous_conflict = true; - return Err(create_conflict_explanation( + return Err(create_explanation_profile_height( context.as_readonly(), - self.inference_code.unwrap(), + self.inference_code, conflicting_profile, self.parameters.options.explanation_type, ) @@ -395,14 +451,19 @@ impl pumpkin_assert_extreme!( self.time_table .values() - .all(|profile| profile.height <= self.parameters.capacity) + .all(|profile| profile.height <= context.upper_bound(&self.parameters.capacity)) ); Ok(()) } } -impl Propagator - for TimeTablePerPointIncrementalPropagator +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, + const SYNCHRONISE: bool, +> Propagator for TimeTablePerPointIncrementalPropagator { fn propagate(&mut self, mut context: PropagationContextMut) -> PropagationStatusCP { pumpkin_assert_advanced!( @@ -417,16 +478,22 @@ impl Propagator if self.parameters.is_infeasible { return Err(Inconsistency::Conflict(PropagatorConflict { conjunction: conjunction!(), - inference_code: self.inference_code.unwrap(), + inference_code: self.inference_code, })); } // We update the time-table based on the stored updates self.update_time_table(&mut context)?; - pumpkin_assert_extreme!(debug::time_tables_are_the_same_point::( - context.as_readonly(), - self.inference_code.unwrap(), + pumpkin_assert_extreme!(debug::time_tables_are_the_same_point::< + Var, + PVar, + RVar, + CVar, + SYNCHRONISE, + >( + &mut context, + self.inference_code, &self.time_table, &self.parameters )); @@ -437,7 +504,7 @@ impl Propagator // could cause another propagation by a profile which has not been updated propagate_based_on_timetable( &mut context, - self.inference_code.unwrap(), + self.inference_code, self.time_table.values(), &self.parameters, &mut self.updatable_structures, @@ -448,7 +515,7 @@ impl Propagator &mut self, context: PropagationContextWithTrailedValues, local_id: LocalId, - event: OpaqueDomainEvent, + _event: OpaqueDomainEvent, ) -> EnqueueDecision { let updated_task = Rc::clone(&self.parameters.tasks[local_id.unpack() as usize]); // Note that we do not take into account the fact that the time-table could be outdated @@ -476,11 +543,11 @@ impl Propagator &updated_task, ); - if matches!( - updated_task.start_variable.unpack_event(event), - DomainEvent::Assign - ) { - self.updatable_structures.fix_task(&updated_task); + if context.is_fixed(&updated_task.start_variable) + && context.is_fixed(&updated_task.processing_time) + && context.is_fixed(&updated_task.resource_usage) + { + self.updatable_structures.fix_task(&updated_task) } result.decision @@ -543,7 +610,7 @@ impl Propagator // Use the same debug propagator from `TimeTablePerPoint` debug_propagate_from_scratch_time_table_point( &mut context, - self.inference_code.unwrap(), + self.inference_code, &self.parameters, &self.updatable_structures, ) @@ -553,7 +620,7 @@ impl Propagator /// Contains functions related to debugging mod debug { - use crate::engine::propagation::PropagationContext; + use crate::engine::propagation::PropagationContextMut; use crate::proof::InferenceCode; use crate::propagators::CumulativeParameters; use crate::propagators::PerPointTimeTableType; @@ -571,12 +638,15 @@ mod debug { /// the same! pub(crate) fn time_tables_are_the_same_point< Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, const SYNCHRONISE: bool, >( - context: PropagationContext, + context: &mut PropagationContextMut, inference_code: InferenceCode, - time_table: &PerPointTimeTableType, - parameters: &CumulativeParameters, + time_table: &PerPointTimeTableType, + parameters: &CumulativeParameters, ) -> bool { let time_table_scratch = create_time_table_per_point_from_scratch(context, inference_code, parameters) @@ -622,17 +692,18 @@ mod debug { #[cfg(test)] mod tests { use crate::basic_types::Inconsistency; + use crate::basic_types::PropagatorConflict; use crate::conjunction; + use crate::constraint_arguments::CumulativeExplanationType; use crate::engine::predicates::predicate::Predicate; use crate::engine::propagation::EnqueueDecision; use crate::engine::test_solver::TestSolver; use crate::predicate; use crate::predicates::PredicateConstructor; use crate::propagators::ArgTask; - use crate::propagators::CumulativeExplanationType; use crate::propagators::CumulativePropagatorOptions; - use crate::propagators::TimeTablePerPointIncrementalPropagator; - use crate::propagators::TimeTablePerPointPropagator; + use crate::propagators::TimeTablePerPointConstructor; + use crate::propagators::TimeTablePerPointIncrementalConstructor; use crate::variables::DomainId; #[test] @@ -643,27 +714,31 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator( - TimeTablePerPointIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 4, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 3, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions::default(), - constraint_tag, - ), - ) + .new_propagator(TimeTablePerPointIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 4, + resource_usage: 1, + }, + ArgTask { + start_time: s2, + processing_time: 3, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions::default(), + constraint_tag, + )) .expect("No conflict"); assert_eq!(solver.lower_bound(s2), 5); assert_eq!(solver.upper_bound(s2), 8); @@ -678,9 +753,67 @@ mod tests { let s2 = solver.new_variable(1, 1); let constraint_tag = solver.new_constraint_tag(); - let result = solver.new_propagator( - TimeTablePerPointIncrementalPropagator::::new( - &[ + let result = solver.new_propagator(TimeTablePerPointIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 4, + resource_usage: 1, + }, + ArgTask { + start_time: s2, + processing_time: 4, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions { + explanation_type: CumulativeExplanationType::Naive, + ..Default::default() + }, + constraint_tag, + )); + + assert!(result.is_err()); + let reason = solver.get_reason_int(Predicate::trivially_false()); + let expected = [ + predicate!(s1 <= 1), + predicate!(s1 >= 1), + predicate!(s2 >= 1), + predicate!(s2 <= 1), + ]; + assert!( + expected + .iter() + .all(|y| { reason.iter().collect::>().contains(&y) }) + && reason.iter().all(|y| expected.contains(y)) + ); + } + + #[test] + fn propagator_propagates_nothing() { + let mut solver = TestSolver::default(); + let s1 = solver.new_variable(0, 6); + let s2 = solver.new_variable(0, 6); + let constraint_tag = solver.new_constraint_tag(); + + let _ = solver + .new_propagator(TimeTablePerPointIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ ArgTask { start_time: s1, processing_time: 4, @@ -688,68 +821,16 @@ mod tests { }, ArgTask { start_time: s2, - processing_time: 4, + processing_time: 3, resource_usage: 1, }, ] .into_iter() .collect::>(), 1, - CumulativePropagatorOptions { - explanation_type: CumulativeExplanationType::Naive, - ..Default::default() - }, + CumulativePropagatorOptions::default(), constraint_tag, - ), - ); - assert!(match result { - Err(Inconsistency::Conflict(x)) => { - let expected = [ - predicate!(s1 <= 1), - predicate!(s1 >= 1), - predicate!(s2 <= 1), - predicate!(s2 >= 1), - ]; - expected.iter().all(|y| { - x.conjunction - .iter() - .collect::>() - .contains(&y) - }) && x.conjunction.iter().all(|y| expected.contains(y)) - } - _ => false, - }); - } - - #[test] - fn propagator_propagates_nothing() { - let mut solver = TestSolver::default(); - let s1 = solver.new_variable(0, 6); - let s2 = solver.new_variable(0, 6); - let constraint_tag = solver.new_constraint_tag(); - - let _ = solver - .new_propagator( - TimeTablePerPointIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 4, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 3, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions::default(), - constraint_tag, - ), - ) + )) .expect("No conflict"); assert_eq!(solver.lower_bound(s2), 0); assert_eq!(solver.upper_bound(s2), 6); @@ -769,47 +850,51 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator( - TimeTablePerPointIncrementalPropagator::::new( - &[ - ArgTask { - start_time: a, - processing_time: 2, - resource_usage: 1, - }, - ArgTask { - start_time: b, - processing_time: 6, - resource_usage: 2, - }, - ArgTask { - start_time: c, - processing_time: 2, - resource_usage: 4, - }, - ArgTask { - start_time: d, - processing_time: 2, - resource_usage: 2, - }, - ArgTask { - start_time: e, - processing_time: 5, - resource_usage: 2, - }, - ArgTask { - start_time: f, - processing_time: 6, - resource_usage: 2, - }, - ] - .into_iter() - .collect::>(), - 5, - CumulativePropagatorOptions::default(), - constraint_tag, - ), - ) + .new_propagator(TimeTablePerPointIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: a, + processing_time: 2, + resource_usage: 1, + }, + ArgTask { + start_time: b, + processing_time: 6, + resource_usage: 2, + }, + ArgTask { + start_time: c, + processing_time: 2, + resource_usage: 4, + }, + ArgTask { + start_time: d, + processing_time: 2, + resource_usage: 2, + }, + ArgTask { + start_time: e, + processing_time: 5, + resource_usage: 2, + }, + ArgTask { + start_time: f, + processing_time: 6, + resource_usage: 2, + }, + ] + .into_iter() + .collect::>(), + 5, + CumulativePropagatorOptions::default(), + constraint_tag, + )) .expect("No conflict"); assert_eq!(solver.lower_bound(f), 10); } @@ -822,27 +907,31 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator( - TimeTablePerPointIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 2, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 3, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions::default(), - constraint_tag, - ), - ) + .new_propagator(TimeTablePerPointIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 2, + resource_usage: 1, + }, + ArgTask { + start_time: s2, + processing_time: 3, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions::default(), + constraint_tag, + )) .expect("No conflict"); assert_eq!(solver.lower_bound(s2), 6); assert_eq!(solver.upper_bound(s2), 10); @@ -870,30 +959,34 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator( - TimeTablePerPointIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 4, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 3, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions { - explanation_type: CumulativeExplanationType::Naive, - ..Default::default() - }, - constraint_tag, - ), - ) + .new_propagator(TimeTablePerPointIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 4, + resource_usage: 1, + }, + ArgTask { + start_time: s2, + processing_time: 3, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions { + explanation_type: CumulativeExplanationType::Naive, + ..Default::default() + }, + constraint_tag, + )) .expect("No conflict"); let result = solver.propagate_until_fixed_point(propagator); assert!(result.is_ok()); @@ -918,47 +1011,51 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator( - TimeTablePerPointIncrementalPropagator::::new( - &[ - ArgTask { - start_time: a, - processing_time: 2, - resource_usage: 1, - }, - ArgTask { - start_time: b, - processing_time: 6, - resource_usage: 2, - }, - ArgTask { - start_time: c, - processing_time: 2, - resource_usage: 4, - }, - ArgTask { - start_time: d, - processing_time: 2, - resource_usage: 2, - }, - ArgTask { - start_time: e, - processing_time: 4, - resource_usage: 2, - }, - ArgTask { - start_time: f, - processing_time: 6, - resource_usage: 2, - }, - ] - .into_iter() - .collect::>(), - 5, - CumulativePropagatorOptions::default(), - constraint_tag, - ), - ) + .new_propagator(TimeTablePerPointIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: a, + processing_time: 2, + resource_usage: 1, + }, + ArgTask { + start_time: b, + processing_time: 6, + resource_usage: 2, + }, + ArgTask { + start_time: c, + processing_time: 2, + resource_usage: 4, + }, + ArgTask { + start_time: d, + processing_time: 2, + resource_usage: 2, + }, + ArgTask { + start_time: e, + processing_time: 4, + resource_usage: 2, + }, + ArgTask { + start_time: f, + processing_time: 6, + resource_usage: 2, + }, + ] + .into_iter() + .collect::>(), + 5, + CumulativePropagatorOptions::default(), + constraint_tag, + )) .expect("No conflict"); assert_eq!(solver.lower_bound(a), 0); assert_eq!(solver.upper_bound(a), 1); @@ -996,52 +1093,56 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator( - TimeTablePerPointIncrementalPropagator::::new( - &[ - ArgTask { - start_time: a, - processing_time: 2, - resource_usage: 1, - }, - ArgTask { - start_time: b1, - processing_time: 2, - resource_usage: 2, - }, - ArgTask { - start_time: b2, - processing_time: 3, - resource_usage: 2, - }, - ArgTask { - start_time: c, - processing_time: 2, - resource_usage: 4, - }, - ArgTask { - start_time: d, - processing_time: 2, - resource_usage: 2, - }, - ArgTask { - start_time: e, - processing_time: 4, - resource_usage: 2, - }, - ArgTask { - start_time: f, - processing_time: 6, - resource_usage: 2, - }, - ] - .into_iter() - .collect::>(), - 5, - CumulativePropagatorOptions::default(), - constraint_tag, - ), - ) + .new_propagator(TimeTablePerPointIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: a, + processing_time: 2, + resource_usage: 1, + }, + ArgTask { + start_time: b1, + processing_time: 2, + resource_usage: 2, + }, + ArgTask { + start_time: b2, + processing_time: 3, + resource_usage: 2, + }, + ArgTask { + start_time: c, + processing_time: 2, + resource_usage: 4, + }, + ArgTask { + start_time: d, + processing_time: 2, + resource_usage: 2, + }, + ArgTask { + start_time: e, + processing_time: 4, + resource_usage: 2, + }, + ArgTask { + start_time: f, + processing_time: 6, + resource_usage: 2, + }, + ] + .into_iter() + .collect::>(), + 5, + CumulativePropagatorOptions::default(), + constraint_tag, + )) .expect("No conflict"); assert_eq!(solver.lower_bound(a), 0); assert_eq!(solver.upper_bound(a), 1); @@ -1072,30 +1173,34 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator( - TimeTablePerPointIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 4, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 3, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions { - explanation_type: CumulativeExplanationType::Naive, - ..Default::default() - }, - constraint_tag, - ), - ) + .new_propagator(TimeTablePerPointIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 4, + resource_usage: 1, + }, + ArgTask { + start_time: s2, + processing_time: 3, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions { + explanation_type: CumulativeExplanationType::Naive, + ..Default::default() + }, + constraint_tag, + )) .expect("No conflict"); assert_eq!(solver.lower_bound(s2), 5); assert_eq!(solver.upper_bound(s2), 8); @@ -1125,35 +1230,39 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator( - TimeTablePerPointIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 2, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 2, - resource_usage: 1, - }, - ArgTask { - start_time: s3, - processing_time: 4, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions { - explanation_type: CumulativeExplanationType::Naive, - ..Default::default() - }, - constraint_tag, - ), - ) + .new_propagator(TimeTablePerPointIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 2, + resource_usage: 1, + }, + ArgTask { + start_time: s2, + processing_time: 2, + resource_usage: 1, + }, + ArgTask { + start_time: s3, + processing_time: 4, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions { + explanation_type: CumulativeExplanationType::Naive, + ..Default::default() + }, + constraint_tag, + )) .expect("No conflict"); assert_eq!(solver.lower_bound(s3), 7); assert_eq!(solver.upper_bound(s3), 15); @@ -1181,31 +1290,35 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator( - TimeTablePerPointIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 4, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 3, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions { - explanation_type: CumulativeExplanationType::Naive, - allow_holes_in_domain: true, - ..Default::default() - }, - constraint_tag, - ), - ) + .new_propagator(TimeTablePerPointIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 4, + resource_usage: 1, + }, + ArgTask { + start_time: s2, + processing_time: 3, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions { + explanation_type: CumulativeExplanationType::Naive, + allow_holes_in_domain: true, + ..Default::default() + }, + constraint_tag, + )) .expect("No conflict"); assert_eq!(solver.lower_bound(s2), 0); assert_eq!(solver.upper_bound(s2), 8); @@ -1227,8 +1340,8 @@ mod tests { let s3_scratch = solver_scratch.new_variable(1, 10); let constraint_tag = solver_scratch.new_constraint_tag(); let propagator_scratch = solver_scratch - .new_propagator(TimeTablePerPointPropagator::new( - &[ + .new_propagator(TimeTablePerPointConstructor::new( + [ ArgTask { start_time: s1_scratch, processing_time: 2, @@ -1267,54 +1380,56 @@ mod tests { let s3 = solver.new_variable(1, 10); let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator( - TimeTablePerPointIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 2, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 4, - resource_usage: 1, - }, - ArgTask { - start_time: s3, - processing_time: 4, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions { - explanation_type: CumulativeExplanationType::Naive, - ..Default::default() - }, - constraint_tag, - ), - ) + .new_propagator(TimeTablePerPointIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + true, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 2, + resource_usage: 1, + }, + ArgTask { + start_time: s2, + processing_time: 4, + resource_usage: 1, + }, + ArgTask { + start_time: s3, + processing_time: 4, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions { + explanation_type: CumulativeExplanationType::Naive, + ..Default::default() + }, + constraint_tag, + )) .expect("No conflict"); let _ = solver.increase_lower_bound_and_notify(propagator, 2, s3, 7); let _ = solver.increase_lower_bound_and_notify(propagator, 1, s2, 7); let result = solver.propagate(propagator); - assert!( - { - if let Err(Inconsistency::Conflict(conflict)) = &result { - if let Err(Inconsistency::Conflict(explanation_scratch)) = &result_scratch { - conflict.conjunction.iter().collect::>() - == explanation_scratch.conjunction.iter().collect::>() - } else { - false - } - } else { - false - } - }, - "The results are different than expected - Expected: {result_scratch:?} but was: {result:?}" - ); + if let Err(Inconsistency::Conflict(conflict)) = &result + && let Err(Inconsistency::EmptyDomain) = &result_scratch + { + let reason_scratch = solver_scratch.get_reason_empty_domain(); + assert_eq!( + conflict.conjunction.iter().copied().collect::>(), + reason_scratch + ) + } else { + panic!( + "The results are different than expected - Expected: {result_scratch:?} but was: {result:?}" + ) + } } #[test] @@ -1325,8 +1440,8 @@ mod tests { let s3_scratch = solver_scratch.new_variable(1, 10); let constraint_tag = solver_scratch.new_constraint_tag(); let propagator_scratch = solver_scratch - .new_propagator(TimeTablePerPointPropagator::new( - &[ + .new_propagator(TimeTablePerPointConstructor::new( + [ ArgTask { start_time: s1_scratch, processing_time: 2, @@ -1364,54 +1479,58 @@ mod tests { let s3 = solver.new_variable(1, 10); let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator( - TimeTablePerPointIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 2, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 4, - resource_usage: 1, - }, - ArgTask { - start_time: s3, - processing_time: 4, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions { - explanation_type: CumulativeExplanationType::Naive, - ..Default::default() - }, - constraint_tag, - ), - ) + .new_propagator(TimeTablePerPointIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + true, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 2, + resource_usage: 1, + }, + ArgTask { + start_time: s2, + processing_time: 4, + resource_usage: 1, + }, + ArgTask { + start_time: s3, + processing_time: 4, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions { + explanation_type: CumulativeExplanationType::Naive, + ..Default::default() + }, + constraint_tag, + )) .expect("No conflict"); let _ = solver.increase_lower_bound_and_notify(propagator, 2, s3, 7); let _ = solver.increase_lower_bound_and_notify(propagator, 1, s2, 7); let result = solver.propagate(propagator); - assert!(result.is_err()); let result_scratch = solver_scratch.propagate(propagator_scratch); - assert!(result_scratch.is_err()); - assert!({ - if let Err(Inconsistency::Conflict(explanation)) = &result { - if let Err(Inconsistency::Conflict(explanation_scratch)) = &result_scratch { - explanation.conjunction.iter().collect::>() - == explanation_scratch.conjunction.iter().collect::>() - } else { - false - } - } else { - false - } - }); + + if let Err(Inconsistency::Conflict(explanation)) = &result + && let Err(Inconsistency::EmptyDomain) = &result_scratch + { + let reason_scratch = solver_scratch.get_reason_empty_domain(); + assert_eq!( + explanation.conjunction.iter().copied().collect::>(), + reason_scratch + ) + } else { + panic!( + "Expected {result_scratch:?} to be an empty domain and {result:?} to be a conflict" + ) + } } #[test] @@ -1422,8 +1541,8 @@ mod tests { let s3_scratch = solver_scratch.new_variable(1, 10); let constraint_tag = solver_scratch.new_constraint_tag(); let propagator_scratch = solver_scratch - .new_propagator(TimeTablePerPointPropagator::new( - &[ + .new_propagator(TimeTablePerPointConstructor::new( + [ ArgTask { start_time: s1_scratch, processing_time: 2, @@ -1454,6 +1573,7 @@ mod tests { solver_scratch.increase_lower_bound_and_notify(propagator_scratch, 2, s3_scratch, 7); let _ = solver_scratch.increase_lower_bound_and_notify(propagator_scratch, 1, s2_scratch, 7); + let result_scratch = solver_scratch.propagate(propagator_scratch); let mut solver = TestSolver::default(); let s1 = solver.new_variable(5, 5); @@ -1461,52 +1581,55 @@ mod tests { let s3 = solver.new_variable(1, 10); let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator( - TimeTablePerPointIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 2, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 4, - resource_usage: 1, - }, - ArgTask { - start_time: s3, - processing_time: 4, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions { - explanation_type: CumulativeExplanationType::Naive, - ..Default::default() - }, - constraint_tag, - ), - ) + .new_propagator(TimeTablePerPointIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 2, + resource_usage: 1, + }, + ArgTask { + start_time: s2, + processing_time: 4, + resource_usage: 1, + }, + ArgTask { + start_time: s3, + processing_time: 4, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions { + explanation_type: CumulativeExplanationType::Naive, + ..Default::default() + }, + constraint_tag, + )) .expect("No conflict"); let _ = solver.increase_lower_bound_and_notify(propagator, 2, s3, 7); let _ = solver.increase_lower_bound_and_notify(propagator, 1, s2, 7); let result = solver.propagate(propagator); - let result_scratch = solver_scratch.propagate(propagator_scratch); - assert!({ - if let Err(Inconsistency::Conflict(explanation)) = &result { - if let Err(Inconsistency::Conflict(explanation_scratch)) = &result_scratch { - explanation.conjunction.iter().collect::>() - != explanation_scratch.conjunction.iter().collect::>() - } else { - false - } - } else { - false - } - }); + + if let Err(Inconsistency::Conflict(explanation)) = &result + && let Err(Inconsistency::EmptyDomain) = &result_scratch + { + let reason_scratch = solver_scratch.get_reason_empty_domain(); + assert_ne!( + explanation.conjunction.iter().copied().collect::>(), + reason_scratch + ) + } else { + panic!("{result:?} is not an error or {result_scratch:?} is not an error") + } } #[test] @@ -1517,8 +1640,8 @@ mod tests { let s3_scratch = solver_scratch.new_variable(5, 11); let constraint_tag = solver_scratch.new_constraint_tag(); let propagator_scratch = solver_scratch - .new_propagator(TimeTablePerPointPropagator::new( - &[ + .new_propagator(TimeTablePerPointConstructor::new( + [ ArgTask { start_time: s1_scratch, processing_time: 2, @@ -1556,35 +1679,39 @@ mod tests { let s3 = solver.new_variable(5, 11); let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator( - TimeTablePerPointIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 2, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 4, - resource_usage: 1, - }, - ArgTask { - start_time: s3, - processing_time: 4, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 2, - CumulativePropagatorOptions { - explanation_type: CumulativeExplanationType::Naive, - ..Default::default() - }, - constraint_tag, - ), - ) + .new_propagator(TimeTablePerPointIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + true, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 2, + resource_usage: 1, + }, + ArgTask { + start_time: s2, + processing_time: 4, + resource_usage: 1, + }, + ArgTask { + start_time: s3, + processing_time: 4, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 2, + CumulativePropagatorOptions { + explanation_type: CumulativeExplanationType::Naive, + ..Default::default() + }, + constraint_tag, + )) .expect("No conflict"); let _ = solver.increase_lower_bound_and_notify(propagator, 1, s2, 5); let result = solver.propagate(propagator); @@ -1611,8 +1738,8 @@ mod tests { let s3_scratch = solver_scratch.new_variable(5, 11); let constraint_tag = solver_scratch.new_constraint_tag(); let propagator_scratch = solver_scratch - .new_propagator(TimeTablePerPointPropagator::new( - &[ + .new_propagator(TimeTablePerPointConstructor::new( + [ ArgTask { start_time: s1_scratch, processing_time: 2, @@ -1649,35 +1776,39 @@ mod tests { let s3 = solver.new_variable(5, 11); let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator( - TimeTablePerPointIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s1, - processing_time: 2, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 4, - resource_usage: 1, - }, - ArgTask { - start_time: s3, - processing_time: 4, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 2, - CumulativePropagatorOptions { - explanation_type: CumulativeExplanationType::Naive, - ..Default::default() - }, - constraint_tag, - ), - ) + .new_propagator(TimeTablePerPointIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: s1, + processing_time: 2, + resource_usage: 1, + }, + ArgTask { + start_time: s2, + processing_time: 4, + resource_usage: 1, + }, + ArgTask { + start_time: s3, + processing_time: 4, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 2, + CumulativePropagatorOptions { + explanation_type: CumulativeExplanationType::Naive, + ..Default::default() + }, + constraint_tag, + )) .expect("No conflict"); let _ = solver.increase_lower_bound_and_notify(propagator, 1, s2, 5); let result = solver.propagate(propagator); @@ -1709,8 +1840,8 @@ mod tests { let constraint_tag = solver_scratch.new_constraint_tag(); let propagator_scratch = solver_scratch - .new_propagator(TimeTablePerPointPropagator::new( - &[ + .new_propagator(TimeTablePerPointConstructor::new( + [ ArgTask { start_time: s0_scratch, processing_time: 4, @@ -1753,35 +1884,39 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator( - TimeTablePerPointIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s0, - processing_time: 4, - resource_usage: 1, - }, - ArgTask { - start_time: s1, - processing_time: 1, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 1, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions { - explanation_type: CumulativeExplanationType::Naive, - ..Default::default() - }, - constraint_tag, - ), - ) + .new_propagator(TimeTablePerPointIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + false, + >::new( + [ + ArgTask { + start_time: s0, + processing_time: 4, + resource_usage: 1, + }, + ArgTask { + start_time: s1, + processing_time: 1, + resource_usage: 1, + }, + ArgTask { + start_time: s2, + processing_time: 1, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions { + explanation_type: CumulativeExplanationType::Naive, + ..Default::default() + }, + constraint_tag, + )) .expect("No conflict"); let _ = solver.increase_lower_bound_and_notify(propagator, 2, s2, 5); let _ = solver.increase_lower_bound_and_notify(propagator, 1, s1, 5); @@ -1792,26 +1927,20 @@ mod tests { assert!(result_scratch.is_err()); let result = solver.propagate(propagator); assert!(result.is_err()); - if let ( - Err(Inconsistency::Conflict(explanation)), - Err(Inconsistency::Conflict(explanation_scratch)), - ) = (result, result_scratch) - { - assert_ne!(explanation, explanation_scratch); - let explanation_vec = explanation.conjunction.iter().cloned().collect::>(); - let explanation_scratch_vec = explanation_scratch - .conjunction - .iter() - .cloned() - .collect::>(); - println!("{explanation_vec:?}"); - println!("{explanation_scratch_vec:?}"); + let reason_scratch = solver_scratch.get_reason_int(Predicate::trivially_false()); - assert!(explanation_vec.contains(&s2.lower_bound_predicate(5))); - assert!(!explanation_scratch_vec.contains(&s2.lower_bound_predicate(5))); + if let Err(Inconsistency::Conflict(PropagatorConflict { + conjunction, + inference_code: _, + })) = result + { + assert_ne!(conjunction, reason_scratch); + + assert!(conjunction.contains(s2.lower_bound_predicate(5))); + assert!(!reason_scratch.contains(s2.lower_bound_predicate(5))); } else { - panic!("Incorrect result") + panic!() } } @@ -1824,8 +1953,8 @@ mod tests { let constraint_tag = solver_scratch.new_constraint_tag(); let propagator_scratch = solver_scratch - .new_propagator(TimeTablePerPointPropagator::new( - &[ + .new_propagator(TimeTablePerPointConstructor::new( + [ ArgTask { start_time: s0_scratch, processing_time: 4, @@ -1867,35 +1996,39 @@ mod tests { let s2 = solver.new_variable(1, 5); let propagator = solver - .new_propagator( - TimeTablePerPointIncrementalPropagator::::new( - &[ - ArgTask { - start_time: s0, - processing_time: 4, - resource_usage: 1, - }, - ArgTask { - start_time: s1, - processing_time: 1, - resource_usage: 1, - }, - ArgTask { - start_time: s2, - processing_time: 1, - resource_usage: 1, - }, - ] - .into_iter() - .collect::>(), - 1, - CumulativePropagatorOptions { - explanation_type: CumulativeExplanationType::Naive, - ..Default::default() - }, - constraint_tag, - ), - ) + .new_propagator(TimeTablePerPointIncrementalConstructor::< + DomainId, + i32, + i32, + i32, + true, + >::new( + [ + ArgTask { + start_time: s0, + processing_time: 4, + resource_usage: 1, + }, + ArgTask { + start_time: s1, + processing_time: 1, + resource_usage: 1, + }, + ArgTask { + start_time: s2, + processing_time: 1, + resource_usage: 1, + }, + ] + .into_iter() + .collect::>(), + 1, + CumulativePropagatorOptions { + explanation_type: CumulativeExplanationType::Naive, + ..Default::default() + }, + constraint_tag, + )) .expect("No conflict"); let _ = solver.increase_lower_bound_and_notify(propagator, 2, s2, 5); let _ = solver.increase_lower_bound_and_notify(propagator, 1, s1, 5); @@ -1906,15 +2039,11 @@ mod tests { assert!(result_scratch.is_err()); let result = solver.propagate(propagator); assert!(result.is_err()); - if let ( - Err(Inconsistency::Conflict(explanation)), - Err(Inconsistency::Conflict(explanation_scratch)), - ) = (result, result_scratch) - { - assert_eq!( - explanation.conjunction.iter().collect::>(), - explanation_scratch.conjunction.iter().collect::>() - ); + + let reason_scratch = solver_scratch.get_reason_int(Predicate::trivially_false()); + + if let Err(Inconsistency::Conflict(explanation)) = result { + assert_eq!(explanation.conjunction, reason_scratch); } else { panic!("Incorrect result") } diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/propagation_handler.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/propagation_handler.rs index e490b14ed..39f51edc6 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/propagation_handler.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/propagation_handler.rs @@ -84,14 +84,18 @@ impl CumulativePropagationHandler { /// Propagates the lower-bound of the `propagating_task` to not conflict with all of the /// `profiles` anymore. - pub(crate) fn propagate_chain_of_lower_bounds_with_explanations( + pub(crate) fn propagate_chain_of_lower_bounds_with_explanations( &mut self, context: &mut PropagationContextMut, - profiles: &[&ResourceProfile], - propagating_task: &Rc>, + profiles: &[&ResourceProfile], + propagating_task: &Rc>, + capacity: CVar, ) -> Result<(), EmptyDomain> where Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, { pumpkin_assert_simple!(!profiles.is_empty()); match self.explanation_type { @@ -100,11 +104,17 @@ impl CumulativePropagationHandler { for profile in profiles { let explanation = match self.explanation_type { - CumulativeExplanationType::Naive => { - create_naive_propagation_explanation(profile, context.as_readonly()) - } + CumulativeExplanationType::Naive => create_naive_propagation_explanation( + profile, + context.as_readonly(), + capacity.clone(), + ), CumulativeExplanationType::BigStep => { - create_big_step_propagation_explanation(profile) + create_big_step_propagation_explanation( + context.as_readonly(), + profile, + capacity.clone(), + ) } CumulativeExplanationType::Pointwise => { unreachable!( @@ -141,6 +151,7 @@ impl CumulativePropagationHandler { context, profiles, propagating_task, + capacity, self.inference_code, ) } @@ -149,14 +160,18 @@ impl CumulativePropagationHandler { /// Propagates the upper-bound of the `propagating_task` to not conflict with all of the /// `profiles` anymore. - pub(crate) fn propagate_chain_of_upper_bounds_with_explanations( + pub(crate) fn propagate_chain_of_upper_bounds_with_explanations( &mut self, context: &mut PropagationContextMut, - profiles: &[&ResourceProfile], - propagating_task: &Rc>, + profiles: &[&ResourceProfile], + propagating_task: &Rc>, + capacity: CVar, ) -> Result<(), EmptyDomain> where Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, { pumpkin_assert_simple!(!profiles.is_empty()); @@ -166,11 +181,17 @@ impl CumulativePropagationHandler { for profile in profiles { let explanation = match self.explanation_type { - CumulativeExplanationType::Naive => { - create_naive_propagation_explanation(profile, context.as_readonly()) - } + CumulativeExplanationType::Naive => create_naive_propagation_explanation( + profile, + context.as_readonly(), + capacity.clone(), + ), CumulativeExplanationType::BigStep => { - create_big_step_propagation_explanation(profile) + create_big_step_propagation_explanation( + context.as_readonly(), + profile, + capacity.clone(), + ) } CumulativeExplanationType::Pointwise => { unreachable!( @@ -193,7 +214,8 @@ impl CumulativePropagationHandler { ); let predicate = predicate![ propagating_task.start_variable - <= profiles[0].start - propagating_task.processing_time + <= profiles[0].start + - context.lower_bound(&propagating_task.processing_time) ]; pumpkin_assert_extreme!(check_explanation( predicate, @@ -207,6 +229,7 @@ impl CumulativePropagationHandler { context, profiles, propagating_task, + capacity, self.inference_code, ) } @@ -214,14 +237,18 @@ impl CumulativePropagationHandler { } /// Propagates the lower-bound of the `propagating_task` to not conflict with `profile` anymore. - pub(crate) fn propagate_lower_bound_with_explanations( + pub(crate) fn propagate_lower_bound_with_explanations( &mut self, context: &mut PropagationContextMut, - profile: &ResourceProfile, - propagating_task: &Rc>, + profile: &ResourceProfile, + propagating_task: &Rc>, + capacity: CVar, ) -> Result<(), EmptyDomain> where Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, { pumpkin_assert_advanced!( context.lower_bound(&propagating_task.start_variable) < profile.end + 1 @@ -233,8 +260,9 @@ impl CumulativePropagationHandler { // `get_stored_profile_explanation_or_init` and // `create_predicate_propagating_task_lower_bound_propagation` both use the // explanation type to create the explanations. - let explanation = self.get_stored_profile_explanation_or_init(context, profile); - let lower_bound_predicate_propagating_task = + let explanation = + self.get_stored_profile_explanation_or_init(context, profile, capacity); + let lower_bounds_predicate_propagating_task = create_predicate_propagating_task_lower_bound_propagation( self.explanation_type, context.as_readonly(), @@ -250,7 +278,7 @@ impl CumulativePropagationHandler { )); let mut reason = (*explanation).clone(); - reason.add(lower_bound_predicate_propagating_task); + reason.extend(lower_bounds_predicate_propagating_task); context.post(predicate, reason, self.inference_code) } CumulativeExplanationType::Pointwise => { @@ -258,6 +286,7 @@ impl CumulativePropagationHandler { context, &[profile], propagating_task, + capacity, self.inference_code, ) } @@ -265,18 +294,22 @@ impl CumulativePropagationHandler { } /// Propagates the upper-bound of the `propagating_task` to not conflict with `profile` anymore. - pub(crate) fn propagate_upper_bound_with_explanations( + pub(crate) fn propagate_upper_bound_with_explanations( &mut self, context: &mut PropagationContextMut, - profile: &ResourceProfile, - propagating_task: &Rc>, + profile: &ResourceProfile, + propagating_task: &Rc>, + capacity: CVar, ) -> Result<(), EmptyDomain> where Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, { pumpkin_assert_advanced!( context.upper_bound(&propagating_task.start_variable) - > profile.start - propagating_task.processing_time + > profile.start - context.lower_bound(&propagating_task.processing_time) ); match self.explanation_type { @@ -285,8 +318,9 @@ impl CumulativePropagationHandler { // `get_stored_profile_explanation_or_init` and // `create_predicate_propagating_task_upper_bound_propagation` both use the // explanation type to create the explanations. - let explanation = self.get_stored_profile_explanation_or_init(context, profile); - let upper_bound_predicate_propagating_task = + let explanation = + self.get_stored_profile_explanation_or_init(context, profile, capacity); + let upper_bounds_predicate_propagating_task = create_predicate_propagating_task_upper_bound_propagation( self.explanation_type, context.as_readonly(), @@ -296,7 +330,7 @@ impl CumulativePropagationHandler { ); let predicate = predicate![ propagating_task.start_variable - <= profile.start - propagating_task.processing_time + <= profile.start - context.lower_bound(&propagating_task.processing_time) ]; pumpkin_assert_extreme!(check_explanation( predicate, @@ -305,7 +339,7 @@ impl CumulativePropagationHandler { )); let mut reason = (*explanation).clone(); - reason.add(upper_bound_predicate_propagating_task); + reason.extend(upper_bounds_predicate_propagating_task); context.post(predicate, reason, self.inference_code) } CumulativeExplanationType::Pointwise => { @@ -313,6 +347,7 @@ impl CumulativePropagationHandler { context, &[profile], propagating_task, + capacity, self.inference_code, ) } @@ -321,14 +356,18 @@ impl CumulativePropagationHandler { /// Propagates a hole in the domain; note that this explanation does not contain any of the /// bounds of `propagating_task`. - pub(crate) fn propagate_holes_in_domain( + pub(crate) fn propagate_holes_in_domain( &mut self, context: &mut PropagationContextMut, - profile: &ResourceProfile, - propagating_task: &Rc>, + profile: &ResourceProfile, + propagating_task: &Rc>, + capacity: CVar, ) -> Result<(), EmptyDomain> where Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, { // We go through all of the time-points which cause `task` to overlap // with the resource profile @@ -341,7 +380,7 @@ impl CumulativePropagationHandler { // time-point in which case we simply start from the lower-bound of the task. let lower_bound_removed_time_points = max( context.lower_bound(&propagating_task.start_variable), - profile.start - propagating_task.processing_time + 1, + profile.start - context.lower_bound(&propagating_task.processing_time) + 1, ); // There are also two options for determine the highest value to remove @@ -365,7 +404,11 @@ impl CumulativePropagationHandler { // We use the same procedure for the explanation using naive and bigstep, note // that `get_stored_profile_explanation_or_init` uses the // explanation type to create the explanations. - let explanation = self.get_stored_profile_explanation_or_init(context, profile); + let explanation = self.get_stored_profile_explanation_or_init( + context, + profile, + capacity.clone(), + ); let predicate = predicate![propagating_task.start_variable != time_point]; pumpkin_assert_extreme!(check_explanation( predicate, @@ -388,7 +431,7 @@ impl CumulativePropagationHandler { // together with the propagating task would overflow the capacity) let corresponding_profile_explanation_point = if time_point < profile.start { min( - time_point + propagating_task.processing_time - 1, + time_point + context.lower_bound(&propagating_task.processing_time) - 1, (profile.end - profile.start) / 2 + profile.start, ) } else { @@ -396,8 +439,10 @@ impl CumulativePropagationHandler { }; let explanation = create_pointwise_propagation_explanation( + context.as_readonly(), corresponding_profile_explanation_point, profile, + capacity.clone(), ); let predicate = predicate![propagating_task.start_variable != time_point]; pumpkin_assert_extreme!(check_explanation( @@ -420,22 +465,26 @@ impl CumulativePropagationHandler { } /// Either we get the stored stored profile explanation or we initialize it. - fn get_stored_profile_explanation_or_init( + fn get_stored_profile_explanation_or_init( &mut self, context: &mut PropagationContextMut, - profile: &ResourceProfile, + profile: &ResourceProfile, + capacity: CVar, ) -> Rc where Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, { Rc::clone(self.stored_profile_explanation.get_or_init(|| { Rc::new( match self.explanation_type { CumulativeExplanationType::Naive => { - create_naive_propagation_explanation(profile, context.as_readonly()) + create_naive_propagation_explanation(profile, context.as_readonly(), capacity) }, CumulativeExplanationType::BigStep => { - create_big_step_propagation_explanation(profile) + create_big_step_propagation_explanation(context.as_readonly(), profile, capacity) }, CumulativeExplanationType::Pointwise => { unreachable!("At the moment, we do not store the profile explanation for the pointwise explanation since it consists of multiple explanations") @@ -448,24 +497,26 @@ impl CumulativePropagationHandler { /// Creates an explanation of the conflict caused by `conflict_profile` based on the provided /// `explanation_type`. -pub(crate) fn create_conflict_explanation( - context: Context, +pub(crate) fn create_explanation_profile_height( + context: PropagationContext, inference_code: InferenceCode, - conflict_profile: &ResourceProfile, + conflict_profile: &ResourceProfile, explanation_type: CumulativeExplanationType, ) -> PropagatorConflict where Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, { let conjunction = match explanation_type { CumulativeExplanationType::Naive => { create_naive_conflict_explanation(conflict_profile, context) } CumulativeExplanationType::BigStep => { - create_big_step_conflict_explanation(conflict_profile) + create_big_step_conflict_explanation(context, conflict_profile) } CumulativeExplanationType::Pointwise => { - create_pointwise_conflict_explanation(conflict_profile) + create_pointwise_conflict_explanation(context, conflict_profile) } }; @@ -481,7 +532,7 @@ pub(crate) mod test_propagation_handler { use super::CumulativeExplanationType; use super::CumulativePropagationHandler; - use super::create_conflict_explanation; + use super::create_explanation_profile_height; use crate::containers::StorageKey; use crate::engine::Assignments; use crate::engine::TrailedValues; @@ -548,7 +599,7 @@ pub(crate) mod test_propagation_handler { height: 1, }; - let reason = create_conflict_explanation( + let reason = create_explanation_profile_height( PropagationContext::new(&self.assignments), self.propagation_handler.inference_code, &profile, @@ -600,6 +651,7 @@ pub(crate) mod test_propagation_handler { ), &profile, &Rc::new(propagating_task), + 1, ); assert!(result.is_ok()); assert_eq!(self.assignments.get_lower_bound(x), 19); @@ -665,6 +717,7 @@ pub(crate) mod test_propagation_handler { ), &[&profile_y, &profile_z], &Rc::new(propagating_task), + 1, ); assert!(result.is_ok()); assert_eq!(self.assignments.get_lower_bound(x), 22); @@ -716,6 +769,7 @@ pub(crate) mod test_propagation_handler { ), &profile, &Rc::new(propagating_task), + 1, ); assert!(result.is_ok()); assert_eq!(self.assignments.get_upper_bound(x), 10); @@ -781,6 +835,7 @@ pub(crate) mod test_propagation_handler { ), &[&profile_z, &profile_y], &Rc::new(propagating_task), + 1, ); assert!(result.is_ok()); assert_eq!(self.assignments.get_upper_bound(x), 3); diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_over_interval.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_over_interval.rs index b3141d9ec..043bbcb62 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_over_interval.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_over_interval.rs @@ -7,7 +7,6 @@ use crate::basic_types::Inconsistency; use crate::basic_types::PropagationStatusCP; use crate::basic_types::PropagatorConflict; use crate::conjunction; -use crate::engine::notifications::DomainEvent; use crate::engine::notifications::OpaqueDomainEvent; use crate::engine::propagation::EnqueueDecision; use crate::engine::propagation::LocalId; @@ -19,6 +18,7 @@ use crate::engine::propagation::constructor::PropagatorConstructor; use crate::engine::propagation::constructor::PropagatorConstructorContext; use crate::engine::propagation::contexts::PropagationContextWithTrailedValues; use crate::engine::variables::IntegerVariable; +use crate::predicate; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; use crate::propagators::ArgTask; @@ -29,7 +29,7 @@ use crate::propagators::Task; #[cfg(doc)] use crate::propagators::TimeTablePerPointPropagator; use crate::propagators::UpdatableStructures; -use crate::propagators::cumulative::time_table::propagation_handler::create_conflict_explanation; +use crate::propagators::cumulative::time_table::propagation_handler::create_explanation_profile_height; use crate::propagators::util::create_tasks; use crate::propagators::util::register_tasks; use crate::propagators::util::update_bounds_task; @@ -39,14 +39,14 @@ use crate::pumpkin_assert_simple; /// An event storing the start and end of mandatory parts used for creating the time-table #[derive(Debug)] -pub(crate) struct Event { +pub(crate) struct Event { /// The time-point at which the [`Event`] took place time_stamp: i32, /// Change in resource usage at [time_stamp][Event::time_stamp], positive if it is the start of /// a mandatory part and negative otherwise change_in_resource_usage: i32, /// The [`Task`] which has caused the event to take place - task: Rc>, + task: Rc>, } /// [`Propagator`] responsible for using time-table reasoning to propagate the [Cumulative](https://sofdem.github.io/gccat/gccat/Ccumulative.html) constraint @@ -60,82 +60,131 @@ pub(crate) struct Event { /// \[1\] A. Schutt, Improving scheduling by learning. University of Melbourne, Department of /// Computer Science and Software Engineering, 2011. #[derive(Debug)] -pub(crate) struct TimeTableOverIntervalPropagator { +pub(crate) struct TimeTableOverIntervalPropagator { /// Stores whether the time-table is empty is_time_table_empty: bool, /// Stores the input parameters to the cumulative constraint - parameters: CumulativeParameters, + parameters: CumulativeParameters, /// Stores structures which change during the search; used to store the bounds - updatable_structures: UpdatableStructures, + updatable_structures: UpdatableStructures, - // TODO: Update with propagator constructor. + inference_code: InferenceCode, +} + +pub(crate) struct TimeTableOverIntervalConstructor { + tasks: Vec>, + capacity: CVar, + cumulative_options: CumulativePropagatorOptions, constraint_tag: ConstraintTag, - inference_code: Option, +} + +impl TimeTableOverIntervalConstructor { + pub(crate) fn new( + arg_tasks: Vec>, + capacity: CVar, + cumulative_options: CumulativePropagatorOptions, + constraint_tag: ConstraintTag, + ) -> Self { + Self { + tasks: arg_tasks, + capacity, + cumulative_options, + constraint_tag, + } + } +} + +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +> PropagatorConstructor for TimeTableOverIntervalConstructor +{ + type PropagatorImpl = TimeTableOverIntervalPropagator; + + fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + let inference_code = context.create_inference_code(self.constraint_tag, TimeTable); + + TimeTableOverIntervalPropagator::new( + context, + &self.tasks, + self.capacity, + self.cumulative_options, + inference_code, + ) + } } /// The type of the time-table used by propagators which use time-table reasoning over intervals. /// /// The [ResourceProfile]s are sorted based on start time and they are non-overlapping; each entry /// in the [`Vec`] represents the mandatory resource usage across an interval. -pub(crate) type OverIntervalTimeTableType = Vec>; +pub(crate) type OverIntervalTimeTableType = Vec>; -impl TimeTableOverIntervalPropagator { - pub(crate) fn new( - arg_tasks: &[ArgTask], - capacity: i32, +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +> TimeTableOverIntervalPropagator +{ + fn new( + mut context: PropagatorConstructorContext, + arg_tasks: &[ArgTask], + capacity: CVar, cumulative_options: CumulativePropagatorOptions, - constraint_tag: ConstraintTag, - ) -> TimeTableOverIntervalPropagator { - let tasks = create_tasks(arg_tasks); - let parameters = CumulativeParameters::new(tasks, capacity, cumulative_options); - let updatable_structures = UpdatableStructures::new(¶meters); + inference_code: InferenceCode, + ) -> TimeTableOverIntervalPropagator { + let tasks = create_tasks(context.as_readonly(), arg_tasks); + + let parameters = + CumulativeParameters::new(context.as_readonly(), tasks, capacity, cumulative_options); + register_tasks( + ¶meters.tasks, + ¶meters.capacity, + context.reborrow(), + false, + ); + + let mut updatable_structures = UpdatableStructures::new(¶meters); + updatable_structures.initialise_bounds_and_remove_fixed(context.as_readonly(), ¶meters); TimeTableOverIntervalPropagator { is_time_table_empty: true, parameters, updatable_structures, - constraint_tag, - inference_code: None, + inference_code, } } } -impl PropagatorConstructor - for TimeTableOverIntervalPropagator +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +> Propagator for TimeTableOverIntervalPropagator { - type PropagatorImpl = Self; - - fn create(mut self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { - self.updatable_structures - .initialise_bounds_and_remove_fixed(context.as_readonly(), &self.parameters); - register_tasks(&self.parameters.tasks, context.reborrow(), false); - - self.inference_code = Some(context.create_inference_code(self.constraint_tag, TimeTable)); - - self - } -} - -impl Propagator for TimeTableOverIntervalPropagator { fn propagate(&mut self, mut context: PropagationContextMut) -> PropagationStatusCP { if self.parameters.is_infeasible { return Err(Inconsistency::Conflict(PropagatorConflict { conjunction: conjunction!(), - inference_code: self.inference_code.unwrap(), + inference_code: self.inference_code, })); } let time_table = create_time_table_over_interval_from_scratch( - context.as_readonly(), + &mut context, &self.parameters, - self.inference_code.unwrap(), + self.inference_code, )?; self.is_time_table_empty = time_table.is_empty(); // No error has been found -> Check for updates (i.e. go over all profiles and all tasks and // check whether an update can take place) propagate_based_on_timetable( &mut context, - self.inference_code.unwrap(), + self.inference_code, time_table.iter(), &self.parameters, &mut self.updatable_structures, @@ -151,8 +200,13 @@ impl Propagator for TimeTableOverIntervalPropaga &mut self, context: PropagationContextWithTrailedValues, local_id: LocalId, - event: OpaqueDomainEvent, + _event: OpaqueDomainEvent, ) -> EnqueueDecision { + if local_id.unpack() as usize >= self.parameters.tasks.len() { + // The upper-bound of the capacity has been updated; we should enqueue + return EnqueueDecision::Enqueue; + } + let updated_task = Rc::clone(&self.parameters.tasks[local_id.unpack() as usize]); // Note that it could be the case that `is_time_table_empty` is inaccurate here since it // wasn't updated in `synchronise`; however, `synchronise` will only remove profiles @@ -173,10 +227,10 @@ impl Propagator for TimeTableOverIntervalPropaga &updated_task, ); - if matches!( - updated_task.start_variable.unpack_event(event), - DomainEvent::Assign - ) { + if context.is_fixed(&updated_task.start_variable) + && context.is_fixed(&updated_task.processing_time) + && context.is_fixed(&updated_task.resource_usage) + { self.updatable_structures.fix_task(&updated_task) } @@ -199,7 +253,7 @@ impl Propagator for TimeTableOverIntervalPropaga &mut context, &self.parameters, &self.updatable_structures, - self.inference_code.unwrap(), + self.inference_code, ) } } @@ -216,14 +270,16 @@ impl Propagator for TimeTableOverIntervalPropaga /// conflict in the form of an [`Inconsistency`]. pub(crate) fn create_time_table_over_interval_from_scratch< Var: IntegerVariable + 'static, - Context: ReadDomains + Copy, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, >( - context: Context, - parameters: &CumulativeParameters, + context: &mut PropagationContextMut, + parameters: &CumulativeParameters, inference_code: InferenceCode, -) -> Result, PropagatorConflict> { +) -> Result, Inconsistency> { // First we create a list of all the events (i.e. start and ends of mandatory parts) - let events = create_events(context, parameters); + let events = create_events(context.as_readonly(), parameters); // Then we create a time-table using these events create_time_table_from_events(events, context, inference_code, parameters) @@ -236,17 +292,23 @@ pub(crate) fn create_time_table_over_interval_from_scratch< /// is resolved by placing the events which signify the ends of mandatory parts first (if the /// tie is between events of the same type then the tie-breaking is done on the id in /// non-decreasing order). -fn create_events( +fn create_events< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, + Context: ReadDomains + Copy, +>( context: Context, - parameters: &CumulativeParameters, -) -> Vec> { + parameters: &CumulativeParameters, +) -> Vec> { // First we create a list of events with which we will create the time-table - let mut events: Vec> = Vec::new(); + let mut events: Vec> = Vec::new(); // Then we go over every task for task in parameters.tasks.iter() { let upper_bound = context.upper_bound(&task.start_variable); let lower_bound = context.lower_bound(&task.start_variable); - if upper_bound < lower_bound + task.processing_time { + if upper_bound < lower_bound + context.lower_bound(&task.processing_time) { // The task has a mandatory part, we need to add the appropriate events to the // events list @@ -254,15 +316,15 @@ fn create_events( // resource usage) events.push(Event { time_stamp: upper_bound, - change_in_resource_usage: task.resource_usage, + change_in_resource_usage: context.lower_bound(&task.resource_usage), task: Rc::clone(task), }); // Then we create an event for the end of a mandatory part (with negative resource // usage) events.push(Event { - time_stamp: lower_bound + task.processing_time, - change_in_resource_usage: -task.resource_usage, + time_stamp: lower_bound + context.lower_bound(&task.processing_time), + change_in_resource_usage: -context.lower_bound(&task.resource_usage), task: Rc::clone(task), }); } @@ -296,12 +358,17 @@ fn create_events( /// Creates a time-table based on the provided `events` (which are assumed to be sorted /// chronologically, with tie-breaking performed in such a way that the ends of mandatory parts /// are before the starts of mandatory parts). -fn create_time_table_from_events( - events: Vec>, - context: Context, +fn create_time_table_from_events< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( + events: Vec>, + context: &mut PropagationContextMut, inference_code: InferenceCode, - parameters: &CumulativeParameters, -) -> Result, PropagatorConflict> { + parameters: &CumulativeParameters, +) -> Result, Inconsistency> { pumpkin_assert_extreme!( events.is_empty() || (0..events.len() - 1) @@ -317,16 +384,14 @@ fn create_time_table_from_events = Default::default(); + let mut time_table: OverIntervalTimeTableType = Default::default(); // The tasks which are contributing to the current profile under consideration - let mut current_profile_tasks: Vec>> = Vec::new(); + let mut current_profile_tasks: Vec>> = Vec::new(); // The cumulative resource usage of the tasks which are contributing to the current profile // under consideration let mut current_resource_usage: i32 = 0; // The beginning of the current interval under consideration let mut start_of_interval: i32 = -1; - // Determines whether a conflict has occurred - let mut is_conflicting = false; // We go over all the events and create the time-table for event in events { @@ -349,12 +414,6 @@ fn create_time_table_from_events parameters.capacity { - is_conflicting = true; - } - // Potentially we need to end the current profile and start a new one due to the // addition/removal of the current task if start_of_interval != event.time_stamp { @@ -364,20 +423,24 @@ fn create_time_table_from_events context.lower_bound(¶meters.capacity) { + context.post( + predicate!(parameters.capacity >= new_profile.height), + create_explanation_profile_height( + context.as_readonly(), + inference_code, + &new_profile, + parameters.options.explanation_type, + ) + .conjunction, inference_code, - &new_profile, - parameters.options.explanation_type, - )); - } else { - // We end the current profile, creating a profile from [start_of_interval, - // time_stamp) - time_table.push(new_profile); + )?; } + // We end the current profile, creating a profile from [start_of_interval, + // time_stamp) + time_table.push(new_profile); } // Process the current event, note that `change_in_resource_usage` can be negative pumpkin_assert_simple!( @@ -396,7 +459,6 @@ fn create_time_table_from_events( - event: &Event, +fn check_starting_new_profile_invariants< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + event: &Event, current_resource_usage: i32, - current_profile_tasks: &[Rc>], + current_profile_tasks: &[Rc>], ) -> bool { if event.change_in_resource_usage <= 0 { eprintln!( @@ -449,19 +512,21 @@ fn check_starting_new_profile_invariants( && current_profile_tasks.is_empty() } -pub(crate) fn debug_propagate_from_scratch_time_table_interval( +pub(crate) fn debug_propagate_from_scratch_time_table_interval< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( context: &mut PropagationContextMut, - parameters: &CumulativeParameters, - updatable_structures: &UpdatableStructures, + parameters: &CumulativeParameters, + updatable_structures: &UpdatableStructures, inference_code: InferenceCode, ) -> PropagationStatusCP { // We first create a time-table over interval and return an error if there was // an overflow of the resource capacity while building the time-table - let time_table = create_time_table_over_interval_from_scratch( - context.as_readonly(), - parameters, - inference_code, - )?; + let time_table = + create_time_table_over_interval_from_scratch(context, parameters, inference_code)?; // Then we check whether propagation can take place propagate_based_on_timetable( context, @@ -474,16 +539,15 @@ pub(crate) fn debug_propagate_from_scratch_time_table_interval { - match e { - Inconsistency::EmptyDomain => false, - Inconsistency::Conflict(x) => { - let expected = [ - predicate!(s1 <= 1), - predicate!(s1 >= 1), - predicate!(s2 >= 1), - predicate!(s2 <= 1), - ]; - expected.iter().all(|y| { - x.conjunction - .iter() - .collect::>() - .contains(&y) - }) && x.conjunction.iter().all(|y| expected.contains(y)) - } - } - } - _ => false, - }); + assert!(result.is_err()); + let reason = solver.get_reason_int(Predicate::trivially_false()); + let expected = [ + predicate!(s1 <= 1), + predicate!(s1 >= 1), + predicate!(s2 >= 1), + predicate!(s2 <= 1), + ]; + assert!( + expected + .iter() + .all(|y| { reason.iter().collect::>().contains(&y) }) + && reason.iter().all(|y| expected.contains(y)) + ); } #[test] @@ -581,8 +637,8 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator(TimeTableOverIntervalPropagator::new( - &[ + .new_propagator(TimeTableOverIntervalConstructor::new( + [ ArgTask { start_time: s1, processing_time: 4, @@ -619,8 +675,8 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator(TimeTableOverIntervalPropagator::new( - &[ + .new_propagator(TimeTableOverIntervalConstructor::new( + [ ArgTask { start_time: a, processing_time: 2, @@ -670,8 +726,8 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator(TimeTableOverIntervalPropagator::new( - &[ + .new_propagator(TimeTableOverIntervalConstructor::new( + [ ArgTask { start_time: s1, processing_time: 2, @@ -716,8 +772,8 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator(TimeTableOverIntervalPropagator::new( - &[ + .new_propagator(TimeTableOverIntervalConstructor::new( + [ ArgTask { start_time: s1, processing_time: 4, @@ -760,8 +816,8 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator(TimeTableOverIntervalPropagator::new( - &[ + .new_propagator(TimeTableOverIntervalConstructor::new( + [ ArgTask { start_time: a, processing_time: 2, @@ -837,8 +893,8 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator(TimeTableOverIntervalPropagator::new( - &[ + .new_propagator(TimeTableOverIntervalConstructor::new( + [ ArgTask { start_time: a, processing_time: 2, @@ -911,8 +967,8 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator(TimeTableOverIntervalPropagator::new( - &[ + .new_propagator(TimeTableOverIntervalConstructor::new( + [ ArgTask { start_time: s1, processing_time: 4, @@ -952,8 +1008,8 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator(TimeTableOverIntervalPropagator::new( - &[ + .new_propagator(TimeTableOverIntervalConstructor::new( + [ ArgTask { start_time: s1, processing_time: 2, @@ -999,8 +1055,8 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator(TimeTableOverIntervalPropagator::new( - &[ + .new_propagator(TimeTableOverIntervalConstructor::new( + [ ArgTask { start_time: s1, processing_time: 4, diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_per_point.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_per_point.rs index 62c87c32d..4675970d8 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_per_point.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_per_point.rs @@ -24,6 +24,7 @@ use crate::engine::propagation::constructor::PropagatorConstructor; use crate::engine::propagation::constructor::PropagatorConstructorContext; use crate::engine::propagation::contexts::PropagationContextWithTrailedValues; use crate::engine::variables::IntegerVariable; +use crate::predicate; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; use crate::propagators::ArgTask; @@ -31,7 +32,7 @@ use crate::propagators::CumulativeParameters; use crate::propagators::CumulativePropagatorOptions; use crate::propagators::ResourceProfile; use crate::propagators::UpdatableStructures; -use crate::propagators::cumulative::time_table::propagation_handler::create_conflict_explanation; +use crate::propagators::cumulative::time_table::propagation_handler::create_explanation_profile_height; use crate::propagators::util::create_tasks; use crate::propagators::util::register_tasks; use crate::propagators::util::update_bounds_task; @@ -50,18 +51,15 @@ use crate::pumpkin_assert_extreme; /// \[1\] A. Schutt, Improving scheduling by learning. University of Melbourne, Department of /// Computer Science and Software Engineering, 2011. #[derive(Debug)] - -pub(crate) struct TimeTablePerPointPropagator { +pub(crate) struct TimeTablePerPointPropagator { /// Stores whether the time-table is empty is_time_table_empty: bool, /// Stores the input parameters to the cumulative constraint - parameters: CumulativeParameters, + parameters: CumulativeParameters, /// Stores structures which change during the search; used to store the bounds - updatable_structures: UpdatableStructures, + updatable_structures: UpdatableStructures, - // TODO: Update with proapgator constructor. - constraint_tag: ConstraintTag, - inference_code: Option, + inference_code: InferenceCode, } /// The type of the time-table used by propagators which use time-table reasoning per time-point; @@ -71,55 +69,109 @@ pub(crate) struct TimeTablePerPointPropagator { /// The key t (representing a time-point) holds the mandatory resource consumption of tasks at /// that time (stored in a [`ResourceProfile`]); the [ResourceProfile]s are sorted based on /// start time and they are non-overlapping -pub(crate) type PerPointTimeTableType = BTreeMap>; +pub(crate) type PerPointTimeTableType = + BTreeMap>; + +pub(crate) struct TimeTablePerPointConstructor { + tasks: Vec>, + capacity: CVar, + cumulative_options: CumulativePropagatorOptions, + constraint_tag: ConstraintTag, +} -impl TimeTablePerPointPropagator { +impl TimeTablePerPointConstructor { pub(crate) fn new( - arg_tasks: &[ArgTask], - capacity: i32, + arg_tasks: Vec>, + capacity: CVar, cumulative_options: CumulativePropagatorOptions, constraint_tag: ConstraintTag, - ) -> TimeTablePerPointPropagator { - let tasks = create_tasks(arg_tasks); - let parameters = CumulativeParameters::new(tasks, capacity, cumulative_options); - let updatable_structures = UpdatableStructures::new(¶meters); - - TimeTablePerPointPropagator { - is_time_table_empty: true, - parameters, - updatable_structures, + ) -> Self { + Self { + tasks: arg_tasks, + capacity, + cumulative_options, constraint_tag, - inference_code: None, } } } -impl PropagatorConstructor for TimeTablePerPointPropagator { - type PropagatorImpl = Self; +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +> PropagatorConstructor for TimeTablePerPointConstructor +{ + type PropagatorImpl = TimeTablePerPointPropagator; + + fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { + let inference_code = context.create_inference_code(self.constraint_tag, TimeTable); + + TimeTablePerPointPropagator::new( + context, + &self.tasks, + self.capacity, + self.cumulative_options, + inference_code, + ) + } +} - fn create(mut self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { - self.updatable_structures - .initialise_bounds_and_remove_fixed(context.as_readonly(), &self.parameters); - register_tasks(&self.parameters.tasks, context.reborrow(), false); +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +> TimeTablePerPointPropagator +{ + fn new( + mut context: PropagatorConstructorContext, + arg_tasks: &[ArgTask], + capacity: CVar, + cumulative_options: CumulativePropagatorOptions, + inference_code: InferenceCode, + ) -> TimeTablePerPointPropagator { + let tasks = create_tasks(context.as_readonly(), arg_tasks); + + let parameters = + CumulativeParameters::new(context.as_readonly(), tasks, capacity, cumulative_options); + register_tasks( + ¶meters.tasks, + ¶meters.capacity, + context.reborrow(), + false, + ); - self.inference_code = Some(context.create_inference_code(self.constraint_tag, TimeTable)); + let mut updatable_structures = UpdatableStructures::new(¶meters); + updatable_structures.initialise_bounds_and_remove_fixed(context.as_readonly(), ¶meters); - self + TimeTablePerPointPropagator { + is_time_table_empty: true, + parameters, + updatable_structures, + inference_code, + } } } -impl Propagator for TimeTablePerPointPropagator { +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +> Propagator for TimeTablePerPointPropagator +{ fn propagate(&mut self, mut context: PropagationContextMut) -> PropagationStatusCP { if self.parameters.is_infeasible { return Err(Inconsistency::Conflict(PropagatorConflict { conjunction: conjunction!(), - inference_code: self.inference_code.unwrap(), + inference_code: self.inference_code, })); } let time_table = create_time_table_per_point_from_scratch( - context.as_readonly(), - self.inference_code.unwrap(), + &mut context, + self.inference_code, &self.parameters, )?; self.is_time_table_empty = time_table.is_empty(); @@ -127,7 +179,7 @@ impl Propagator for TimeTablePerPointPropagator< // check whether an update can take place) propagate_based_on_timetable( &mut context, - self.inference_code.unwrap(), + self.inference_code, time_table.values(), &self.parameters, &mut self.updatable_structures, @@ -145,6 +197,11 @@ impl Propagator for TimeTablePerPointPropagator< local_id: LocalId, event: OpaqueDomainEvent, ) -> EnqueueDecision { + if local_id.unpack() as usize >= self.parameters.tasks.len() { + // The upper-bound of the capacity has been updated; we should enqueue + return EnqueueDecision::Enqueue; + } + let updated_task = Rc::clone(&self.parameters.tasks[local_id.unpack() as usize]); // Note that it could be the case that `is_time_table_empty` is inaccurate here since it // wasn't updated in `synchronise`; however, `synchronise` will only remove profiles @@ -159,7 +216,7 @@ impl Propagator for TimeTablePerPointPropagator< self.is_time_table_empty, ); - // Note that the non-incremental proapgator does not make use of `result.updated` since it + // Note that the non-incremental propagator does not make use of `result.updated` since it // propagates from scratch anyways update_bounds_task( context.as_readonly(), @@ -191,7 +248,7 @@ impl Propagator for TimeTablePerPointPropagator< ) -> PropagationStatusCP { debug_propagate_from_scratch_time_table_point( &mut context, - self.inference_code.unwrap(), + self.inference_code, &self.parameters, &self.updatable_structures, ) @@ -208,39 +265,44 @@ impl Propagator for TimeTablePerPointPropagator< /// conflict in the form of an [`Inconsistency`]. pub(crate) fn create_time_table_per_point_from_scratch< Var: IntegerVariable + 'static, - Context: ReadDomains + Copy, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, >( - context: Context, + context: &mut PropagationContextMut, inference_code: InferenceCode, - parameters: &CumulativeParameters, -) -> Result, PropagatorConflict> { - let mut time_table: PerPointTimeTableType = PerPointTimeTableType::new(); + parameters: &CumulativeParameters, +) -> Result, Inconsistency> { + let mut time_table: PerPointTimeTableType = PerPointTimeTableType::new(); // First we go over all tasks and determine their mandatory parts for task in parameters.tasks.iter() { let upper_bound = context.upper_bound(&task.start_variable); let lower_bound = context.lower_bound(&task.start_variable); - if upper_bound < lower_bound + task.processing_time { + if upper_bound < lower_bound + context.lower_bound(&task.processing_time) { // There is a mandatory part - for i in upper_bound..(lower_bound + task.processing_time) { + for i in upper_bound..(lower_bound + context.lower_bound(&task.processing_time)) { // For every time-point of the mandatory part, // add the resource usage of the current task to the ResourceProfile and add it // to the profile tasks of the resource - let current_profile: &mut ResourceProfile = time_table + let current_profile: &mut ResourceProfile = time_table .entry(i as u32) .or_insert(ResourceProfile::default(i)); - current_profile.height += task.resource_usage; + current_profile.height += context.lower_bound(&task.resource_usage); current_profile.profile_tasks.push(Rc::clone(task)); - if current_profile.height > parameters.capacity { - // The addition of the current task to the resource profile has caused an - // overflow - return Err(create_conflict_explanation( - context, + if current_profile.height > context.lower_bound(¶meters.capacity) { + context.post( + predicate!(parameters.capacity >= current_profile.height), + create_explanation_profile_height( + context.as_readonly(), + inference_code, + current_profile, + parameters.options.explanation_type, + ) + .conjunction, inference_code, - current_profile, - parameters.options.explanation_type, - )); + )?; } } } @@ -254,19 +316,20 @@ pub(crate) fn create_time_table_per_point_from_scratch< Ok(time_table) } -pub(crate) fn debug_propagate_from_scratch_time_table_point( +pub(crate) fn debug_propagate_from_scratch_time_table_point< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( context: &mut PropagationContextMut, inference_code: InferenceCode, - parameters: &CumulativeParameters, - updatable_structures: &UpdatableStructures, + parameters: &CumulativeParameters, + updatable_structures: &UpdatableStructures, ) -> PropagationStatusCP { // We first create a time-table per point and return an error if there was // an overflow of the resource capacity while building the time-table - let time_table = create_time_table_per_point_from_scratch( - context.as_readonly(), - inference_code, - parameters, - )?; + let time_table = create_time_table_per_point_from_scratch(context, inference_code, parameters)?; // Then we check whether propagation can take place propagate_based_on_timetable( context, @@ -279,16 +342,15 @@ pub(crate) fn debug_propagate_from_scratch_time_table_point match e { - Inconsistency::EmptyDomain => false, - Inconsistency::Conflict(x) => { - let expected = [ - predicate!(s1 <= 1), - predicate!(s1 >= 1), - predicate!(s2 <= 1), - predicate!(s2 >= 1), - ]; - expected.iter().all(|y| { - x.conjunction - .iter() - .collect::>() - .contains(&y) - }) && x.conjunction.iter().all(|y| expected.contains(y)) - } - }, - Ok(_) => false, - }); + assert!(result.is_err()); + let reason = solver.get_reason_int(Predicate::trivially_false()); + let expected = [ + predicate!(s1 <= 1), + predicate!(s1 >= 1), + predicate!(s2 >= 1), + predicate!(s2 <= 1), + ]; + assert!( + expected + .iter() + .all(|y| { reason.iter().collect::>().contains(&y) }) + && reason.iter().all(|y| expected.contains(y)) + ); } #[test] @@ -384,8 +440,8 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator(TimeTablePerPointPropagator::new( - &[ + .new_propagator(TimeTablePerPointConstructor::new( + [ ArgTask { start_time: s1, processing_time: 4, @@ -422,8 +478,8 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator(TimeTablePerPointPropagator::new( - &[ + .new_propagator(TimeTablePerPointConstructor::new( + [ ArgTask { start_time: a, processing_time: 2, @@ -473,8 +529,8 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator(TimeTablePerPointPropagator::new( - &[ + .new_propagator(TimeTablePerPointConstructor::new( + [ ArgTask { start_time: s1, processing_time: 2, @@ -519,8 +575,8 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator(TimeTablePerPointPropagator::new( - &[ + .new_propagator(TimeTablePerPointConstructor::new( + [ ArgTask { start_time: s1, processing_time: 4, @@ -565,8 +621,8 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator(TimeTablePerPointPropagator::new( - &[ + .new_propagator(TimeTablePerPointConstructor::new( + [ ArgTask { start_time: a, processing_time: 2, @@ -641,8 +697,8 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let propagator = solver - .new_propagator(TimeTablePerPointPropagator::new( - &[ + .new_propagator(TimeTablePerPointConstructor::new( + [ ArgTask { start_time: a, processing_time: 2, @@ -715,8 +771,8 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator(TimeTablePerPointPropagator::new( - &[ + .new_propagator(TimeTablePerPointConstructor::new( + [ ArgTask { start_time: s1, processing_time: 4, @@ -766,8 +822,8 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator(TimeTablePerPointPropagator::new( - &[ + .new_propagator(TimeTablePerPointConstructor::new( + [ ArgTask { start_time: s1, processing_time: 2, @@ -820,8 +876,8 @@ mod tests { let constraint_tag = solver.new_constraint_tag(); let _ = solver - .new_propagator(TimeTablePerPointPropagator::new( - &[ + .new_propagator(TimeTablePerPointConstructor::new( + [ ArgTask { start_time: s1, processing_time: 4, diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_util.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_util.rs index 6da4af598..b75dabd9c 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_util.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_util.rs @@ -25,7 +25,7 @@ use crate::pumpkin_assert_extreme; /// The result of [`should_enqueue`], contains the [`EnqueueDecision`] whether the propagator should /// currently be enqueued and potentially the updated [`Task`] (in the form of a /// [`UpdatedTaskInfo`]) if the mandatory part of this [`Task`] has changed. -pub(crate) struct ShouldEnqueueResult { +pub(crate) struct ShouldEnqueueResult { /// Whether the propagator which called this method should be enqueued pub(crate) decision: EnqueueDecision, /// If the mandatory part of the task passed to [`should_enqueue`] has changed then this field @@ -33,28 +33,25 @@ pub(crate) struct ShouldEnqueueResult { /// /// In general, non-incremental propagators will not make use of this field since they will /// propagate from scratch anyways. - pub(crate) update: Option>, + pub(crate) update: Option>, } /// Determines whether a time-table propagator should enqueue and returns a structure containing the /// [`EnqueueDecision`] and the info of the task with the extended mandatory part (or [`None`] if no /// such task exists). This method should be called in the /// [`ConstraintProgrammingPropagator::notify`] method. -pub(crate) fn should_enqueue( - parameters: &CumulativeParameters, - updatable_structures: &UpdatableStructures, - updated_task: &Rc>, +pub(crate) fn should_enqueue< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( + parameters: &CumulativeParameters, + updatable_structures: &UpdatableStructures, + updated_task: &Rc>, context: PropagationContext, empty_time_table: bool, -) -> ShouldEnqueueResult { - pumpkin_assert_extreme!( - context.lower_bound(&updated_task.start_variable) - > updatable_structures.get_stored_lower_bound(updated_task) - || updatable_structures.get_stored_upper_bound(updated_task) - >= context.upper_bound(&updated_task.start_variable), - "Either the stored lower-bound was larger than or equal to the actual lower bound or the upper-bound was smaller than or equal to the actual upper-bound\nThis either indicates that the propagator subscribed to events other than lower-bound and upper-bound updates or the stored bounds were not managed properly" - ); - +) -> ShouldEnqueueResult { let mut result = ShouldEnqueueResult { decision: EnqueueDecision::Skip, update: None, @@ -63,12 +60,6 @@ pub(crate) fn should_enqueue( let old_lower_bound = updatable_structures.get_stored_lower_bound(updated_task); let old_upper_bound = updatable_structures.get_stored_upper_bound(updated_task); - if old_lower_bound == context.lower_bound(&updated_task.start_variable) - && old_upper_bound == context.upper_bound(&updated_task.start_variable) - { - return result; - } - // We check whether a mandatory part was extended/introduced if has_mandatory_part(context, updated_task) { result.update = Some(UpdatedTaskInfo { @@ -105,19 +96,27 @@ pub(crate) fn should_enqueue( result } -pub(crate) fn has_mandatory_part( +pub(crate) fn has_mandatory_part< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( context: PropagationContext, - task: &Rc>, + task: &Rc>, ) -> bool { context.upper_bound(&task.start_variable) - < context.lower_bound(&task.start_variable) + task.processing_time + < context.lower_bound(&task.start_variable) + context.lower_bound(&task.processing_time) } /// Checks whether a specific task (indicated by id) has a mandatory part which overlaps with the /// interval [start, end] -pub(crate) fn has_mandatory_part_in_interval( +pub(crate) fn has_mandatory_part_in_interval< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( context: PropagationContext, - task: &Rc>, + task: &Rc>, start: i32, end: i32, ) -> bool { @@ -126,21 +125,30 @@ pub(crate) fn has_mandatory_part_in_interval( context.upper_bound(&task.start_variable), ); // There exists a mandatory part - (upper_bound < (lower_bound + task.processing_time)) - && has_overlap_with_interval(upper_bound, lower_bound + task.processing_time, start, end) + (upper_bound < (lower_bound + context.lower_bound(&task.processing_time))) + && has_overlap_with_interval( + upper_bound, + lower_bound + context.lower_bound(&task.processing_time), + start, + end, + ) // Determine whether the mandatory part overlaps with the provided bounds } /// Checks whether the lower and upper bound of a task overlap with the provided interval -pub(crate) fn task_has_overlap_with_interval( +pub(crate) fn task_has_overlap_with_interval< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( context: PropagationContext, - task: &Rc>, + task: &Rc>, start: i32, end: i32, ) -> bool { let (lower_bound, upper_bound) = ( context.lower_bound(&task.start_variable), - context.upper_bound(&task.start_variable) + task.processing_time, + context.upper_bound(&task.start_variable) + context.lower_bound(&task.processing_time), ); // The release time of the task and the deadline has_overlap_with_interval(lower_bound, upper_bound, start, end) } @@ -160,8 +168,13 @@ pub(crate) fn has_overlap_with_interval( /// based on start time and that the profiles are maximal (i.e. the [`ResourceProfile::start`] and /// [`ResourceProfile::end`] cannot be increased or decreased, respectively). It returns true if /// both of these invariants hold and false otherwise. -fn debug_check_whether_profiles_are_maximal_and_sorted<'a, Var: IntegerVariable + 'static>( - time_table: impl Iterator> + Clone, +fn debug_check_whether_profiles_are_maximal_and_sorted< + 'a, + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + time_table: impl Iterator> + Clone, ) -> bool { let collected_time_table = time_table.clone().collect::>(); let sorted_profiles = collected_time_table.is_empty() @@ -199,12 +212,18 @@ fn debug_check_whether_profiles_are_maximal_and_sorted<'a, Var: IntegerVariable /// sorted in increasing order in terms of [`ResourceProfile::start`] and that the /// [`ResourceProfile`] is maximal (i.e. the [`ResourceProfile::start`] and [`ResourceProfile::end`] /// cannot be increased or decreased, respectively). -pub(crate) fn propagate_based_on_timetable<'a, Var: IntegerVariable + 'static>( +pub(crate) fn propagate_based_on_timetable< + 'a, + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( context: &mut PropagationContextMut, inference_code: InferenceCode, - time_table: impl Iterator> + Clone, - parameters: &CumulativeParameters, - updatable_structures: &mut UpdatableStructures, + time_table: impl Iterator> + Clone, + parameters: &CumulativeParameters, + updatable_structures: &mut UpdatableStructures, ) -> PropagationStatusCP { pumpkin_assert_extreme!( debug_check_whether_profiles_are_maximal_and_sorted(time_table.clone()), @@ -214,13 +233,19 @@ pub(crate) fn propagate_based_on_timetable<'a, Var: IntegerVariable + 'static>( pumpkin_assert_extreme!( updatable_structures .get_unfixed_tasks() - .all(|unfixed_task| !context.is_fixed(&unfixed_task.start_variable)), + .all( + |unfixed_task| !context.is_fixed(&unfixed_task.start_variable) + || !context.is_fixed(&unfixed_task.processing_time) + || !context.is_fixed(&unfixed_task.resource_usage) + ), "All of the unfixed tasks should not be fixed at this point" ); pumpkin_assert_extreme!( updatable_structures .get_fixed_tasks() - .all(|fixed_task| context.is_fixed(&fixed_task.start_variable)), + .all(|fixed_task| context.is_fixed(&fixed_task.start_variable) + && context.is_fixed(&fixed_task.processing_time) + && context.is_fixed(&fixed_task.resource_usage)), "All of the fixed tasks should be fixed at this point" ); @@ -254,12 +279,18 @@ pub(crate) fn propagate_based_on_timetable<'a, Var: IntegerVariable + 'static>( /// /// This type of propagation is likely to be less beneficial for the explanation /// [`CumulativeExplanationType::Pointwise`]. -fn propagate_single_profiles<'a, Var: IntegerVariable + 'static>( +fn propagate_single_profiles< + 'a, + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( context: &mut PropagationContextMut, inference_code: InferenceCode, - time_table: impl Iterator> + Clone, - updatable_structures: &mut UpdatableStructures, - parameters: &CumulativeParameters, + time_table: impl Iterator> + Clone, + updatable_structures: &mut UpdatableStructures, + parameters: &CumulativeParameters, ) -> PropagationStatusCP { // We create the structure responsible for propagations and explanations let mut propagation_handler = @@ -275,7 +306,10 @@ fn propagate_single_profiles<'a, Var: IntegerVariable + 'static>( let mut task_index = 0; while task_index < updatable_structures.number_of_unfixed_tasks() { let task = updatable_structures.get_unfixed_task_at_index(task_index); - if context.is_fixed(&task.start_variable) { + if context.is_fixed(&task.start_variable) + && context.is_fixed(&task.resource_usage) + && context.is_fixed(&task.processing_time) + { // The task is currently fixed after propagating // // Note that we fix this task temporarily and then wait for the notification to @@ -289,7 +323,10 @@ fn propagate_single_profiles<'a, Var: IntegerVariable + 'static>( } continue; } - if profile.start > context.upper_bound(&task.start_variable) + task.processing_time { + if profile.start + > context.upper_bound(&task.start_variable) + + context.lower_bound(&task.processing_time) + { // The start of the current profile is necessarily after the latest // completion time of the task under consideration The profiles are // sorted by start time (and non-overlapping) so we can remove the task from @@ -310,10 +347,14 @@ fn propagate_single_profiles<'a, Var: IntegerVariable + 'static>( context.as_readonly(), &task, profile, - parameters.capacity, + parameters.capacity.clone(), ) { - let result = propagation_handler - .propagate_lower_bound_with_explanations(context, profile, &task); + let result = propagation_handler.propagate_lower_bound_with_explanations( + context, + profile, + &task, + parameters.capacity.clone(), + ); if result.is_err() { updatable_structures.restore_temporarily_removed(); result?; @@ -323,10 +364,14 @@ fn propagate_single_profiles<'a, Var: IntegerVariable + 'static>( context.as_readonly(), &task, profile, - parameters.capacity, + parameters.capacity.clone(), ) { - let result = propagation_handler - .propagate_upper_bound_with_explanations(context, profile, &task); + let result = propagation_handler.propagate_upper_bound_with_explanations( + context, + profile, + &task, + parameters.capacity.clone(), + ); if result.is_err() { updatable_structures.restore_temporarily_removed(); result?; @@ -337,10 +382,15 @@ fn propagate_single_profiles<'a, Var: IntegerVariable + 'static>( context.as_readonly(), &task, profile, - parameters.capacity, + parameters.capacity.clone(), ) { - let result = propagation_handler.propagate_holes_in_domain(context, profile, &task); + let result = propagation_handler.propagate_holes_in_domain( + context, + profile, + &task, + parameters.capacity.clone(), + ); if result.is_err() { updatable_structures.restore_temporarily_removed(); @@ -362,12 +412,18 @@ fn propagate_single_profiles<'a, Var: IntegerVariable + 'static>( /// /// Especially in the case of [`CumulativeExplanationType::Pointwise`] this is likely to be /// beneficial. -fn propagate_sequence_of_profiles<'a, Var: IntegerVariable + 'static>( +fn propagate_sequence_of_profiles< + 'a, + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( context: &mut PropagationContextMut, inference_code: InferenceCode, - time_table: impl Iterator> + Clone, - updatable_structures: &mut UpdatableStructures, - parameters: &CumulativeParameters, + time_table: impl Iterator> + Clone, + updatable_structures: &UpdatableStructures, + parameters: &CumulativeParameters, ) -> PropagationStatusCP { let mut profile_buffer = Vec::default(); @@ -384,7 +440,10 @@ fn propagate_sequence_of_profiles<'a, Var: IntegerVariable + 'static>( // Then we go over all the possible tasks for task in updatable_structures.get_unfixed_tasks() { - if context.is_fixed(&task.start_variable) { + if context.is_fixed(&task.start_variable) + && context.is_fixed(&task.resource_usage) + && context.is_fixed(&task.processing_time) + { // If the task is fixed then we are not able to propagate it further continue; } @@ -420,7 +479,9 @@ fn propagate_sequence_of_profiles<'a, Var: IntegerVariable + 'static>( // `lower_bound_index..upper_bound_index` instead of // `lower_bound_index..=upper_bound_index`) let upper_bound_index = time_table.partition_point(|profile| { - profile.start < context.upper_bound(&task.start_variable) + task.processing_time + profile.start + < context.upper_bound(&task.start_variable) + + context.lower_bound(&task.processing_time) }); for profile in &time_table[lower_bound_index..upper_bound_index] { // Check whether this profile can cause an update @@ -428,11 +489,16 @@ fn propagate_sequence_of_profiles<'a, Var: IntegerVariable + 'static>( context.as_readonly(), task, profile, - parameters.capacity, + parameters.capacity.clone(), ) { // If we allow the propagation of holes in the domain then we simply let the // propagation handler handle it - propagation_handler.propagate_holes_in_domain(context, profile, task)?; + propagation_handler.propagate_holes_in_domain( + context, + profile, + task, + parameters.capacity.clone(), + )?; } } } @@ -443,13 +509,19 @@ fn propagate_sequence_of_profiles<'a, Var: IntegerVariable + 'static>( /// Propagates the lower-bound of the provided `task`. /// /// This method makes use of the fact that the provided `time_table` is sorted chronologically. -fn sweep_forward<'a, Var: IntegerVariable + 'static>( - task: &Rc>, +fn sweep_forward< + 'a, + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( + task: &Rc>, propagation_handler: &mut CumulativePropagationHandler, context: &mut PropagationContextMut, - time_table: &[&'a ResourceProfile], - parameters: &CumulativeParameters, - profile_buffer: &mut Vec<&'a ResourceProfile>, + time_table: &[&'a ResourceProfile], + parameters: &CumulativeParameters, + profile_buffer: &mut Vec<&'a ResourceProfile>, ) -> PropagationStatusCP { // First we find the lowest index such that there is some overlap with a profile if a task is // started at its earliest possible start time @@ -460,7 +532,9 @@ fn sweep_forward<'a, Var: IntegerVariable + 'static>( 'lower_bound_profile_loop: while profile_index < time_table.len() { let profile = time_table[profile_index]; - if profile.start > context.lower_bound(&task.start_variable) + task.processing_time { + if profile.start + > context.lower_bound(&task.start_variable) + context.lower_bound(&task.processing_time) + { // There is no way that the lower-bound can be updated by any subsequent profile // since starting the task at its earliest start time does not overlap with any further // profiles. @@ -474,7 +548,7 @@ fn sweep_forward<'a, Var: IntegerVariable + 'static>( context.as_readonly(), task, profile, - parameters.capacity, + parameters.capacity.clone(), ) { // Now we find the profiles which will propagate the lower-bound to its maximu value and // store them in the profile buffer @@ -483,7 +557,7 @@ fn sweep_forward<'a, Var: IntegerVariable + 'static>( time_table, context.as_readonly(), task, - parameters.capacity, + parameters.capacity.clone(), profile_buffer, ); @@ -493,6 +567,7 @@ fn sweep_forward<'a, Var: IntegerVariable + 'static>( context, profile_buffer, task, + parameters.capacity.clone(), )?; // We have found an update and pushed the lower-bound to its maximum value, we can stop @@ -507,19 +582,27 @@ fn sweep_forward<'a, Var: IntegerVariable + 'static>( Ok(()) } -fn sweep_backward<'a, Var: IntegerVariable + 'static>( - task: &Rc>, +fn sweep_backward< + 'a, + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( + task: &Rc>, propagation_handler: &mut CumulativePropagationHandler, context: &mut PropagationContextMut, - time_table: &[&'a ResourceProfile], - parameters: &CumulativeParameters, - profile_buffer: &mut Vec<&'a ResourceProfile>, + time_table: &[&'a ResourceProfile], + parameters: &CumulativeParameters, + profile_buffer: &mut Vec<&'a ResourceProfile>, ) -> PropagationStatusCP { // First we find the smallest index such that the profile starts after the latest completion // time of the provided task let mut profile_index = min( time_table.partition_point(|profile| { - profile.start < context.upper_bound(&task.start_variable) + task.processing_time + profile.start + < context.upper_bound(&task.start_variable) + + context.lower_bound(&task.processing_time) }), time_table.len() - 1, ); @@ -542,7 +625,7 @@ fn sweep_backward<'a, Var: IntegerVariable + 'static>( context.as_readonly(), task, profile, - parameters.capacity, + parameters.capacity.clone(), ) { // Now we find the profiles which will propagate the upper-bound to its minimum value // and store them in the profile buffer @@ -551,7 +634,7 @@ fn sweep_backward<'a, Var: IntegerVariable + 'static>( time_table, context.as_readonly(), task, - parameters.capacity, + parameters.capacity.clone(), profile_buffer, ); // Then we provide the propagation handler with the chain of profiles and propagate @@ -560,6 +643,7 @@ fn sweep_backward<'a, Var: IntegerVariable + 'static>( context, profile_buffer, task, + parameters.capacity.clone(), )?; // We have found an update and pushed the upper-bound to its minimum value, we can stop @@ -582,13 +666,19 @@ fn sweep_backward<'a, Var: IntegerVariable + 'static>( /// value in `profile_buffer`. /// /// Note: this can include non-consecutive profiles. -fn find_profiles_which_propagate_lower_bound<'a, Var: IntegerVariable + 'static>( +fn find_profiles_which_propagate_lower_bound< + 'a, + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( profile_index: usize, - time_table: &[&'a ResourceProfile], + time_table: &[&'a ResourceProfile], context: PropagationContext, - task: &Rc>, - capacity: i32, - profile_buffer: &mut Vec<&'a ResourceProfile>, + task: &Rc>, + capacity: CVar, + profile_buffer: &mut Vec<&'a ResourceProfile>, ) { profile_buffer.clear(); profile_buffer.push(time_table[profile_index]); @@ -599,11 +689,18 @@ fn find_profiles_which_propagate_lower_bound<'a, Var: IntegerVariable + 'static> while current_index < time_table.len() { let next_profile = time_table[current_index]; - if next_profile.start - time_table[last_propagating_index].end >= task.processing_time { + if next_profile.start - time_table[last_propagating_index].end + >= context.lower_bound(&task.processing_time) + { break; } - if overflows_capacity_and_is_not_part_of_profile(context, task, next_profile, capacity) { + if overflows_capacity_and_is_not_part_of_profile( + context, + task, + next_profile, + capacity.clone(), + ) { last_propagating_index = current_index; profile_buffer.push(time_table[current_index]) } @@ -615,13 +712,19 @@ fn find_profiles_which_propagate_lower_bound<'a, Var: IntegerVariable + 'static> /// value in `profile_buffer`. /// /// Note: this can include non-consecutive profiles. -fn find_profiles_which_propagate_upper_bound<'a, Var: IntegerVariable + 'static>( +fn find_profiles_which_propagate_upper_bound< + 'a, + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( profile_index: usize, - time_table: &[&'a ResourceProfile], + time_table: &[&'a ResourceProfile], context: PropagationContext, - task: &Rc>, - capacity: i32, - profile_buffer: &mut Vec<&'a ResourceProfile>, + task: &Rc>, + capacity: CVar, + profile_buffer: &mut Vec<&'a ResourceProfile>, ) { profile_buffer.clear(); profile_buffer.push(time_table[profile_index]); @@ -634,12 +737,18 @@ fn find_profiles_which_propagate_upper_bound<'a, Var: IntegerVariable + 'static> let mut current_index = profile_index - 1; loop { let previous_profile = time_table[current_index]; - if time_table[last_propagating].start - previous_profile.end >= task.processing_time { + if time_table[last_propagating].start - previous_profile.end + >= context.lower_bound(&task.processing_time) + { break; } - if overflows_capacity_and_is_not_part_of_profile(context, task, previous_profile, capacity) - { + if overflows_capacity_and_is_not_part_of_profile( + context, + task, + previous_profile, + capacity.clone(), + ) { last_propagating = current_index; profile_buffer.push(time_table[current_index]); } @@ -662,14 +771,20 @@ fn find_profiles_which_propagate_upper_bound<'a, Var: IntegerVariable + 'static> /// /// Note: It is assumed that task.resource_usage + height > capacity (i.e. the task has the /// potential to overflow the capacity in combination with the profile) -fn lower_bound_can_be_propagated_by_profile( +fn lower_bound_can_be_propagated_by_profile< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( context: PropagationContext, - task: &Rc>, - profile: &ResourceProfile, - capacity: i32, + task: &Rc>, + profile: &ResourceProfile, + capacity: CVar, ) -> bool { can_be_updated_by_profile(context, task, profile, capacity) - && (context.lower_bound(&task.start_variable) + task.processing_time) > profile.start + && (context.lower_bound(&task.start_variable) + context.lower_bound(&task.processing_time)) + > profile.start && context.lower_bound(&task.start_variable) <= profile.end } @@ -679,14 +794,20 @@ fn lower_bound_can_be_propagated_by_profile( /// [`ResourceProfile`] /// * ub(s) <= end, i.e. the latest start time is before the end of the [`ResourceProfile`] /// Note: It is assumed that the task is known to overflow the [`ResourceProfile`] -fn upper_bound_can_be_propagated_by_profile( +fn upper_bound_can_be_propagated_by_profile< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( context: PropagationContext, - task: &Rc>, - profile: &ResourceProfile, - capacity: i32, + task: &Rc>, + profile: &ResourceProfile, + capacity: CVar, ) -> bool { can_be_updated_by_profile(context, task, profile, capacity) - && (context.upper_bound(&task.start_variable) + task.processing_time) > profile.start + && (context.upper_bound(&task.start_variable) + context.lower_bound(&task.processing_time)) + > profile.start && context.upper_bound(&task.start_variable) <= profile.end } @@ -697,11 +818,16 @@ fn upper_bound_can_be_propagated_by_profile( /// /// If the first condition is true, the second false and the third true then this method returns /// true (otherwise it returns false) -fn can_be_updated_by_profile( +fn can_be_updated_by_profile< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( context: PropagationContext, - task: &Rc>, - profile: &ResourceProfile, - capacity: i32, + task: &Rc>, + profile: &ResourceProfile, + capacity: CVar, ) -> bool { overflows_capacity_and_is_not_part_of_profile(context, task, profile, capacity) && task_has_overlap_with_interval(context, task, profile.start, profile.end) @@ -713,20 +839,29 @@ fn can_be_updated_by_profile( /// /// If the first condition is true, and the second false then this method returns /// true (otherwise it returns false) -fn overflows_capacity_and_is_not_part_of_profile( +fn overflows_capacity_and_is_not_part_of_profile< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( context: PropagationContext, - task: &Rc>, - profile: &ResourceProfile, - capacity: i32, + task: &Rc>, + profile: &ResourceProfile, + capacity: CVar, ) -> bool { - profile.height + task.resource_usage > capacity + profile.height + context.lower_bound(&task.resource_usage) > context.upper_bound(&capacity) && !has_mandatory_part_in_interval(context, task, profile.start, profile.end) } -pub(crate) fn insert_update( - updated_task: &Rc>, - updatable_structures: &mut UpdatableStructures, - potential_update: Option>, +pub(crate) fn insert_update< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + updated_task: &Rc>, + updatable_structures: &mut UpdatableStructures, + potential_update: Option>, ) { if let Some(update) = potential_update { updatable_structures.task_has_been_updated(updated_task); @@ -734,10 +869,14 @@ pub(crate) fn insert_update( } } -pub(crate) fn backtrack_update( +pub(crate) fn backtrack_update< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( context: PropagationContext, - updatable_structures: &mut UpdatableStructures, - updated_task: &Rc>, + updatable_structures: &mut UpdatableStructures, + updated_task: &Rc>, ) { // Stores whether the stored lower-bound is equal to the current lower-bound let lower_bound_equal_to_stored = updatable_structures.get_stored_lower_bound(updated_task) @@ -750,7 +889,8 @@ pub(crate) fn backtrack_update( // Stores whether the stored bounds did not include a mandatory part let previously_did_not_have_mandatory_part = updatable_structures .get_stored_upper_bound(updated_task) - >= updatable_structures.get_stored_lower_bound(updated_task) + updated_task.processing_time; + >= updatable_structures.get_stored_lower_bound(updated_task) + + context.lower_bound(&updated_task.processing_time); // If the stored bounds are already the same or the previous stored bounds did not include a // mandatory part (which means that this task will also not have mandatory part after diff --git a/pumpkin-crates/core/src/propagators/cumulative/utils/mod.rs b/pumpkin-crates/core/src/propagators/cumulative/utils/mod.rs index 411609aeb..65c2b1954 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/utils/mod.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/utils/mod.rs @@ -6,3 +6,4 @@ mod structs; pub(crate) use structs::*; pub(crate) mod util; +pub use structs::ArgTask; diff --git a/pumpkin-crates/core/src/propagators/cumulative/utils/structs/mandatory_part_adjustments.rs b/pumpkin-crates/core/src/propagators/cumulative/utils/structs/mandatory_part_adjustments.rs index 50136337c..65e18f315 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/utils/structs/mandatory_part_adjustments.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/utils/structs/mandatory_part_adjustments.rs @@ -2,6 +2,9 @@ use std::cmp::Ordering; use std::ops::Range; use super::UpdatedTaskInfo; +use crate::engine::cp::propagation::contexts::propagation_context::ReadDomains; +use crate::engine::propagation::PropagationContext; +use crate::variables::IntegerVariable; /// Represents adjustments to a mandatory part due to bound changes. /// @@ -76,16 +79,19 @@ impl MandatoryPartAdjustments { } } -impl UpdatedTaskInfo { +impl UpdatedTaskInfo { /// Returns the adjustments which need to be made to the time-table in the form of a /// [`MandatoryPartAdjustments`]. - pub(crate) fn get_mandatory_part_adjustments(&self) -> MandatoryPartAdjustments { + pub(crate) fn get_mandatory_part_adjustments( + &self, + context: PropagationContext, + ) -> MandatoryPartAdjustments { // We get the previous mandatory part - let previous_mandatory_part = - self.old_upper_bound..self.old_lower_bound + self.task.processing_time; + let previous_mandatory_part = self.old_upper_bound + ..self.old_lower_bound + context.lower_bound(&self.task.processing_time); // We also get the new mandatory part - let new_mandatory_part = - self.new_upper_bound..self.new_lower_bound + self.task.processing_time; + let new_mandatory_part = self.new_upper_bound + ..self.new_lower_bound + context.lower_bound(&self.task.processing_time); if previous_mandatory_part.is_empty() && new_mandatory_part.is_empty() { // If both are empty then no adjustments should be made diff --git a/pumpkin-crates/core/src/propagators/cumulative/utils/structs/mod.rs b/pumpkin-crates/core/src/propagators/cumulative/utils/structs/mod.rs index 03d40a593..81960874a 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/utils/structs/mod.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/utils/structs/mod.rs @@ -8,6 +8,7 @@ mod updated_task_info; pub(crate) use mandatory_part_adjustments::*; pub(crate) use parameters::*; pub(crate) use resource_profile::*; +pub use task::ArgTask; pub(crate) use task::*; pub(crate) use updatable_structures::*; pub(crate) use updated_task_info::*; diff --git a/pumpkin-crates/core/src/propagators/cumulative/utils/structs/parameters.rs b/pumpkin-crates/core/src/propagators/cumulative/utils/structs/parameters.rs index e11075741..2a872d341 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/utils/structs/parameters.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/utils/structs/parameters.rs @@ -1,6 +1,8 @@ use std::rc::Rc; use super::Task; +use crate::engine::cp::propagation::contexts::propagation_context::ReadDomains; +use crate::engine::propagation::PropagationContext; use crate::propagators::CumulativePropagatorOptions; use crate::variables::IntegerVariable; @@ -9,14 +11,14 @@ use crate::variables::IntegerVariable; /// - The capacity of the resource /// - The options for propagating the cumulative constraint #[derive(Debug, Clone)] -pub(crate) struct CumulativeParameters { +pub(crate) struct CumulativeParameters { /// The Set of [`Task`]s; for each [`Task`], the [`Task::id`] is assumed to correspond to its /// index in this [`Vec`]; this is stored as a [`Box`] of [`Rc`]'s to accomodate the /// sharing of the tasks - pub(crate) tasks: Box<[Rc>]>, + pub(crate) tasks: Box<[Rc>]>, /// The capacity of the resource (i.e. how much resource consumption can be maximally /// accomodated at each time point) - pub(crate) capacity: i32, + pub(crate) capacity: CVar, /// The [`CumulativeOptions`] which influence the behaviour of the cumulative propagator(s). pub(crate) options: CumulativePropagatorOptions, /// Indicates that the constraint is infeasible. @@ -25,17 +27,25 @@ pub(crate) struct CumulativeParameters { pub(crate) is_infeasible: bool, } -impl CumulativeParameters { +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +> CumulativeParameters +{ pub(crate) fn new( - tasks: Vec>, - capacity: i32, + context: PropagationContext, + tasks: Vec>, + capacity: CVar, options: CumulativePropagatorOptions, - ) -> CumulativeParameters { + ) -> CumulativeParameters { let mut is_infeasible = false; let tasks = tasks .into_iter() .map(|task| { - is_infeasible |= task.resource_usage > capacity; + is_infeasible |= + context.lower_bound(&task.resource_usage) > context.upper_bound(&capacity); Rc::new(task) }) .collect::>() diff --git a/pumpkin-crates/core/src/propagators/cumulative/utils/structs/resource_profile.rs b/pumpkin-crates/core/src/propagators/cumulative/utils/structs/resource_profile.rs index fc3be6708..2c6dee9e2 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/utils/structs/resource_profile.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/utils/structs/resource_profile.rs @@ -7,31 +7,26 @@ use crate::variables::IntegerVariable; /// Structures used for storing the data related to resource profiles; /// A [`ResourceProfile`] represents a rectangle where the height is the cumulative mandatory /// resource usage of the [`profile tasks`][ResourceProfile::profile_tasks] -#[derive(Clone)] -pub(crate) struct ResourceProfile { +#[derive(Clone, Debug)] +pub(crate) struct ResourceProfile { /// The start time of the [`ResourceProfile`] (inclusive) pub(crate) start: i32, /// The end time of the [`ResourceProfile`] (inclusive) pub(crate) end: i32, /// The IDs of the tasks which are part of the profile - pub(crate) profile_tasks: Vec>>, + pub(crate) profile_tasks: Vec>>, /// The amount of cumulative resource usage of all [`profile /// tasks`][ResourceProfile::profile_tasks] (i.e. the height of the rectangle) pub(crate) height: i32, } -impl Debug for ResourceProfile { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - f.debug_struct("ResourceProfile") - .field("start", &self.start) - .field("end", &self.end) - .field("height", &self.height) - .finish() - } -} - -impl ResourceProfile { - pub(crate) fn default(time: i32) -> ResourceProfile { +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +> ResourceProfile +{ + pub(crate) fn default(time: i32) -> ResourceProfile { ResourceProfile { start: time, end: time, diff --git a/pumpkin-crates/core/src/propagators/cumulative/utils/structs/task.rs b/pumpkin-crates/core/src/propagators/cumulative/utils/structs/task.rs index dff382659..89bb419d5 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/utils/structs/task.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/utils/structs/task.rs @@ -7,55 +7,67 @@ use crate::variables::IntegerVariable; /// Structure which stores the variables related to a task; for now, only the start times are /// assumed to be variable -pub(crate) struct Task { +#[derive(Debug)] +pub(crate) struct Task { /// The variable representing the start time of a task pub(crate) start_variable: Var, /// The processing time of the `start_variable` (also referred to as duration of a task) - pub(crate) processing_time: i32, + pub(crate) processing_time: PVar, /// How much of the resource the given task uses during its non-preemptive execution - pub(crate) resource_usage: i32, + pub(crate) resource_usage: RVar, /// The [`LocalId`] of the task pub(crate) id: LocalId, } -impl Debug for Task { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - f.debug_struct("Task") - .field("processing_time", &self.processing_time) - .field("resource_usage", &self.resource_usage) - .field("local_id", &self.id) - .finish() - } -} - -impl Task { - pub(crate) fn get_id(task: &Rc>) -> usize { +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +> Task +{ + pub(crate) fn get_id(task: &Rc>) -> usize { task.id.unpack() as usize } } -impl Hash for Task { +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +> Hash for Task +{ fn hash(&self, state: &mut H) { self.id.hash(state); } } -impl PartialEq for Task { +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +> PartialEq for Task +{ fn eq(&self, other: &Self) -> bool { self.id.unpack() == other.id.unpack() } } -impl Eq for Task {} +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +> Eq for Task +{ +} /// The task which is passed as argument #[derive(Clone, Debug)] -pub(crate) struct ArgTask { +pub struct ArgTask { /// The [`IntegerVariable`] representing the start time of a task - pub(crate) start_time: Var, + pub start_time: Var, /// The processing time of the [`start_time`][ArgTask::start_time] (also referred to as /// duration of a task) - pub(crate) processing_time: i32, + pub processing_time: PVar, /// How much of the resource the given task uses during its non-preemptive execution - pub(crate) resource_usage: i32, + pub resource_usage: RVar, } diff --git a/pumpkin-crates/core/src/propagators/cumulative/utils/structs/updatable_structures.rs b/pumpkin-crates/core/src/propagators/cumulative/utils/structs/updatable_structures.rs index 948cb9c93..860625c49 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/utils/structs/updatable_structures.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/utils/structs/updatable_structures.rs @@ -12,7 +12,7 @@ use crate::variables::IntegerVariable; /// Structures which are adjusted during search; either due to incrementality or to keep track of /// bounds. #[derive(Debug, Clone)] -pub(crate) struct UpdatableStructures { +pub(crate) struct UpdatableStructures { /// The current known bounds of the different [tasks][CumulativeParameters::tasks]; stored as /// (lower bound, upper bound) /// @@ -20,15 +20,20 @@ pub(crate) struct UpdatableStructures { bounds: Vec<(i32, i32)>, /// The [`Task`]s which have been updated since the last round of propagation, this structure /// is updated by the (incremental) propagator - updates: Vec>, + updates: Vec>, /// The tasks which have been updated since the last iteration - updated_tasks: SparseSet>>, + updated_tasks: SparseSet>>, /// The tasks which are unfixed - unfixed_tasks: SparseSet>>, + unfixed_tasks: SparseSet>>, } -impl UpdatableStructures { - pub(crate) fn new(parameters: &CumulativeParameters) -> Self { +impl< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +> UpdatableStructures +{ + pub(crate) fn new(parameters: &CumulativeParameters) -> Self { let mut updated_tasks = SparseSet::new(parameters.tasks.to_vec(), Task::get_id); updated_tasks.set_to_empty(); @@ -47,7 +52,7 @@ impl UpdatableStructures { } /// Returns the next updated task and removes it from the updated list - pub(crate) fn pop_next_updated_task(&mut self) -> Option>> { + pub(crate) fn pop_next_updated_task(&mut self) -> Option>> { if self.updated_tasks.is_empty() { return None; } @@ -60,14 +65,14 @@ impl UpdatableStructures { /// whether the updated task was actually updated). pub(crate) fn get_update_for_task( &mut self, - updated_task: &Rc>, - ) -> UpdatedTaskInfo { + updated_task: &Rc>, + ) -> UpdatedTaskInfo { self.updates[updated_task.id.unpack() as usize].clone() } /// Resets the stored update for the current task to be equal to the current scenario; i.e. /// resets the old bounds to be equal to the new bounds - pub(crate) fn reset_update_for_task(&mut self, updated_task: &Rc>) { + pub(crate) fn reset_update_for_task(&mut self, updated_task: &Rc>) { let update = &mut self.updates[updated_task.id.unpack() as usize]; update.old_lower_bound = update.new_lower_bound; @@ -85,30 +90,30 @@ impl UpdatableStructures { } /// Returns the stored lower-bound for a task. - pub(crate) fn get_stored_lower_bound(&self, task: &Rc>) -> i32 { + pub(crate) fn get_stored_lower_bound(&self, task: &Rc>) -> i32 { self.bounds[task.id.unpack() as usize].0 } /// Returns the stored upper-bound for a task. - pub(crate) fn get_stored_upper_bound(&self, task: &Rc>) -> i32 { + pub(crate) fn get_stored_upper_bound(&self, task: &Rc>) -> i32 { self.bounds[task.id.unpack() as usize].1 } /// Fixes a task in the internal structure(s). - pub(crate) fn fix_task(&mut self, updated_task: &Rc>) { + pub(crate) fn fix_task(&mut self, updated_task: &Rc>) { self.unfixed_tasks.remove(updated_task); } /// Unfixes a task in the internal structure(s). - pub(crate) fn unfix_task(&mut self, updated_task: Rc>) { + pub(crate) fn unfix_task(&mut self, updated_task: Rc>) { self.unfixed_tasks.insert(updated_task); } /// Removes the fixed tasks from the internal structure(s). - pub(crate) fn remove_fixed( + pub(crate) fn remove_fixed( &mut self, context: PropagationContext, - parameters: &CumulativeParameters, + parameters: &CumulativeParameters, ) { for task in parameters.tasks.iter() { // If the task is fixed then we remove it, otherwise we insert it as an unfixed task @@ -122,10 +127,10 @@ impl UpdatableStructures { /// Resets all of the bounds to the current values in the context and removes all of the fixed /// tasks from the internal structure(s). - pub(crate) fn reset_all_bounds_and_remove_fixed( + pub(crate) fn reset_all_bounds_and_remove_fixed( &mut self, context: PropagationContext, - parameters: &CumulativeParameters, + parameters: &CumulativeParameters, ) { for task in parameters.tasks.iter() { if self.updates.len() <= task.id.unpack() as usize { @@ -172,29 +177,39 @@ impl UpdatableStructures { } // Initialises all stored bounds to their current values and removes any tasks which are fixed - pub(crate) fn initialise_bounds_and_remove_fixed( + pub(crate) fn initialise_bounds_and_remove_fixed( &mut self, context: PropagationContext, - parameters: &CumulativeParameters, + parameters: &CumulativeParameters, ) { for task in parameters.tasks.iter() { + self.updates.push(UpdatedTaskInfo { + task: Rc::clone(task), + old_lower_bound: context.lower_bound(&task.start_variable), + old_upper_bound: context.upper_bound(&task.start_variable), + new_lower_bound: context.lower_bound(&task.start_variable), + new_upper_bound: context.upper_bound(&task.start_variable), + }); self.bounds.push(( context.lower_bound(&task.start_variable), context.upper_bound(&task.start_variable), )); - if context.is_fixed(&task.start_variable) { + if context.is_fixed(&task.start_variable) + && context.is_fixed(&task.processing_time) + && context.is_fixed(&task.resource_usage) + { self.fix_task(task); } } } /// Returns all of the tasks which are not currently fixed - pub(crate) fn get_unfixed_tasks(&self) -> impl Iterator>> { + pub(crate) fn get_unfixed_tasks(&self) -> impl Iterator>> { self.unfixed_tasks.iter() } // Returns all of the tasks which are currently fixed - pub(crate) fn get_fixed_tasks(&self) -> impl Iterator>> { + pub(crate) fn get_fixed_tasks(&self) -> impl Iterator>> { self.unfixed_tasks.out_of_domain() } @@ -209,7 +224,10 @@ impl UpdatableStructures { } // Temporarily removes a task from the set of unfixed tasks - pub(crate) fn temporarily_remove_task_from_unfixed(&mut self, task: &Rc>) { + pub(crate) fn temporarily_remove_task_from_unfixed( + &mut self, + task: &Rc>, + ) { self.unfixed_tasks.remove_temporarily(task) } @@ -219,12 +237,12 @@ impl UpdatableStructures { } // Returns the unfixed task at the specified index - pub(crate) fn get_unfixed_task_at_index(&self, index: usize) -> Rc> { + pub(crate) fn get_unfixed_task_at_index(&self, index: usize) -> Rc> { Rc::clone(self.unfixed_tasks.get(index)) } // Marks a task as updated in the internal structure(s) - pub(crate) fn task_has_been_updated(&mut self, task: &Rc>) { + pub(crate) fn task_has_been_updated(&mut self, task: &Rc>) { self.updated_tasks.insert(Rc::clone(task)) } @@ -232,8 +250,8 @@ impl UpdatableStructures { // are updated to the ones provided in the update pub(crate) fn insert_update_for_task( &mut self, - task: &Rc>, - updated_task_info: UpdatedTaskInfo, + task: &Rc>, + updated_task_info: UpdatedTaskInfo, ) { let stored_updated_task_info = &mut self.updates[task.id.unpack() as usize]; @@ -242,10 +260,10 @@ impl UpdatableStructures { } /// Used for creating the dynamic structures from the provided context - pub(crate) fn recreate_from_context( + pub(crate) fn recreate_from_context( &self, context: PropagationContext, - parameters: &CumulativeParameters, + parameters: &CumulativeParameters, ) -> Self { let mut other = self.clone(); diff --git a/pumpkin-crates/core/src/propagators/cumulative/utils/structs/updated_task_info.rs b/pumpkin-crates/core/src/propagators/cumulative/utils/structs/updated_task_info.rs index d354447ff..59b2833d9 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/utils/structs/updated_task_info.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/utils/structs/updated_task_info.rs @@ -5,10 +5,10 @@ use super::Task; /// Stores the information of an updated task; for example in the context of /// [`TimeTablePerPointPropagator`] this is a task whose mandatory part has changed. #[derive(Debug, Clone)] -pub(crate) struct UpdatedTaskInfo { +pub(crate) struct UpdatedTaskInfo { /// The task which has been updated (where "updated" is according to some context-dependent /// definition) - pub(crate) task: Rc>, + pub(crate) task: Rc>, /// The lower-bound of the [`Task`] before the update pub(crate) old_lower_bound: i32, /// The upper-bound of the [`Task`] before the update diff --git a/pumpkin-crates/core/src/propagators/cumulative/utils/util.rs b/pumpkin-crates/core/src/propagators/cumulative/utils/util.rs index 98ee1bcee..bb98603e7 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/utils/util.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/utils/util.rs @@ -19,23 +19,28 @@ use crate::propagators::Task; /// registered for [`DomainEvents`]. /// /// It sorts [`Task`]s on non-decreasing resource usage and removes [`Task`]s with resource usage 0. -pub(crate) fn create_tasks( - arg_tasks: &[ArgTask], -) -> Vec> { +pub(crate) fn create_tasks< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( + context: PropagationContext, + arg_tasks: &[ArgTask], +) -> Vec> { // We order the tasks by non-decreasing resource usage, this allows certain optimizations let mut ordered_tasks = arg_tasks.to_vec(); - ordered_tasks.sort_by(|a, b| b.resource_usage.cmp(&a.resource_usage)); + ordered_tasks.sort_by_key(|a| context.lower_bound(&a.resource_usage)); let mut id = 0; ordered_tasks .iter() .filter_map(|x| { // We only add tasks which have a non-zero resource usage - if x.resource_usage > 0 { + if context.lower_bound(&x.resource_usage) > 0 { let return_value = Some(Task { start_variable: x.start_time.clone(), - processing_time: x.processing_time, - resource_usage: x.resource_usage, + processing_time: x.processing_time.clone(), + resource_usage: x.resource_usage.clone(), id: LocalId::from(id), }); @@ -45,14 +50,26 @@ pub(crate) fn create_tasks( None } }) - .collect::>>() + .collect::>>() } -pub(crate) fn register_tasks( - tasks: &[Rc>], +pub(crate) fn register_tasks< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, + CVar: IntegerVariable + 'static, +>( + tasks: &[Rc>], + capacity: &CVar, mut context: PropagatorConstructorContext<'_>, register_backtrack: bool, ) { + context.register( + capacity.clone(), + DomainEvents::create_with_int_events(enum_set!(DomainEvent::UpperBound)), + LocalId::from(tasks.len() as u32), + ); + tasks.iter().for_each(|task| { context.register( task.start_variable.clone(), @@ -61,6 +78,21 @@ pub(crate) fn register_tasks( )), task.id, ); + context.register( + task.processing_time.clone(), + DomainEvents::create_with_int_events(enum_set!( + DomainEvent::LowerBound | DomainEvent::Assign + )), + task.id, + ); + context.register( + task.resource_usage.clone(), + DomainEvents::create_with_int_events(enum_set!( + DomainEvent::LowerBound | DomainEvent::Assign + )), + task.id, + ); + if register_backtrack { context.register_for_backtrack_events( task.start_variable.clone(), @@ -75,10 +107,14 @@ pub(crate) fn register_tasks( /// Updates the bounds of the provided [`Task`] to those stored in /// `context`. -pub(crate) fn update_bounds_task( +pub(crate) fn update_bounds_task< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( context: PropagationContext, bounds: &mut [(i32, i32)], - task: &Rc>, + task: &Rc>, ) { bounds[task.id.unpack() as usize] = ( context.lower_bound(&task.start_variable), @@ -87,9 +123,13 @@ pub(crate) fn update_bounds_task( } /// Determines whether the stored bounds are equal when propagation occurs -pub(crate) fn check_bounds_equal_at_propagation( +pub(crate) fn check_bounds_equal_at_propagation< + Var: IntegerVariable + 'static, + PVar: IntegerVariable + 'static, + RVar: IntegerVariable + 'static, +>( context: PropagationContext, - tasks: &[Rc>], + tasks: &[Rc>], bounds: &[(i32, i32)], ) -> bool { tasks.iter().all(|current| { diff --git a/pumpkin-crates/core/src/propagators/mod.rs b/pumpkin-crates/core/src/propagators/mod.rs index 7c8c73093..149f40a64 100644 --- a/pumpkin-crates/core/src/propagators/mod.rs +++ b/pumpkin-crates/core/src/propagators/mod.rs @@ -9,6 +9,7 @@ pub(crate) mod element; pub(crate) mod nogoods; mod reified_propagator; pub(crate) use arithmetic::*; +pub use cumulative::ArgTask; pub use cumulative::CumulativeExplanationType; pub use cumulative::CumulativeOptions; pub use cumulative::CumulativePropagationMethod; diff --git a/pumpkin-macros/src/lib.rs b/pumpkin-macros/src/lib.rs index f9f92b661..8b051feb4 100644 --- a/pumpkin-macros/src/lib.rs +++ b/pumpkin-macros/src/lib.rs @@ -65,6 +65,36 @@ pub fn cumulative(item: TokenStream) -> TokenStream { } .into(); output.extend(stream); + + let test_name_var = format_ident!( + "{}_var", + stringcase::snake_case( + &[ + "cumulative", + &propagation_method, + explanation_type, + &option_string, + ] + .into_iter() + .filter(|string| !string.is_empty()) + .join("_") + ) + ); + let stream: TokenStream = quote! { + mzn_test!( + #test_name_var, + "cumulative_var", + vec![ + "--cumulative-propagation-method".to_string(), + stringcase::kebab_case(#propagation_method), + "--cumulative-explanation-type".to_string(), + #explanation_type.to_string(), + #(#options.to_string()),* + ] + ); + } + .into(); + output.extend(stream); } } diff --git a/pumpkin-solver-py/src/constraints/globals.rs b/pumpkin-solver-py/src/constraints/globals.rs index ab553579a..1b7d61664 100644 --- a/pumpkin-solver-py/src/constraints/globals.rs +++ b/pumpkin-solver-py/src/constraints/globals.rs @@ -1,8 +1,12 @@ +use pumpkin_solver::constraint_arguments::ArgTask; use pumpkin_solver::constraints::Constraint; use pumpkin_solver::constraints::{self}; +use pumpkin_solver::variables::AffineView; +use pumpkin_solver::variables::DomainId; use pyo3::pyclass; use pyo3::pymethods; +use crate::constraints::arguments::PythonConstraintArg; use crate::model::Tag; use crate::variables::*; @@ -94,15 +98,6 @@ python_constraint! { } } -python_constraint! { - Cumulative: cumulative { - start_times: Vec, - durations: Vec, - resource_requirements: Vec, - resource_capacity: i32, - } -} - python_constraint! { Division: division { numerator: IntExpression, @@ -195,3 +190,42 @@ python_constraint! { table: Vec>, } } + +python_constraint! { + Cumulative: cumulative { + tasks: Vec, + capacity: i32 + } +} + +#[pyclass(eq, hash, frozen)] +#[derive(Clone, Copy, PartialEq, Eq, Hash)] +pub struct Task { + start_time: IntExpression, + processing_time: i32, + resource_usage: i32, +} + +#[pymethods] +impl Task { + #[new] + fn new(start_time: IntExpression, processing_time: i32, resource_usage: i32) -> Self { + Self { + start_time, + processing_time, + resource_usage, + } + } +} + +impl PythonConstraintArg for Task { + type Output = ArgTask, i32, i32>; + + fn to_solver_constraint_argument(self, variable_map: &VariableMap) -> Self::Output { + ArgTask { + start_time: self.start_time.to_solver_constraint_argument(variable_map), + processing_time: self.processing_time, + resource_usage: self.resource_usage, + } + } +} diff --git a/pumpkin-solver-py/src/constraints/mod.rs b/pumpkin-solver-py/src/constraints/mod.rs index ec8080366..bd972a3cc 100644 --- a/pumpkin-solver-py/src/constraints/mod.rs +++ b/pumpkin-solver-py/src/constraints/mod.rs @@ -36,6 +36,7 @@ macro_rules! declare_constraints { pub fn register(m: &Bound<'_, PyModule>) -> PyResult<()> { $(m.add_class::<$constraint>()?;)+ + m.add_class::()?; Ok(()) } }; diff --git a/pumpkin-solver-py/tests/test_constraints.py b/pumpkin-solver-py/tests/test_constraints.py index 0901863a5..cfcf972f7 100644 --- a/pumpkin-solver-py/tests/test_constraints.py +++ b/pumpkin-solver-py/tests/test_constraints.py @@ -1,15 +1,14 @@ -""" -Generate constraints and expressions based on the grammar supported by the API +"""Generate constraints and expressions based on the grammar supported by the API. -Generates linear constraints, special operators and global constraints. -Whenever possible, the script also generates 'boolean as integer' versions of the arguments +Generates linear constraints, special operators and global constraints. Whenever possible, the script also generates +'boolean as integer' versions of the arguments """ from random import randint +import pumpkin_solver import pytest from pumpkin_solver import constraints -import pumpkin_solver # generate all linear sum-expressions @@ -28,10 +27,7 @@ def generate_linear(): for i in range(3) ] else: - args = [ - model.new_integer_variable(-3, 5, name=f"x[{i}]") - for i in range(3) - ] + args = [model.new_integer_variable(-3, 5, name=f"x[{i}]") for i in range(3)] if scaled: # do scaling (0, -2, 4,...) args = [ a.scaled(-2 * i + 1) for i, a in enumerate(args) @@ -43,9 +39,7 @@ def generate_linear(): if comp == "!=": cons = constraints.NotEquals(args, rhs, model.new_constraint_tag()) if comp == "<=": - cons = constraints.LessThanOrEquals( - args, rhs, model.new_constraint_tag() - ) + cons = constraints.LessThanOrEquals(args, rhs, model.new_constraint_tag()) yield model, cons, comp, scaled, bool @@ -66,10 +60,7 @@ def generate_operators(): for i in range(3) ] else: - args = [ - model.new_integer_variable(-3, 5, name=f"x[{i}]") - for i in range(3) - ] + args = [model.new_integer_variable(-3, 5, name=f"x[{i}]") for i in range(3)] if scaled: # do scaling (0, -2, 4,...) args = [ a.scaled(-2 * i + 1) for i, a in enumerate(args) @@ -78,26 +69,18 @@ def generate_operators(): rhs = model.new_integer_variable(-3, 5, name="rhs") if name == "div": denom = model.new_integer_variable(1, 3, name="denom") - cons = constraints.Division( - args[0], denom, rhs, model.new_constraint_tag() - ) + cons = constraints.Division(args[0], denom, rhs, model.new_constraint_tag()) if name == "mul": cons = constraints.Times(*args[:2], rhs, model.new_constraint_tag()) if name == "abs": - cons = constraints.Absolute( - args[0], rhs, model.new_constraint_tag() - ) + cons = constraints.Absolute(args[0], rhs, model.new_constraint_tag()) if name == "min": cons = constraints.Minimum(args, rhs, model.new_constraint_tag()) if name == "max": cons = constraints.Maximum(args, rhs, model.new_constraint_tag()) if name == "element": - idx = model.new_integer_variable( - -1, 5, name="idx" - ) # sneaky, idx can be out of bounds - cons = constraints.Element( - idx, args, rhs, model.new_constraint_tag() - ) + idx = model.new_integer_variable(-1, 5, name="idx") # sneaky, idx can be out of bounds + cons = constraints.Element(idx, args, rhs, model.new_constraint_tag()) yield model, cons, name, scaled, bool @@ -116,9 +99,7 @@ def generate_alldiff(): for i in range(3) ] else: - args = [ - model.new_integer_variable(-3, 5, name=f"x[{i}]") for i in range(3) - ] + args = [model.new_integer_variable(-3, 5, name=f"x[{i}]") for i in range(3)] if scaled or bool: # do scaling (0, -2, 4,...) args = [ a.scaled(-2 * i + 1) for i, a in enumerate(args) @@ -154,17 +135,31 @@ def generate_cumulative(): capacity = 4 model = pumpkin_solver.Model() - start = [model.new_integer_variable(-3, 5, name=f"x[{i}]") for i in range(3)] + start = [model.new_integer_variable(0, 5, name=f"x[{i}]") for i in range(3)] cons = constraints.Cumulative( - start, duration, demand, capacity, model.new_constraint_tag() + list( + map( + lambda task: constraints.Task(*task), + zip(start, duration, demand), + ) + ), + capacity, + model.new_constraint_tag(), ) yield model, cons, "cumulative", False, False model = pumpkin_solver.Model() - start = [model.new_integer_variable(-3, 5, name=f"x[{i}]") for i in range(3)] + start = [model.new_integer_variable(0, 5, name=f"x[{i}]") for i in range(3)] start = [a.scaled(-2 * i) for i, a in enumerate(start)] cons = constraints.Cumulative( - start, duration, demand, capacity, model.new_constraint_tag() + list( + map( + lambda task: constraints.Task(*task), + zip(start, duration, demand), + ) + ), + capacity, + model.new_constraint_tag(), ) yield model, cons, "cumulative", True, False @@ -177,17 +172,13 @@ def generate_globals(): def label(model, cons, name, scaled, bool): - return " ".join( - ["Scaled" if scaled else "Unscaled", "Boolean" if bool else "Integer", name] - ) + return " ".join(["Scaled" if scaled else "Unscaled", "Boolean" if bool else "Integer", name]) LINEAR = list(generate_operators()) -@pytest.mark.parametrize( - ("model", "cons", "name", "scaled", "bool"), LINEAR, ids=[label(*a) for a in LINEAR] -) +@pytest.mark.parametrize(("model", "cons", "name", "scaled", "bool"), LINEAR, ids=[label(*a) for a in LINEAR]) def test_linear(model, cons, name, scaled, bool): model.add_constraint(cons) res = model.satisfy() @@ -222,9 +213,7 @@ def test_global(model, cons, name, scaled, bool): assert isinstance(res, pumpkin_solver.SatisfactionResult.Satisfiable) -ALL_EXPR = ( - list(generate_operators()) + list(generate_linear()) + list(generate_globals()) -) +ALL_EXPR = list(generate_operators()) + list(generate_linear()) + list(generate_globals()) @pytest.mark.parametrize( diff --git a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/post_constraints.rs b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/post_constraints.rs index cf49dbe57..01d9cb11c 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/post_constraints.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/post_constraints.rs @@ -3,6 +3,7 @@ use std::rc::Rc; use pumpkin_core::constraint_arguments::ArgDisjunctiveTask; +use pumpkin_core::constraint_arguments::ArgTask; use pumpkin_solver::constraints; use pumpkin_solver::constraints::Constraint; use pumpkin_solver::constraints::NegatableConstraint; @@ -343,9 +344,9 @@ pub(crate) fn run( } "pumpkin_cumulative" => compile_cumulative(context, exprs, options, constraint_tag)?, - "pumpkin_cumulative_var" => todo!( - "The `cumulative` constraint with variable duration/resource consumption/bound is not implemented yet!" - ), + "pumpkin_cumulative_vars" => { + compile_cumulative_vars(context, exprs, options, constraint_tag)? + } unknown => todo!("unsupported constraint {unknown}"), }; @@ -409,9 +410,52 @@ fn compile_cumulative( let resource_capacity = context.resolve_integer_constant_from_expr(&exprs[3])?; let post_result = constraints::cumulative_with_options( - start_times.iter().copied(), - durations.iter().copied(), - resource_requirements.iter().copied(), + start_times + .iter() + .zip(durations.iter()) + .zip(resource_requirements.iter()) + .map( + |((&start_time, &processing_time), &resource_usage)| ArgTask { + start_time, + processing_time, + resource_usage, + }, + ) + .collect::>(), + resource_capacity, + options.cumulative_options, + constraint_tag, + ) + .post(context.solver); + Ok(post_result.is_ok()) +} + +fn compile_cumulative_vars( + context: &mut CompilationContext<'_>, + exprs: &[flatzinc::Expr], + options: &FlatZincOptions, + constraint_tag: ConstraintTag, +) -> Result { + check_parameters!(exprs, 4, "pumpkin_cumulative_vars"); + + let start_times = context.resolve_integer_variable_array(&exprs[0])?; + let durations = context.resolve_integer_variable_array(&exprs[1])?; + let resource_requirements = context.resolve_integer_variable_array(&exprs[2])?; + let resource_capacity = context.resolve_integer_variable(&exprs[3])?; + + let post_result = constraints::cumulative_with_options( + start_times + .iter() + .zip(durations.iter()) + .zip(resource_requirements.iter()) + .map( + |((&start_time, &processing_time), &resource_usage)| ArgTask { + start_time, + processing_time, + resource_usage, + }, + ) + .collect::>(), resource_capacity, options.cumulative_options, constraint_tag, diff --git a/pumpkin-solver/tests/mzn_constraints/cumulative_var.expected b/pumpkin-solver/tests/mzn_constraints/cumulative_var.expected new file mode 100644 index 000000000..b3ba0474f --- /dev/null +++ b/pumpkin-solver/tests/mzn_constraints/cumulative_var.expected @@ -0,0 +1,1101 @@ +s1 = 2; +s2 = 3; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 5; +s2 = 3; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 3; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 5; +s2 = 3; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 3; +s3 = 5; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 3; +s3 = 5; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 3; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 5; +s2 = 3; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 3; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 5; +s2 = 3; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 3; +s3 = 5; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 3; +s3 = 5; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 4; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 4; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 4; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 4; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 4; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 4; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 4; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 4; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 4; +s3 = 3; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 4; +s3 = 3; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 4; +s3 = 3; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 4; +s3 = 3; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 5; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 5; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 4; +s2 = 5; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 5; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 5; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 4; +s2 = 5; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 5; +s3 = 3; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 5; +s3 = 3; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 4; +s2 = 5; +s3 = 3; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 5; +s3 = 4; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 5; +s3 = 4; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 5; +s3 = 4; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 5; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 5; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 4; +s2 = 5; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 5; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 5; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 4; +s2 = 5; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 5; +s3 = 3; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 5; +s3 = 3; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 4; +s2 = 5; +s3 = 3; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 5; +s3 = 4; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 5; +s3 = 4; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 5; +s3 = 4; +p1 = 1; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 3; +s3 = 5; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 3; +s3 = 5; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 5; +s2 = 3; +s3 = 1; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 5; +s2 = 3; +s3 = 1; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 5; +s2 = 3; +s3 = 2; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 5; +s2 = 3; +s3 = 2; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 4; +s3 = 3; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 4; +s3 = 3; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 4; +s3 = 1; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 4; +s3 = 1; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 5; +s3 = 3; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 5; +s3 = 3; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 5; +s3 = 4; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 5; +s3 = 4; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 5; +s3 = 1; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 5; +s3 = 1; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 5; +s3 = 4; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 5; +s3 = 4; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 5; +s3 = 1; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 5; +s3 = 1; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 5; +s3 = 2; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 5; +s3 = 2; +p1 = 2; +p2 = 2; +p3 = 1; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 5; +s2 = 3; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 5; +s2 = 3; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 3; +s3 = 5; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 3; +s3 = 5; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 3; +s3 = 5; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 3; +s3 = 5; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 4; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 4; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 4; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 4; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 5; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 5; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 4; +s2 = 5; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 4; +s2 = 5; +s3 = 1; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 5; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 5; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 4; +s2 = 5; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 4; +s2 = 5; +s3 = 2; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 5; +s3 = 3; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 5; +s3 = 3; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 5; +s3 = 3; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 2; +s2 = 5; +s3 = 3; +p1 = 1; +p2 = 2; +p3 = 2; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 5; +s2 = 3; +s3 = 1; +p1 = 2; +p2 = 2; +p3 = 2; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 5; +s2 = 3; +s3 = 1; +p1 = 2; +p2 = 2; +p3 = 2; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 3; +s3 = 5; +p1 = 2; +p2 = 2; +p3 = 2; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 3; +s3 = 5; +p1 = 2; +p2 = 2; +p3 = 2; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 5; +s3 = 1; +p1 = 2; +p2 = 2; +p3 = 2; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 3; +s2 = 5; +s3 = 1; +p1 = 2; +p2 = 2; +p3 = 2; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 5; +s3 = 3; +p1 = 2; +p2 = 2; +p3 = 2; +r1 = 3; +r2 = 2; +r3 = 4; +c = 4; +---------- +s1 = 1; +s2 = 5; +s3 = 3; +p1 = 2; +p2 = 2; +p3 = 2; +r1 = 4; +r2 = 2; +r3 = 4; +c = 4; +---------- +========== diff --git a/pumpkin-solver/tests/mzn_constraints/cumulative_var.fzn b/pumpkin-solver/tests/mzn_constraints/cumulative_var.fzn new file mode 100644 index 000000000..f3a8f9671 --- /dev/null +++ b/pumpkin-solver/tests/mzn_constraints/cumulative_var.fzn @@ -0,0 +1,17 @@ +var 1..5: s1:: output_var; +var 3..5: s2:: output_var; +var 1..5: s3:: output_var; + +var 1..2: p1:: output_var; +var 2..2: p2:: output_var; +var 1..2: p3:: output_var; + +var 3..4: r1:: output_var; +var 2..2: r2:: output_var; +var 4..5: r3:: output_var; + +var 1..4: c:: output_var; + +constraint pumpkin_cumulative_vars([s1, s2, s3], [p1, p2, p3], [r1, r2, r3], c); + +solve satisfy; diff --git a/pumpkin-solver/tests/mzn_constraints/cumulative_var.template b/pumpkin-solver/tests/mzn_constraints/cumulative_var.template new file mode 100644 index 000000000..1747124b9 --- /dev/null +++ b/pumpkin-solver/tests/mzn_constraints/cumulative_var.template @@ -0,0 +1,23 @@ +predicate gecode_cumulatives(array [int] of var int: start_times, + array [int] of var int: durations, + array [int] of var int: resource_requirements, + var int: resource_capacity +); + +var 1..5: s1:: output_var; +var 3..5: s2:: output_var; +var 1..5: s3:: output_var; + +var 1..2: p1:: output_var; +var 2..2: p2:: output_var; +var 1..2: p3:: output_var; + +var 3..4: r1:: output_var; +var 2..2: r2:: output_var; +var 4..5: r3:: output_var; + +var 1..4: c:: output_var; + +constraint gecode_cumulatives([s1, s2, s3], [p1, p2, p3], [r1, r2, r3], c); + +solve satisfy;