From 2e9cba5b18049478a161dc333aa385c95ea9c7b6 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Fri, 27 Feb 2026 15:16:12 +1100 Subject: [PATCH 01/10] Initial implementation of consistency checkers --- pumpkin-crates/core/src/engine/state.rs | 25 +++++- .../core/src/engine/variables/affine_view.rs | 17 ++++ .../core/src/engine/variables/domain_id.rs | 13 +++ .../src/engine/variables/integer_variable.rs | 2 + .../core/src/engine/variables/literal.rs | 12 +++ .../checkers/consistency_checker.rs | 39 ++++++++ .../checkers/domain_consistency_checker.rs | 90 +++++++++++++++++++ .../core/src/propagation/checkers/mod.rs | 27 ++++++ .../core/src/propagation/checkers/scope.rs | 30 +++++++ .../core/src/propagation/checkers/variable.rs | 35 ++++++++ .../core/src/propagation/checkers/witness.rs | 44 +++++++++ .../propagation/checkers/witness_generator.rs | 16 ++++ .../core/src/propagation/constructor.rs | 21 ++++- pumpkin-crates/core/src/propagation/mod.rs | 2 + .../hypercube_linear/propagator.rs | 11 ++- .../src/propagators/reified_propagator.rs | 12 ++- .../propagators/arithmetic/absolute_value.rs | 9 +- .../arithmetic/binary/binary_equals.rs | 34 ++++++- .../arithmetic/binary/binary_not_equals.rs | 9 +- .../arithmetic/integer_division.rs | 9 +- .../arithmetic/integer_multiplication.rs | 9 +- .../arithmetic/linear_less_or_equal.rs | 9 +- .../arithmetic/linear_not_equal.rs | 9 +- .../src/propagators/arithmetic/maximum.rs | 9 +- .../time_table_over_interval_incremental.rs | 9 +- .../time_table_per_point_incremental.rs | 9 +- .../time_table/time_table_over_interval.rs | 8 +- .../time_table/time_table_per_point.rs | 9 +- .../disjunctive/disjunctive_propagator.rs | 11 ++- .../propagators/src/propagators/element.rs | 11 ++- 30 files changed, 531 insertions(+), 19 deletions(-) create mode 100644 pumpkin-crates/core/src/propagation/checkers/consistency_checker.rs create mode 100644 pumpkin-crates/core/src/propagation/checkers/domain_consistency_checker.rs create mode 100644 pumpkin-crates/core/src/propagation/checkers/mod.rs create mode 100644 pumpkin-crates/core/src/propagation/checkers/scope.rs create mode 100644 pumpkin-crates/core/src/propagation/checkers/variable.rs create mode 100644 pumpkin-crates/core/src/propagation/checkers/witness.rs create mode 100644 pumpkin-crates/core/src/propagation/checkers/witness_generator.rs diff --git a/pumpkin-crates/core/src/engine/state.rs b/pumpkin-crates/core/src/engine/state.rs index 1ced792ee..ff8ce9f87 100644 --- a/pumpkin-crates/core/src/engine/state.rs +++ b/pumpkin-crates/core/src/engine/state.rs @@ -39,6 +39,8 @@ use crate::propagation::Propagator; use crate::propagation::PropagatorConstructor; use crate::propagation::PropagatorConstructorContext; use crate::propagation::PropagatorId; +#[cfg(feature = "check-propagations")] +use crate::propagation::checkers::BoxedConsistencyChecker; use crate::propagation::store::PropagatorStore; use crate::pumpkin_assert_advanced; use crate::pumpkin_assert_eq_simple; @@ -83,6 +85,8 @@ pub struct State { /// Inference checkers to run in the propagation loop. checkers: HashMap>>, + #[cfg(feature = "check-propagations")] + consistency_checkers: HashMap, } create_statistics_struct!(StateStatistics { @@ -177,6 +181,8 @@ impl Default for State { statistics: StateStatistics::default(), constraint_tags: KeyGenerator::default(), checkers: HashMap::default(), + #[cfg(feature = "check-propagations")] + consistency_checkers: HashMap::default(), }; // As a convention, the assignments contain a dummy domain_id=0, which represents a 0-1 // variable that is assigned to one. We use it to represent predicates that are @@ -389,7 +395,7 @@ impl State { Constructor::PropagatorImpl: 'static, { #[cfg(feature = "check-propagations")] - constructor.add_inference_checkers(InferenceCheckers::new(self)); + let consistency_checker = constructor.add_inference_checkers(InferenceCheckers::new(self)); let original_handle: PropagatorHandle = self.propagators.new_propagator().key(); @@ -408,6 +414,23 @@ impl State { let slot = self.propagators.new_propagator(); let handle = slot.populate(propagator); + #[cfg(feature = "check-propagations")] + { + use crate::propagation::checkers::ConsistencyChecker; + + #[allow(trivial_casts, reason = "removing it causes a compiler error")] + let previous_checker = self.consistency_checkers.insert( + handle.propagator_id(), + BoxedConsistencyChecker::from( + Box::new(consistency_checker) as Box + ), + ); + assert!( + previous_checker.is_none(), + "somehow adding multiple consistency checkers to the same propagator" + ); + } + pumpkin_assert_eq_simple!(handle.propagator_id(), original_handle.propagator_id()); #[allow(deprecated, reason = "Will be refactored")] diff --git a/pumpkin-crates/core/src/engine/variables/affine_view.rs b/pumpkin-crates/core/src/engine/variables/affine_view.rs index 404184e57..0f7bd070c 100644 --- a/pumpkin-crates/core/src/engine/variables/affine_view.rs +++ b/pumpkin-crates/core/src/engine/variables/affine_view.rs @@ -14,6 +14,9 @@ use crate::engine::predicates::predicate_constructor::PredicateConstructor; use crate::engine::variables::DomainId; use crate::engine::variables::IntegerVariable; use crate::math::num_ext::NumExt; +use crate::propagation::checkers::SingleVariableAssignment; +use crate::propagation::checkers::ValueToWitness; +use crate::propagation::checkers::WitnessedVariable; /// Models the constraint `y = ax + b`, by expressing the domain of `y` as a transformation of the /// domain of `x`. @@ -406,6 +409,20 @@ enum Rounding { Down, } +impl WitnessedVariable for AffineView { + fn unpack_value(&self, value: ValueToWitness) -> i32 { + let inner_value = self.inner.unpack_value(value); + + self.map(inner_value) + } + + fn assign(&self, value: i32) -> SingleVariableAssignment { + assert_eq!((value - self.offset) % self.scale, 0); + let inner_assignment = (value - self.offset) / self.scale; + self.inner.assign(inner_assignment) + } +} + #[cfg(test)] mod tests { use super::*; diff --git a/pumpkin-crates/core/src/engine/variables/domain_id.rs b/pumpkin-crates/core/src/engine/variables/domain_id.rs index 556d46052..988b88558 100644 --- a/pumpkin-crates/core/src/engine/variables/domain_id.rs +++ b/pumpkin-crates/core/src/engine/variables/domain_id.rs @@ -10,6 +10,9 @@ use crate::engine::notifications::Watchers; use crate::engine::variables::AffineView; use crate::engine::variables::IntegerVariable; use crate::predicates::Predicate; +use crate::propagation::checkers::SingleVariableAssignment; +use crate::propagation::checkers::ValueToWitness; +use crate::propagation::checkers::WitnessedVariable; use crate::pumpkin_assert_simple; /// A structure which represents the most basic [`IntegerVariable`]; it is simply the id which links @@ -191,6 +194,16 @@ impl TransformableVariable> for DomainId { } } +impl WitnessedVariable for DomainId { + fn unpack_value(&self, value: ValueToWitness) -> i32 { + value.unpack() + } + + fn assign(&self, value: i32) -> SingleVariableAssignment { + SingleVariableAssignment::new(*self, value) + } +} + impl StorageKey for DomainId { fn index(&self) -> usize { self.id as usize diff --git a/pumpkin-crates/core/src/engine/variables/integer_variable.rs b/pumpkin-crates/core/src/engine/variables/integer_variable.rs index 09badb92e..851294fb8 100644 --- a/pumpkin-crates/core/src/engine/variables/integer_variable.rs +++ b/pumpkin-crates/core/src/engine/variables/integer_variable.rs @@ -10,6 +10,7 @@ use crate::engine::notifications::OpaqueDomainEvent; use crate::engine::notifications::Watchers; use crate::engine::predicates::predicate_constructor::PredicateConstructor; use crate::predicates::Predicate; +use crate::propagation::checkers::WitnessedVariable; /// A trait specifying the required behaviour of an integer variable such as retrieving a /// lower-bound ([`IntegerVariable::lower_bound`]). @@ -19,6 +20,7 @@ pub trait IntegerVariable: + TransformableVariable + Debug + CheckerVariable + + WitnessedVariable { type AffineView: IntegerVariable; diff --git a/pumpkin-crates/core/src/engine/variables/literal.rs b/pumpkin-crates/core/src/engine/variables/literal.rs index 980ffa737..be99195f0 100644 --- a/pumpkin-crates/core/src/engine/variables/literal.rs +++ b/pumpkin-crates/core/src/engine/variables/literal.rs @@ -15,6 +15,8 @@ use crate::engine::notifications::Watchers; use crate::engine::predicates::predicate::Predicate; use crate::engine::predicates::predicate_constructor::PredicateConstructor; use crate::engine::variables::AffineView; +use crate::propagation::checkers::ValueToWitness; +use crate::propagation::checkers::WitnessedVariable; #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub struct Literal { @@ -222,3 +224,13 @@ impl TransformableVariable> for Literal { AffineView::new(*self, 1, offset) } } + +impl WitnessedVariable for Literal { + fn unpack_value(&self, value: ValueToWitness) -> i32 { + self.integer_variable.unpack_value(value) + } + + fn assign(&self, value: i32) -> crate::propagation::checkers::SingleVariableAssignment { + self.integer_variable.assign(value) + } +} diff --git a/pumpkin-crates/core/src/propagation/checkers/consistency_checker.rs b/pumpkin-crates/core/src/propagation/checkers/consistency_checker.rs new file mode 100644 index 000000000..3d60eb501 --- /dev/null +++ b/pumpkin-crates/core/src/propagation/checkers/consistency_checker.rs @@ -0,0 +1,39 @@ +use std::fmt::Debug; + +use dyn_clone::DynClone; + +use crate::propagation::Domains; +use crate::propagation::checkers::Scope; + +/// A consistency checker ensures that a propagator is at a certain level of consistency. +/// +/// Given a current set of domains and a scope, the checker identifies whether the desired +/// consistency level is reached. +pub trait ConsistencyChecker: Debug + DynClone { + /// Returns `true` if the variables in `scope` are at the required consistency in + /// `domains`. + fn check_consistency(&self, domains: Domains<'_>, scope: &Scope) -> bool; +} + +/// Wrapper around `Box` that implements [`Clone`]. +#[derive(Debug)] +pub struct BoxedConsistencyChecker(Box); + +impl Clone for BoxedConsistencyChecker { + fn clone(&self) -> Self { + BoxedConsistencyChecker(dyn_clone::clone_box(&*self.0)) + } +} + +impl From> for BoxedConsistencyChecker { + fn from(value: Box) -> Self { + BoxedConsistencyChecker(value) + } +} + +impl BoxedConsistencyChecker { + /// See [`ConsistencyChecker::check_consistency`]. + pub fn check_consistency(&self, domains: Domains<'_>, scope: &Scope) -> bool { + self.0.check_consistency(domains, scope) + } +} diff --git a/pumpkin-crates/core/src/propagation/checkers/domain_consistency_checker.rs b/pumpkin-crates/core/src/propagation/checkers/domain_consistency_checker.rs new file mode 100644 index 000000000..27e8d46cb --- /dev/null +++ b/pumpkin-crates/core/src/propagation/checkers/domain_consistency_checker.rs @@ -0,0 +1,90 @@ +use pumpkin_checking::InferenceChecker; +use pumpkin_checking::VariableState; + +use crate::containers::HashMap; +use crate::predicate; +use crate::predicates::Predicate; +use crate::propagation::Domains; +use crate::propagation::ReadDomains; +use crate::propagation::checkers::ConsistencyChecker; +use crate::propagation::checkers::Scope; +use crate::propagation::checkers::Witness; +use crate::propagation::checkers::WitnessGenerator; + +#[derive(Clone, Debug)] +pub struct DomainConsistencyChecker { + witness_generator: C, +} + +impl DomainConsistencyChecker { + pub fn new(witness_generator: C) -> Self { + DomainConsistencyChecker { witness_generator } + } +} + +impl> DomainConsistencyChecker { + /// Validate that the witness is a valid solution. + fn validate_witness(&self, witness: &Witness) -> bool { + let premises = witness + .iter() + .map(|(domain, value)| predicate![domain == value]) + .collect::>(); + + let state = VariableState::prepare_for_conflict_check(premises.clone(), None) + .expect("the witness is consistent by construction"); + + let state_is_conflicting = self.witness_generator.check(state, &premises, None); + + !state_is_conflicting + } +} + +impl ConsistencyChecker for DomainConsistencyChecker +where + C: WitnessGenerator + InferenceChecker + Clone, +{ + fn check_consistency(&self, domains: Domains<'_>, scope: &Scope) -> bool { + // A propagator is domain consistent if all values for all variables participate in + // at least one solution to the constraint. + + let mut supported_values = HashMap::new(); + + for (local_id, domain_id) in scope.iter() { + let supported_values_in_domain: Vec<_> = + std::mem::take(supported_values.entry(domain_id).or_default()); + + for value in domains.iterate_domain(&domain_id) { + if supported_values_in_domain.contains(&value) { + // If the value is already supported, no need to generate a witness + // for it. + continue; + } + + let witness = self.witness_generator.support(local_id, value.into()); + + assert_eq!( + Some(value), + witness.value_for(domain_id), + "the witness for a variable assignment must contain that variable assignment" + ); + + assert!( + self.validate_witness(&witness), + "witness should satisfy the constraint" + ); + + // Add all the assigned variables as supported values as well. + for (witness_domain_id, witness_value) in witness.iter() { + let supports = supported_values.entry(witness_domain_id).or_default(); + supports.push(witness_value); + } + } + + let _ = supported_values + .insert(domain_id, supported_values_in_domain) + .expect("a element was inserted at the beginning of the loop"); + } + + true + } +} diff --git a/pumpkin-crates/core/src/propagation/checkers/mod.rs b/pumpkin-crates/core/src/propagation/checkers/mod.rs new file mode 100644 index 000000000..591697dd0 --- /dev/null +++ b/pumpkin-crates/core/src/propagation/checkers/mod.rs @@ -0,0 +1,27 @@ +mod consistency_checker; +mod domain_consistency_checker; +mod scope; +mod variable; +mod witness; +mod witness_generator; + +pub use consistency_checker::*; +pub use domain_consistency_checker::*; +pub use scope::*; +pub use variable::*; +pub use witness::*; +pub use witness_generator::*; + +use crate::propagation::Domains; + +#[deprecated = "only here to aid refactoring"] +#[doc(hidden)] +#[derive(Clone, Copy, Debug)] +pub struct DefaultChecker; + +#[allow(deprecated, reason = "only here to aid refactoring")] +impl ConsistencyChecker for DefaultChecker { + fn check_consistency(&self, _: Domains<'_>, _: &Scope) -> bool { + true + } +} diff --git a/pumpkin-crates/core/src/propagation/checkers/scope.rs b/pumpkin-crates/core/src/propagation/checkers/scope.rs new file mode 100644 index 000000000..748cf1ff4 --- /dev/null +++ b/pumpkin-crates/core/src/propagation/checkers/scope.rs @@ -0,0 +1,30 @@ +use crate::propagation::LocalId; +use crate::variables::DomainId; + +/// The scope of a propagator consists of the variables the propagator reasons over. +#[derive(Clone, Debug)] +pub struct Scope(Vec<(LocalId, DomainId)>); + +impl Scope { + /// Iterate over all domains in the scope. + /// + /// For each [`DomainId`] this indicates the [`LocalId`] that the domain is registered as. + /// It can happen that a propagator registers the same [`DomainId`] for different + /// [`LocalId`]s. + pub fn iter(&self) -> impl ExactSizeIterator { + self.0.iter().copied() + } +} + +#[derive(Clone, Debug, Default)] +pub struct ScopeBuilder(Vec<(LocalId, DomainId)>); + +impl ScopeBuilder { + pub fn add(&mut self, local_id: LocalId, domain_id: DomainId) { + self.0.push((local_id, domain_id)); + } + + pub fn build(self) -> Scope { + Scope(self.0) + } +} diff --git a/pumpkin-crates/core/src/propagation/checkers/variable.rs b/pumpkin-crates/core/src/propagation/checkers/variable.rs new file mode 100644 index 000000000..29f3ac25d --- /dev/null +++ b/pumpkin-crates/core/src/propagation/checkers/variable.rs @@ -0,0 +1,35 @@ +use crate::propagation::checkers::SingleVariableAssignment; +#[cfg(doc)] +use crate::propagation::checkers::Witness; + +/// A variable that can be part of a [`Witness`]. +pub trait WitnessedVariable { + /// Convert a [`ValueToWitness`] to an integer. + /// + /// See the documentation for [`ValueToWitness`] for why this abstraction is necessary. + fn unpack_value(&self, value: ValueToWitness) -> i32; + + /// Create a [`SingleVariableAssignment`] representing `self = value`. + fn assign(&self, value: i32) -> SingleVariableAssignment; +} + +/// Models a value that needs to be unpacked by a [`WitnessedVariable`]. +/// +/// Since propagators (and by extension, propagation checkers) will often use views to abstract +/// over the variable type, it is difficult to relate the domain_id to the logical variable in the +/// propagator or checker. This is why the [`ValueToWitness`] exists, as it allows the view to map +/// the value according to the view implementation. +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct ValueToWitness(i32); + +impl From for ValueToWitness { + fn from(value: i32) -> Self { + ValueToWitness(value) + } +} + +impl ValueToWitness { + pub(crate) fn unpack(&self) -> i32 { + self.0 + } +} diff --git a/pumpkin-crates/core/src/propagation/checkers/witness.rs b/pumpkin-crates/core/src/propagation/checkers/witness.rs new file mode 100644 index 000000000..957265911 --- /dev/null +++ b/pumpkin-crates/core/src/propagation/checkers/witness.rs @@ -0,0 +1,44 @@ +use crate::containers::HashMap; +use crate::variables::DomainId; + +/// A light-weight variable assignment used during propagation checking. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct Witness(HashMap); + +impl Witness { + /// Create a new [`Witness`] from the given `assignments`. + pub fn new(assignments: impl IntoIterator) -> Witness { + Witness( + assignments + .into_iter() + .map(|assignment| (assignment.domain_id, assignment.value)) + .collect(), + ) + } + + /// Get the value for the given [`DomainId`] in the witness. + /// + /// If the domain is not part of the witness, [`None`] is returned. + pub fn value_for(&self, domain_id: DomainId) -> Option { + self.0.get(&domain_id).copied() + } + + /// Iterate over all assigned domains. + pub fn iter(&self) -> impl ExactSizeIterator { + self.0.iter().map(|(key, value)| (*key, *value)) + } +} + +/// Models an assignment of `variable = value`. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub struct SingleVariableAssignment { + domain_id: DomainId, + value: i32, +} + +impl SingleVariableAssignment { + /// Create a new assignment. + pub fn new(domain_id: DomainId, value: i32) -> SingleVariableAssignment { + SingleVariableAssignment { domain_id, value } + } +} diff --git a/pumpkin-crates/core/src/propagation/checkers/witness_generator.rs b/pumpkin-crates/core/src/propagation/checkers/witness_generator.rs new file mode 100644 index 000000000..310840e0b --- /dev/null +++ b/pumpkin-crates/core/src/propagation/checkers/witness_generator.rs @@ -0,0 +1,16 @@ +use crate::propagation::LocalId; +use crate::propagation::checkers::ValueToWitness; +use crate::propagation::checkers::Witness; +#[cfg(doc)] +use crate::propagation::checkers::WitnessedVariable; + +/// A witness generator is responsible for constructing witness that a variable can be assigned a +/// value. The created witnesses should be solutions to a single constraint. The solutions are then +/// used by consistency checkers to determine whether propagators are at their claimed level of +/// consistency. +pub trait WitnessGenerator { + /// Create a [`Witness`] such that the variable identified by `local_id` is assigned to `value`. + /// + /// Use [`WitnessedVariable::unpack_value`] to convert the [`ValueToWitness`] to an `i32`. + fn support(&self, local_id: LocalId, value: ValueToWitness) -> Witness; +} diff --git a/pumpkin-crates/core/src/propagation/constructor.rs b/pumpkin-crates/core/src/propagation/constructor.rs index 791627880..cead8ddf8 100644 --- a/pumpkin-crates/core/src/propagation/constructor.rs +++ b/pumpkin-crates/core/src/propagation/constructor.rs @@ -25,6 +25,10 @@ use crate::proof::InferenceCode; #[cfg(doc)] use crate::propagation::DomainEvent; use crate::propagation::DomainEvents; +use crate::propagation::checkers::ConsistencyChecker; +#[allow(deprecated, reason = "TODO to implement for reified")] +use crate::propagation::checkers::DefaultChecker; +use crate::propagation::checkers::ScopeBuilder; use crate::propagators::reified_propagator::ReifiedChecker; use crate::variables::IntegerVariable; use crate::variables::Literal; @@ -45,7 +49,13 @@ pub trait PropagatorConstructor { /// to verify the propagations done by this propagator are correct. /// /// See [`InferenceChecker`] for more information. - fn add_inference_checkers(&self, _checkers: InferenceCheckers<'_>) {} + fn add_inference_checkers( + &self, + _checkers: InferenceCheckers<'_>, + ) -> impl ConsistencyChecker + 'static { + #[allow(deprecated, reason = "TODO to implement for reified")] + DefaultChecker + } /// Create the propagator instance from `Self`. fn create(self, context: PropagatorConstructorContext) -> Self::PropagatorImpl; @@ -102,6 +112,9 @@ pub struct PropagatorConstructorContext<'a> { state: &'a mut State, pub(crate) propagator_id: PropagatorId, + /// The scope of the propagator that is being accumulated. + scope_builder: RefOrOwned<'a, ScopeBuilder>, + /// A [`LocalId`] that is guaranteed not to be used to register any variables yet. This is /// either a reference or an owned value, to support /// [`PropagatorConstructorContext::reborrow`]. @@ -122,6 +135,7 @@ impl PropagatorConstructorContext<'_> { propagator_id, state, did_register: RefOrOwned::Owned(false), + scope_builder: RefOrOwned::Owned(ScopeBuilder::default()), } } @@ -166,6 +180,10 @@ impl PropagatorConstructorContext<'_> { let mut watchers = Watchers::new(propagator_var, &mut self.state.notification_engine); var.watch_all(&mut watchers, domain_events.events()); + + // This is a bit hacky to get the domain, but it works for now. + let domain_id = crate::predicate![var == 1].get_domain(); + self.scope_builder.add(local_id, domain_id); } /// Register the propagator to be enqueued when the given [`Predicate`] becomes true. @@ -225,6 +243,7 @@ impl PropagatorConstructorContext<'_> { next_local_id: self.next_local_id.reborrow(), did_register: self.did_register.reborrow(), state: self.state, + scope_builder: self.scope_builder.reborrow(), } } diff --git a/pumpkin-crates/core/src/propagation/mod.rs b/pumpkin-crates/core/src/propagation/mod.rs index 7c4b5b02b..d288501f3 100644 --- a/pumpkin-crates/core/src/propagation/mod.rs +++ b/pumpkin-crates/core/src/propagation/mod.rs @@ -72,6 +72,8 @@ mod domains; mod local_id; mod propagator; +pub mod checkers; + pub(crate) mod propagator_id; pub(crate) mod propagator_var_id; pub(crate) mod store; diff --git a/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs b/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs index 8cab794e6..f7d5d4277 100644 --- a/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs +++ b/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs @@ -13,6 +13,9 @@ use crate::propagation::Propagator; use crate::propagation::PropagatorConstructor; use crate::propagation::PropagatorConstructorContext; use crate::propagation::ReadDomains; +use crate::propagation::checkers::ConsistencyChecker; +#[allow(deprecated, reason = "TODO to implement for reified")] +use crate::propagation::checkers::DefaultChecker; use crate::propagators::hypercube_linear::Hypercube; use crate::propagators::hypercube_linear::HypercubeLinearChecker; use crate::propagators::hypercube_linear::LinearInequality; @@ -33,7 +36,10 @@ pub struct HypercubeLinearConstructor { impl PropagatorConstructor for HypercubeLinearConstructor { type PropagatorImpl = HypercubeLinearPropagator; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { + fn add_inference_checkers( + &self, + mut checkers: InferenceCheckers<'_>, + ) -> impl ConsistencyChecker + 'static { checkers.add_inference_checker( InferenceCode::new(self.constraint_tag, HypercubeLinear), Box::new(HypercubeLinearChecker { @@ -42,6 +48,9 @@ impl PropagatorConstructor for HypercubeLinearConstructor { bound: self.linear.bound(), }), ); + + #[allow(deprecated, reason = "TODO to implement for reified")] + DefaultChecker } fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { diff --git a/pumpkin-crates/core/src/propagators/reified_propagator.rs b/pumpkin-crates/core/src/propagators/reified_propagator.rs index b0411158b..2d4f53fa6 100644 --- a/pumpkin-crates/core/src/propagators/reified_propagator.rs +++ b/pumpkin-crates/core/src/propagators/reified_propagator.rs @@ -19,6 +19,7 @@ use crate::propagation::Propagator; use crate::propagation::PropagatorConstructor; use crate::propagation::PropagatorConstructorContext; use crate::propagation::ReadDomains; +use crate::propagation::checkers::ConsistencyChecker; use crate::pumpkin_assert_simple; use crate::state::Conflict; use crate::variables::Literal; @@ -63,10 +64,17 @@ where } } - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { + fn add_inference_checkers( + &self, + mut checkers: InferenceCheckers<'_>, + ) -> impl ConsistencyChecker + 'static { checkers.with_reification_literal(self.reification_literal); - self.propagator.add_inference_checkers(checkers); + // TODO: Handle consistency check in reified propagators. + let _ = self.propagator.add_inference_checkers(checkers); + + #[allow(deprecated, reason = "TODO to implement for reified")] + crate::propagation::checkers::DefaultChecker } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs index 95b6e334a..808fd29b7 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs @@ -16,6 +16,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::checkers::ConsistencyChecker; use pumpkin_core::results::PropagationStatusCP; use pumpkin_core::variables::IntegerVariable; @@ -35,7 +36,10 @@ where { type PropagatorImpl = AbsoluteValuePropagator; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { + fn add_inference_checkers( + &self, + mut checkers: InferenceCheckers<'_>, + ) -> impl ConsistencyChecker + 'static { checkers.add_inference_checker( InferenceCode::new(self.constraint_tag, AbsoluteValue), Box::new(AbsoluteValueChecker { @@ -43,6 +47,9 @@ where absolute: self.absolute.clone(), }), ); + + #[allow(deprecated, reason = "TODO to implement for reified")] + pumpkin_core::propagation::checkers::DefaultChecker } fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs index 7241fd3ae..1dbaadc73 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs @@ -31,6 +31,12 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::checkers::ConsistencyChecker; +use pumpkin_core::propagation::checkers::DomainConsistencyChecker; +use pumpkin_core::propagation::checkers::ValueToWitness; +use pumpkin_core::propagation::checkers::Witness; +use pumpkin_core::propagation::checkers::WitnessGenerator; +use pumpkin_core::propagation::checkers::WitnessedVariable; use pumpkin_core::results::PropagationStatusCP; use pumpkin_core::state::EmptyDomainConflict; use pumpkin_core::state::PropagatorConflict; @@ -53,7 +59,10 @@ where { type PropagatorImpl = BinaryEqualsPropagator; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { + fn add_inference_checkers( + &self, + mut checkers: InferenceCheckers<'_>, + ) -> impl ConsistencyChecker + 'static { checkers.add_inference_checker( InferenceCode::new(self.constraint_tag, BinaryEquals), Box::new(BinaryEqualsChecker { @@ -61,6 +70,11 @@ where rhs: self.b.clone(), }), ); + + DomainConsistencyChecker::new(BinaryEqualsChecker { + lhs: self.a.clone(), + rhs: self.b.clone(), + }) } fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { @@ -439,6 +453,24 @@ where } } +impl WitnessGenerator + for BinaryEqualsChecker +{ + fn support(&self, local_id: LocalId, value: ValueToWitness) -> Witness { + match local_id.unpack() { + 0 => { + let value = self.lhs.unpack_value(value); + Witness::new([self.lhs.assign(value), self.rhs.assign(value)]) + } + 1 => { + let value = self.lhs.unpack_value(value); + Witness::new([self.lhs.assign(value), self.rhs.assign(value)]) + } + _ => unreachable!("Binary equals does not register variables with ID {local_id}"), + } + } +} + #[allow(deprecated, reason = "Will be refactored")] #[cfg(test)] mod tests { diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs index efe6d8768..c3322d970 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs @@ -16,6 +16,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::checkers::ConsistencyChecker; use pumpkin_core::results::PropagationStatusCP; use pumpkin_core::state::PropagatorConflict; use pumpkin_core::variables::IntegerVariable; @@ -37,7 +38,10 @@ where { type PropagatorImpl = BinaryNotEqualsPropagator; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { + fn add_inference_checkers( + &self, + mut checkers: InferenceCheckers<'_>, + ) -> impl ConsistencyChecker + 'static { checkers.add_inference_checker( InferenceCode::new(self.constraint_tag, BinaryNotEquals), Box::new(BinaryNotEqualsChecker { @@ -45,6 +49,9 @@ where rhs: self.b.clone(), }), ); + + #[allow(deprecated, reason = "TODO to implement for reified")] + pumpkin_core::propagation::checkers::DefaultChecker } fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs index 526f1511c..22c9d1c79 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs @@ -17,6 +17,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::checkers::ConsistencyChecker; use pumpkin_core::results::PropagationStatusCP; use pumpkin_core::variables::IntegerVariable; @@ -70,7 +71,10 @@ where } } - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { + fn add_inference_checkers( + &self, + mut checkers: InferenceCheckers<'_>, + ) -> impl ConsistencyChecker + 'static { checkers.add_inference_checker( InferenceCode::new(self.constraint_tag, Division), Box::new(IntegerDivisionChecker { @@ -79,6 +83,9 @@ where rhs: self.rhs.clone(), }), ); + + #[allow(deprecated, reason = "TODO to implement for reified")] + pumpkin_core::propagation::checkers::DefaultChecker } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs index 79dd4de68..52f654505 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs @@ -16,6 +16,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::checkers::ConsistencyChecker; use pumpkin_core::results::PropagationStatusCP; use pumpkin_core::state::PropagatorConflict; use pumpkin_core::variables::IntegerVariable; @@ -39,7 +40,10 @@ where { type PropagatorImpl = IntegerMultiplicationPropagator; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { + fn add_inference_checkers( + &self, + mut checkers: InferenceCheckers<'_>, + ) -> impl ConsistencyChecker + 'static { checkers.add_inference_checker( InferenceCode::new(self.constraint_tag, IntegerMultiplication), Box::new(IntegerMultiplicationChecker { @@ -48,6 +52,9 @@ where c: self.c.clone(), }), ); + + #[allow(deprecated, reason = "TODO to implement for reified")] + pumpkin_core::propagation::checkers::DefaultChecker } fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs index e1e616574..4f91edd66 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs @@ -25,6 +25,7 @@ use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::propagation::TrailedInteger; +use pumpkin_core::propagation::checkers::ConsistencyChecker; use pumpkin_core::results::PropagationStatusCP; use pumpkin_core::state::PropagatorConflict; use pumpkin_core::variables::IntegerVariable; @@ -45,7 +46,10 @@ where { type PropagatorImpl = LinearLessOrEqualPropagator; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { + fn add_inference_checkers( + &self, + mut checkers: InferenceCheckers<'_>, + ) -> impl ConsistencyChecker + 'static { checkers.add_inference_checker( InferenceCode::new(self.constraint_tag, LinearBounds), Box::new(LinearLessOrEqualInferenceChecker::new( @@ -53,6 +57,9 @@ where self.c, )), ); + + #[allow(deprecated, reason = "TODO to implement for reified")] + pumpkin_core::propagation::checkers::DefaultChecker } fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs index 31f8a96e3..427f2df26 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs @@ -28,6 +28,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::checkers::ConsistencyChecker; use pumpkin_core::results::PropagationStatusCP; use pumpkin_core::state::PropagatorConflict; use pumpkin_core::variables::IntegerVariable; @@ -50,7 +51,10 @@ where { type PropagatorImpl = LinearNotEqualPropagator; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { + fn add_inference_checkers( + &self, + mut checkers: InferenceCheckers<'_>, + ) -> impl ConsistencyChecker + 'static { checkers.add_inference_checker( InferenceCode::new(self.constraint_tag, LinearNotEquals), Box::new(LinearNotEqualChecker { @@ -58,6 +62,9 @@ where bound: self.rhs, }), ); + + #[allow(deprecated, reason = "TODO to implement for reified")] + pumpkin_core::propagation::checkers::DefaultChecker } fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs index d1f927697..7e843a58c 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs @@ -17,6 +17,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::checkers::ConsistencyChecker; use pumpkin_core::results::PropagationStatusCP; use pumpkin_core::variables::IntegerVariable; @@ -36,7 +37,10 @@ where { type PropagatorImpl = MaximumPropagator; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { + fn add_inference_checkers( + &self, + mut checkers: InferenceCheckers<'_>, + ) -> impl ConsistencyChecker + 'static { checkers.add_inference_checker( InferenceCode::new(self.constraint_tag, Maximum), Box::new(MaximumChecker { @@ -44,6 +48,9 @@ where rhs: self.rhs.clone(), }), ); + + #[allow(deprecated, reason = "TODO to implement for reified")] + pumpkin_core::propagation::checkers::DefaultChecker } fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs index 07e5b8cb2..0df0ad3a2 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs @@ -20,6 +20,7 @@ use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::checkers::ConsistencyChecker; use pumpkin_core::results::PropagationStatusCP; use pumpkin_core::state::Conflict; use pumpkin_core::state::PropagatorConflict; @@ -111,7 +112,10 @@ impl PropagatorConstruc { type PropagatorImpl = Self; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { + fn add_inference_checkers( + &self, + mut checkers: InferenceCheckers<'_>, + ) -> impl ConsistencyChecker + 'static { checkers.add_inference_checker( InferenceCode::new(self.constraint_tag, TimeTable), Box::new(TimeTableChecker { @@ -128,6 +132,9 @@ impl PropagatorConstruc capacity: self.parameters.capacity, }), ); + + #[allow(deprecated, reason = "TODO to implement for reified")] + pumpkin_core::propagation::checkers::DefaultChecker } fn create(mut self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs index 3ab30639d..f5c08f547 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs @@ -20,6 +20,7 @@ use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::checkers::ConsistencyChecker; use pumpkin_core::results::PropagationStatusCP; use pumpkin_core::state::Conflict; use pumpkin_core::state::PropagatorConflict; @@ -108,7 +109,10 @@ impl Propagator { type PropagatorImpl = Self; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { + fn add_inference_checkers( + &self, + mut checkers: InferenceCheckers<'_>, + ) -> impl ConsistencyChecker + 'static { checkers.add_inference_checker( InferenceCode::new(self.constraint_tag, TimeTable), Box::new(TimeTableChecker { @@ -125,6 +129,9 @@ impl Propagator capacity: self.parameters.capacity, }), ); + + #[allow(deprecated, reason = "TODO to implement for reified")] + pumpkin_core::propagation::checkers::DefaultChecker } fn create(mut self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs index 3d3640783..7cc3ad6a6 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs @@ -19,6 +19,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::checkers::ConsistencyChecker; use pumpkin_core::results::PropagationStatusCP; use pumpkin_core::state::Conflict; use pumpkin_core::state::PropagatorConflict; @@ -110,7 +111,10 @@ impl PropagatorConstructor { type PropagatorImpl = Self; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { + fn add_inference_checkers( + &self, + mut checkers: InferenceCheckers<'_>, + ) -> impl ConsistencyChecker + 'static { checkers.add_inference_checker( InferenceCode::new(self.constraint_tag, TimeTable), Box::new(TimeTableChecker { @@ -127,6 +131,8 @@ impl PropagatorConstructor capacity: self.parameters.capacity, }), ); + #[allow(deprecated, reason = "TODO to implement for reified")] + pumpkin_core::propagation::checkers::DefaultChecker } fn create(mut self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs index 2b26a43b2..3fe356511 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs @@ -21,6 +21,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::checkers::ConsistencyChecker; use pumpkin_core::results::PropagationStatusCP; use pumpkin_core::state::Conflict; use pumpkin_core::state::PropagatorConflict; @@ -100,7 +101,10 @@ impl TimeTablePerPointPropagator { impl PropagatorConstructor for TimeTablePerPointPropagator { type PropagatorImpl = Self; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { + fn add_inference_checkers( + &self, + mut checkers: InferenceCheckers<'_>, + ) -> impl ConsistencyChecker + 'static { checkers.add_inference_checker( InferenceCode::new(self.constraint_tag, TimeTable), Box::new(TimeTableChecker { @@ -117,6 +121,9 @@ impl PropagatorConstructor for TimeTablePerPoint capacity: self.parameters.capacity, }), ); + + #[allow(deprecated, reason = "TODO to implement for reified")] + pumpkin_core::propagation::checkers::DefaultChecker } fn create(mut self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { diff --git a/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs b/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs index 8799b938c..f2c0a6d32 100644 --- a/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs +++ b/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs @@ -15,6 +15,9 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::checkers::ConsistencyChecker; +#[allow(deprecated, reason = "TODO to implement for reified")] +use pumpkin_core::propagation::checkers::DefaultChecker; use pumpkin_core::results::PropagationStatusCP; use pumpkin_core::state::Conflict; use pumpkin_core::state::PropagatorConflict; @@ -108,7 +111,10 @@ impl PropagatorConstructor for DisjunctiveConstr } } - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { + fn add_inference_checkers( + &self, + mut checkers: InferenceCheckers<'_>, + ) -> impl ConsistencyChecker + 'static { checkers.add_inference_checker( InferenceCode::new(self.constraint_tag, DisjunctiveEdgeFinding), Box::new(DisjunctiveEdgeFindingChecker { @@ -122,6 +128,9 @@ impl PropagatorConstructor for DisjunctiveConstr .collect(), }), ); + + #[allow(deprecated, reason = "TODO to implement for reified")] + DefaultChecker } } diff --git a/pumpkin-crates/propagators/src/propagators/element.rs b/pumpkin-crates/propagators/src/propagators/element.rs index c401eb847..63341633d 100644 --- a/pumpkin-crates/propagators/src/propagators/element.rs +++ b/pumpkin-crates/propagators/src/propagators/element.rs @@ -26,6 +26,9 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::checkers::ConsistencyChecker; +#[allow(deprecated, reason = "TODO to implement for reified")] +use pumpkin_core::propagation::checkers::DefaultChecker; use pumpkin_core::results::PropagationStatusCP; use pumpkin_core::variables::IntegerVariable; use pumpkin_core::variables::Reason; @@ -48,7 +51,10 @@ where { type PropagatorImpl = ElementPropagator; - fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) { + fn add_inference_checkers( + &self, + mut checkers: InferenceCheckers<'_>, + ) -> impl ConsistencyChecker + 'static { checkers.add_inference_checker( InferenceCode::new(self.constraint_tag, Element), Box::new(ElementChecker::new( @@ -57,6 +63,9 @@ where self.rhs.clone(), )), ); + + #[allow(deprecated, reason = "TODO to implement for reified")] + DefaultChecker } fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { From aacd712758754c41afb5c43f5717c8abc99b8726 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Fri, 27 Feb 2026 15:30:05 +1100 Subject: [PATCH 02/10] Run the consistency checkers when enabled --- .../core/src/engine/notifications/mod.rs | 19 +++++++++++++++ pumpkin-crates/core/src/engine/state.rs | 23 +++++++++++++++++++ .../core/src/propagation/constructor.rs | 7 ++++++ 3 files changed, 49 insertions(+) diff --git a/pumpkin-crates/core/src/engine/notifications/mod.rs b/pumpkin-crates/core/src/engine/notifications/mod.rs index ba6a5e64e..b60230896 100644 --- a/pumpkin-crates/core/src/engine/notifications/mod.rs +++ b/pumpkin-crates/core/src/engine/notifications/mod.rs @@ -11,6 +11,8 @@ use enumset::EnumSet; pub(crate) use predicate_notification::PredicateNotifier; use crate::basic_types::PredicateId; +#[cfg(feature = "check-propagations")] +use crate::containers::HashSet; use crate::containers::KeyedVec; use crate::engine::Assignments; use crate::engine::PropagatorQueue; @@ -43,6 +45,10 @@ pub(crate) struct NotificationEngine { /// Backtrack events which have occurred since the last of backtrack notifications have taken /// place backtrack_events: EventSink, + /// All the propagators that have been notified since the last call to + /// [`Self::drain_notified_propagators`]. + #[cfg(feature = "check-propagations")] + notified_propagators: HashSet, } impl Default for NotificationEngine { @@ -54,6 +60,8 @@ impl Default for NotificationEngine { last_notified_trail_index: 0, events: Default::default(), backtrack_events: Default::default(), + #[cfg(feature = "check-propagations")] + notified_propagators: Default::default(), }; // Grow for the dummy predicate result.grow(); @@ -77,6 +85,8 @@ impl NotificationEngine { last_notified_trail_index: usize::MAX, events: Default::default(), backtrack_events: Default::default(), + #[cfg(feature = "check-propagations")] + notified_propagators: Default::default(), }; // Grow for the dummy predicate result.grow(); @@ -333,6 +343,9 @@ impl NotificationEngine { assignments, trailed_values, ); + + #[cfg(feature = "check-propagations")] + let _ = self.notified_propagators.insert(propagator_id); } } @@ -579,4 +592,10 @@ impl NotificationEngine { .predicate_id_assignments .synchronise(backtrack_level) } + + /// Get all propagagators that have been notified since the previous call to this function. + #[cfg(feature = "check-propagations")] + pub(crate) fn drain_notified_propagators(&mut self) -> impl Iterator { + self.notified_propagators.drain() + } } diff --git a/pumpkin-crates/core/src/engine/state.rs b/pumpkin-crates/core/src/engine/state.rs index ff8ce9f87..7e650766c 100644 --- a/pumpkin-crates/core/src/engine/state.rs +++ b/pumpkin-crates/core/src/engine/state.rs @@ -41,6 +41,8 @@ use crate::propagation::PropagatorConstructorContext; use crate::propagation::PropagatorId; #[cfg(feature = "check-propagations")] use crate::propagation::checkers::BoxedConsistencyChecker; +#[cfg(feature = "check-propagations")] +use crate::propagation::checkers::Scope; use crate::propagation::store::PropagatorStore; use crate::pumpkin_assert_advanced; use crate::pumpkin_assert_eq_simple; @@ -85,6 +87,9 @@ pub struct State { /// Inference checkers to run in the propagation loop. checkers: HashMap>>, + /// For every propagator identify what variables are associated with it. + #[cfg(feature = "check-propagations")] + pub(crate) scopes: HashMap, #[cfg(feature = "check-propagations")] consistency_checkers: HashMap, } @@ -182,6 +187,8 @@ impl Default for State { constraint_tags: KeyGenerator::default(), checkers: HashMap::default(), #[cfg(feature = "check-propagations")] + scopes: HashMap::default(), + #[cfg(feature = "check-propagations")] consistency_checkers: HashMap::default(), }; // As a convention, the assignments contain a dummy domain_id=0, which represents a 0-1 @@ -813,6 +820,22 @@ impl State { self.propagate(propagator_id)?; } + #[cfg(feature = "check-propagations")] + for propagator in self.notification_engine.drain_notified_propagators() { + let checker = &self.consistency_checkers[&propagator]; + let scope = &self.scopes[&propagator]; + + let propagator_name = self.propagators[propagator].name(); + + assert!( + checker.check_consistency( + Domains::new(&self.assignments, &mut self.trailed_values), + scope, + ), + "propagator {propagator_name} is not at its reported consistency" + ); + } + // Only check fixed point propagation if there was no reported conflict, // since otherwise the state may be inconsistent. pumpkin_assert_extreme!(DebugHelper::debug_fixed_point_propagation( diff --git a/pumpkin-crates/core/src/propagation/constructor.rs b/pumpkin-crates/core/src/propagation/constructor.rs index cead8ddf8..f20f37ec5 100644 --- a/pumpkin-crates/core/src/propagation/constructor.rs +++ b/pumpkin-crates/core/src/propagation/constructor.rs @@ -286,6 +286,13 @@ impl Drop for PropagatorConstructorContext<'_> { "Propagator did not register to be enqueued. If this is intentional, call PropagatorConstructorContext::will_not_register_any_events()." ); } + + #[cfg(feature = "check-propagations")] + { + // Make sure to register the scope of this propagator with the state. + let scope = std::mem::take(self.scope_builder.deref_mut()).build(); + let _ = self.state.scopes.insert(self.propagator_id, scope); + } } } From ece98c75a420bf247b1027323cfcc119e6ded10f Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Fri, 27 Feb 2026 15:42:31 +1100 Subject: [PATCH 03/10] Implement bound consistency checker --- .../checkers/bound_consistency_checker.rs | 94 +++++++++++++++++++ .../core/src/propagation/checkers/mod.rs | 2 + 2 files changed, 96 insertions(+) create mode 100644 pumpkin-crates/core/src/propagation/checkers/bound_consistency_checker.rs diff --git a/pumpkin-crates/core/src/propagation/checkers/bound_consistency_checker.rs b/pumpkin-crates/core/src/propagation/checkers/bound_consistency_checker.rs new file mode 100644 index 000000000..b5c2e4c41 --- /dev/null +++ b/pumpkin-crates/core/src/propagation/checkers/bound_consistency_checker.rs @@ -0,0 +1,94 @@ +use pumpkin_checking::InferenceChecker; +use pumpkin_checking::VariableState; + +use crate::containers::HashMap; +use crate::predicate; +use crate::predicates::Predicate; +use crate::propagation::Domains; +use crate::propagation::ReadDomains; +use crate::propagation::checkers::ConsistencyChecker; +use crate::propagation::checkers::Scope; +use crate::propagation::checkers::Witness; +use crate::propagation::checkers::WitnessGenerator; + +#[derive(Clone, Debug)] +pub struct BoundConsistencyChecker { + witness_generator: C, +} + +impl BoundConsistencyChecker { + pub fn new(witness_generator: C) -> Self { + BoundConsistencyChecker { witness_generator } + } +} + +impl> BoundConsistencyChecker { + /// Validate that the witness is a valid solution. + fn validate_witness(&self, witness: &Witness) -> bool { + let premises = witness + .iter() + .map(|(domain, value)| predicate![domain == value]) + .collect::>(); + + let state = VariableState::prepare_for_conflict_check(premises.clone(), None) + .expect("the witness is consistent by construction"); + + let state_is_conflicting = self.witness_generator.check(state, &premises, None); + + !state_is_conflicting + } +} + +impl ConsistencyChecker for BoundConsistencyChecker +where + C: WitnessGenerator + InferenceChecker + Clone, +{ + fn check_consistency(&self, domains: Domains<'_>, scope: &Scope) -> bool { + // A propagator is domain consistent if all values for all variables participate in + // at least one solution to the constraint. + + let mut supported_values = HashMap::new(); + + for (local_id, domain_id) in scope.iter() { + let supported_values_in_domain: Vec<_> = + std::mem::take(supported_values.entry(domain_id).or_default()); + + for value in [ + domains.lower_bound(&domain_id), + domains.upper_bound(&domain_id), + ] { + if supported_values_in_domain.contains(&value) { + // If the value is already supported, no need to generate a witness + // for it. + continue; + } + + let witness = self.witness_generator.support(local_id, value.into()); + + assert_eq!( + Some(value), + witness.value_for(domain_id), + "the witness for a variable assignment must contain that variable assignment" + ); + + assert!( + self.validate_witness(&witness), + "witness should satisfy the constraint" + ); + + // Add all the assigned variables as supported values as well. + for (witness_domain_id, witness_value) in witness.iter() { + let supports = supported_values.entry(witness_domain_id).or_default(); + supports.push(witness_value); + } + } + + let dummy = supported_values + .insert(domain_id, supported_values_in_domain) + .expect("a element was inserted at the beginning of the loop"); + assert!(dummy.is_empty(), "no values should be put into the dummy"); + } + + true + } +} diff --git a/pumpkin-crates/core/src/propagation/checkers/mod.rs b/pumpkin-crates/core/src/propagation/checkers/mod.rs index 591697dd0..24239cd0e 100644 --- a/pumpkin-crates/core/src/propagation/checkers/mod.rs +++ b/pumpkin-crates/core/src/propagation/checkers/mod.rs @@ -1,3 +1,4 @@ +mod bound_consistency_checker; mod consistency_checker; mod domain_consistency_checker; mod scope; @@ -5,6 +6,7 @@ mod variable; mod witness; mod witness_generator; +pub use bound_consistency_checker::*; pub use consistency_checker::*; pub use domain_consistency_checker::*; pub use scope::*; From 501352723ede34b22f2a4487a2c01d53ab066e11 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Fri, 27 Feb 2026 15:52:46 +1100 Subject: [PATCH 04/10] Give access to domains in witness generator --- pumpkin-checker/src/inferences/linear.rs | 4 +-- .../checkers/bound_consistency_checker.rs | 9 +++++- .../checkers/domain_consistency_checker.rs | 9 +++++- .../propagation/checkers/witness_generator.rs | 3 +- .../arithmetic/binary/binary_equals.rs | 2 +- .../arithmetic/linear_less_or_equal.rs | 30 ++++++++++++------- 6 files changed, 41 insertions(+), 16 deletions(-) diff --git a/pumpkin-checker/src/inferences/linear.rs b/pumpkin-checker/src/inferences/linear.rs index 4cd522d49..9297af6e2 100644 --- a/pumpkin-checker/src/inferences/linear.rs +++ b/pumpkin-checker/src/inferences/linear.rs @@ -1,6 +1,6 @@ use pumpkin_checking::InferenceChecker; use pumpkin_checking::VariableState; -use pumpkin_propagators::arithmetic::LinearLessOrEqualInferenceChecker; +use pumpkin_propagators::arithmetic::LinearLessOrEqualChecker; use crate::inferences::Fact; use crate::inferences::InvalidInference; @@ -52,7 +52,7 @@ fn verify_linear_inference( fact: &Fact, state: VariableState, ) -> Result<(), InvalidInference> { - let checker = LinearLessOrEqualInferenceChecker::new(linear.terms.clone().into(), linear.bound); + let checker = LinearLessOrEqualChecker::new(linear.terms.clone().into(), linear.bound); if checker.check(state, &fact.premises, fact.consequent.as_ref()) { Ok(()) diff --git a/pumpkin-crates/core/src/propagation/checkers/bound_consistency_checker.rs b/pumpkin-crates/core/src/propagation/checkers/bound_consistency_checker.rs index b5c2e4c41..1575f8f59 100644 --- a/pumpkin-crates/core/src/propagation/checkers/bound_consistency_checker.rs +++ b/pumpkin-crates/core/src/propagation/checkers/bound_consistency_checker.rs @@ -63,7 +63,9 @@ where continue; } - let witness = self.witness_generator.support(local_id, value.into()); + let witness = self + .witness_generator + .support(&domains, local_id, value.into()); assert_eq!( Some(value), @@ -78,6 +80,11 @@ where // Add all the assigned variables as supported values as well. for (witness_domain_id, witness_value) in witness.iter() { + assert!( + domains.contains(&witness_domain_id, witness_value), + "witness uses values outside domain" + ); + let supports = supported_values.entry(witness_domain_id).or_default(); supports.push(witness_value); } diff --git a/pumpkin-crates/core/src/propagation/checkers/domain_consistency_checker.rs b/pumpkin-crates/core/src/propagation/checkers/domain_consistency_checker.rs index 27e8d46cb..3f561dba3 100644 --- a/pumpkin-crates/core/src/propagation/checkers/domain_consistency_checker.rs +++ b/pumpkin-crates/core/src/propagation/checkers/domain_consistency_checker.rs @@ -60,7 +60,9 @@ where continue; } - let witness = self.witness_generator.support(local_id, value.into()); + let witness = self + .witness_generator + .support(&domains, local_id, value.into()); assert_eq!( Some(value), @@ -75,6 +77,11 @@ where // Add all the assigned variables as supported values as well. for (witness_domain_id, witness_value) in witness.iter() { + assert!( + domains.contains(&witness_domain_id, witness_value), + "witness uses values outside domain" + ); + let supports = supported_values.entry(witness_domain_id).or_default(); supports.push(witness_value); } diff --git a/pumpkin-crates/core/src/propagation/checkers/witness_generator.rs b/pumpkin-crates/core/src/propagation/checkers/witness_generator.rs index 310840e0b..02456c6ab 100644 --- a/pumpkin-crates/core/src/propagation/checkers/witness_generator.rs +++ b/pumpkin-crates/core/src/propagation/checkers/witness_generator.rs @@ -1,3 +1,4 @@ +use crate::propagation::Domains; use crate::propagation::LocalId; use crate::propagation::checkers::ValueToWitness; use crate::propagation::checkers::Witness; @@ -12,5 +13,5 @@ pub trait WitnessGenerator { /// Create a [`Witness`] such that the variable identified by `local_id` is assigned to `value`. /// /// Use [`WitnessedVariable::unpack_value`] to convert the [`ValueToWitness`] to an `i32`. - fn support(&self, local_id: LocalId, value: ValueToWitness) -> Witness; + fn support(&self, domains: &Domains<'_>, local_id: LocalId, value: ValueToWitness) -> Witness; } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs index 1dbaadc73..027a33f98 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs @@ -456,7 +456,7 @@ where impl WitnessGenerator for BinaryEqualsChecker { - fn support(&self, local_id: LocalId, value: ValueToWitness) -> Witness { + fn support(&self, _: &Domains<'_>, local_id: LocalId, value: ValueToWitness) -> Witness { match local_id.unpack() { 0 => { let value = self.lhs.unpack_value(value); diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs index 4f91edd66..4f7ddd5b9 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs @@ -25,7 +25,11 @@ use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::propagation::TrailedInteger; +use pumpkin_core::propagation::checkers::BoundConsistencyChecker; use pumpkin_core::propagation::checkers::ConsistencyChecker; +use pumpkin_core::propagation::checkers::ValueToWitness; +use pumpkin_core::propagation::checkers::Witness; +use pumpkin_core::propagation::checkers::WitnessGenerator; use pumpkin_core::results::PropagationStatusCP; use pumpkin_core::state::PropagatorConflict; use pumpkin_core::variables::IntegerVariable; @@ -52,14 +56,10 @@ where ) -> impl ConsistencyChecker + 'static { checkers.add_inference_checker( InferenceCode::new(self.constraint_tag, LinearBounds), - Box::new(LinearLessOrEqualInferenceChecker::new( - self.x.clone(), - self.c, - )), + Box::new(LinearLessOrEqualChecker::new(self.x.clone(), self.c)), ); - #[allow(deprecated, reason = "TODO to implement for reified")] - pumpkin_core::propagation::checkers::DefaultChecker + BoundConsistencyChecker::new(LinearLessOrEqualChecker::new(self.x.clone(), self.c)) } fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { @@ -295,18 +295,18 @@ where } #[derive(Debug, Clone)] -pub struct LinearLessOrEqualInferenceChecker { +pub struct LinearLessOrEqualChecker { terms: Box<[Var]>, bound: i32, } -impl LinearLessOrEqualInferenceChecker { +impl LinearLessOrEqualChecker { pub fn new(terms: Box<[Var]>, bound: i32) -> Self { - LinearLessOrEqualInferenceChecker { terms, bound } + LinearLessOrEqualChecker { terms, bound } } } -impl InferenceChecker for LinearLessOrEqualInferenceChecker +impl InferenceChecker for LinearLessOrEqualChecker where Var: CheckerVariable, Atomic: AtomicConstraint, @@ -331,6 +331,16 @@ where } } +impl WitnessGenerator for LinearLessOrEqualChecker { + fn support(&self, domains: &Domains<'_>, _: LocalId, _: ValueToWitness) -> Witness { + Witness::new( + self.terms + .iter() + .map(|term| term.assign(domains.lower_bound(term))), + ) + } +} + #[allow(deprecated, reason = "Will be refactored")] #[cfg(test)] mod tests { From c7a3b9c6d5483e29128126bfa3c99483e84d5109 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Fri, 27 Feb 2026 15:57:14 +1100 Subject: [PATCH 05/10] Implement checker for absolute value --- .../propagators/arithmetic/absolute_value.rs | 30 +++++++++++++++++-- 1 file changed, 28 insertions(+), 2 deletions(-) diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs index 808fd29b7..5d769a762 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs @@ -8,6 +8,7 @@ use pumpkin_core::predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; use pumpkin_core::propagation::DomainEvents; +use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::Priority; @@ -16,7 +17,12 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::propagation::checkers::BoundConsistencyChecker; use pumpkin_core::propagation::checkers::ConsistencyChecker; +use pumpkin_core::propagation::checkers::ValueToWitness; +use pumpkin_core::propagation::checkers::Witness; +use pumpkin_core::propagation::checkers::WitnessGenerator; +use pumpkin_core::propagation::checkers::WitnessedVariable; use pumpkin_core::results::PropagationStatusCP; use pumpkin_core::variables::IntegerVariable; @@ -48,8 +54,10 @@ where }), ); - #[allow(deprecated, reason = "TODO to implement for reified")] - pumpkin_core::propagation::checkers::DefaultChecker + BoundConsistencyChecker::new(AbsoluteValueChecker { + signed: self.signed.clone(), + absolute: self.absolute.clone(), + }) } fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { @@ -212,6 +220,24 @@ where } } +impl WitnessGenerator + for AbsoluteValueChecker +{ + fn support(&self, _: &Domains<'_>, local_id: LocalId, value: ValueToWitness) -> Witness { + match local_id.unpack() { + 0 => { + let value = self.signed.unpack_value(value); + Witness::new([self.signed.assign(value), self.absolute.assign(value)]) + } + 1 => { + let value = self.absolute.unpack_value(value); + Witness::new([self.signed.assign(value), self.absolute.assign(value)]) + } + _ => unreachable!("absolute value does not register local id {local_id}"), + } + } +} + #[allow(deprecated, reason = "Will be refactored")] #[cfg(test)] mod tests { From 5fbad2555723c97fe04c7990648f0df0d3f3596e Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Fri, 27 Feb 2026 16:12:28 +1100 Subject: [PATCH 06/10] Remove redundant min --- .../core/src/propagators/hypercube_linear/propagator.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs b/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs index f7d5d4277..2a8f4817b 100644 --- a/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs +++ b/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs @@ -69,7 +69,7 @@ impl PropagatorConstructor for HypercubeLinearConstructor { } else { let last_idx = hypercube_predicates.len() - 1; [ - context.register_predicate(hypercube_predicates[0.min(last_idx)]), + context.register_predicate(hypercube_predicates[0]), context.register_predicate(hypercube_predicates[1.min(last_idx)]), ] }; From fd04f2e16368c5c002f34caabbc7a4b9b6df1a7f Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Fri, 27 Feb 2026 16:33:03 +1100 Subject: [PATCH 07/10] Include the value to support in linear witness generator --- .../arithmetic/linear_less_or_equal.rs | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs index 4f7ddd5b9..9c6bb4f35 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs @@ -332,12 +332,17 @@ where } impl WitnessGenerator for LinearLessOrEqualChecker { - fn support(&self, domains: &Domains<'_>, _: LocalId, _: ValueToWitness) -> Witness { - Witness::new( - self.terms - .iter() - .map(|term| term.assign(domains.lower_bound(term))), - ) + fn support(&self, domains: &Domains<'_>, local_id: LocalId, value: ValueToWitness) -> Witness { + let variable_index = local_id.unpack() as usize; + let value = self.terms[variable_index].unpack_value(value); + + Witness::new(self.terms.iter().enumerate().map(|(idx, term)| { + if idx == variable_index { + term.assign(value) + } else { + term.assign(domains.lower_bound(term)) + } + })) } } From 0e7329ebf9cd8aad5b4bb2bebba4d5e11383eafb Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Fri, 27 Feb 2026 17:09:04 +1100 Subject: [PATCH 08/10] Don't add to supported values of the domain being witnessed --- .../checkers/bound_consistency_checker.rs | 79 +----------- .../checkers/domain_consistency_checker.rs | 75 +----------- .../core/src/propagation/checkers/mod.rs | 115 ++++++++++++++++++ 3 files changed, 127 insertions(+), 142 deletions(-) diff --git a/pumpkin-crates/core/src/propagation/checkers/bound_consistency_checker.rs b/pumpkin-crates/core/src/propagation/checkers/bound_consistency_checker.rs index 1575f8f59..43ce134cd 100644 --- a/pumpkin-crates/core/src/propagation/checkers/bound_consistency_checker.rs +++ b/pumpkin-crates/core/src/propagation/checkers/bound_consistency_checker.rs @@ -1,14 +1,9 @@ use pumpkin_checking::InferenceChecker; -use pumpkin_checking::VariableState; -use crate::containers::HashMap; -use crate::predicate; use crate::predicates::Predicate; use crate::propagation::Domains; -use crate::propagation::ReadDomains; use crate::propagation::checkers::ConsistencyChecker; use crate::propagation::checkers::Scope; -use crate::propagation::checkers::Witness; use crate::propagation::checkers::WitnessGenerator; #[derive(Clone, Debug)] @@ -22,79 +17,17 @@ impl BoundConsistencyChecker { } } -impl> BoundConsistencyChecker { - /// Validate that the witness is a valid solution. - fn validate_witness(&self, witness: &Witness) -> bool { - let premises = witness - .iter() - .map(|(domain, value)| predicate![domain == value]) - .collect::>(); - - let state = VariableState::prepare_for_conflict_check(premises.clone(), None) - .expect("the witness is consistent by construction"); - - let state_is_conflicting = self.witness_generator.check(state, &premises, None); - - !state_is_conflicting - } -} - impl ConsistencyChecker for BoundConsistencyChecker where C: WitnessGenerator + InferenceChecker + Clone, { fn check_consistency(&self, domains: Domains<'_>, scope: &Scope) -> bool { - // A propagator is domain consistent if all values for all variables participate in - // at least one solution to the constraint. - - let mut supported_values = HashMap::new(); - - for (local_id, domain_id) in scope.iter() { - let supported_values_in_domain: Vec<_> = - std::mem::take(supported_values.entry(domain_id).or_default()); - - for value in [ - domains.lower_bound(&domain_id), - domains.upper_bound(&domain_id), - ] { - if supported_values_in_domain.contains(&value) { - // If the value is already supported, no need to generate a witness - // for it. - continue; - } - - let witness = self - .witness_generator - .support(&domains, local_id, value.into()); - - assert_eq!( - Some(value), - witness.value_for(domain_id), - "the witness for a variable assignment must contain that variable assignment" - ); - - assert!( - self.validate_witness(&witness), - "witness should satisfy the constraint" - ); - - // Add all the assigned variables as supported values as well. - for (witness_domain_id, witness_value) in witness.iter() { - assert!( - domains.contains(&witness_domain_id, witness_value), - "witness uses values outside domain" - ); - - let supports = supported_values.entry(witness_domain_id).or_default(); - supports.push(witness_value); - } - } - - let dummy = supported_values - .insert(domain_id, supported_values_in_domain) - .expect("a element was inserted at the beginning of the loop"); - assert!(dummy.is_empty(), "no values should be put into the dummy"); - } + super::assert_consistency( + domains, + scope, + &self.witness_generator, + super::Consistency::Bounds, + ); true } diff --git a/pumpkin-crates/core/src/propagation/checkers/domain_consistency_checker.rs b/pumpkin-crates/core/src/propagation/checkers/domain_consistency_checker.rs index 3f561dba3..cf8058b73 100644 --- a/pumpkin-crates/core/src/propagation/checkers/domain_consistency_checker.rs +++ b/pumpkin-crates/core/src/propagation/checkers/domain_consistency_checker.rs @@ -1,14 +1,9 @@ use pumpkin_checking::InferenceChecker; -use pumpkin_checking::VariableState; -use crate::containers::HashMap; -use crate::predicate; use crate::predicates::Predicate; use crate::propagation::Domains; -use crate::propagation::ReadDomains; use crate::propagation::checkers::ConsistencyChecker; use crate::propagation::checkers::Scope; -use crate::propagation::checkers::Witness; use crate::propagation::checkers::WitnessGenerator; #[derive(Clone, Debug)] @@ -22,75 +17,17 @@ impl DomainConsistencyChecker { } } -impl> DomainConsistencyChecker { - /// Validate that the witness is a valid solution. - fn validate_witness(&self, witness: &Witness) -> bool { - let premises = witness - .iter() - .map(|(domain, value)| predicate![domain == value]) - .collect::>(); - - let state = VariableState::prepare_for_conflict_check(premises.clone(), None) - .expect("the witness is consistent by construction"); - - let state_is_conflicting = self.witness_generator.check(state, &premises, None); - - !state_is_conflicting - } -} - impl ConsistencyChecker for DomainConsistencyChecker where C: WitnessGenerator + InferenceChecker + Clone, { fn check_consistency(&self, domains: Domains<'_>, scope: &Scope) -> bool { - // A propagator is domain consistent if all values for all variables participate in - // at least one solution to the constraint. - - let mut supported_values = HashMap::new(); - - for (local_id, domain_id) in scope.iter() { - let supported_values_in_domain: Vec<_> = - std::mem::take(supported_values.entry(domain_id).or_default()); - - for value in domains.iterate_domain(&domain_id) { - if supported_values_in_domain.contains(&value) { - // If the value is already supported, no need to generate a witness - // for it. - continue; - } - - let witness = self - .witness_generator - .support(&domains, local_id, value.into()); - - assert_eq!( - Some(value), - witness.value_for(domain_id), - "the witness for a variable assignment must contain that variable assignment" - ); - - assert!( - self.validate_witness(&witness), - "witness should satisfy the constraint" - ); - - // Add all the assigned variables as supported values as well. - for (witness_domain_id, witness_value) in witness.iter() { - assert!( - domains.contains(&witness_domain_id, witness_value), - "witness uses values outside domain" - ); - - let supports = supported_values.entry(witness_domain_id).or_default(); - supports.push(witness_value); - } - } - - let _ = supported_values - .insert(domain_id, supported_values_in_domain) - .expect("a element was inserted at the beginning of the loop"); - } + super::assert_consistency( + domains, + scope, + &self.witness_generator, + super::Consistency::Domain, + ); true } diff --git a/pumpkin-crates/core/src/propagation/checkers/mod.rs b/pumpkin-crates/core/src/propagation/checkers/mod.rs index 24239cd0e..a4c76c5eb 100644 --- a/pumpkin-crates/core/src/propagation/checkers/mod.rs +++ b/pumpkin-crates/core/src/propagation/checkers/mod.rs @@ -9,12 +9,20 @@ mod witness_generator; pub use bound_consistency_checker::*; pub use consistency_checker::*; pub use domain_consistency_checker::*; +use pumpkin_checking::InferenceChecker; +use pumpkin_checking::VariableState; pub use scope::*; pub use variable::*; pub use witness::*; pub use witness_generator::*; +use crate::containers::HashMap; +use crate::predicate; +use crate::predicates::Predicate; use crate::propagation::Domains; +use crate::propagation::LocalId; +use crate::propagation::ReadDomains; +use crate::variables::DomainId; #[deprecated = "only here to aid refactoring"] #[doc(hidden)] @@ -27,3 +35,110 @@ impl ConsistencyChecker for DefaultChecker { true } } + +enum Consistency { + Bounds, + Domain, +} + +fn assert_consistency( + domains: Domains<'_>, + scope: &Scope, + witness_generator: &PropagationChecker, + consistency: Consistency, +) where + PropagationChecker: WitnessGenerator + InferenceChecker, +{ + let mut supported_values: HashMap> = HashMap::default(); + + for (local_id, domain_id) in scope.iter() { + let _ = supported_values.entry(domain_id).or_insert(vec![]); + + match consistency { + Consistency::Domain => { + // A propagator is domain consistent if all values for all variables participate in + // at least one solution to the constraint. + for value in domains.iterate_domain(&domain_id) { + support_value( + &domains, + witness_generator, + local_id, + domain_id, + value, + &mut supported_values, + ); + } + } + Consistency::Bounds => { + for value in [ + domains.lower_bound(&domain_id), + domains.upper_bound(&domain_id), + ] { + support_value( + &domains, + witness_generator, + local_id, + domain_id, + value, + &mut supported_values, + ); + } + } + } + } +} + +fn support_value( + domains: &Domains<'_>, + witness_generator: &PropagationChecker, + local_id: LocalId, + domain_id: DomainId, + value: i32, + supported_values: &mut HashMap>, +) where + PropagationChecker: WitnessGenerator + InferenceChecker, +{ + if supported_values[&domain_id].contains(&value) { + // If the value is already supported, no need to generate a witness + // for it. + return; + } + + let witness = witness_generator.support(domains, local_id, value.into()); + + assert_eq!( + Some(value), + witness.value_for(domain_id), + "the witness for a variable assignment must contain that variable assignment" + ); + + assert!( + validate_witness(witness_generator, &witness), + "witness should satisfy the constraint" + ); + + // Add all the assigned variables as supported values as well. + for (witness_domain_id, witness_value) in witness.iter() { + assert!( + domains.contains(&witness_domain_id, witness_value), + "witness uses values outside domain" + ); + + let supports = supported_values.entry(witness_domain_id).or_default(); + supports.push(witness_value); + } +} + +fn validate_witness(checker: &impl InferenceChecker, witness: &Witness) -> bool { + let premises = witness + .iter() + .map(|(domain, value)| predicate![domain == value]) + .collect::>(); + + let state = VariableState::prepare_for_conflict_check(premises.clone(), None) + .expect("the witness is consistent by construction"); + + let state_is_conflicting = checker.check(state, &premises, None); + + !state_is_conflicting +} From 5c7a9d1482c49ebd67a9412b92b16be5fb520a51 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Fri, 27 Feb 2026 17:46:08 +1100 Subject: [PATCH 09/10] Proper mechanism to add to the scope --- .../core/src/engine/variables/affine_view.rs | 6 ++++++ .../core/src/engine/variables/domain_id.rs | 6 ++++++ pumpkin-crates/core/src/engine/variables/literal.rs | 6 ++++++ .../core/src/propagation/checkers/scope.rs | 4 ++++ .../core/src/propagation/checkers/variable.rs | 5 +++++ pumpkin-crates/core/src/propagation/constructor.rs | 12 +++++++----- .../propagators/arithmetic/linear_less_or_equal.rs | 4 ++++ 7 files changed, 38 insertions(+), 5 deletions(-) diff --git a/pumpkin-crates/core/src/engine/variables/affine_view.rs b/pumpkin-crates/core/src/engine/variables/affine_view.rs index 0f7bd070c..2a466b549 100644 --- a/pumpkin-crates/core/src/engine/variables/affine_view.rs +++ b/pumpkin-crates/core/src/engine/variables/affine_view.rs @@ -14,6 +14,8 @@ use crate::engine::predicates::predicate_constructor::PredicateConstructor; use crate::engine::variables::DomainId; use crate::engine::variables::IntegerVariable; use crate::math::num_ext::NumExt; +use crate::propagation::LocalId; +use crate::propagation::checkers::ScopeBuilder; use crate::propagation::checkers::SingleVariableAssignment; use crate::propagation::checkers::ValueToWitness; use crate::propagation::checkers::WitnessedVariable; @@ -410,6 +412,10 @@ enum Rounding { } impl WitnessedVariable for AffineView { + fn add_to_scope(&self, scope: &mut ScopeBuilder, local_id: LocalId) { + self.inner.add_to_scope(scope, local_id); + } + fn unpack_value(&self, value: ValueToWitness) -> i32 { let inner_value = self.inner.unpack_value(value); diff --git a/pumpkin-crates/core/src/engine/variables/domain_id.rs b/pumpkin-crates/core/src/engine/variables/domain_id.rs index 988b88558..a60f04426 100644 --- a/pumpkin-crates/core/src/engine/variables/domain_id.rs +++ b/pumpkin-crates/core/src/engine/variables/domain_id.rs @@ -10,6 +10,8 @@ use crate::engine::notifications::Watchers; use crate::engine::variables::AffineView; use crate::engine::variables::IntegerVariable; use crate::predicates::Predicate; +use crate::propagation::LocalId; +use crate::propagation::checkers::ScopeBuilder; use crate::propagation::checkers::SingleVariableAssignment; use crate::propagation::checkers::ValueToWitness; use crate::propagation::checkers::WitnessedVariable; @@ -195,6 +197,10 @@ impl TransformableVariable> for DomainId { } impl WitnessedVariable for DomainId { + fn add_to_scope(&self, scope: &mut ScopeBuilder, local_id: LocalId) { + scope.add(local_id, *self); + } + fn unpack_value(&self, value: ValueToWitness) -> i32 { value.unpack() } diff --git a/pumpkin-crates/core/src/engine/variables/literal.rs b/pumpkin-crates/core/src/engine/variables/literal.rs index be99195f0..7c268d3fd 100644 --- a/pumpkin-crates/core/src/engine/variables/literal.rs +++ b/pumpkin-crates/core/src/engine/variables/literal.rs @@ -15,6 +15,8 @@ use crate::engine::notifications::Watchers; use crate::engine::predicates::predicate::Predicate; use crate::engine::predicates::predicate_constructor::PredicateConstructor; use crate::engine::variables::AffineView; +use crate::propagation::LocalId; +use crate::propagation::checkers::ScopeBuilder; use crate::propagation::checkers::ValueToWitness; use crate::propagation::checkers::WitnessedVariable; @@ -226,6 +228,10 @@ impl TransformableVariable> for Literal { } impl WitnessedVariable for Literal { + fn add_to_scope(&self, scope: &mut ScopeBuilder, local_id: LocalId) { + self.integer_variable.add_to_scope(scope, local_id); + } + fn unpack_value(&self, value: ValueToWitness) -> i32 { self.integer_variable.unpack_value(value) } diff --git a/pumpkin-crates/core/src/propagation/checkers/scope.rs b/pumpkin-crates/core/src/propagation/checkers/scope.rs index 748cf1ff4..408c52c68 100644 --- a/pumpkin-crates/core/src/propagation/checkers/scope.rs +++ b/pumpkin-crates/core/src/propagation/checkers/scope.rs @@ -14,6 +14,10 @@ impl Scope { pub fn iter(&self) -> impl ExactSizeIterator { self.0.iter().copied() } + + pub fn is_empty(&self) -> bool { + self.0.is_empty() + } } #[derive(Clone, Debug, Default)] diff --git a/pumpkin-crates/core/src/propagation/checkers/variable.rs b/pumpkin-crates/core/src/propagation/checkers/variable.rs index 29f3ac25d..c1ad56949 100644 --- a/pumpkin-crates/core/src/propagation/checkers/variable.rs +++ b/pumpkin-crates/core/src/propagation/checkers/variable.rs @@ -1,9 +1,14 @@ +use crate::propagation::LocalId; +use crate::propagation::checkers::ScopeBuilder; use crate::propagation::checkers::SingleVariableAssignment; #[cfg(doc)] use crate::propagation::checkers::Witness; /// A variable that can be part of a [`Witness`]. pub trait WitnessedVariable { + /// Add self to the scope. + fn add_to_scope(&self, scope: &mut ScopeBuilder, local_id: LocalId); + /// Convert a [`ValueToWitness`] to an integer. /// /// See the documentation for [`ValueToWitness`] for why this abstraction is necessary. diff --git a/pumpkin-crates/core/src/propagation/constructor.rs b/pumpkin-crates/core/src/propagation/constructor.rs index f20f37ec5..23b61dc96 100644 --- a/pumpkin-crates/core/src/propagation/constructor.rs +++ b/pumpkin-crates/core/src/propagation/constructor.rs @@ -171,6 +171,8 @@ impl PropagatorConstructorContext<'_> { ) { self.will_not_register_any_events(); + var.add_to_scope(&mut self.scope_builder, local_id); + let propagator_var = PropagatorVarId { propagator: self.propagator_id, variable: local_id, @@ -180,10 +182,6 @@ impl PropagatorConstructorContext<'_> { let mut watchers = Watchers::new(propagator_var, &mut self.state.notification_engine); var.watch_all(&mut watchers, domain_events.events()); - - // This is a bit hacky to get the domain, but it works for now. - let domain_id = crate::predicate![var == 1].get_domain(); - self.scope_builder.add(local_id, domain_id); } /// Register the propagator to be enqueued when the given [`Predicate`] becomes true. @@ -289,8 +287,12 @@ impl Drop for PropagatorConstructorContext<'_> { #[cfg(feature = "check-propagations")] { + let RefOrOwned::Owned(scope_builder) = &mut self.scope_builder else { + unreachable!("other fields were already owned"); + }; + // Make sure to register the scope of this propagator with the state. - let scope = std::mem::take(self.scope_builder.deref_mut()).build(); + let scope = std::mem::take(scope_builder).build(); let _ = self.state.scopes.insert(self.propagator_id, scope); } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs index 9c6bb4f35..604db617f 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs @@ -69,6 +69,8 @@ where constraint_tag, } = self; + dbg!(&x); + let mut lower_bound_left_hand_side = 0_i64; let mut current_bounds = vec![]; @@ -333,6 +335,8 @@ where impl WitnessGenerator for LinearLessOrEqualChecker { fn support(&self, domains: &Domains<'_>, local_id: LocalId, value: ValueToWitness) -> Witness { + dbg!(self); + let variable_index = local_id.unpack() as usize; let value = self.terms[variable_index].unpack_value(value); From 8b143beeb126ce82a0eb6171147456b919bb52e7 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Fri, 27 Feb 2026 17:53:02 +1100 Subject: [PATCH 10/10] Update todo notes --- .../propagators/arithmetic/absolute_value.rs | 30 ++----------------- .../arithmetic/binary/binary_not_equals.rs | 2 +- .../arithmetic/integer_division.rs | 2 +- .../arithmetic/integer_multiplication.rs | 2 +- .../arithmetic/linear_not_equal.rs | 2 +- .../src/propagators/arithmetic/maximum.rs | 2 +- 6 files changed, 7 insertions(+), 33 deletions(-) diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs index 5d769a762..d5a77ed4b 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs @@ -8,7 +8,6 @@ use pumpkin_core::predicate; use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; use pumpkin_core::propagation::DomainEvents; -use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::InferenceCheckers; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::Priority; @@ -17,12 +16,7 @@ use pumpkin_core::propagation::Propagator; use pumpkin_core::propagation::PropagatorConstructor; use pumpkin_core::propagation::PropagatorConstructorContext; use pumpkin_core::propagation::ReadDomains; -use pumpkin_core::propagation::checkers::BoundConsistencyChecker; use pumpkin_core::propagation::checkers::ConsistencyChecker; -use pumpkin_core::propagation::checkers::ValueToWitness; -use pumpkin_core::propagation::checkers::Witness; -use pumpkin_core::propagation::checkers::WitnessGenerator; -use pumpkin_core::propagation::checkers::WitnessedVariable; use pumpkin_core::results::PropagationStatusCP; use pumpkin_core::variables::IntegerVariable; @@ -54,10 +48,8 @@ where }), ); - BoundConsistencyChecker::new(AbsoluteValueChecker { - signed: self.signed.clone(), - absolute: self.absolute.clone(), - }) + #[allow(deprecated, reason = "TODO to implement for int abs")] + pumpkin_core::propagation::checkers::DefaultChecker } fn create(self, mut context: PropagatorConstructorContext) -> Self::PropagatorImpl { @@ -220,24 +212,6 @@ where } } -impl WitnessGenerator - for AbsoluteValueChecker -{ - fn support(&self, _: &Domains<'_>, local_id: LocalId, value: ValueToWitness) -> Witness { - match local_id.unpack() { - 0 => { - let value = self.signed.unpack_value(value); - Witness::new([self.signed.assign(value), self.absolute.assign(value)]) - } - 1 => { - let value = self.absolute.unpack_value(value); - Witness::new([self.signed.assign(value), self.absolute.assign(value)]) - } - _ => unreachable!("absolute value does not register local id {local_id}"), - } - } -} - #[allow(deprecated, reason = "Will be refactored")] #[cfg(test)] mod tests { diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs index c3322d970..956e18281 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs @@ -50,7 +50,7 @@ where }), ); - #[allow(deprecated, reason = "TODO to implement for reified")] + #[allow(deprecated, reason = "TODO to implement for binary not equal")] pumpkin_core::propagation::checkers::DefaultChecker } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs index 22c9d1c79..8230c6a4b 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs @@ -84,7 +84,7 @@ where }), ); - #[allow(deprecated, reason = "TODO to implement for reified")] + #[allow(deprecated, reason = "TODO to implement for division")] pumpkin_core::propagation::checkers::DefaultChecker } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs index 52f654505..01d369dd2 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs @@ -53,7 +53,7 @@ where }), ); - #[allow(deprecated, reason = "TODO to implement for reified")] + #[allow(deprecated, reason = "TODO to implement for multiplication")] pumpkin_core::propagation::checkers::DefaultChecker } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs index 427f2df26..b2dd63cda 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs @@ -63,7 +63,7 @@ where }), ); - #[allow(deprecated, reason = "TODO to implement for reified")] + #[allow(deprecated, reason = "TODO to implement for not equal")] pumpkin_core::propagation::checkers::DefaultChecker } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs index 7e843a58c..4bc4b7a0f 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs @@ -49,7 +49,7 @@ where }), ); - #[allow(deprecated, reason = "TODO to implement for reified")] + #[allow(deprecated, reason = "TODO to implement for maximum")] pumpkin_core::propagation::checkers::DefaultChecker }