diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index bd6cc876e..7a2d27a94 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -26,7 +26,13 @@ jobs: target/ key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} - uses: dtolnay/rust-toolchain@stable - - run: cargo test --release --no-fail-fast --features pumpkin-solver/check-propagations --features pumpkin-core/check-deductions + - run: | + cargo test \ + --release \ + --no-fail-fast \ + --features pumpkin-solver/check-propagations \ + --features pumpkin-core/check-consistency \ + --features pumpkin-core/check-deductions wasm-test: name: Test Suite for pumpkin-core in WebAssembly diff --git a/Cargo.lock b/Cargo.lock index 8141d4c57..f4565b4b2 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -120,6 +120,24 @@ version = "1.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f2032f911046de80f0a198e0901378627c33f59ea0ac00e363d481118bd70a53" +[[package]] +name = "bit-set" +version = "0.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "09ec2f926cc3060f09db9ebc5b52823d85268d24bb917e472c0c4bea35780a7d" +dependencies = [ + "bit-vec", +] + +[[package]] +name = "bit-vec" +version = "0.9.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b71798fca2c1fe1086445a7258a4bc81e6e49dcd24c8d0dd9a1e57395b603f51" +dependencies = [ + "serde", +] + [[package]] name = "bitfield" version = "0.19.5" @@ -991,6 +1009,7 @@ dependencies = [ name = "pumpkin-core" version = "0.5.0" dependencies = [ + "bit-set", "bitfield", "bitfield-struct", "clap", @@ -1056,6 +1075,7 @@ dependencies = [ "clap", "convert_case", "enumset", + "log", "pumpkin-checking", "pumpkin-core", ] 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/Cargo.toml b/pumpkin-crates/core/Cargo.toml index 75192229d..db5185bae 100644 --- a/pumpkin-crates/core/Cargo.toml +++ b/pumpkin-crates/core/Cargo.toml @@ -30,6 +30,7 @@ clap = { version = "4.5.40", optional = true, features=["derive"] } indexmap = "2.10.0" dyn-clone = "1.0.20" flate2 = { version = "1.1.2" } +bit-set = "0.10.0" [target.'cfg(target_arch = "wasm32")'.dependencies] web-time = "1.1" @@ -39,6 +40,7 @@ getrandom = { version = "0.4.2", features = ["wasm_js"] } wasm-bindgen-test = "0.3" [features] +check-consistency = [] check-propagations = [] check-deductions = [] debug-checks = [] diff --git a/pumpkin-crates/core/src/api/mod.rs b/pumpkin-crates/core/src/api/mod.rs index 8d66f9873..7014c9f06 100644 --- a/pumpkin-crates/core/src/api/mod.rs +++ b/pumpkin-crates/core/src/api/mod.rs @@ -70,8 +70,8 @@ pub mod options { pub use crate::engine::ConflictResolverType; pub use crate::engine::RestartOptions; pub use crate::engine::SatisfactionSolverOptions as SolverOptions; + pub use crate::propagators::ReifiedPropagatorArgs; pub use crate::propagators::nogoods::LearningOptions; - pub use crate::propagators::reified_propagator::ReifiedPropagatorArgs; } pub mod termination { diff --git a/pumpkin-crates/core/src/basic_types/propositional_conjunction.rs b/pumpkin-crates/core/src/basic_types/propositional_conjunction.rs index 97c2f2ef1..517b82de4 100644 --- a/pumpkin-crates/core/src/basic_types/propositional_conjunction.rs +++ b/pumpkin-crates/core/src/basic_types/propositional_conjunction.rs @@ -21,6 +21,12 @@ impl Deref for PropositionalConjunction { } } +impl From for Box<[Predicate]> { + fn from(val: PropositionalConjunction) -> Self { + val.predicates_in_conjunction.into() + } +} + impl PropositionalConjunction { pub fn new(predicates_in_conjunction: Vec) -> Self { PropositionalConjunction { diff --git a/pumpkin-crates/core/src/checkers/mod.rs b/pumpkin-crates/core/src/checkers/mod.rs index fca730d27..bf0289bc3 100644 --- a/pumpkin-crates/core/src/checkers/mod.rs +++ b/pumpkin-crates/core/src/checkers/mod.rs @@ -1,3 +1,13 @@ +mod propagation_checker; +mod retention_checker; +mod retention_store; +mod scope; +mod self_disabling; mod store; +pub use propagation_checker::*; +pub use retention_checker::*; +pub use retention_store::*; +pub use scope::*; +pub use self_disabling::*; pub use store::*; diff --git a/pumpkin-crates/core/src/checkers/propagation_checker.rs b/pumpkin-crates/core/src/checkers/propagation_checker.rs new file mode 100644 index 000000000..7c7d5289a --- /dev/null +++ b/pumpkin-crates/core/src/checkers/propagation_checker.rs @@ -0,0 +1,64 @@ +use pumpkin_checking::BoxedChecker; +use pumpkin_checking::VariableState; + +use crate::predicates::Predicate; +use crate::propagation::Domains; +use crate::propagation::ReadDomains; +use crate::variables::DomainId; + +/// Tests whether an inference is correct given the solver state. +/// +/// An inference is correct when: +/// 1. All premises are satisfied. +/// 2. The conjunction of the premises and negation of the consequent is consistent. +/// 3. The consequent is logically entailed given the inference code. +#[derive(Clone, Debug)] +pub struct PropagationChecker { + inference_checker: BoxedChecker, +} + +impl PropagationChecker { + /// Create a new propagation checker given an inference checker and inference code. + pub fn new(inference_checker: BoxedChecker) -> PropagationChecker { + PropagationChecker { inference_checker } + } + + /// Run the propagation checker for the given inference. + pub fn check( + &self, + premises: &[Predicate], + consequent: Option, + domains: Domains<'_>, + ) -> Result<(), InvalidInference> { + let premises_satisfied = premises + .iter() + .all(|&premise| domains.evaluate_predicate(premise) == Some(true)); + + if !premises_satisfied { + return Err(InvalidInference::UnsatisfiedPremises); + } + + let variable_state = + VariableState::prepare_for_conflict_check(premises.iter().copied(), consequent) + .map_err(InvalidInference::InconsistentPredicates)?; + + if self + .inference_checker + .check(variable_state, premises, consequent.as_ref()) + { + Ok(()) + } else { + Err(InvalidInference::Unsound) + } + } +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum InvalidInference { + /// Not all premises are true given the current state. + UnsatisfiedPremises, + /// The predicates that make up the inference are trivially inconsistent. + InconsistentPredicates(DomainId), + /// Cannot establish that the inference is sound. + Unsound, +} diff --git a/pumpkin-crates/core/src/checkers/retention_checker.rs b/pumpkin-crates/core/src/checkers/retention_checker.rs new file mode 100644 index 000000000..3dbb79a93 --- /dev/null +++ b/pumpkin-crates/core/src/checkers/retention_checker.rs @@ -0,0 +1,43 @@ +use std::fmt::Debug; + +use dyn_clone::DynClone; + +use crate::checkers::Scope; +use crate::propagation::Domains; + +/// A runtime verifier that determines whether a propagator has nothing left to propagate. +/// +/// The contract mirrors the retention conditions of the formally verified proof checker: in the +/// current domains no inference of the propagator's rule applies, i.e. giving any variable in +/// the scope any value of its domain does not let the rule report a conflict. Each propagator +/// supplies its own checker, which may exploit the structure of its rule to decide this cheaply. +pub trait RetentionChecker: Debug + DynClone { + /// Returns `true` if the propagator has nothing left to propagate in `domains`, and `false` + /// if some inference of its rule still applies. + fn check_retention(&mut self, scope: &Scope, domains: Domains<'_>) -> bool; +} + +/// Wrapper around `Box` that implements [`Clone`]. +#[derive(Debug)] +pub struct BoxedRetentionChecker(Box); + +impl Clone for BoxedRetentionChecker { + fn clone(&self) -> Self { + BoxedRetentionChecker(dyn_clone::clone_box(&*self.0)) + } +} + +impl From for BoxedRetentionChecker +where + T: RetentionChecker + 'static, +{ + fn from(value: T) -> Self { + BoxedRetentionChecker(Box::new(value)) + } +} + +impl BoxedRetentionChecker { + pub fn check_retention(&mut self, scope: &Scope, domains: Domains<'_>) -> bool { + self.0.check_retention(scope, domains) + } +} diff --git a/pumpkin-crates/core/src/checkers/retention_store.rs b/pumpkin-crates/core/src/checkers/retention_store.rs new file mode 100644 index 000000000..2392e05c6 --- /dev/null +++ b/pumpkin-crates/core/src/checkers/retention_store.rs @@ -0,0 +1,90 @@ +use crate::checkers::BoxedRetentionChecker; +use crate::checkers::Scope; +use crate::containers::KeyedBitSet; +use crate::containers::KeyedVec; +use crate::containers::StorageKey; +use crate::propagation::Domains; +use crate::variables::DomainId; + +/// Holds the retention checkers in the solver. +/// +/// Also responsible for enqueueing the checkers and dispatching them when instructed via +/// [`RetentionCheckerStore::run_enqueued`]. +#[derive(Clone, Debug, Default)] +pub struct RetentionCheckerStore { + /// The checkers in the store. + store: KeyedVec, + /// Map from [`DomainId`] to the relevant checkers via their ID. + watch_list: KeyedVec>, + /// The checkers to run the next time. + queue: Vec, + /// Marks which checkers are enqueued to prevent duplicate checkers in + /// [`RetentionCheckerStore::queue`]. + enqueued: KeyedBitSet, +} + +impl RetentionCheckerStore { + /// Add a new `checker` to the store with the given `scope`. + pub fn register(&mut self, scope: Scope, checker: BoxedRetentionChecker) { + let checker_slot = self.store.new_slot(); + + for (_, domain) in scope.domains() { + self.watch_list.accomodate(domain, vec![]); + self.watch_list[domain].push(checker_slot.key()); + } + + let _ = checker_slot.populate((scope, checker)); + } + + /// Called when the domain is modified. + /// + /// Causes the checkers for this domain to be enqueued. + pub fn on_domain_event(&mut self, domain_id: DomainId) { + let Some(list) = self.watch_list.get(domain_id) else { + return; + }; + + for &checker_id in list { + if !self.enqueued.insert(checker_id) { + continue; + } + + self.queue.push(checker_id); + } + } + + /// Run the enqueued retention checkers. + pub fn run_enqueued(&mut self, mut domains: Domains<'_>) -> bool { + for checker_id in self.queue.drain(..) { + assert!(self.enqueued.remove(checker_id)); + + let (scope, checker) = &mut self.store[checker_id]; + + if !checker.check_retention(scope, domains.reborrow()) { + return false; + } + } + + true + } + + /// Clear the queue of retention checkers. + pub fn clear_queue(&mut self) { + self.queue.clear(); + self.enqueued.clear(); + } +} + +/// An identifier for added checkers. +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord)] +struct CheckerId(u32); + +impl StorageKey for CheckerId { + fn index(&self) -> usize { + self.0 as usize + } + + fn create_from_index(index: usize) -> Self { + CheckerId(index as u32) + } +} diff --git a/pumpkin-crates/core/src/checkers/scope.rs b/pumpkin-crates/core/src/checkers/scope.rs new file mode 100644 index 000000000..a72b7718b --- /dev/null +++ b/pumpkin-crates/core/src/checkers/scope.rs @@ -0,0 +1,82 @@ +use crate::containers::HashMap; +use crate::propagation::LocalId; +use crate::variables::DomainId; + +/// The scope of a constraint is the collection of variables involved in the relation. +#[derive(Clone, Debug, Default)] +pub struct Scope { + domains: HashMap, +} + +impl FromIterator<(LocalId, DomainId)> for Scope { + fn from_iter>(iter: T) -> Self { + Scope { + domains: iter.into_iter().collect(), + } + } +} + +impl Scope { + /// The scope of the given variables, with the [`LocalId`] of each variable its position. + pub fn from_variables<'a, Variable: ScopeItem + 'a>( + variables: impl IntoIterator, + ) -> Scope { + let mut scope = Scope::default(); + for (index, variable) in variables.into_iter().enumerate() { + variable.add_to_scope(&mut scope, LocalId::from(index as u32)); + } + scope + } + + /// Add a new domain to the scope with the given local id. + /// + /// Any previous occurrance of this local id will be overridden. + pub fn add_domain(&mut self, local_id: LocalId, domain_id: DomainId) { + let _ = self.domains.insert(local_id, domain_id); + } + + /// The integer domains in the scope with the [`LocalId`]s they are registered. + pub fn domains(&self) -> impl ExactSizeIterator { + self.domains.iter().map(|(lid, did)| (*lid, *did)) + } + + /// Returns a copy of this scope with the entry for `local_id` removed. + pub fn without(&self, local_id: LocalId) -> Scope { + let mut scope = self.clone(); + let _ = scope.domains.remove(&local_id); + scope + } +} + +macro_rules! impl_scope_from_tuple { + ($($lid_name:ident,$var_name:ident : $ty_name:ident),+) => { + impl<$($ty_name),+> From<($((LocalId, &$ty_name)),+)> for Scope + where + $($ty_name: ScopeItem),+ + { + fn from( + ($(($lid_name, $var_name)),+): ($((LocalId, &$ty_name)),+), + ) -> Self { + let mut scope = Scope::default(); + + $($var_name.add_to_scope(&mut scope, $lid_name);)+ + + scope + } + } + }; +} + +impl_scope_from_tuple!(la,va: VA, lb,vb: VB); +impl_scope_from_tuple!(la,va: VA, lb,vb: VB, lc,vc: VC); + +pub trait ScopeItem { + /// Adds self to the given scope with the given [`LocalId`]. + fn add_to_scope(&self, scope: &mut Scope, local_id: LocalId); +} + +impl ScopeItem for i32 { + fn add_to_scope(&self, _: &mut Scope, _: LocalId) { + // Do nothing + } +} diff --git a/pumpkin-crates/core/src/checkers/self_disabling.rs b/pumpkin-crates/core/src/checkers/self_disabling.rs new file mode 100644 index 000000000..ae7ff5f4e --- /dev/null +++ b/pumpkin-crates/core/src/checkers/self_disabling.rs @@ -0,0 +1,44 @@ +use std::sync::Arc; +use std::sync::atomic::AtomicBool; +use std::sync::atomic::Ordering; + +use super::RetentionChecker; +use super::Scope; +use crate::propagation::Domains; + +/// A [`RetentionChecker`] wrapper that skips the inner check when the associated constraint has +/// been deleted. +/// +/// The deletion flag is shared with the constraint owner (e.g. the nogood propagator). Setting the +/// flag to `true` causes the checker to become a permanent no-op. +#[derive(Debug, Clone)] +pub struct SelfDisablingChecker { + inner: T, + is_deleted: Arc, +} + +impl SelfDisablingChecker { + /// Create a new self-disabling checker. + /// + /// The deletion flag can be obtained with [`SelfDisablingChecker::deletion_flag`]. + pub fn new(checker: T) -> Self { + SelfDisablingChecker { + inner: checker, + is_deleted: Arc::new(AtomicBool::new(false)), + } + } + + /// The deletion flag for this self-disabling checker. + pub fn deletion_flag(&self) -> Arc { + Arc::clone(&self.is_deleted) + } +} + +impl RetentionChecker for SelfDisablingChecker { + fn check_retention(&mut self, scope: &Scope, domains: Domains<'_>) -> bool { + if self.is_deleted.load(Ordering::Relaxed) { + return true; + } + self.inner.check_retention(scope, domains) + } +} diff --git a/pumpkin-crates/core/src/checkers/store.rs b/pumpkin-crates/core/src/checkers/store.rs index 5806afb38..35e591d21 100644 --- a/pumpkin-crates/core/src/checkers/store.rs +++ b/pumpkin-crates/core/src/checkers/store.rs @@ -5,6 +5,7 @@ use pumpkin_checking::BoxedChecker; #[cfg(doc)] use pumpkin_checking::InferenceChecker; +use crate::checkers::PropagationChecker; use crate::containers::HashMap; use crate::predicates::Predicate; use crate::proof::InferenceCode; @@ -12,19 +13,24 @@ use crate::proof::InferenceCode; /// Owns the runtime checkers present in the solver. /// /// The runtime checkers consist of: -/// - inference checkers, which verify that propagations are sound. +/// - inference checkers, which verify that propagations are sound. Each is wrapped in a +/// [`PropagationChecker`], which evaluates the inference against the solver state. +/// +/// The retention checkers, which verify that propagation is complete, are owned by the +/// [`RetentionCheckerStore`](crate::checkers::RetentionCheckerStore) since they are scheduled +/// rather than looked up. #[derive(Clone, Debug, Default)] pub struct CheckerStore { /// For each inference code we associate possibly many inference checkers. - inference_checkers: HashMap>>, + inference_checkers: HashMap>, } impl CheckerStore { - /// Get the [`InferenceChecker`]s for the given inference code. + /// Get the [`PropagationChecker`]s for the given inference code. pub fn for_inference_code( &self, inference_code: &InferenceCode, - ) -> impl ExactSizeIterator> { + ) -> impl ExactSizeIterator { self.inference_checkers .get(inference_code) .map(|checkers| itertools::Either::Left(checkers.iter())) @@ -33,7 +39,7 @@ impl CheckerStore { /// Add a new inference checker for the inference code. /// - /// An inference code can have multiple checkers, so if an inference checker was already + /// An inference code can have multiple checkers, so if an [`InferenceChecker`] was already /// registered for the given code, this new checker is simply added to the collection. pub fn add_inference_checker( &mut self, @@ -41,8 +47,8 @@ impl CheckerStore { checker: BoxedChecker, ) { self.inference_checkers - .entry(inference_code.clone()) + .entry(inference_code) .or_default() - .push(checker); + .push(PropagationChecker::new(checker)); } } diff --git a/pumpkin-crates/core/src/constraints/mod.rs b/pumpkin-crates/core/src/constraints/mod.rs index e3ed52161..dbf84927a 100644 --- a/pumpkin-crates/core/src/constraints/mod.rs +++ b/pumpkin-crates/core/src/constraints/mod.rs @@ -1,7 +1,7 @@ //! Defines the main building blocks of constraints. use crate::Solver; use crate::propagation::PropagatorConstructor; -use crate::propagators::reified_propagator::ReifiedPropagatorArgs; +use crate::propagators::ReifiedPropagatorArgs; use crate::variables::Literal; mod constraint_poster; diff --git a/pumpkin-crates/core/src/containers/keyed_bit_set.rs b/pumpkin-crates/core/src/containers/keyed_bit_set.rs new file mode 100644 index 000000000..194a22874 --- /dev/null +++ b/pumpkin-crates/core/src/containers/keyed_bit_set.rs @@ -0,0 +1,56 @@ +use std::marker::PhantomData; + +use bit_set::BitSet; + +use crate::containers::StorageKey; + +/// A bit-set for types that implement [`StorageKey`]. +#[derive(Debug)] +pub struct KeyedBitSet { + bitset: BitSet, + key: PhantomData, +} + +impl KeyedBitSet { + /// Add the key to the set. + /// + /// Returns `true` if the set did _not_ previously contain `key`. + pub fn insert(&mut self, key: Key) -> bool { + self.bitset.insert(key.index()) + } + + /// Remove the key from the set. + /// + /// If the key was present, returns true. + pub fn remove(&mut self, key: Key) -> bool { + self.bitset.remove(key.index()) + } + + /// Get all keys in the set and remove them. + pub fn drain(&self) -> impl Iterator { + self.bitset.iter().map(Key::create_from_index) + } + + /// Remove all keys in the set. + pub fn clear(&mut self) { + self.bitset.make_empty(); + } +} + +impl Clone for KeyedBitSet { + fn clone(&self) -> Self { + Self { + bitset: self.bitset.clone(), + key: PhantomData, + } + } +} + +impl Default for KeyedBitSet { + fn default() -> Self { + Self { + bitset: BitSet::default(), + key: PhantomData, + } + } +} diff --git a/pumpkin-crates/core/src/containers/mod.rs b/pumpkin-crates/core/src/containers/mod.rs index 39343eb44..d16b86ae7 100644 --- a/pumpkin-crates/core/src/containers/mod.rs +++ b/pumpkin-crates/core/src/containers/mod.rs @@ -1,12 +1,14 @@ //! Contains containers which are used by the solver. mod key_generator; mod key_value_heap; +mod keyed_bit_set; mod keyed_vec; mod sparse_set; use fnv::FnvBuildHasher; pub use key_generator::*; pub use key_value_heap::*; +pub use keyed_bit_set::*; pub use keyed_vec::*; pub use sparse_set::*; diff --git a/pumpkin-crates/core/src/engine/cp/mod.rs b/pumpkin-crates/core/src/engine/cp/mod.rs index c0af305bb..aabf9bbbc 100644 --- a/pumpkin-crates/core/src/engine/cp/mod.rs +++ b/pumpkin-crates/core/src/engine/cp/mod.rs @@ -14,6 +14,8 @@ pub use trailed::*; mod tests { use assignments::Assignments; + #[cfg(feature = "check-consistency")] + use crate::checkers::RetentionCheckerStore; use crate::conjunction; use crate::containers::StorageKey; use crate::engine::TrailedValues; @@ -36,12 +38,16 @@ mod tests { assert_eq!(reason_store.len(), 0); { let mut notification_engine = NotificationEngine::default(); + #[cfg(feature = "check-consistency")] + let mut consistency_checker_store = RetentionCheckerStore::default(); let mut context = PropagationContext::new( &mut trailed_values, &mut assignments, &mut reason_store, &mut notification_engine, PropagatorId(0), + #[cfg(feature = "check-consistency")] + &mut consistency_checker_store, ); let result = context.post( @@ -67,12 +73,16 @@ mod tests { assert_eq!(reason_store.len(), 0); { let mut notification_engine = NotificationEngine::default(); + #[cfg(feature = "check-consistency")] + let mut consistency_checker_store = RetentionCheckerStore::default(); let mut context = PropagationContext::new( &mut trailed_values, &mut assignments, &mut reason_store, &mut notification_engine, PropagatorId(0), + #[cfg(feature = "check-consistency")] + &mut consistency_checker_store, ); let result = context.post( @@ -98,12 +108,16 @@ mod tests { assert_eq!(reason_store.len(), 0); { let mut notification_engine = NotificationEngine::default(); + #[cfg(feature = "check-consistency")] + let mut consistency_checker_store = RetentionCheckerStore::default(); let mut context = PropagationContext::new( &mut trailed_values, &mut assignments, &mut reason_store, &mut notification_engine, PropagatorId(0), + #[cfg(feature = "check-consistency")] + &mut consistency_checker_store, ); let result = context.post( diff --git a/pumpkin-crates/core/src/engine/cp/test_solver.rs b/pumpkin-crates/core/src/engine/cp/test_solver.rs index 077c4af30..e09d91ab9 100644 --- a/pumpkin-crates/core/src/engine/cp/test_solver.rs +++ b/pumpkin-crates/core/src/engine/cp/test_solver.rs @@ -240,14 +240,28 @@ impl TestSolver { } pub fn propagate(&mut self, propagator: PropagatorId) -> Result<(), Conflict> { + let State { + propagators, + trailed_values, + assignments, + reason_store, + notification_engine, + #[cfg(feature = "check-consistency")] + retention_checkers, + .. + } = &mut self.state; + let context = PropagationContext::new( - &mut self.state.trailed_values, - &mut self.state.assignments, - &mut self.state.reason_store, - &mut self.state.notification_engine, + trailed_values, + assignments, + reason_store, + notification_engine, propagator, + #[cfg(feature = "check-consistency")] + retention_checkers, ); - self.state.propagators[propagator].propagate(context) + + propagators[propagator].propagate(context) } pub fn propagate_until_fixed_point( @@ -259,14 +273,28 @@ impl TestSolver { loop { { // Specify the life-times to be able to retrieve the trail entries + let State { + propagators, + trailed_values, + assignments, + reason_store, + notification_engine, + #[cfg(feature = "check-consistency")] + retention_checkers, + .. + } = &mut self.state; + let context = PropagationContext::new( - &mut self.state.trailed_values, - &mut self.state.assignments, - &mut self.state.reason_store, - &mut self.state.notification_engine, + trailed_values, + assignments, + reason_store, + notification_engine, propagator, + #[cfg(feature = "check-consistency")] + retention_checkers, ); - self.state.propagators[propagator].propagate(context)?; + + propagators[propagator].propagate(context)?; self.notify_propagator(propagator); } if self.state.assignments.num_trail_entries() == num_trail_entries { diff --git a/pumpkin-crates/core/src/engine/debug_helper.rs b/pumpkin-crates/core/src/engine/debug_helper.rs index 6704a156d..9eec98d60 100644 --- a/pumpkin-crates/core/src/engine/debug_helper.rs +++ b/pumpkin-crates/core/src/engine/debug_helper.rs @@ -9,6 +9,8 @@ use super::notifications::NotificationEngine; use super::predicates::predicate::Predicate; use super::reason::ReasonStore; use crate::basic_types::PropositionalConjunction; +#[cfg(feature = "check-consistency")] +use crate::checkers::RetentionCheckerStore; use crate::engine::cp::Assignments; use crate::propagation::ExplanationContext; use crate::propagation::PropagationContext; @@ -76,6 +78,9 @@ impl DebugHelper { let num_entries_on_trail_before_propagation = assignments_clone.num_trail_entries(); + #[cfg(feature = "check-consistency")] + let mut retention_checkers = RetentionCheckerStore::default(); + let mut reason_store = Default::default(); let context = PropagationContext::new( &mut trailed_values_clone, @@ -83,6 +88,8 @@ impl DebugHelper { &mut reason_store, &mut notification_engine_clone, PropagatorId(propagator_id as u32), + #[cfg(feature = "check-consistency")] + &mut retention_checkers, ); let propagation_status_cp = propagator.propagate_from_scratch(context); @@ -252,6 +259,9 @@ impl DebugHelper { notification_engine_clone.debug_create_from_assignments(&assignments_clone); if adding_predicates_was_successful { + #[cfg(feature = "check-consistency")] + let mut retention_checkers = RetentionCheckerStore::default(); + // Now propagate using the debug propagation method. let mut reason_store = Default::default(); let context = PropagationContext::new( @@ -260,6 +270,8 @@ impl DebugHelper { &mut reason_store, &mut notification_engine_clone, propagator_id, + #[cfg(feature = "check-consistency")] + &mut retention_checkers, ); let debug_propagation_status_cp = propagator.propagate_from_scratch(context); @@ -369,12 +381,17 @@ impl DebugHelper { loop { let num_predicates_before = assignments_clone.num_trail_entries(); + #[cfg(feature = "check-consistency")] + let mut retention_checkers = RetentionCheckerStore::default(); + let context = PropagationContext::new( &mut trailed_values_clone, &mut assignments_clone, &mut reason_store, &mut notification_engine_clone, propagator_id, + #[cfg(feature = "check-consistency")] + &mut retention_checkers, ); let debug_propagation_status_cp = propagator.propagate_from_scratch(context); @@ -433,6 +450,9 @@ impl DebugHelper { notification_engine_clone.debug_create_from_assignments(&assignments_clone); if adding_predicates_was_successful { + #[cfg(feature = "check-consistency")] + let mut retention_checkers = RetentionCheckerStore::default(); + // now propagate using the debug propagation method let mut reason_store = Default::default(); let context = PropagationContext::new( @@ -441,6 +461,8 @@ impl DebugHelper { &mut reason_store, &mut notification_engine_clone, propagator_id, + #[cfg(feature = "check-consistency")] + &mut retention_checkers, ); let debug_propagation_status_cp = propagator.propagate_from_scratch(context); assert!( diff --git a/pumpkin-crates/core/src/engine/state.rs b/pumpkin-crates/core/src/engine/state.rs index a144e7b33..475747908 100644 --- a/pumpkin-crates/core/src/engine/state.rs +++ b/pumpkin-crates/core/src/engine/state.rs @@ -2,10 +2,11 @@ use std::sync::Arc; use pumpkin_checking::BoxedChecker; use pumpkin_checking::InferenceChecker; -#[cfg(feature = "check-propagations")] -use pumpkin_checking::VariableState; +use crate::checkers::BoxedRetentionChecker; use crate::checkers::CheckerStore; +use crate::checkers::RetentionCheckerStore; +use crate::checkers::Scope; use crate::containers::KeyGenerator; use crate::create_statistics_struct; use crate::engine::Assignments; @@ -83,6 +84,8 @@ pub struct State { /// Runtime checkers to run in the propagation loop. checkers: CheckerStore, + /// The retention checkers, which verify that propagation is complete, and their scheduling. + pub(crate) retention_checkers: RetentionCheckerStore, } create_statistics_struct!(StateStatistics { @@ -113,6 +116,7 @@ impl Default for State { statistics: StateStatistics::default(), constraint_tags: KeyGenerator::default(), checkers: CheckerStore::default(), + retention_checkers: Default::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 @@ -356,15 +360,23 @@ impl State { .register(domain_id, events, propagator_var); } + let (inference_checkers, retention_checkers) = checkers.into_parts(); + if cfg!(feature = "check-propagations") { // Only register the checkers when this feature is enabled. This is an if statement // instead of a #[cfg(...)] to avoid the 'unused variable' warning that we would // otherwise get on `self.checkers`. - for (inference_code, checker) in checkers.into_iter() { + for (inference_code, checker) in inference_checkers { self.checkers.add_inference_checker(inference_code, checker); } } + if cfg!(feature = "check-consistency") { + for (scope, checker) in retention_checkers { + self.retention_checkers.register(scope, checker); + } + } + pumpkin_assert_simple!( propagator.priority() as u8 <= 5, "The propagator priority exceeds 5. @@ -401,6 +413,16 @@ impl State { .add_inference_checker(inference_code.clone(), BoxedChecker::new(Box::new(checker))); inference_code } + + /// Add a retention checker for the scope. + pub fn add_retention_checker( + &mut self, + scope: impl Into, + checker: impl Into, + ) { + self.retention_checkers + .register(scope.into(), checker.into()); + } } /// Operations for retrieving propagators. @@ -437,16 +459,27 @@ impl State { &mut self, handle: PropagatorHandle

, ) -> (Option<&mut P>, PropagationContext<'_>) { - ( - self.propagators.get_propagator_mut(handle), - PropagationContext::new( - &mut self.trailed_values, - &mut self.assignments, - &mut self.reason_store, - &mut self.notification_engine, - handle.propagator_id(), - ), - ) + let Self { + propagators, + trailed_values, + assignments, + reason_store, + notification_engine, + #[cfg(feature = "check-consistency")] + retention_checkers, + .. + } = self; + let propagator = propagators.get_propagator_mut(handle); + let context = PropagationContext::new( + trailed_values, + assignments, + reason_store, + notification_engine, + handle.propagator_id(), + #[cfg(feature = "check-consistency")] + retention_checkers, + ); + (propagator, context) } } @@ -629,13 +662,25 @@ impl State { let num_trail_entries_before = self.assignments.num_trail_entries(); let propagation_status = { - let propagator = &mut self.propagators[propagator_id]; + let Self { + propagators, + trailed_values, + assignments, + reason_store, + notification_engine, + #[cfg(feature = "check-consistency")] + retention_checkers, + .. + } = self; + let propagator = &mut propagators[propagator_id]; let context = PropagationContext::new( - &mut self.trailed_values, - &mut self.assignments, - &mut self.reason_store, - &mut self.notification_engine, + trailed_values, + assignments, + reason_store, + notification_engine, propagator_id, + #[cfg(feature = "check-consistency")] + retention_checkers, ); propagator.propagate(context) }; @@ -643,6 +688,9 @@ impl State { #[cfg(feature = "check-propagations")] self.check_propagations(num_trail_entries_before); + #[cfg(feature = "check-consistency")] + self.enqueue_retention_checkers(num_trail_entries_before); + match propagation_status { Ok(_) => { // Notify other propagators of the propagations and continue. @@ -670,6 +718,9 @@ impl State { #[cfg(feature = "check-propagations")] self.check_conflict(&conflict); + #[cfg(feature = "check-consistency")] + self.retention_checkers.clear_queue(); + self.statistics.num_conflicts += 1; if let Conflict::Propagator(inner) = &conflict { pumpkin_assert_advanced!(DebugHelper::debug_reported_failure( @@ -743,6 +794,16 @@ impl State { } } + #[cfg(feature = "check-consistency")] + fn enqueue_retention_checkers(&mut self, first_propagation_index: usize) { + for trail_index in first_propagation_index..self.assignments.num_trail_entries() { + let entry = self.assignments.get_trail_entry(trail_index); + + self.retention_checkers + .on_domain_event(entry.predicate.get_domain()); + } + } + /// Performs fixed-point propagation using the propagators defined in the [`State`]. /// /// The posted [`Predicate`]s (using [`State::post`]) and added propagators (using @@ -771,6 +832,13 @@ impl State { self.propagate(propagator_id)?; } + if cfg!(feature = "check-consistency") { + assert!( + self.retention_checkers + .run_enqueued(Domains::new(&self.assignments, &mut self.trailed_values)) + ); + } + // 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( @@ -788,37 +856,33 @@ impl State { impl State { /// Run the checker for the given inference code on the given inference. fn run_checker( - &self, + &mut self, premises: impl IntoIterator, consequent: Option, inference_code: &InferenceCode, ) { let premises: Vec<_> = premises.into_iter().collect(); - let any_checker_accepts_inference = - self.checkers - .for_inference_code(inference_code) - .any(|checker| { - // Construct the variable state for the conflict check. - let variable_state = VariableState::prepare_for_conflict_check( - premises.clone(), - consequent, - ) - .unwrap_or_else(|domain| { - panic!( - "inconsistent atomics over domain {domain:?} in inference by {inference_code:?}" - ) - }); - - checker.check(variable_state, &premises, consequent.as_ref()) - }); + let checkers = self.checkers.for_inference_code(inference_code); + assert!( + checkers.len() > 0, + "missing checker for inference code {inference_code:?}" + ); + + let results = checkers + .map(|checker| { + checker.check( + &premises, + consequent, + Domains::new(&self.assignments, &mut self.trailed_values), + ) + }) + .collect::>(); + let any_checker_accepts_inference = results.iter().any(Result::is_ok); assert!( any_checker_accepts_inference, - "checker for inference code {:?} fails on inference {:?} -> {:?}", - inference_code, - premises.into_iter().collect::>(), - consequent, + "checker for inference code {inference_code:?} fails on inference {premises:?} -> {consequent:?}: {results:?}" ); } } @@ -1159,12 +1223,23 @@ impl State { } pub fn get_propagation_context(&mut self) -> PropagationContext<'_> { + let Self { + trailed_values, + assignments, + reason_store, + notification_engine, + #[cfg(feature = "check-consistency")] + retention_checkers, + .. + } = self; PropagationContext::new( - &mut self.trailed_values, - &mut self.assignments, - &mut self.reason_store, - &mut self.notification_engine, + trailed_values, + assignments, + reason_store, + notification_engine, PropagatorId(0), + #[cfg(feature = "check-consistency")] + retention_checkers, ) } } diff --git a/pumpkin-crates/core/src/engine/variables/affine_view.rs b/pumpkin-crates/core/src/engine/variables/affine_view.rs index 9142f0ba5..4473216d8 100644 --- a/pumpkin-crates/core/src/engine/variables/affine_view.rs +++ b/pumpkin-crates/core/src/engine/variables/affine_view.rs @@ -5,6 +5,8 @@ use pumpkin_checking::CheckerVariable; use pumpkin_checking::IntExt; use super::TransformableVariable; +use crate::checkers::Scope; +use crate::checkers::ScopeItem; use crate::engine::Assignments; use crate::engine::notifications::DomainEvent; use crate::engine::notifications::OpaqueDomainEvent; @@ -57,6 +59,12 @@ impl AffineView { } } +impl ScopeItem for AffineView { + fn add_to_scope(&self, scope: &mut Scope, local_id: LocalId) { + self.inner.add_to_scope(scope, local_id); + } +} + impl EventTarget for AffineView { fn register( &self, diff --git a/pumpkin-crates/core/src/engine/variables/domain_id.rs b/pumpkin-crates/core/src/engine/variables/domain_id.rs index 0d1c42b62..0c53b3dcc 100644 --- a/pumpkin-crates/core/src/engine/variables/domain_id.rs +++ b/pumpkin-crates/core/src/engine/variables/domain_id.rs @@ -2,6 +2,8 @@ use enumset::EnumSet; use pumpkin_checking::CheckerVariable; use super::TransformableVariable; +use crate::checkers::Scope; +use crate::checkers::ScopeItem; use crate::containers::StorageKey; use crate::engine::Assignments; use crate::engine::notifications::DomainEvent; @@ -35,6 +37,12 @@ impl DomainId { } } +impl ScopeItem for DomainId { + fn add_to_scope(&self, scope: &mut Scope, local_id: LocalId) { + scope.add_domain(local_id, *self); + } +} + impl EventTarget for DomainId { fn register( &self, diff --git a/pumpkin-crates/core/src/engine/variables/integer_variable.rs b/pumpkin-crates/core/src/engine/variables/integer_variable.rs index 34083bbd5..37eacb35d 100644 --- a/pumpkin-crates/core/src/engine/variables/integer_variable.rs +++ b/pumpkin-crates/core/src/engine/variables/integer_variable.rs @@ -4,6 +4,7 @@ use enumset::EnumSet; use pumpkin_checking::CheckerVariable; use super::TransformableVariable; +use crate::checkers::ScopeItem; use crate::engine::Assignments; use crate::engine::notifications::DomainEvent; use crate::engine::notifications::OpaqueDomainEvent; @@ -20,6 +21,7 @@ pub trait IntegerVariable: + TransformableVariable + Debug + CheckerVariable + + ScopeItem + EventTarget { type AffineView: IntegerVariable; diff --git a/pumpkin-crates/core/src/engine/variables/literal.rs b/pumpkin-crates/core/src/engine/variables/literal.rs index 3b358031f..8bf89d02f 100644 --- a/pumpkin-crates/core/src/engine/variables/literal.rs +++ b/pumpkin-crates/core/src/engine/variables/literal.rs @@ -8,6 +8,8 @@ use pumpkin_checking::VariableState; use super::DomainId; use super::IntegerVariable; use super::TransformableVariable; +use crate::checkers::Scope; +use crate::checkers::ScopeItem; use crate::engine::Assignments; use crate::engine::notifications::DomainEvent; use crate::engine::notifications::OpaqueDomainEvent; @@ -76,6 +78,12 @@ macro_rules! forward { } } +impl ScopeItem for Literal { + fn add_to_scope(&self, scope: &mut Scope, local_id: LocalId) { + self.integer_variable.add_to_scope(scope, local_id); + } +} + impl EventTarget for Literal { fn register( &self, diff --git a/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs b/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs index f39d337b0..3c8350685 100644 --- a/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs +++ b/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs @@ -1,6 +1,10 @@ use enumset::EnumSet; use crate::basic_types::PredicateId; +use crate::checkers::BoxedRetentionChecker; +#[cfg(feature = "check-consistency")] +use crate::checkers::RetentionCheckerStore; +use crate::checkers::Scope; use crate::engine::Assignments; use crate::engine::EmptyDomain; use crate::engine::EmptyDomainConflict; @@ -89,6 +93,9 @@ pub struct PropagationContext<'a> { pub(crate) propagator_id: PropagatorId, pub(crate) notification_engine: &'a mut NotificationEngine, reification_literal: Option, + + #[cfg(feature = "check-consistency")] + pub(crate) retention_checkers: &'a mut RetentionCheckerStore, } impl<'a> HasAssignments for PropagationContext<'a> { @@ -112,6 +119,7 @@ impl<'a> PropagationContext<'a> { reason_store: &'a mut ReasonStore, notification_engine: &'a mut NotificationEngine, propagator_id: PropagatorId, + #[cfg(feature = "check-consistency")] retention_checkers: &'a mut RetentionCheckerStore, ) -> Self { PropagationContext { trailed_values, @@ -120,6 +128,33 @@ impl<'a> PropagationContext<'a> { propagator_id, notification_engine, reification_literal: None, + #[cfg(feature = "check-consistency")] + retention_checkers, + } + } + + /// Add a retention checker for the given constraint and scope. + /// + /// If the `check-consistency` feature is not enabled, this is a no-op. + pub fn add_retention_checker( + &mut self, + scope: impl Into, + checker: impl Into, + ) { + pumpkin_assert_simple!( + self.reification_literal.is_none(), + "Cannot add retention checkers from within a reified propagation context." + ); + + #[cfg(feature = "check-consistency")] + self.retention_checkers + .register(scope.into(), checker.into()); + + // Use variables to avoid unused warnings. + #[cfg(not(feature = "check-consistency"))] + { + let _ = scope; + let _ = checker; } } @@ -233,6 +268,8 @@ impl<'a> PropagationContext<'a> { propagator_id: self.propagator_id, notification_engine: self.notification_engine, reification_literal: self.reification_literal, + #[cfg(feature = "check-consistency")] + retention_checkers: self.retention_checkers, } } } diff --git a/pumpkin-crates/core/src/propagation/runtime_checkers.rs b/pumpkin-crates/core/src/propagation/runtime_checkers.rs index aa2917247..700b48e45 100644 --- a/pumpkin-crates/core/src/propagation/runtime_checkers.rs +++ b/pumpkin-crates/core/src/propagation/runtime_checkers.rs @@ -1,6 +1,9 @@ use pumpkin_checking::BoxedChecker; use pumpkin_checking::InferenceChecker; +use crate::checkers::BoxedRetentionChecker; +use crate::checkers::RetentionChecker; +use crate::checkers::Scope; use crate::predicates::Predicate; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; @@ -10,10 +13,14 @@ use crate::propagation::PropagatorConstructor; /// Holds the runtime checkers that are added by a propagator. /// -/// Used when creating a new propagator in [`PropagatorConstructor::create`]. +/// Used when creating a new propagator in [`PropagatorConstructor::create`]. Two kinds of checkers +/// can be added: +/// - inference checkers, which verify that the propagations are sound, +/// - retention checkers, which verify that the propagator has nothing left to propagate. #[derive(Clone, Debug)] pub struct RuntimeCheckers { inference_checkers: Vec<(InferenceCode, BoxedChecker)>, + retention_checkers: Vec<(Scope, BoxedRetentionChecker)>, } impl RuntimeCheckers { @@ -24,17 +31,16 @@ impl RuntimeCheckers { pub fn empty() -> RuntimeCheckers { RuntimeCheckers { inference_checkers: vec![], + retention_checkers: vec![], } } /// Create a [`RuntimeCheckersBuilder`] to add runtime checkers. /// - /// The [`RuntimeCheckersBuilder::build`] will panic if no checkers are added. + /// The [`RuntimeCheckersBuilder::build`] will panic if no inference checkers are added. pub fn builder() -> RuntimeCheckersBuilder { RuntimeCheckersBuilder { - checkers: RuntimeCheckers { - inference_checkers: vec![], - }, + checkers: RuntimeCheckers::empty(), } } @@ -52,19 +58,48 @@ impl RuntimeCheckers { inference_code } -} -impl IntoIterator for RuntimeCheckers { - type Item = (InferenceCode, BoxedChecker); + /// Add a [`RetentionChecker`] over the given scope to verify that the propagator has nothing + /// left to propagate at fixpoints. + pub fn add_retention_checker( + &mut self, + scope: impl Into, + checker: impl Into, + ) { + self.retention_checkers.push((scope.into(), checker.into())); + } - type IntoIter = std::vec::IntoIter; + /// Add a checker that is both the inference checker and the retention checker of the + /// propagator's rule, with the retention checker over `scope`. + pub fn add_rule( + &mut self, + scope: impl Into, + constraint_tag: ConstraintTag, + inference_label: impl InferenceLabel, + checker: Checker, + ) -> InferenceCode + where + Checker: InferenceChecker + RetentionChecker + Clone + 'static, + { + let inference_code = + self.add_inference_checker(constraint_tag, inference_label, checker.clone()); + self.add_retention_checker(scope, checker); + inference_code + } - fn into_iter(self) -> Self::IntoIter { - self.inference_checkers.into_iter() + /// Split the checkers into the inference checkers and the retention checkers. + #[allow(clippy::type_complexity, reason = "the tuple mirrors the two fields")] + pub fn into_parts( + self, + ) -> ( + Vec<(InferenceCode, BoxedChecker)>, + Vec<(Scope, BoxedRetentionChecker)>, + ) { + (self.inference_checkers, self.retention_checkers) } } -/// A builder for the [`RuntimeCheckers`] that ensures at least one checker is added. +/// A builder for the [`RuntimeCheckers`] that ensures at least one inference checker is added. #[derive(Clone, Debug)] pub struct RuntimeCheckersBuilder { checkers: RuntimeCheckers, @@ -82,10 +117,36 @@ impl RuntimeCheckersBuilder { .add_inference_checker(constraint_tag, inference_label, checker) } + /// Add a [`RetentionChecker`] over the given scope to verify that the propagator has nothing + /// left to propagate at fixpoints. + pub fn add_retention_checker( + &mut self, + scope: impl Into, + checker: impl Into, + ) { + self.checkers.add_retention_checker(scope, checker); + } + + /// Add a checker that is both the inference checker and the retention checker of the + /// propagator's rule, with the retention checker over `scope`. + pub fn add_rule( + &mut self, + scope: impl Into, + constraint_tag: ConstraintTag, + inference_label: impl InferenceLabel, + checker: Checker, + ) -> InferenceCode + where + Checker: InferenceChecker + RetentionChecker + Clone + 'static, + { + self.checkers + .add_rule(scope, constraint_tag, inference_label, checker) + } + /// Finish adding runtime checkers. /// - /// Panics if runtime verification is enabled and no checkers are added. If it is expected - /// behavior that no checkers are added, use [`RuntimeCheckers::empty`]. + /// Panics if runtime verification is enabled and no inference checkers are added. If it is + /// expected behavior that no checkers are added, use [`RuntimeCheckers::empty`]. pub fn build(self) -> RuntimeCheckers { if cfg!(feature = "check-propagations") { assert!( diff --git a/pumpkin-crates/core/src/propagators/mod.rs b/pumpkin-crates/core/src/propagators/mod.rs index 2af1b61a5..25afdc21d 100644 --- a/pumpkin-crates/core/src/propagators/mod.rs +++ b/pumpkin-crates/core/src/propagators/mod.rs @@ -1,5 +1,5 @@ pub mod hypercube_linear; pub mod nogoods; -pub(crate) mod reified_propagator; +mod reified_propagator; pub use reified_propagator::*; diff --git a/pumpkin-crates/core/src/propagators/nogoods/checker.rs b/pumpkin-crates/core/src/propagators/nogoods/checker.rs index 700ee6a2c..c6f3b94ea 100644 --- a/pumpkin-crates/core/src/propagators/nogoods/checker.rs +++ b/pumpkin-crates/core/src/propagators/nogoods/checker.rs @@ -2,6 +2,15 @@ use std::fmt::Debug; use pumpkin_checking::AtomicConstraint; use pumpkin_checking::InferenceChecker; +use pumpkin_checking::VariableState; + +use crate::checkers::RetentionChecker; +use crate::checkers::Scope; +use crate::containers::HashSet; +use crate::predicates::Predicate; +use crate::predicates::PredicateType; +use crate::propagation::Domains; +use crate::propagation::ReadDomains; #[derive(Debug, Clone)] pub struct NogoodChecker { @@ -12,12 +21,240 @@ impl InferenceChecker for NogoodChecker where Atomic: AtomicConstraint + Clone + Debug, { - fn check( - &self, - state: pumpkin_checking::VariableState, - _: &[Atomic], - _: Option<&Atomic>, - ) -> bool { + fn check(&self, state: VariableState, _: &[Atomic], _: Option<&Atomic>) -> bool { self.nogood.iter().all(|atomic| state.is_true(atomic)) } } + +impl RetentionChecker for NogoodChecker { + fn check_retention(&mut self, _: &Scope, domains: Domains<'_>) -> bool { + // For unit propagation, the state is consistent if: + // - at least two predicates are unassigned + // - or otherwise, at least one predicate is assigned + + let untrue_predicate_count = self + .nogood + .iter() + .filter(|&&predicate| domains.evaluate_predicate(predicate) != Some(true)) + .count(); + + // If at least two predicates are not true, or any predicate is false, then the domains are + // unit-propagation consistent. + let is_consistent = untrue_predicate_count >= 2 + || self + .nogood + .iter() + .any(|&predicate| domains.evaluate_predicate(predicate) == Some(false)); + + if !is_consistent { + log::error!( + "The nogood {:?} is not unit-propagation consistent; truth values: {:?}", + self.nogood, + self.nogood + .iter() + .map(|&predicate| (predicate, domains.evaluate_predicate(predicate))) + .collect::>() + ); + } + + is_consistent + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::conjunction; + use crate::propagation::LocalId; + use crate::state::State; + + #[test] + fn a_nogood_with_multiple_untrue_predicates_is_consistent() { + let mut state = State::default(); + + let x = state.new_interval_variable(1, 5, Some("x".into())); + let y = state.new_interval_variable(1, 5, Some("y".into())); + + let mut checker = NogoodChecker { + nogood: conjunction!([x >= 4] & [y <= 2]).into(), + }; + + let scope = Scope::from_iter([(LocalId::from(0), x), (LocalId::from(1), y)]); + assert!(checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn a_nogood_with_one_untrue_predicates_and_no_false_predicates_is_inconsistent() { + let mut state = State::default(); + + let x = state.new_interval_variable(1, 5, Some("x".into())); + let y = state.new_interval_variable(1, 5, Some("y".into())); + + let mut checker = NogoodChecker { + nogood: conjunction!([x >= 4] & [y <= 5]).into(), + }; + + let scope = Scope::from_iter([(LocalId::from(0), x), (LocalId::from(1), y)]); + assert!(!checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn a_nogood_with_any_false_predicates_is_consistent() { + let mut state = State::default(); + + let x = state.new_interval_variable(1, 3, Some("x".into())); + let y = state.new_interval_variable(1, 5, Some("y".into())); + + let mut checker = NogoodChecker { + nogood: conjunction!([x >= 4] & [y <= 2]).into(), + }; + + let scope = Scope::from_iter([(LocalId::from(0), x), (LocalId::from(1), y)]); + assert!(checker.check_retention(&scope, state.get_domains())); + } +} + +/// The retention checker for extended nogood propagation: when the atomic constraints over all +/// but one variable hold, that variable has no value left that satisfies its atomic constraints. +#[derive(Debug, Clone)] +pub struct ExtendedNogoodChecker { + pub nogood: Box<[Predicate]>, +} + +impl RetentionChecker for ExtendedNogoodChecker { + fn check_retention(&mut self, _: &Scope, domains: Domains<'_>) -> bool { + // 1. Determine the variables with a predicate which is not true; if there are none then the + // nogood is conflicting + let free_domains = self + .nogood + .iter() + .filter(|&&predicate| domains.evaluate_predicate(predicate) != Some(true)) + .map(|predicate| predicate.get_domain()) + .collect::>(); + if free_domains.is_empty() { + log::error!( + "The nogood {:?} holds; it should have been reported as a conflict", + self.nogood + ); + return false; + } + + // 2. If predicates over at least two variables are not true then nothing can be propagated + let free_domain = free_domains[0]; + if free_domains.iter().any(|&domain| domain != free_domain) { + return true; + } + + // 3. Determine the values of the remaining variable which satisfy all of its predicates + let mut lower = domains.lower_bound(&free_domain); + let mut upper = domains.upper_bound(&free_domain); + let mut excluded: HashSet = domains.get_holes(&free_domain).collect(); + for predicate in self + .nogood + .iter() + .filter(|predicate| predicate.get_domain() == free_domain) + { + let value = predicate.get_right_hand_side(); + match predicate.get_predicate_type() { + PredicateType::LowerBound => lower = lower.max(value), + PredicateType::UpperBound => upper = upper.min(value), + PredicateType::NotEqual => { + let _ = excluded.insert(value); + } + PredicateType::Equal => { + lower = lower.max(value); + upper = upper.min(value); + } + } + } + + // 4. Assert that none of these values remain in the domain + let num_values = (i64::from(upper) - i64::from(lower) + 1).max(0); + let num_excluded = excluded + .iter() + .filter(|&&value| lower <= value && value <= upper) + .count() as i64; + let no_value_allowed = num_excluded == num_values; + + if !no_value_allowed { + log::error!( + "The values of {free_domain} in [{lower}, {upper}] could be removed by the nogood {:?}", + self.nogood + ); + } + + no_value_allowed + } +} + +#[cfg(test)] +mod extended_tests { + use super::*; + use crate::conjunction; + use crate::predicate; + use crate::propagation::LocalId; + use crate::state::State; + + #[test] + fn a_free_variable_with_allowed_values_is_not_consistent_under_extended_propagation() { + let mut state = State::default(); + let x = state.new_interval_variable(0, 10, Some("x".into())); + let y = state.new_interval_variable(1, 1, Some("y".into())); + let nogood: Box<[Predicate]> = conjunction!([x >= 3] & [x <= 5] & [y == 1]).into(); + let scope = Scope::from_iter([(LocalId::from(0), x), (LocalId::from(1), y)]); + + let mut extended = ExtendedNogoodChecker { + nogood: nogood.clone(), + }; + assert!(!extended.check_retention(&scope, state.get_domains())); + + // Unit propagation cannot fire with two atomic constraints over `x` unassigned. + let mut unit = NogoodChecker { nogood }; + assert!(unit.check_retention(&scope, state.get_domains())); + } + + #[test] + fn a_free_variable_without_allowed_values_is_consistent() { + let mut state = State::default(); + let x = state.new_interval_variable(0, 10, Some("x".into())); + let y = state.new_interval_variable(1, 1, Some("y".into())); + for value in 3..=5 { + let _ = state.post(predicate![x != value]).unwrap(); + } + + let mut checker = ExtendedNogoodChecker { + nogood: conjunction!([x >= 3] & [x <= 5] & [y == 1]).into(), + }; + let scope = Scope::from_iter([(LocalId::from(0), x), (LocalId::from(1), y)]); + + assert!(checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn two_free_variables_are_consistent() { + let mut state = State::default(); + let x = state.new_interval_variable(0, 10, Some("x".into())); + let y = state.new_interval_variable(0, 5, Some("y".into())); + + let mut checker = ExtendedNogoodChecker { + nogood: conjunction!([x >= 3] & [x <= 5] & [y == 1]).into(), + }; + let scope = Scope::from_iter([(LocalId::from(0), x), (LocalId::from(1), y)]); + + assert!(checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn a_nogood_that_holds_is_not_consistent() { + let mut state = State::default(); + let x = state.new_interval_variable(4, 4, Some("x".into())); + let y = state.new_interval_variable(1, 1, Some("y".into())); + + let mut checker = ExtendedNogoodChecker { + nogood: conjunction!([x >= 3] & [x <= 5] & [y == 1]).into(), + }; + let scope = Scope::from_iter([(LocalId::from(0), x), (LocalId::from(1), y)]); + + assert!(!checker.check_retention(&scope, state.get_domains())); + } +} diff --git a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs index 798cf0e67..5b9aed141 100644 --- a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs +++ b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs @@ -1,5 +1,11 @@ use std::cmp::max; use std::ops::Not; +#[cfg(feature = "check-consistency")] +use std::sync::Arc; +#[cfg(feature = "check-consistency")] +use std::sync::atomic::AtomicBool; +#[cfg(feature = "check-consistency")] +use std::sync::atomic::Ordering; use bitfield_struct::bitfield; use log::warn; @@ -9,6 +15,10 @@ use super::NogoodId; use super::NogoodInfo; use crate::basic_types::PredicateId; use crate::basic_types::PropositionalConjunction; +#[cfg(feature = "check-consistency")] +use crate::checkers::Scope; +#[cfg(feature = "check-consistency")] +use crate::checkers::SelfDisablingChecker; use crate::containers::HashSet; use crate::containers::KeyedVec; use crate::containers::StorageKey; @@ -91,6 +101,13 @@ pub struct NogoodPropagator { /// proapgated literal to see if this propagator propagated a predicate. #[allow(unused, reason = "Will be reintroduced with database management")] handle: PropagatorHandle, + + /// Flags shared with retention checkers to signal that a nogood has been deleted. + /// + /// When clause management deletes a nogood, the corresponding flag is set to `true`, causing + /// the checker to become a no-op. + #[cfg(feature = "check-consistency")] + deletion_flags: KeyedVec>, /// What form of propagation is performed (e.g., unit propagation, or extended nogood /// propagation). /// @@ -194,6 +211,8 @@ impl PropagatorConstructor for NogoodPropagatorConstructor { lbd_helper: Default::default(), bumped_nogoods: Default::default(), temp_nogood_reason: Default::default(), + #[cfg(feature = "check-consistency")] + deletion_flags: Default::default(), propagation_mode: self.propagation_mode, semantic_minimiser: Default::default(), priority: self.priority, @@ -1094,6 +1113,10 @@ impl NogoodPropagator { .propagation_mode .calculate_lbd(context, &nogood, &mut self.lbd_helper); + // Capture checker predicates before conversion to PredicateIds. + #[cfg(feature = "check-consistency")] + let checker_predicates: Box<[Predicate]> = nogood.clone().into(); + let nogood = nogood .iter() .map(|predicate| context.get_id(*predicate)) @@ -1108,6 +1131,9 @@ impl NogoodPropagator { .push(NogoodInfo::new_learned_nogood_info(lbd)); let _ = self.inference_codes.push(inference_code); + #[cfg(feature = "check-consistency")] + self.add_retention_checker(checker_predicates, context); + let watcher = Watcher { nogood_id, cached_predicate: self.nogood_predicates.get_nogood(nogood_id)[0], @@ -1270,6 +1296,9 @@ impl NogoodPropagator { // // The preprocessing ensures that all predicates are unassigned. else { + #[cfg(feature = "check-consistency")] + let num_nogoods_before = self.nogood_info.len(); + self.propagation_mode.add_permanent_nogood_non_unit( nogood, &input_nogood, @@ -1282,7 +1311,15 @@ impl NogoodPropagator { &mut self.permanent_nogood_ids, &self.statistics, &mut self.propagation_buffer, - ) + ); + + // The retention checker is only registered when the nogood was actually stored: + // extended nogood propagation buffers nogoods over a single domain instead. The + // deletion flags must stay index-aligned with `nogood_info`. + #[cfg(feature = "check-consistency")] + if self.nogood_info.len() > num_nogoods_before { + self.add_retention_checker(input_nogood.into(), context); + } } } } @@ -1367,6 +1404,69 @@ fn get_domain_info( ) } +impl NogoodPropagator { + /// Add a retention checker for the given nogood predicates. + #[cfg(feature = "check-consistency")] + fn add_retention_checker( + &mut self, + nogood: Box<[Predicate]>, + context: &mut PropagationContext, + ) { + let scope = build_nogood_scope(&nogood); + match self.propagation_mode { + PropagationMode::UnitPropagation => { + let checker = SelfDisablingChecker::new(super::NogoodChecker { nogood }); + let _ = self.deletion_flags.push(checker.deletion_flag()); + context.add_retention_checker(scope, checker); + } + PropagationMode::ExtendedNogoodPropagation => { + let checker = SelfDisablingChecker::new(super::ExtendedNogoodChecker { nogood }); + let _ = self.deletion_flags.push(checker.deletion_flag()); + context.add_retention_checker(scope, checker); + } + } + } +} + +/// Build a [`Scope`] for a nogood by extracting unique [`DomainId`]s from its predicates. +/// +/// Avoids multiple enqueuing of the retention checker if the nogood contains multiple +/// predicates over the same variable. +#[cfg(feature = "check-consistency")] +fn build_nogood_scope(predicates: &[Predicate]) -> Scope { + use crate::containers::HashSet; + use crate::containers::KeyGenerator; + use crate::variables::DomainId; + + let mut scope = Scope::default(); + let mut seen: HashSet = HashSet::default(); + let mut id_generator = KeyGenerator::default(); + + for predicate in predicates { + let domain = predicate.get_domain(); + if seen.insert(domain) { + scope.add_domain(id_generator.next_key(), domain); + } + } + + scope +} + +#[cfg(feature = "check-consistency")] +impl NogoodPropagator { + /// Set the deletion flag for every nogood that has been marked as deleted in `nogood_info`. + /// + /// Called after clause management removes nogoods so that retention checkers self-disable. + fn signal_deleted_checker_flags(&self) { + for idx in 0..self.nogood_info.len() { + let idx = NogoodIndex::create_from_index(idx); + if self.nogood_info[idx].is_deleted { + self.deletion_flags[idx].store(true, Ordering::Relaxed); + } + } + } +} + /// Methods concerning the watchers and watch lists impl NogoodPropagator { /// Adds a watcher to the predicate. @@ -1515,6 +1615,8 @@ impl NogoodPropagator { } if removed_at_least_one_nogood { + #[cfg(feature = "check-consistency")] + self.signal_deleted_checker_flags(); self.remove_deleted_nogoods_from_watchers(assignments, notification_engine); } } diff --git a/pumpkin-crates/core/src/propagators/reified_propagator/checker.rs b/pumpkin-crates/core/src/propagators/reified_propagator/checker.rs new file mode 100644 index 000000000..2e5055837 --- /dev/null +++ b/pumpkin-crates/core/src/propagators/reified_propagator/checker.rs @@ -0,0 +1,68 @@ +use pumpkin_checking::AtomicConstraint; +use pumpkin_checking::BoxedChecker; +use pumpkin_checking::CheckerVariable; +use pumpkin_checking::InferenceChecker; +use pumpkin_checking::VariableState; + +use crate::checkers::BoxedRetentionChecker; +use crate::checkers::RetentionChecker; +use crate::checkers::Scope; +use crate::propagation::Domains; +use crate::propagation::LocalId; +use crate::propagation::ReadDomains; +use crate::variables::Literal; + +/// A [`RetentionChecker`] wrapper that skips the inner check when the reification literal is +/// not assigned to true. +#[derive(Debug, Clone)] +pub struct ReifiedRetentionChecker { + pub inner: BoxedRetentionChecker, + pub reification_literal: Literal, + /// The [`LocalId`] of the reification literal in the scope, used to strip it before passing + /// the scope to the inner checker. + pub reification_literal_id: LocalId, +} + +impl RetentionChecker for ReifiedRetentionChecker { + fn check_retention(&mut self, scope: &Scope, domains: Domains<'_>) -> bool { + if domains.evaluate_literal(self.reification_literal) != Some(true) { + return true; + } + + let inner_scope = scope.without(self.reification_literal_id); + self.inner.check_retention(&inner_scope, domains) + } +} + +#[derive(Debug, Clone)] +pub struct ReifiedChecker { + pub inner: BoxedChecker, + pub reification_literal: Var, +} + +impl InferenceChecker for ReifiedChecker +where + Atomic: AtomicConstraint + Clone, + Var: CheckerVariable, +{ + fn check( + &self, + state: VariableState, + premises: &[Atomic], + consequent: Option<&Atomic>, + ) -> bool { + if self.reification_literal.induced_domain_contains(&state, 0) { + return false; + } + + if let Some(consequent) = consequent + && self + .reification_literal + .does_atomic_constrain_self(consequent) + { + self.inner.check(state, premises, None) + } else { + self.inner.check(state, premises, consequent) + } + } +} diff --git a/pumpkin-crates/core/src/propagators/reified_propagator/constructor.rs b/pumpkin-crates/core/src/propagators/reified_propagator/constructor.rs new file mode 100644 index 000000000..0f9818d89 --- /dev/null +++ b/pumpkin-crates/core/src/propagators/reified_propagator/constructor.rs @@ -0,0 +1,101 @@ +use crate::checkers::ScopeItem; +use crate::propagation::DomainEvents; +use crate::propagation::Propagator; +use crate::propagation::PropagatorConstructor; +use crate::propagation::PropagatorConstructorContext; +use crate::propagation::PropagatorSpec; +use crate::propagation::RuntimeCheckers; +use crate::propagators::ReifiedChecker; +use crate::propagators::ReifiedPropagator; +use crate::propagators::ReifiedRetentionChecker; +use crate::variables::Literal; + +/// A [`PropagatorConstructor`] for the reified propagator. +#[derive(Clone, Debug)] +pub struct ReifiedPropagatorArgs { + pub propagator: WrappedArgs, + pub reification_literal: Literal, +} + +impl PropagatorConstructor for ReifiedPropagatorArgs +where + WrappedArgs: PropagatorConstructor, + WrappedPropagator: Propagator + Clone, +{ + type PropagatorImpl = ReifiedPropagator; + + fn create( + self, + mut context: PropagatorConstructorContext, + ) -> PropagatorSpec { + let ReifiedPropagatorArgs { + propagator, + reification_literal, + } = self; + + let PropagatorSpec { + mut registration, + propagator, + checkers, + } = propagator.create(context.reborrow()); + + // The local ID for the reification literal will be one larger than the largest ID + // registered by the wrapped propagator. + let reification_literal_id = registration + .iter() + .map(|(_, _, lid)| lid) + .max() + .expect("cannot reify propagators that do not register all variables immediately") + .successor(); + + registration.add( + &reification_literal, + DomainEvents::BOUNDS, + reification_literal_id, + ); + + let (inference_checkers, retention_checkers) = checkers.into_parts(); + + let mut wrapped_checkers = RuntimeCheckers::empty(); + for (inference_code, checker) in inference_checkers { + let _ = wrapped_checkers.add_inference_checker( + inference_code.tag(), + inference_code.label(), + ReifiedChecker { + inner: checker, + reification_literal, + }, + ); + } + + // The reification literal becomes part of the scope of every wrapped retention checker, + // since whether the wrapped constraint has to hold depends on it. + for (mut scope, checker) in retention_checkers { + reification_literal.add_to_scope(&mut scope, reification_literal_id); + wrapped_checkers.add_retention_checker( + scope, + ReifiedRetentionChecker { + inner: checker, + reification_literal, + reification_literal_id, + }, + ); + } + + let name = format!("Reified({})", propagator.name()); + + let propagator = ReifiedPropagator { + propagator, + reification_literal, + reification_literal_id, + name, + reason_buffer: vec![], + }; + + PropagatorSpec { + registration, + checkers: wrapped_checkers, + propagator, + } + } +} diff --git a/pumpkin-crates/core/src/propagators/reified_propagator/mod.rs b/pumpkin-crates/core/src/propagators/reified_propagator/mod.rs new file mode 100644 index 000000000..550564f93 --- /dev/null +++ b/pumpkin-crates/core/src/propagators/reified_propagator/mod.rs @@ -0,0 +1,7 @@ +mod checker; +mod constructor; +mod propagator; + +pub use checker::*; +pub use constructor::*; +pub use propagator::*; diff --git a/pumpkin-crates/core/src/propagators/reified_propagator.rs b/pumpkin-crates/core/src/propagators/reified_propagator/propagator.rs similarity index 80% rename from pumpkin-crates/core/src/propagators/reified_propagator.rs rename to pumpkin-crates/core/src/propagators/reified_propagator/propagator.rs index d9cd5b0fe..086649e3a 100644 --- a/pumpkin-crates/core/src/propagators/reified_propagator.rs +++ b/pumpkin-crates/core/src/propagators/reified_propagator/propagator.rs @@ -1,12 +1,6 @@ -use pumpkin_checking::AtomicConstraint; -use pumpkin_checking::BoxedChecker; -use pumpkin_checking::CheckerVariable; -use pumpkin_checking::InferenceChecker; - use crate::engine::PropagationStatusCP; use crate::engine::notifications::OpaqueDomainEvent; use crate::predicates::Predicate; -use crate::propagation::DomainEvents; use crate::propagation::Domains; use crate::propagation::EnqueueDecision; use crate::propagation::ExplanationContext; @@ -16,89 +10,11 @@ use crate::propagation::NotificationContext; use crate::propagation::Priority; use crate::propagation::PropagationContext; use crate::propagation::Propagator; -use crate::propagation::PropagatorConstructor; -use crate::propagation::PropagatorConstructorContext; -use crate::propagation::PropagatorSpec; use crate::propagation::ReadDomains; -use crate::propagation::RuntimeCheckers; use crate::pumpkin_assert_simple; use crate::state::Conflict; use crate::variables::Literal; -/// A [`PropagatorConstructor`] for the reified propagator. -#[derive(Clone, Debug)] -pub struct ReifiedPropagatorArgs { - pub propagator: WrappedArgs, - pub reification_literal: Literal, -} - -impl PropagatorConstructor for ReifiedPropagatorArgs -where - WrappedArgs: PropagatorConstructor, - WrappedPropagator: Propagator + Clone, -{ - type PropagatorImpl = ReifiedPropagator; - - fn create( - self, - mut context: PropagatorConstructorContext, - ) -> PropagatorSpec { - let ReifiedPropagatorArgs { - propagator, - reification_literal, - } = self; - - let PropagatorSpec { - mut registration, - propagator, - checkers, - } = propagator.create(context.reborrow()); - - // The local ID for the reification literal will be one larger than the largest ID - // registered by the wrapped propagator. - let reification_literal_id = registration - .iter() - .map(|(_, _, lid)| lid) - .max() - .expect("cannot reify propagators that do not register all variables immediately") - .successor(); - - registration.add( - &self.reification_literal, - DomainEvents::BOUNDS, - reification_literal_id, - ); - - let mut wrapped_checkers = RuntimeCheckers::empty(); - for (inference_code, checker) in checkers.into_iter() { - let _ = wrapped_checkers.add_inference_checker( - inference_code.tag(), - inference_code.label(), - ReifiedChecker { - inner: checker, - reification_literal, - }, - ); - } - - let name = format!("Reified({})", propagator.name()); - - let propagator = ReifiedPropagator { - propagator, - reification_literal, - reification_literal_id, - name, - reason_buffer: vec![], - }; - - PropagatorSpec { - registration, - checkers: wrapped_checkers, - propagator, - } - } -} - /// Propagator for the constraint `r -> p`, where `r` is a Boolean literal and `p` is an arbitrary /// propagator. /// @@ -108,16 +24,16 @@ where /// propagated to false. #[derive(Clone, Debug)] pub struct ReifiedPropagator { - propagator: WrappedPropagator, - reification_literal: Literal, + pub(super) propagator: WrappedPropagator, + pub(super) reification_literal: Literal, /// The formatted name of the propagator. - name: String, + pub(super) name: String, /// The `LocalId` of the reification literal. Is guaranteed to be a larger ID than any of the /// registered ids of the wrapped propagator. - reification_literal_id: LocalId, + pub(super) reification_literal_id: LocalId, /// Holds the lazy explanations. - reason_buffer: Vec, + pub(super) reason_buffer: Vec, } impl Propagator for ReifiedPropagator { @@ -259,37 +175,6 @@ impl ReifiedPropagator { } } -#[derive(Debug, Clone)] -pub struct ReifiedChecker { - pub inner: BoxedChecker, - pub reification_literal: Var, -} - -impl> InferenceChecker - for ReifiedChecker -{ - fn check( - &self, - state: pumpkin_checking::VariableState, - premises: &[Atomic], - consequent: Option<&Atomic>, - ) -> bool { - if self.reification_literal.induced_domain_contains(&state, 0) { - return false; - } - - if let Some(consequent) = consequent - && self - .reification_literal - .does_atomic_constrain_self(consequent) - { - self.inner.check(state, premises, None) - } else { - self.inner.check(state, premises, consequent) - } - } -} - #[allow(deprecated, reason = "Will be refactored")] #[cfg(test)] mod tests { @@ -303,7 +188,13 @@ mod tests { use crate::proof::ConstraintTag; use crate::proof::InferenceCode; use crate::proof::Unknown; + use crate::propagation::DomainEvents; use crate::propagation::EventsToRegister; + use crate::propagation::PropagatorConstructor; + use crate::propagation::PropagatorConstructorContext; + use crate::propagation::PropagatorSpec; + use crate::propagation::RuntimeCheckers; + use crate::propagators::ReifiedPropagatorArgs; use crate::variables::DomainId; #[test] diff --git a/pumpkin-crates/propagators/Cargo.toml b/pumpkin-crates/propagators/Cargo.toml index 63eda94db..d4ab5be5f 100644 --- a/pumpkin-crates/propagators/Cargo.toml +++ b/pumpkin-crates/propagators/Cargo.toml @@ -11,6 +11,7 @@ description = "The propagators of the Pumpkin constraint programming solver." workspace = true [dependencies] +log = "0.4.30" pumpkin-core = { version = "0.5.0", path = "../core" } pumpkin-checking = { version = "0.5.0", path = "../checking" } enumset = "1.1.13" diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs index ef27dfe70..670623949 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs @@ -2,12 +2,15 @@ use pumpkin_checking::AtomicConstraint; use pumpkin_checking::CheckerVariable; use pumpkin_checking::InferenceChecker; use pumpkin_checking::IntExt; +use pumpkin_core::checkers::RetentionChecker; +use pumpkin_core::checkers::Scope; use pumpkin_core::conjunction; use pumpkin_core::declare_inference_label; 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::EventsToRegister; use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::Priority; @@ -50,7 +53,8 @@ where .build(); let mut checkers = RuntimeCheckers::builder(); - let inference_code = checkers.add_inference_checker( + let inference_code = checkers.add_rule( + ((LocalId::from(0), &signed), (LocalId::from(1), &absolute)), constraint_tag, AbsoluteValue, AbsoluteValueChecker { @@ -226,6 +230,71 @@ where } } +impl RetentionChecker for AbsoluteValueChecker +where + VA: IntegerVariable + 'static, + VB: IntegerVariable + 'static, +{ + fn check_retention(&mut self, _: &Scope, domains: Domains<'_>) -> bool { + let signed_lower = i64::from(domains.lower_bound(&self.signed)); + let signed_upper = i64::from(domains.upper_bound(&self.signed)); + let absolute_lower = i64::from(domains.lower_bound(&self.absolute)); + let absolute_upper = i64::from(domains.upper_bound(&self.absolute)); + + let greatest_absolute = signed_lower.abs().max(signed_upper.abs()); + let least_absolute = if signed_lower <= 0 && 0 <= signed_upper { + 0 + } else { + signed_lower.abs().min(signed_upper.abs()) + }; + + // 1. Assert that the lower bound of absolute is at least the least absolute value of + // signed, which is 0 when signed can be 0 + if absolute_lower < least_absolute { + log::error!( + "The lower bound of {:?} could be raised to {least_absolute} by the absolute value of {:?}", + self.absolute, + self.signed + ); + return false; + } + + // 2. Assert that the upper bound of absolute equals the greatest absolute value of signed + // The bounds of signed lie within [-ub(absolute), ub(absolute)] at the same time. + if absolute_upper != greatest_absolute { + log::error!( + "The upper bound of {:?} is {absolute_upper} while the greatest absolute value of {:?} is {greatest_absolute}", + self.absolute, + self.signed + ); + return false; + } + + // 3. Assert that the bound of signed nearest to zero is at least the lower bound of + // absolute in magnitude when the sign of signed is fixed + // When signed can be 0, the propagator does not remove the values nearest to zero. + if signed_upper <= 0 && -signed_upper < absolute_lower { + log::error!( + "The upper bound of {:?} could be lowered to {} by the lower bound of {:?}", + self.signed, + -absolute_lower, + self.absolute + ); + return false; + } + if signed_lower >= 0 && signed_lower < absolute_lower { + log::error!( + "The lower bound of {:?} could be raised to {absolute_lower} by the lower bound of {:?}", + self.signed, + self.absolute + ); + return false; + } + + true + } +} + #[cfg(test)] mod tests { use pumpkin_core::state::State; @@ -341,3 +410,66 @@ mod tests { state.assert_bounds(signed, 3, 5); } } + +#[cfg(test)] +mod retention_tests { + use pumpkin_core::state::State; + + use super::*; + + #[test] + fn retention_fails_when_the_upper_bound_of_absolute_exceeds_the_greatest_absolute_value() { + let mut state = State::default(); + let signed = state.new_interval_variable(-3, 5, None); + let absolute = state.new_interval_variable(0, 10, None); + + let mut checker = AbsoluteValueChecker { signed, absolute }; + let scope = Scope::from_variables([signed, absolute].iter()); + + assert!(!checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn retention_fails_when_the_lower_bound_of_absolute_is_below_the_least_absolute_value() { + let mut state = State::default(); + let signed = state.new_interval_variable(2, 5, None); + let absolute = state.new_interval_variable(0, 5, None); + + let mut checker = AbsoluteValueChecker { signed, absolute }; + let scope = Scope::from_variables([signed, absolute].iter()); + + assert!(!checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn retention_fails_when_a_sign_fixed_signed_reaches_below_the_lower_bound_of_absolute() { + let mut state = State::default(); + let signed = state.new_interval_variable(-5, -1, None); + let absolute = state.new_interval_variable(3, 5, None); + + let mut checker = AbsoluteValueChecker { signed, absolute }; + let scope = Scope::from_variables([signed, absolute].iter()); + + assert!(!checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn retention_holds_at_the_fixpoint_of_the_propagator() { + let mut state = State::default(); + let signed = state.new_interval_variable(-3, 5, None); + let absolute = state.new_interval_variable(0, 10, None); + let constraint_tag = state.new_constraint_tag(); + + let _ = state.add_propagator(AbsoluteValueArgs { + signed, + absolute, + constraint_tag, + }); + state.propagate_to_fixed_point().expect("no empty domains"); + + let mut checker = AbsoluteValueChecker { signed, absolute }; + let scope = Scope::from_variables([signed, absolute].iter()); + + assert!(checker.check_retention(&scope, state.get_domains())); + } +} 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 c9bde00eb..2c19a7005 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 @@ -1,6 +1,8 @@ use pumpkin_checking::AtomicConstraint; use pumpkin_checking::CheckerVariable; use pumpkin_checking::InferenceChecker; +use pumpkin_core::checkers::RetentionChecker; +use pumpkin_core::checkers::Scope; use pumpkin_core::conjunction; use pumpkin_core::declare_inference_label; use pumpkin_core::predicate; @@ -53,7 +55,8 @@ where .build(); let mut checkers = RuntimeCheckers::builder(); - let inference_code = checkers.add_inference_checker( + let inference_code = checkers.add_rule( + ((LocalId::from(0), &a), (LocalId::from(1), &b)), constraint_tag, BinaryNotEquals, BinaryNotEqualsChecker { @@ -208,6 +211,57 @@ where } } +impl RetentionChecker for BinaryNotEqualsChecker +where + Lhs: IntegerVariable + 'static, + Rhs: IntegerVariable + 'static, +{ + fn check_retention(&mut self, _: &Scope, domains: Domains<'_>) -> bool { + match ( + domains.fixed_value(&self.lhs), + domains.fixed_value(&self.rhs), + ) { + (Some(lhs), Some(rhs)) => { + // 1. Both sides are fixed: check that the constraint is not conflicting + if lhs == rhs { + log::error!( + "{:?} and {:?} are both fixed to {lhs}; the disequality is violated", + self.lhs, + self.rhs + ); + } + lhs != rhs + } + (Some(value), None) => { + // 2. One side is fixed: assert that its value is removed from the other side + let is_removed = !domains.contains(&self.rhs, value); + if !is_removed { + log::error!( + "The value {value} could be removed from {:?} since {:?} is fixed to it", + self.rhs, + self.lhs + ); + } + is_removed + } + (None, Some(value)) => { + // 2. One side is fixed: assert that its value is removed from the other side + let is_removed = !domains.contains(&self.lhs, value); + if !is_removed { + log::error!( + "The value {value} could be removed from {:?} since {:?} is fixed to it", + self.lhs, + self.rhs + ); + } + is_removed + } + // 3. Neither side is fixed: nothing can be propagated + (None, None) => true, + } + } +} + #[cfg(test)] mod tests { use pumpkin_core::state::State; @@ -302,3 +356,54 @@ mod tests { state.assert_bounds(b, 6, 10); } } + +#[cfg(test)] +mod retention_tests { + use pumpkin_core::state::State; + + use super::*; + + #[test] + fn retention_fails_when_the_fixed_value_is_present_in_the_other_domain() { + let mut state = State::default(); + let a = state.new_interval_variable(3, 3, None); + let b = state.new_interval_variable(0, 5, None); + + let mut checker = BinaryNotEqualsChecker { lhs: a, rhs: b }; + let scope = Scope::from_variables([a, b].iter()); + + assert!(!checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn retention_holds_with_both_sides_unfixed() { + let mut state = State::default(); + let a = state.new_interval_variable(0, 5, None); + let b = state.new_interval_variable(0, 5, None); + + let mut checker = BinaryNotEqualsChecker { lhs: a, rhs: b }; + let scope = Scope::from_variables([a, b].iter()); + + assert!(checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn retention_holds_at_the_fixpoint_of_the_propagator() { + let mut state = State::default(); + let a = state.new_interval_variable(3, 3, None); + let b = state.new_interval_variable(0, 5, None); + let constraint_tag = state.new_constraint_tag(); + + let _ = state.add_propagator(BinaryNotEqualsPropagatorArgs { + a, + b, + constraint_tag, + }); + state.propagate_to_fixed_point().expect("no empty domains"); + + let mut checker = BinaryNotEqualsChecker { lhs: a, rhs: b }; + let scope = Scope::from_variables([a, b].iter()); + + assert!(checker.check_retention(&scope, state.get_domains())); + } +} diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/mod.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/mod.rs index 8d3c6bbb8..39cfb5e78 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/mod.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/mod.rs @@ -1,5 +1,3 @@ -pub(crate) mod binary_equals; pub(crate) mod binary_not_equals; -pub use binary_equals::*; pub use binary_not_equals::*; diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary_equals/checker.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary_equals/checker.rs new file mode 100644 index 000000000..3a6ac7d0f --- /dev/null +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary_equals/checker.rs @@ -0,0 +1,164 @@ +use std::collections::BTreeSet; + +use pumpkin_checking::AtomicConstraint; +use pumpkin_checking::CheckerVariable; +use pumpkin_checking::InferenceChecker; +use pumpkin_checking::IntExt; +use pumpkin_core::checkers::RetentionChecker; +use pumpkin_core::checkers::Scope; +use pumpkin_core::propagation::Domains; +use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::variables::IntegerVariable; + +#[derive(Clone, Debug)] +pub struct BinaryEqualsChecker { + pub lhs: Lhs, + pub rhs: Rhs, +} + +impl InferenceChecker for BinaryEqualsChecker +where + Atomic: AtomicConstraint, + Lhs: CheckerVariable, + Rhs: CheckerVariable, +{ + fn check( + &self, + mut state: pumpkin_checking::VariableState, + _: &[Atomic], + _: Option<&Atomic>, + ) -> bool { + // We apply the domain of variable 2 to variable 1. If the state remains consistent, then + // the step is unsound! + let mut consistent = true; + + if let IntExt::Int(value) = self.rhs.induced_upper_bound(&state) { + let atomic = self.lhs.atomic_less_than(value); + consistent &= state.apply(&atomic); + } + + if let IntExt::Int(value) = self.rhs.induced_lower_bound(&state) { + let atomic = self.lhs.atomic_greater_than(value); + consistent &= state.apply(&atomic); + } + + for value in self.rhs.induced_holes(&state).collect::>() { + let atomic = self.lhs.atomic_not_equal(value); + consistent &= state.apply(&atomic); + } + + !consistent + } +} + +impl RetentionChecker for BinaryEqualsChecker +where + Lhs: IntegerVariable + 'static, + Rhs: IntegerVariable + 'static, +{ + fn check_retention(&mut self, _: &Scope, domains: Domains<'_>) -> bool { + // 1. Assert that the bounds are equal + let lower = domains.lower_bound(&self.lhs); + let upper = domains.upper_bound(&self.lhs); + let same_bounds = + lower == domains.lower_bound(&self.rhs) && upper == domains.upper_bound(&self.rhs); + // 2. Assert that the holes within the bounds are equal + // A domain may record holes outside its bounds, so only those within the shared bounds + // are compared. + let are_equal = same_bounds + && holes_within(&domains, &self.lhs, lower, upper) + == holes_within(&domains, &self.rhs, lower, upper); + + if !are_equal { + log::error!( + "The domains of {:?} and {:?} differ although the two are equal: {:?} and {:?}", + self.lhs, + self.rhs, + domains.iterate_domain(&self.lhs).collect::>(), + domains.iterate_domain(&self.rhs).collect::>() + ); + } + + are_equal + } +} + +fn holes_within( + domains: &Domains<'_>, + variable: &Var, + lower: i32, + upper: i32, +) -> BTreeSet { + domains + .get_holes(variable) + .filter(|&value| lower <= value && value <= upper) + .collect() +} + +#[cfg(test)] +mod retention_tests { + use pumpkin_core::predicate; + use pumpkin_core::state::State; + + use super::*; + use crate::arithmetic::BinaryEqualsPropagatorArgs; + + #[test] + fn retention_fails_when_the_bounds_differ() { + let mut state = State::default(); + let a = state.new_interval_variable(0, 5, None); + let b = state.new_interval_variable(3, 8, None); + + let mut checker = BinaryEqualsChecker { lhs: a, rhs: b }; + let scope = Scope::from_variables([a, b].iter()); + + assert!(!checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn retention_fails_when_a_hole_is_not_shared() { + let mut state = State::default(); + let a = state.new_interval_variable(0, 5, None); + let b = state.new_interval_variable(0, 5, None); + let _ = state.post(predicate![a != 2]).unwrap(); + + let mut checker = BinaryEqualsChecker { lhs: a, rhs: b }; + let scope = Scope::from_variables([a, b].iter()); + + assert!(!checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn retention_holds_when_the_domains_agree_but_the_recorded_holes_differ() { + let mut state = State::default(); + let a = state.new_interval_variable(1, 3, None); + let b = state.new_interval_variable(3, 3, None); + let _ = state.post(predicate![a != 1]).unwrap(); + let _ = state.post(predicate![a != 2]).unwrap(); + + let mut checker = BinaryEqualsChecker { lhs: a, rhs: b }; + let scope = Scope::from_variables([a, b].iter()); + + assert!(checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn retention_holds_at_the_fixpoint_of_the_propagator() { + let mut state = State::default(); + let a = state.new_interval_variable(0, 5, None); + let b = state.new_interval_variable(3, 8, None); + let constraint_tag = state.new_constraint_tag(); + + let _ = state.add_propagator(BinaryEqualsPropagatorArgs { + a, + b, + constraint_tag, + }); + state.propagate_to_fixed_point().expect("no empty domains"); + + let mut checker = BinaryEqualsChecker { lhs: a, rhs: b }; + let scope = Scope::from_variables([a, b].iter()); + + assert!(checker.check_retention(&scope, state.get_domains())); + } +} diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary_equals/constructor.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary_equals/constructor.rs new file mode 100644 index 000000000..04ad0a736 --- /dev/null +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary_equals/constructor.rs @@ -0,0 +1,73 @@ +use pumpkin_core::containers::HashSet; +use pumpkin_core::predicates::Predicate; +use pumpkin_core::proof::ConstraintTag; +use pumpkin_core::propagation::DomainEvents; +use pumpkin_core::propagation::EventsToRegister; +use pumpkin_core::propagation::PropagatorConstructor; +use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::PropagatorSpec; +use pumpkin_core::propagation::RuntimeCheckers; +use pumpkin_core::variables::IntegerVariable; + +use crate::arithmetic::BinaryEqualsChecker; +use crate::arithmetic::BinaryEqualsPropagator; + +/// The [`PropagatorConstructor`] for the [`BinaryEqualsPropagator`]. +#[derive(Clone, Debug)] +pub struct BinaryEqualsPropagatorArgs { + pub a: AVar, + pub b: BVar, + pub constraint_tag: ConstraintTag, +} + +impl PropagatorConstructor for BinaryEqualsPropagatorArgs +where + AVar: IntegerVariable + 'static, + BVar: IntegerVariable + 'static, +{ + type PropagatorImpl = BinaryEqualsPropagator; + + fn create(self, _: PropagatorConstructorContext) -> PropagatorSpec { + let BinaryEqualsPropagatorArgs { + a, + b, + constraint_tag, + } = self; + + let registration = EventsToRegister::builder() + .add(&a, DomainEvents::ANY_INT, super::ID_LHS) + .add(&b, DomainEvents::ANY_INT, super::ID_RHS) + .build(); + + let mut checkers = RuntimeCheckers::builder(); + let inference_code = checkers.add_rule( + ((super::ID_LHS, &a), (super::ID_RHS, &b)), + constraint_tag, + super::BinaryEquals, + BinaryEqualsChecker { + lhs: a.clone(), + rhs: b.clone(), + }, + ); + + let propagator = BinaryEqualsPropagator { + a, + b, + + a_removed_values: HashSet::default(), + b_removed_values: HashSet::default(), + + inference_code, + + has_backtracked: false, + first_propagation_loop: true, + reason: Predicate::trivially_false(), + }; + + PropagatorSpec { + registration, + checkers: checkers.build(), + propagator, + } + } +} diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary_equals/mod.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary_equals/mod.rs new file mode 100644 index 000000000..bc6e585ef --- /dev/null +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary_equals/mod.rs @@ -0,0 +1,14 @@ +mod checker; +mod constructor; +mod propagator; + +pub use checker::*; +pub use constructor::*; +pub use propagator::*; +use pumpkin_core::declare_inference_label; +use pumpkin_core::propagation::LocalId; + +const ID_LHS: LocalId = LocalId::from(0); +const ID_RHS: LocalId = LocalId::from(1); + +declare_inference_label!(BinaryEquals); diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary_equals/propagator.rs similarity index 80% rename from pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs rename to pumpkin-crates/propagators/src/propagators/arithmetic/binary_equals/propagator.rs index 565ce762c..166af6a37 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary_equals/propagator.rs @@ -2,25 +2,17 @@ use std::slice; use bitfield_struct::bitfield; -use pumpkin_checking::AtomicConstraint; -use pumpkin_checking::CheckerVariable; -use pumpkin_checking::InferenceChecker; -use pumpkin_checking::IntExt; use pumpkin_core::asserts::pumpkin_assert_advanced; use pumpkin_core::conjunction; use pumpkin_core::containers::HashSet; -use pumpkin_core::declare_inference_label; use pumpkin_core::predicate; use pumpkin_core::predicates::Predicate; use pumpkin_core::predicates::PredicateConstructor; use pumpkin_core::predicates::PredicateType; -use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; use pumpkin_core::propagation::DomainEvent; -use pumpkin_core::propagation::DomainEvents; use pumpkin_core::propagation::Domains; use pumpkin_core::propagation::EnqueueDecision; -use pumpkin_core::propagation::EventsToRegister; use pumpkin_core::propagation::ExplanationContext; use pumpkin_core::propagation::LazyExplanation; use pumpkin_core::propagation::LocalId; @@ -29,109 +21,44 @@ use pumpkin_core::propagation::OpaqueDomainEvent; use pumpkin_core::propagation::Priority; use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; -use pumpkin_core::propagation::PropagatorConstructor; -use pumpkin_core::propagation::PropagatorConstructorContext; -use pumpkin_core::propagation::PropagatorSpec; use pumpkin_core::propagation::ReadDomains; -use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::EmptyDomainConflict; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::state::PropagatorConflict; use pumpkin_core::variables::IntegerVariable; -declare_inference_label!(BinaryEquals); - -/// The [`PropagatorConstructor`] for the [`BinaryEqualsPropagator`]. -#[derive(Clone, Debug)] -pub struct BinaryEqualsPropagatorArgs { - pub a: AVar, - pub b: BVar, - pub constraint_tag: ConstraintTag, -} - -impl PropagatorConstructor for BinaryEqualsPropagatorArgs -where - AVar: IntegerVariable + 'static, - BVar: IntegerVariable + 'static, -{ - type PropagatorImpl = BinaryEqualsPropagator; - - fn create(self, _: PropagatorConstructorContext) -> PropagatorSpec { - let BinaryEqualsPropagatorArgs { - a, - b, - constraint_tag, - } = self; - - let registration = EventsToRegister::builder() - .add(&a, DomainEvents::ANY_INT, LocalId::from(0)) - .add(&b, DomainEvents::ANY_INT, LocalId::from(1)) - .build(); - - let mut checkers = RuntimeCheckers::builder(); - let inference_code = checkers.add_inference_checker( - constraint_tag, - BinaryEquals, - BinaryEqualsChecker { - lhs: a.clone(), - rhs: b.clone(), - }, - ); - - let propagator = BinaryEqualsPropagator { - a, - b, - - a_removed_values: HashSet::default(), - b_removed_values: HashSet::default(), - - inference_code, - - has_backtracked: false, - first_propagation_loop: true, - reason: Predicate::trivially_false(), - }; - - PropagatorSpec { - registration, - checkers: checkers.build(), - propagator, - } - } -} - /// Propagator for the constraint `a = b`. #[derive(Clone, Debug)] pub struct BinaryEqualsPropagator { - a: AVar, - b: BVar, + pub(super) a: AVar, + pub(super) b: BVar, /// The removed value from [`Self::a`]. /// /// These are tracked to make sure that they are also removed from [`Self::b`]. - a_removed_values: HashSet, + pub(super) a_removed_values: HashSet, /// The removed value from [`Self::b`] /// /// These are tracked to make sure that they are also removed from [`Self::a`]. - b_removed_values: HashSet, + pub(super) b_removed_values: HashSet, /// If a backtrack has occurred which caused one of the removals to be backtracked then we need /// to ensure that we do not erroneously remove values which are now part of the domain after /// backtracking. - has_backtracked: bool, + pub(super) has_backtracked: bool, /// If it is the first time that the propagator is called then we need to ensure that the /// domains of [`Self::a`] and [`Self::b`] are equal to the intersection of these domains. - first_propagation_loop: bool, + pub(super) first_propagation_loop: bool, - inference_code: InferenceCode, + pub(super) inference_code: InferenceCode, /// A re-usable buffer to store the explanations of propagations. This will always be a single /// [`Predicate`]. /// /// This field is only written to in the `lazy_explanation` function, as that returns a slice /// which needs to be owned somewhere. Hence we put that ownership here. - reason: Predicate, + pub(super) reason: Predicate, } impl BinaryEqualsPropagator @@ -411,47 +338,6 @@ struct BinaryEqualsPropagation { __: u16, } -#[derive(Clone, Debug)] -pub struct BinaryEqualsChecker { - pub lhs: Lhs, - pub rhs: Rhs, -} - -impl InferenceChecker for BinaryEqualsChecker -where - Atomic: AtomicConstraint, - Lhs: CheckerVariable, - Rhs: CheckerVariable, -{ - fn check( - &self, - mut state: pumpkin_checking::VariableState, - _: &[Atomic], - _: Option<&Atomic>, - ) -> bool { - // We apply the domain of variable 2 to variable 1. If the state remains consistent, then - // the step is unsound! - let mut consistent = true; - - if let IntExt::Int(value) = self.rhs.induced_upper_bound(&state) { - let atomic = self.lhs.atomic_less_than(value); - consistent &= state.apply(&atomic); - } - - if let IntExt::Int(value) = self.rhs.induced_lower_bound(&state) { - let atomic = self.lhs.atomic_greater_than(value); - consistent &= state.apply(&atomic); - } - - for value in self.rhs.induced_holes(&state).collect::>() { - let atomic = self.lhs.atomic_not_equal(value); - consistent &= state.apply(&atomic); - } - - !consistent - } -} - #[cfg(test)] mod tests { use pumpkin_core::state::State; 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 4611cb1c0..81f00ecf6 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 @@ -4,6 +4,8 @@ use pumpkin_checking::InferenceChecker; use pumpkin_checking::IntExt; use pumpkin_checking::VariableState; use pumpkin_core::asserts::pumpkin_assert_simple; +use pumpkin_core::checkers::RetentionChecker; +use pumpkin_core::checkers::Scope; use pumpkin_core::declare_inference_label; use pumpkin_core::predicate; use pumpkin_core::predicates::Predicate; @@ -72,10 +74,11 @@ where let lower_bound_left_hand_side = context.new_trailed_integer(lower_bound_left_hand_side); let mut checkers = RuntimeCheckers::builder(); - let inference_code = checkers.add_inference_checker( + let inference_code = checkers.add_rule( + Scope::from_variables(x.iter()), constraint_tag, LinearBounds, - LinearLessOrEqualInferenceChecker::new(x.clone(), c), + LinearLessOrEqualChecker::new(x.clone(), c), ); let propagator = LinearLessOrEqualPropagator { @@ -298,18 +301,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, @@ -334,6 +337,46 @@ where } } +impl RetentionChecker for LinearLessOrEqualChecker { + fn check_retention(&mut self, _: &Scope, domains: Domains<'_>) -> bool { + // 1. Check if the constraint is conflicting + let bound = i64::from(self.bound); + let lower_bound_sum = self + .terms + .iter() + .map(|term| i64::from(domains.lower_bound(term))) + .sum::(); + + if lower_bound_sum > bound { + log::error!( + "The lower bounds of {:?} exceed the bound {} of the linear inequality", + self.terms, + self.bound + ); + return false; + } + + // 2. Assert that it is possible to assign the greatest value in the domain for each + // variable + // We do this by effectively assigning the greatest value to the variable whilst keeping + // the other variables at their lower bound. + self.terms.iter().all(|term| { + let greatest = bound - (lower_bound_sum - i64::from(domains.lower_bound(term))); + let is_tight = i64::from(domains.upper_bound(term)) <= greatest; + + if !is_tight { + log::error!( + "The upper bound of {term:?} could be lowered to {greatest} by the linear inequality {:?} <= {}", + self.terms, + self.bound + ); + } + + is_tight + }) + } +} + #[cfg(test)] mod tests { use pumpkin_core::conjunction; @@ -408,6 +451,50 @@ mod tests { .expect_err("Expected overflow to be detected"); } + #[test] + fn retention_fails_when_an_upper_bound_can_be_lowered() { + let mut state = State::default(); + let x = state.new_interval_variable(1, 5, None); + let y = state.new_interval_variable(0, 10, None); + + let mut checker = LinearLessOrEqualChecker::new([x, y].into(), 7); + let scope = Scope::from_variables([x, y].iter()); + + assert!(!checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn retention_holds_at_the_fixpoint_of_the_propagator() { + let mut state = State::default(); + let x = state.new_interval_variable(1, 5, None); + let y = state.new_interval_variable(0, 10, None); + let constraint_tag = state.new_constraint_tag(); + + let _ = state.add_propagator(LinearLessOrEqualPropagatorArgs { + x: [x, y].into(), + c: 7, + constraint_tag, + }); + state.propagate_to_fixed_point().expect("no empty domains"); + + let mut checker = LinearLessOrEqualChecker::new([x, y].into(), 7); + let scope = Scope::from_variables([x, y].iter()); + + assert!(checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn retention_fails_when_the_lower_bounds_exceed_the_bound() { + let mut state = State::default(); + let x = state.new_interval_variable(4, 5, None); + let y = state.new_interval_variable(4, 10, None); + + let mut checker = LinearLessOrEqualChecker::new([x, y].into(), 7); + let scope = Scope::from_variables([x, y].iter()); + + assert!(!checker.check_retention(&scope, state.get_domains())); + } + #[test] fn underflow_leads_to_no_propagation() { let mut state = State::default(); 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 e5a7cbe7a..d13246118 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs @@ -9,6 +9,8 @@ use pumpkin_checking::VariableState; use pumpkin_core::asserts::pumpkin_assert_extreme; use pumpkin_core::asserts::pumpkin_assert_moderate; use pumpkin_core::asserts::pumpkin_assert_simple; +use pumpkin_core::checkers::RetentionChecker; +use pumpkin_core::checkers::Scope; use pumpkin_core::declare_inference_label; use pumpkin_core::predicate; use pumpkin_core::predicates::PropositionalConjunction; @@ -73,7 +75,8 @@ where } let mut checkers = RuntimeCheckers::builder(); - let inference_code = checkers.add_inference_checker( + let inference_code = checkers.add_rule( + Scope::from_variables(terms.iter()), constraint_tag, LinearNotEquals, LinearNotEqualChecker { @@ -398,6 +401,63 @@ where } } +impl RetentionChecker for LinearNotEqualChecker { + fn check_retention(&mut self, _: &Scope, domains: Domains<'_>) -> bool { + let unfixed_terms = self + .terms + .iter() + .filter(|&term| !domains.is_fixed(term)) + .collect::>(); + + let fixed_sum = self + .terms + .iter() + .filter_map(|term| domains.fixed_value(term)) + .map(i64::from) + .sum::(); + + // 1. Check if the constraint is conflicting, which is the case if all terms are fixed and + // sum to the bound + if unfixed_terms.is_empty() { + let is_violated = fixed_sum == i64::from(self.bound); + + if is_violated { + log::error!( + "The fixed terms {:?} sum to the forbidden value {} of the linear disequality", + self.terms, + self.bound + ); + } + + return !is_violated; + } + + // 2. If at least two terms are unfixed then nothing can be propagated + if unfixed_terms.len() >= 2 { + return true; + } + + // 3. Assert that the single unfixed term cannot take the value which completes the sum to + // the bound + let unfixed_term = unfixed_terms[0]; + let forbidden = i64::from(self.bound) - fixed_sum; + let is_removed = match i32::try_from(forbidden) { + Ok(forbidden) => !domains.contains(unfixed_term, forbidden), + Err(_) => true, + }; + + if !is_removed { + log::error!( + "The value {forbidden} could be removed from {unfixed_term:?} by the linear disequality {:?} != {}", + self.terms, + self.bound + ); + } + + is_removed + } +} + #[cfg(test)] mod tests { use pumpkin_core::conjunction; @@ -481,6 +541,67 @@ mod tests { assert_eq!(conjunction!([x == 2]), reason); } + #[test] + fn retention_fails_when_the_forbidden_value_is_present() { + let mut state = State::default(); + let x = state.new_interval_variable(3, 3, None); + let y = state.new_interval_variable(0, 10, None); + + let mut checker = LinearNotEqualChecker { + terms: [x, y].into(), + bound: 5, + }; + let scope = Scope::from_variables([x, y].iter()); + + assert!(!checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn retention_holds_when_the_forbidden_value_is_absent() { + let mut state = State::default(); + let x = state.new_interval_variable(3, 3, None); + let y = state.new_interval_variable(0, 10, None); + let _ = state.post(predicate![y != 2]).unwrap(); + + let mut checker = LinearNotEqualChecker { + terms: [x, y].into(), + bound: 5, + }; + let scope = Scope::from_variables([x, y].iter()); + + assert!(checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn retention_holds_with_two_unfixed_terms() { + let mut state = State::default(); + let x = state.new_interval_variable(0, 5, None); + let y = state.new_interval_variable(0, 10, None); + + let mut checker = LinearNotEqualChecker { + terms: [x, y].into(), + bound: 5, + }; + let scope = Scope::from_variables([x, y].iter()); + + assert!(checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn retention_fails_when_the_fixed_terms_sum_to_the_bound() { + let mut state = State::default(); + let x = state.new_interval_variable(3, 3, None); + let y = state.new_interval_variable(2, 2, None); + + let mut checker = LinearNotEqualChecker { + terms: [x, y].into(), + bound: 5, + }; + let scope = Scope::from_variables([x, y].iter()); + + assert!(!checker.check_retention(&scope, state.get_domains())); + } + #[test] fn satisfied_constraint_does_not_trigger_conflict() { let mut state = State::default(); diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum/checker.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum/checker.rs new file mode 100644 index 000000000..5a6af03b7 --- /dev/null +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum/checker.rs @@ -0,0 +1,201 @@ +use pumpkin_checking::AtomicConstraint; +use pumpkin_checking::CheckerVariable; +use pumpkin_checking::InferenceChecker; +use pumpkin_checking::IntExt; +use pumpkin_core::checkers::RetentionChecker; +use pumpkin_core::checkers::Scope; +use pumpkin_core::propagation::Domains; +use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::variables::IntegerVariable; + +#[derive(Clone, Debug)] +pub struct MaximumChecker { + pub array: Box<[ElementVar]>, + pub rhs: Rhs, +} + +impl InferenceChecker for MaximumChecker +where + Atomic: AtomicConstraint, + ElementVar: CheckerVariable, + Rhs: CheckerVariable, +{ + fn check( + &self, + state: pumpkin_checking::VariableState, + _: &[Atomic], + _: Option<&Atomic>, + ) -> bool { + let lowest_maximum = self + .array + .iter() + .map(|element| element.induced_lower_bound(&state)) + .max() + .unwrap_or(IntExt::NegativeInf); + let highest_maximum = self + .array + .iter() + .map(|element| element.induced_upper_bound(&state)) + .max() + .unwrap_or(IntExt::PositiveInf); + + // If the intersection between the domain of `rhs` and `[lowest_maximum, + // highest_maximum]` is empty, there is a conflict. + + lowest_maximum > self.rhs.induced_upper_bound(&state) + || highest_maximum < self.rhs.induced_lower_bound(&state) + } +} + +impl RetentionChecker for MaximumChecker +where + ElementVar: IntegerVariable + 'static, + Rhs: IntegerVariable + 'static, +{ + fn check_retention(&mut self, _: &Scope, domains: Domains<'_>) -> bool { + if self.array.is_empty() { + return false; + } + + let rhs_lower = domains.lower_bound(&self.rhs); + let rhs_upper = domains.upper_bound(&self.rhs); + let mut greatest_lower = i32::MIN; + let mut greatest_upper = i32::MIN; + for element in self.array.iter() { + greatest_lower = greatest_lower.max(domains.lower_bound(element)); + greatest_upper = greatest_upper.max(domains.upper_bound(element)); + } + + // 1. Assert that the bounds of the maximum match the bounds of the array: its lower bound + // is at least the greatest lower bound and its upper bound is at most the greatest upper + // bound + if rhs_lower < greatest_lower { + log::error!( + "The lower bound of {:?} could be raised to {greatest_lower} by the maximum of {:?}", + self.rhs, + self.array + ); + return false; + } + + if rhs_upper > greatest_upper { + log::error!( + "The upper bound of {:?} could be lowered to {greatest_upper} by the maximum of {:?}", + self.rhs, + self.array + ); + return false; + } + + // 2. Assert that no element exceeds the upper bound of the maximum + for element in self.array.iter() { + if domains.upper_bound(element) > rhs_upper { + log::error!( + "The upper bound of {element:?} could be lowered to {rhs_upper}, the upper bound of the maximum {:?}", + self.rhs + ); + return false; + } + } + + // 3. If only one element can be at least the lower bound of the maximum then it is the + // maximum; assert that its lower bound is at least the lower bound of the maximum, the + // upper bound is already equal by 1 and 2 + // Elements are counted by position, as the propagator does. + let candidates = self + .array + .iter() + .filter(|&element| domains.upper_bound(element) >= rhs_lower) + .collect::>(); + if candidates.len() == 1 && domains.lower_bound(candidates[0]) < rhs_lower { + log::error!( + "The lower bound of {:?} could be raised to {rhs_lower}: it is the only element that can attain the maximum {:?}", + candidates[0], + self.rhs + ); + return false; + } + + true + } +} + +#[cfg(test)] +mod tests { + use pumpkin_core::state::State; + + use super::*; + use crate::arithmetic::MaximumArgs; + + #[test] + fn retention_fails_when_the_lower_bound_of_the_maximum_is_below_the_greatest_lower_bound() { + let mut state = State::default(); + let a = state.new_interval_variable(3, 10, None); + let b = state.new_interval_variable(0, 5, None); + let rhs = state.new_interval_variable(0, 10, None); + + let mut checker = MaximumChecker { + array: [a, b].into(), + rhs, + }; + let scope = Scope::from_variables([a, b, rhs].iter()); + + assert!(!checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn retention_fails_when_an_element_exceeds_the_upper_bound_of_the_maximum() { + let mut state = State::default(); + let a = state.new_interval_variable(0, 10, None); + let b = state.new_interval_variable(0, 5, None); + let rhs = state.new_interval_variable(0, 8, None); + + let mut checker = MaximumChecker { + array: [a, b].into(), + rhs, + }; + let scope = Scope::from_variables([a, b, rhs].iter()); + + assert!(!checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn retention_fails_when_the_sole_candidate_does_not_attain_the_lower_bound_of_the_maximum() { + let mut state = State::default(); + let a = state.new_interval_variable(0, 8, None); + let b = state.new_interval_variable(0, 3, None); + let rhs = state.new_interval_variable(5, 8, None); + + let mut checker = MaximumChecker { + array: [a, b].into(), + rhs, + }; + let scope = Scope::from_variables([a, b, rhs].iter()); + + assert!(!checker.check_retention(&scope, state.get_domains())); + } + + #[test] + fn retention_holds_at_the_fixpoint_of_the_propagator() { + let mut state = State::default(); + let a = state.new_interval_variable(0, 10, None); + let b = state.new_interval_variable(0, 3, None); + let rhs = state.new_interval_variable(5, 8, None); + let constraint_tag = state.new_constraint_tag(); + + let _ = state.add_propagator(MaximumArgs { + array: [a, b].into(), + rhs, + constraint_tag, + }); + state.propagate_to_fixed_point().expect("no empty domains"); + + let mut checker = MaximumChecker { + array: [a, b].into(), + rhs, + }; + let scope = Scope::from_variables([a, b, rhs].iter()); + + assert!(checker.check_retention(&scope, state.get_domains())); + } +} diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum/constructor.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum/constructor.rs new file mode 100644 index 000000000..5948cfc6d --- /dev/null +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum/constructor.rs @@ -0,0 +1,72 @@ +use pumpkin_core::checkers::Scope; +use pumpkin_core::proof::ConstraintTag; +use pumpkin_core::propagation::DomainEvents; +use pumpkin_core::propagation::EventsToRegister; +use pumpkin_core::propagation::LocalId; +use pumpkin_core::propagation::PropagatorConstructor; +use pumpkin_core::propagation::PropagatorConstructorContext; +use pumpkin_core::propagation::PropagatorSpec; +use pumpkin_core::propagation::RuntimeCheckers; +use pumpkin_core::variables::IntegerVariable; + +use crate::arithmetic::MaximumChecker; +use crate::arithmetic::MaximumPropagator; +use crate::arithmetic::maximum::Maximum; + +/// The [`PropagatorConstructor`] for the [`MaximumPropagator`]. +#[derive(Clone, Debug)] +pub struct MaximumArgs { + pub array: Box<[ElementVar]>, + pub rhs: Rhs, + pub constraint_tag: ConstraintTag, +} + +impl PropagatorConstructor for MaximumArgs +where + ElementVar: IntegerVariable + 'static, + Rhs: IntegerVariable + 'static, +{ + type PropagatorImpl = MaximumPropagator; + + fn create(self, _: PropagatorConstructorContext) -> PropagatorSpec { + let MaximumArgs { + array, + rhs, + constraint_tag, + } = self; + + let mut registration = EventsToRegister::builder(); + for (idx, var) in array.iter().enumerate() { + registration = registration.add(var, DomainEvents::BOUNDS, LocalId::from(idx as u32)); + } + + let rhs_local_id = LocalId::from(array.len() as u32); + registration = registration.add(&rhs, DomainEvents::BOUNDS, rhs_local_id); + + let mut scope = Scope::from_variables(array.iter()); + rhs.add_to_scope(&mut scope, rhs_local_id); + + let mut checkers = RuntimeCheckers::builder(); + let inference_code = checkers.add_rule( + scope, + constraint_tag, + Maximum, + MaximumChecker { + array: array.clone(), + rhs: rhs.clone(), + }, + ); + + let propagator = MaximumPropagator { + array, + rhs, + inference_code, + }; + + PropagatorSpec { + registration: registration.build(), + checkers: checkers.build(), + propagator, + } + } +} diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum/mod.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum/mod.rs new file mode 100644 index 000000000..d8029502e --- /dev/null +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum/mod.rs @@ -0,0 +1,11 @@ +mod checker; +mod constructor; +mod propagator; + +pub use checker::*; +pub use constructor::*; +pub use propagator::*; +use pumpkin_core::declare_inference_label; + +// The inference label for maximum. +declare_inference_label!(Maximum); diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum/propagator.rs similarity index 71% rename from pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs rename to pumpkin-crates/propagators/src/propagators/arithmetic/maximum/propagator.rs index 316cfca8a..3de839231 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum/propagator.rs @@ -1,92 +1,24 @@ -use pumpkin_checking::AtomicConstraint; -use pumpkin_checking::CheckerVariable; -use pumpkin_checking::InferenceChecker; -use pumpkin_checking::IntExt; use pumpkin_core::conjunction; -use pumpkin_core::declare_inference_label; use pumpkin_core::predicate; use pumpkin_core::predicates::PropositionalConjunction; -use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; -use pumpkin_core::propagation::DomainEvents; -use pumpkin_core::propagation::EventsToRegister; -use pumpkin_core::propagation::LocalId; use pumpkin_core::propagation::Priority; use pumpkin_core::propagation::PropagationContext; use pumpkin_core::propagation::Propagator; -use pumpkin_core::propagation::PropagatorConstructor; -use pumpkin_core::propagation::PropagatorConstructorContext; -use pumpkin_core::propagation::PropagatorSpec; use pumpkin_core::propagation::ReadDomains; -use pumpkin_core::propagation::RuntimeCheckers; use pumpkin_core::state::PropagationStatusCP; use pumpkin_core::variables::IntegerVariable; -#[derive(Clone, Debug)] -pub struct MaximumArgs { - pub array: Box<[ElementVar]>, - pub rhs: Rhs, - pub constraint_tag: ConstraintTag, -} - -declare_inference_label!(Maximum); - -impl PropagatorConstructor for MaximumArgs -where - ElementVar: IntegerVariable + 'static, - Rhs: IntegerVariable + 'static, -{ - type PropagatorImpl = MaximumPropagator; - - fn create(self, _: PropagatorConstructorContext) -> PropagatorSpec { - let MaximumArgs { - array, - rhs, - constraint_tag, - } = self; - - let mut registration = EventsToRegister::builder(); - for (idx, var) in array.iter().enumerate() { - registration = registration.add(var, DomainEvents::BOUNDS, LocalId::from(idx as u32)); - } - - registration = registration.add( - &rhs, - DomainEvents::BOUNDS, - LocalId::from(array.len() as u32), - ); - - let mut checkers = RuntimeCheckers::builder(); - let inference_code = checkers.add_inference_checker( - constraint_tag, - Maximum, - MaximumChecker { - array: array.clone(), - rhs: rhs.clone(), - }, - ); - - let propagator = MaximumPropagator { - array, - rhs, - inference_code, - }; - - PropagatorSpec { - registration: registration.build(), - checkers: checkers.build(), - propagator, - } - } -} +#[cfg(doc)] +use super::MaximumArgs; /// Bounds-consistent propagator which enforces `max(array) = rhs`. Can be constructed through /// [`MaximumArgs`]. #[derive(Clone, Debug)] pub struct MaximumPropagator { - array: Box<[ElementVar]>, - rhs: Rhs, - inference_code: InferenceCode, + pub(crate) array: Box<[ElementVar]>, + pub(crate) rhs: Rhs, + pub(crate) inference_code: InferenceCode, } impl Propagator @@ -191,45 +123,6 @@ impl Prop } } -#[derive(Clone, Debug)] -pub struct MaximumChecker { - pub array: Box<[ElementVar]>, - pub rhs: Rhs, -} - -impl InferenceChecker for MaximumChecker -where - Atomic: AtomicConstraint, - ElementVar: CheckerVariable, - Rhs: CheckerVariable, -{ - fn check( - &self, - state: pumpkin_checking::VariableState, - _: &[Atomic], - _: Option<&Atomic>, - ) -> bool { - let lowest_maximum = self - .array - .iter() - .map(|element| element.induced_lower_bound(&state)) - .max() - .unwrap_or(IntExt::NegativeInf); - let highest_maximum = self - .array - .iter() - .map(|element| element.induced_upper_bound(&state)) - .max() - .unwrap_or(IntExt::PositiveInf); - - // If the intersection between the domain of `rhs` and `[lowest_maximum, - // highest_maximum]` is empty, there is a conflict. - - lowest_maximum > self.rhs.induced_upper_bound(&state) - || highest_maximum < self.rhs.induced_lower_bound(&state) - } -} - #[cfg(test)] mod tests { use pumpkin_core::predicate; @@ -240,6 +133,7 @@ mod tests { use super::*; use crate::StateExt; + use crate::arithmetic::MaximumArgs; #[test] fn upper_bound_of_rhs_matches_maximum_upper_bound_of_array_at_initialise() { diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/mod.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/mod.rs index 21fc6eb9a..6dcf0811d 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/mod.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/mod.rs @@ -1,6 +1,7 @@ //! Contains a number of propagators for a variety of arithmetic constraints. pub(crate) mod absolute_value; pub(crate) mod binary; +mod binary_equals; pub(crate) mod integer_division; pub(crate) mod integer_multiplication; pub(crate) mod linear_less_or_equal; @@ -9,6 +10,7 @@ pub(crate) mod maximum; pub use absolute_value::*; pub use binary::*; +pub use binary_equals::*; pub use integer_division::*; pub use integer_multiplication::*; pub use linear_less_or_equal::*; diff --git a/pumpkin-crates/propagators/src/propagators/disjunctive/checker.rs b/pumpkin-crates/propagators/src/propagators/disjunctive/checker.rs index f9d18f51f..b9e3e8839 100644 --- a/pumpkin-crates/propagators/src/propagators/disjunctive/checker.rs +++ b/pumpkin-crates/propagators/src/propagators/disjunctive/checker.rs @@ -1,5 +1,4 @@ use std::cmp::max; -use std::cmp::min; use std::marker::PhantomData; use pumpkin_checking::AtomicConstraint; @@ -7,6 +6,7 @@ use pumpkin_checking::CheckerVariable; use pumpkin_checking::InferenceChecker; use pumpkin_checking::IntExt; use pumpkin_checking::VariableState; +use pumpkin_core::asserts::pumpkin_assert_simple; use pumpkin_core::containers::KeyedVec; use pumpkin_core::containers::StorageKey; use pumpkin_core::propagation::LocalId; @@ -20,10 +20,74 @@ pub struct DisjunctiveEdgeFindingChecker { pub tasks: Box<[ArgDisjunctiveTask]>, } +/// Performs overload checking on the provided `tasks` and returns true if a conflict could be +/// found. +/// +/// Recall the following: +/// We try to find a set omega of jobs with the following property: `p_omega > lct_omega - +/// est_omega`. +fn overload_checking>( + tasks: &[ArgDisjunctiveTask], + state: &VariableState, +) -> bool { + // First, we create our theta-lambda tree + let mut theta = CheckerThetaLambdaTree::new( + &tasks + .iter() + .enumerate() + .map(|(index, task)| DisjunctiveTask { + start_time: task.start_time.clone(), + processing_time: task.processing_time, + id: LocalId::from(index as u32), + }) + .collect::>(), + ); + // And update it with the current state. + theta.update(state); + + // Next, we sort based on non-decreasing latest completion time. + let mut sorted_tasks = tasks + .iter() + .enumerate() + .filter(|(_, task)| { + task.start_time.induced_lower_bound(state) != IntExt::NegativeInf + && task.start_time.induced_upper_bound(state) != IntExt::PositiveInf + }) + .collect::>(); + sorted_tasks + .sort_by_key(|(_, task)| task.start_time.induced_upper_bound(state) + task.processing_time); + + // Then we go over the tasks which are bounded in the state. + for (index, task) in sorted_tasks { + pumpkin_assert_simple!( + task.start_time.induced_lower_bound(state) != IntExt::NegativeInf + && task.start_time.induced_upper_bound(state) != IntExt::PositiveInf + ); + // And we add it to the theta. + theta.add_to_theta( + &DisjunctiveTask { + start_time: task.start_time.clone(), + processing_time: task.processing_time, + id: LocalId::from(index as u32), + }, + state, + ); + + // If there is an overload of the interval, then we can report that a conflict has been + // found. + if theta.ect() > task.start_time.induced_upper_bound(state) + task.processing_time { + return true; + } + } + + false +} + impl InferenceChecker for DisjunctiveEdgeFindingChecker where Var: CheckerVariable, Atomic: AtomicConstraint, + ::Identifier: Clone, { fn check( &self, @@ -31,93 +95,46 @@ where _premises: &[Atomic], consequent: Option<&Atomic>, ) -> bool { - // Recall the following: - // - For conflict detection, the explanation represents a set omega with the following - // property: `p_omega > lct_omega - est_omega`. - // - // We simply need to check whether the interval [est_omega, lct_omega] is overloaded - // - For propagation, the explanation represents a set omega (and omega') such that the - // following holds: `min(est_i, est_omega) + p_omega + p_i > lct_omega -> [s_i >= - // ect_omega]`. - let mut lb_interval = i32::MAX; - let mut ub_interval = i32::MIN; - let mut p = 0; - let mut propagating_task = None; - let mut theta = Vec::new(); - - // We go over all of the tasks - for task in self.tasks.iter() { - // Only if they are present in the explanation, do we actually process them - // - For tasks in omega, both bounds should be present to define the interval - // - For the propagating task, the lower-bound should be present, and the negation of - // the consequent ensures that an upper-bound is present - if task.start_time.induced_lower_bound(&state) != IntExt::NegativeInf - && task.start_time.induced_upper_bound(&state) != IntExt::PositiveInf - { - // Now we calculate the durations of tasks - let est_task: i32 = task - .start_time - .induced_lower_bound(&state) - .try_into() - .unwrap(); - let lst_task = - >::try_into(task.start_time.induced_upper_bound(&state)) - .unwrap(); - - let is_propagating_task = if let Some(consequent) = consequent { - task.start_time.does_atomic_constrain_self(consequent) - } else { - false - }; - if !is_propagating_task { - theta.push(task.clone()); - p += task.processing_time; - lb_interval = lb_interval.min(est_task); - ub_interval = ub_interval.max(lst_task + task.processing_time); - } else { - propagating_task = Some(task.clone()); - } - } - } - - if consequent.is_some() { - let propagating_task = propagating_task - .expect("If there is a consequent then there should be a propagating task"); - - let est_task = propagating_task + // We want to detect conflicts, and we split into two cases: + // 1. If it is a conflict explanation then overload checking can be applied directly and + // should lead to a conflict. + // 2. If it is a propagation explanation, then for any value in the domain of the propagated + // variable, scheduling it at that time-point should lead to a conflict (using overload + // checking). + if let Some(consequent) = consequent { + // First we retrieve the propagating task. + let task = self + .tasks + .iter() + .find(|task| task.start_time.does_atomic_constrain_self(consequent)) + .expect("Expected to be able to find atomic"); + + let lb: i32 = task .start_time .induced_lower_bound(&state) .try_into() - .unwrap(); - - let mut theta_lambda_tree = CheckerThetaLambdaTree::new( - &theta - .iter() - .enumerate() - .map(|(index, task)| DisjunctiveTask { - start_time: task.start_time.clone(), - processing_time: task.processing_time, - id: LocalId::from(index as u32), - }) - .collect::>(), - ); - theta_lambda_tree.update(&state); - for (index, task) in theta.iter().enumerate() { - theta_lambda_tree.add_to_theta( - &DisjunctiveTask { - start_time: task.start_time.clone(), - processing_time: task.processing_time, - id: LocalId::from(index as u32), - }, - &state, - ); + .expect("expected non-infinity value"); + let ub: i32 = task + .start_time + .induced_upper_bound(&state) + .try_into() + .expect("expected non-infinity value"); + + // Then we go over every value in its domain. + for i in lb..=ub { + // We assign the propagating variable to that value. + let mut assigned_state = state.clone(); + let _ = assigned_state.apply(&task.start_time.atomic_equal(i)); + + // If we do not find a conflict using overload checking, then it is not a valid + // explanation. + if !overload_checking(&self.tasks, &assigned_state) { + return false; + } } - - min(est_task, lb_interval) + p + propagating_task.processing_time > ub_interval - && theta_lambda_tree.ect() > propagating_task.start_time.induced_upper_bound(&state) + true } else { - // We simply check whether the interval is overloaded - p > (ub_interval - lb_interval) + overload_checking(&self.tasks, &state) } } }