diff --git a/Cargo.lock b/Cargo.lock index dfba694b5..80f55a0be 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -293,6 +293,12 @@ dependencies = [ "thiserror", ] +[[package]] +name = "dyn-clone" +version = "1.0.20" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d0881ea181b1df73ff77ffaaf9c7544ecc11e82fba9b5f27b262a3c73a332555" + [[package]] name = "either" version = "1.15.0" @@ -739,6 +745,7 @@ dependencies = [ "convert_case 0.6.0", "downcast-rs", "drcp-format", + "dyn-clone", "enum-map", "enumset", "flate2", diff --git a/pumpkin-crates/core/Cargo.toml b/pumpkin-crates/core/Cargo.toml index 62b062b79..7521d8355 100644 --- a/pumpkin-crates/core/Cargo.toml +++ b/pumpkin-crates/core/Cargo.toml @@ -27,6 +27,7 @@ num = "0.4.3" enum-map = "2.7.3" clap = { version = "4.5.40", optional = true } indexmap = "2.10.0" +dyn-clone = "1.0.20" flate2 = { version = "1.1.2" } [target.'cfg(target_arch = "wasm32")'.dependencies] diff --git a/pumpkin-crates/core/src/api/mod.rs b/pumpkin-crates/core/src/api/mod.rs index aeb8de03f..eee7cf34c 100644 --- a/pumpkin-crates/core/src/api/mod.rs +++ b/pumpkin-crates/core/src/api/mod.rs @@ -118,6 +118,20 @@ pub mod predicates { use crate::variables::Literal; } +pub mod state { + //! Contains structures for the state containing the propagators and variables. + //! + //! See [`State`] for more information. + pub use crate::api::solver::PropagatorHandle; + pub use crate::basic_types::PropagatorConflict; + pub use crate::engine::Conflict; + pub use crate::engine::EmptyDomain; + pub use crate::engine::EmptyDomainConflict; + pub use crate::engine::State; + pub use crate::engine::propagation::CurrentNogood; + pub use crate::engine::propagation::PropagatorId; +} + pub use crate::basic_types::Function; #[doc(hidden)] diff --git a/pumpkin-crates/core/src/api/solver.rs b/pumpkin-crates/core/src/api/solver.rs index 95f01a5fe..f05cb13a6 100644 --- a/pumpkin-crates/core/src/api/solver.rs +++ b/pumpkin-crates/core/src/api/solver.rs @@ -223,6 +223,7 @@ impl Solver { /// let named_literal = solver.new_named_literal("z"); /// ``` pub fn new_named_literal(&mut self, name: impl Into) -> Literal { + let name = name.into(); self.satisfaction_solver .create_new_literal(Some(name.into())) } @@ -268,6 +269,7 @@ impl Solver { upper_bound: i32, name: impl Into, ) -> DomainId { + let name = name.into(); self.satisfaction_solver.create_new_integer_variable( lower_bound, upper_bound, @@ -388,7 +390,7 @@ impl Solver { CSPSolverExecutionFlag::Infeasible => { if self .satisfaction_solver - .state + .solver_state .is_infeasible_under_assumptions() { // The state is automatically reset when we return this result @@ -509,7 +511,7 @@ impl Solver { impl Solver { /// Creates an instance of the [`DefaultBrancher`]. pub fn default_brancher(&self) -> DefaultBrancher { - DefaultBrancher::default_over_all_variables(&self.satisfaction_solver.assignments) + DefaultBrancher::default_over_all_variables(self.satisfaction_solver.assignments()) } } diff --git a/pumpkin-crates/core/src/basic_types/mod.rs b/pumpkin-crates/core/src/basic_types/mod.rs index dccdafde4..2cfe340ea 100644 --- a/pumpkin-crates/core/src/basic_types/mod.rs +++ b/pumpkin-crates/core/src/basic_types/mod.rs @@ -18,7 +18,7 @@ pub use function::Function; pub(crate) use predicate_id_generators::DeletablePredicateIdGenerator; pub(crate) use predicate_id_generators::PredicateId; pub(crate) use predicate_id_generators::PredicateIdGenerator; -pub(crate) use propagation_status_cp::*; +pub use propagation_status_cp::*; pub use propositional_conjunction::PropositionalConjunction; pub use random::*; pub use solution::ProblemSolution; diff --git a/pumpkin-crates/core/src/basic_types/propagation_status_cp.rs b/pumpkin-crates/core/src/basic_types/propagation_status_cp.rs index 7b4ce2e3d..8296d647c 100644 --- a/pumpkin-crates/core/src/basic_types/propagation_status_cp.rs +++ b/pumpkin-crates/core/src/basic_types/propagation_status_cp.rs @@ -1,36 +1,18 @@ use super::PropositionalConjunction; -use crate::engine::EmptyDomain; use crate::proof::InferenceCode; +use crate::state::Conflict; /// The result of invoking a constraint programming propagator. The propagation can either succeed /// or identify a conflict. The necessary conditions for the conflict must be captured in the error /// variant, i.e. a propositional conjunction. -pub(crate) type PropagationStatusCP = Result<(), Inconsistency>; - -#[derive(Debug, PartialEq, Eq)] -pub(crate) enum Inconsistency { - EmptyDomain, - Conflict(PropagatorConflict), -} - -impl From for Inconsistency { - fn from(_: EmptyDomain) -> Self { - Inconsistency::EmptyDomain - } -} - -impl From for Inconsistency { - fn from(conflict: PropagatorConflict) -> Self { - Inconsistency::Conflict(conflict) - } -} +pub(crate) type PropagationStatusCP = Result<(), Conflict>; /// A conflict stated by a propagator. A propagator that identifies a conflict that is _not_ an /// empty domain, describes that conflict with this type. #[derive(Clone, Debug, PartialEq, Eq)] -pub(crate) struct PropagatorConflict { +pub struct PropagatorConflict { /// The conjunction that describes the infeasible partial assignment. - pub(crate) conjunction: PropositionalConjunction, + pub conjunction: PropositionalConjunction, /// The inference code that identified the conflict. - pub(crate) inference_code: InferenceCode, + pub inference_code: InferenceCode, } diff --git a/pumpkin-crates/core/src/basic_types/propositional_conjunction.rs b/pumpkin-crates/core/src/basic_types/propositional_conjunction.rs index 19ad1e768..97c2f2ef1 100644 --- a/pumpkin-crates/core/src/basic_types/propositional_conjunction.rs +++ b/pumpkin-crates/core/src/basic_types/propositional_conjunction.rs @@ -1,3 +1,4 @@ +use std::ops::Deref; use std::ops::Index; use std::ops::IndexMut; @@ -12,6 +13,14 @@ pub struct PropositionalConjunction { predicates_in_conjunction: Vec, } +impl Deref for PropositionalConjunction { + type Target = [Predicate]; + + fn deref(&self) -> &Self::Target { + &self.predicates_in_conjunction + } +} + impl PropositionalConjunction { pub fn new(predicates_in_conjunction: Vec) -> Self { PropositionalConjunction { @@ -19,38 +28,14 @@ impl PropositionalConjunction { } } - pub fn len(&self) -> usize { - self.predicates_in_conjunction.len() - } - - pub fn is_empty(&self) -> bool { - self.predicates_in_conjunction.is_empty() - } - - pub fn contains(&self, predicate: Predicate) -> bool { - self.predicates_in_conjunction.contains(&predicate) - } - - pub fn num_predicates(&self) -> u32 { - self.predicates_in_conjunction.len() as u32 - } - - pub fn add(&mut self, predicate: Predicate) { - self.predicates_in_conjunction.push(predicate); - } - - pub fn iter(&self) -> impl Iterator + '_ { - self.predicates_in_conjunction.iter() + pub fn clear(&mut self) { + self.predicates_in_conjunction.clear(); } pub fn as_slice(&self) -> &[Predicate] { self.predicates_in_conjunction.as_slice() } - pub fn clear(&mut self) { - self.predicates_in_conjunction.clear(); - } - pub fn push(&mut self, predicate: Predicate) { self.predicates_in_conjunction.push(predicate); } diff --git a/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs b/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs index 1537ad7fc..4d38eeea5 100644 --- a/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs +++ b/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs @@ -2,17 +2,16 @@ use super::propagation_status_cp::PropagatorConflict; use crate::ConstraintOperationError; #[cfg(doc)] use crate::engine::ConstraintSatisfactionSolver; +use crate::engine::EmptyDomainConflict; #[cfg(doc)] use crate::engine::propagation::Propagator; -use crate::engine::reason::ReasonRef; +use crate::engine::state::Conflict; use crate::predicates::Predicate; -use crate::proof::InferenceCode; -use crate::variables::DomainId; -/// A conflict info which can be stored in the solver. -/// Two (related) conflicts can happen: -/// 1) A propagator explicitly detects a conflict. -/// 2) A propagator post a domain change that results in a variable having an empty domain. +/// a conflict info which can be stored in the solver. +/// two (related) conflicts can happen: +/// 1) a propagator explicitly detects a conflict. +/// 2) a propagator post a domain change that results in a variable having an empty domain. #[derive(Debug, PartialEq, Eq, Clone)] pub(crate) enum StoredConflictInfo { Propagator(PropagatorConflict), @@ -24,20 +23,15 @@ pub(crate) enum StoredConflictInfo { RootLevelConflict(ConstraintOperationError), } -/// A conflict because a domain became empty. -#[derive(Clone, Copy, Debug, PartialEq, Eq)] -pub(crate) struct EmptyDomainConflict { - /// The predicate that caused a domain to become empty. - pub(crate) trigger_predicate: Predicate, - /// The reason for [`EmptyDomainConflict::trigger_predicate`] to be true. - pub(crate) trigger_reason: ReasonRef, - /// The [`InferenceCode`] that accompanies [`EmptyDomainConflict::trigger_reason`]. - pub(crate) trigger_inference_code: InferenceCode, -} - -impl EmptyDomainConflict { - /// The domain that became empty. - pub(crate) fn domain(&self) -> DomainId { - self.trigger_predicate.get_domain() +impl From for StoredConflictInfo { + fn from(value: Conflict) -> Self { + match value { + Conflict::Propagator(propagator_conflict) => { + StoredConflictInfo::Propagator(propagator_conflict) + } + Conflict::EmptyDomain(empty_domain_conflict) => { + StoredConflictInfo::EmptyDomain(empty_domain_conflict) + } + } } } diff --git a/pumpkin-crates/core/src/basic_types/trail.rs b/pumpkin-crates/core/src/basic_types/trail.rs index ced779aba..ce3bb26c8 100644 --- a/pumpkin-crates/core/src/basic_types/trail.rs +++ b/pumpkin-crates/core/src/basic_types/trail.rs @@ -6,7 +6,7 @@ use crate::pumpkin_assert_simple; #[derive(Clone, Debug)] pub(crate) struct Trail { - current_decision_level: usize, + current_checkpoint: usize, /// At index i is the position where the i-th decision level ends (exclusive) on the trail trail_delimiter: Vec, trail: Vec, @@ -17,7 +17,7 @@ pub(crate) struct Trail { impl Default for Trail { fn default() -> Self { Trail { - current_decision_level: Default::default(), + current_checkpoint: Default::default(), trail_delimiter: Default::default(), trail: Default::default(), } @@ -25,40 +25,40 @@ impl Default for Trail { } impl Trail { - pub(crate) fn increase_decision_level(&mut self) { - self.current_decision_level += 1; + pub(crate) fn new_checkpoint(&mut self) { + self.current_checkpoint += 1; self.trail_delimiter.push(self.trail.len()); } - pub(crate) fn values_on_decision_level(&self, decision_level: usize) -> &[T] { - assert!(decision_level <= self.current_decision_level); + pub(crate) fn values_at_checkpoint(&self, checkpoint: usize) -> &[T] { + assert!(checkpoint <= self.current_checkpoint); - let start = if decision_level == 0 { + let start = if checkpoint == 0 { 0 } else { - self.trail_delimiter[decision_level - 1] + self.trail_delimiter[checkpoint - 1] }; - let end = if decision_level == self.current_decision_level { + let end = if checkpoint == self.current_checkpoint { self.trail.len() } else { - self.trail_delimiter[decision_level] + self.trail_delimiter[checkpoint] }; &self.trail[start..end] } - pub(crate) fn get_decision_level(&self) -> usize { - self.current_decision_level + pub(crate) fn get_checkpoint(&self) -> usize { + self.current_checkpoint } - pub(crate) fn synchronise(&mut self, new_decision_level: usize) -> Rev> { - pumpkin_assert_simple!(new_decision_level < self.current_decision_level); + pub(crate) fn synchronise(&mut self, new_checkpoint: usize) -> Rev> { + pumpkin_assert_simple!(new_checkpoint < self.current_checkpoint); - let new_trail_len = self.trail_delimiter[new_decision_level]; + let new_trail_len = self.trail_delimiter[new_checkpoint]; - self.current_decision_level = new_decision_level; - self.trail_delimiter.truncate(new_decision_level); + self.current_checkpoint = new_checkpoint; + self.trail_delimiter.truncate(new_checkpoint); self.trail.drain(new_trail_len..).rev() } @@ -100,10 +100,10 @@ mod tests { } #[test] - fn backtracking_removes_elements_beyond_decision_level() { + fn backtracking_removes_elements_beyond_checkpoint() { let mut trail = Trail::default(); - trail.increase_decision_level(); + trail.new_checkpoint(); trail.push(1); let _ = trail.synchronise(0); @@ -115,11 +115,11 @@ mod tests { let mut trail = Trail::default(); trail.push(1); - trail.increase_decision_level(); + trail.new_checkpoint(); trail.push(2); - trail.increase_decision_level(); + trail.new_checkpoint(); trail.push(3); - trail.increase_decision_level(); + trail.new_checkpoint(); trail.push(4); let _ = trail.synchronise(1); @@ -132,11 +132,11 @@ mod tests { let mut trail = Trail::default(); trail.push(1); - trail.increase_decision_level(); + trail.new_checkpoint(); trail.push(2); - trail.increase_decision_level(); + trail.new_checkpoint(); trail.push(3); - trail.increase_decision_level(); + trail.new_checkpoint(); trail.push(4); let popped = trail.synchronise(0).collect::>(); @@ -144,19 +144,19 @@ mod tests { } #[test] - fn elements_at_current_decision_level() { + fn elements_at_current_checkpoint() { let mut trail = Trail::default(); trail.push(1); trail.push(2); - trail.increase_decision_level(); + trail.new_checkpoint(); trail.push(3); - trail.increase_decision_level(); + trail.new_checkpoint(); trail.push(4); trail.push(5); - assert_eq!(&[1, 2], trail.values_on_decision_level(0)); - assert_eq!(&[3], trail.values_on_decision_level(1)); - assert_eq!(&[4, 5], trail.values_on_decision_level(2)); + assert_eq!(&[1, 2], trail.values_at_checkpoint(0)); + assert_eq!(&[3], trail.values_at_checkpoint(1)); + assert_eq!(&[4, 5], trail.values_at_checkpoint(2)); } } diff --git a/pumpkin-crates/core/src/branching/branchers/autonomous_search.rs b/pumpkin-crates/core/src/branching/branchers/autonomous_search.rs index f2d15325f..cb7628570 100644 --- a/pumpkin-crates/core/src/branching/branchers/autonomous_search.rs +++ b/pumpkin-crates/core/src/branching/branchers/autonomous_search.rs @@ -389,19 +389,19 @@ mod tests { )); assert_eq!(decision, Some(predicate)); - assignments.increase_decision_level(); + assignments.new_checkpoint(); // Decision Level 1 let _ = assignments.post_predicate(predicate!(x >= 5), None, &mut notification_engine); - assignments.increase_decision_level(); + assignments.new_checkpoint(); // Decision Level 2 let _ = assignments.post_predicate(predicate!(x >= 7), None, &mut notification_engine); - assignments.increase_decision_level(); + assignments.new_checkpoint(); // Decision Level 3 let _ = assignments.post_predicate(predicate!(x >= 10), None, &mut notification_engine); - assignments.increase_decision_level(); + assignments.new_checkpoint(); // We end at decision level 4 let decision = brancher.next_decision(&mut SelectionContext::new( @@ -461,7 +461,7 @@ mod tests { let x = assignments.grow(0, 10); notification_engine.grow(); - assignments.increase_decision_level(); + assignments.new_checkpoint(); let _ = assignments.post_predicate(predicate!(x == 7), None, &mut notification_engine); let mut brancher = AutonomousSearch::default_over_all_variables(&assignments); diff --git a/pumpkin-crates/core/src/branching/variable_selection/random.rs b/pumpkin-crates/core/src/branching/variable_selection/random.rs index af34fd89a..703570cde 100644 --- a/pumpkin-crates/core/src/branching/variable_selection/random.rs +++ b/pumpkin-crates/core/src/branching/variable_selection/random.rs @@ -139,7 +139,7 @@ mod tests { assert_eq!(selected.unwrap(), integer_variables[1]); } - assignments.increase_decision_level(); + assignments.new_checkpoint(); let _ = assignments.post_predicate( predicate!(integer_variables[1] >= 7), None, diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs b/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs index 5ba85e1d3..23d89d81c 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs @@ -2,26 +2,18 @@ use std::fmt::Debug; use super::minimisers::SemanticMinimiser; use crate::Random; -use crate::basic_types::EmptyDomainConflict; use crate::basic_types::StoredConflictInfo; use crate::branching::Brancher; use crate::containers::HashMap; -use crate::containers::StorageKey; -use crate::engine::Assignments; use crate::engine::ConstraintSatisfactionSolver; -use crate::engine::PropagatorQueue; +use crate::engine::EmptyDomainConflict; use crate::engine::RestartStrategy; -use crate::engine::TrailedValues; -use crate::engine::VariableNames; +use crate::engine::State; use crate::engine::constraint_satisfaction_solver::CSPSolverState; -use crate::engine::notifications::NotificationEngine; use crate::engine::predicates::predicate::Predicate; use crate::engine::predicates::predicate::PredicateType; use crate::engine::propagation::CurrentNogood; use crate::engine::propagation::ExplanationContext; -use crate::engine::propagation::store::PropagatorStore; -use crate::engine::reason::ReasonRef; -use crate::engine::reason::ReasonStore; use crate::engine::solver_statistics::SolverStatistics; use crate::predicate; use crate::predicates::PropositionalConjunction; @@ -37,28 +29,20 @@ use crate::pumpkin_assert_simple; /// /// All fields are made public for the time being for simplicity. In the future that may change. pub(crate) struct ConflictAnalysisContext<'a> { - pub(crate) assignments: &'a mut Assignments, pub(crate) solver_state: &'a mut CSPSolverState, - pub(crate) reason_store: &'a mut ReasonStore, pub(crate) brancher: &'a mut dyn Brancher, - pub(crate) propagators: &'a mut PropagatorStore, pub(crate) semantic_minimiser: &'a mut SemanticMinimiser, - pub(crate) propagator_queue: &'a mut PropagatorQueue, - - pub(crate) notification_engine: &'a mut NotificationEngine, - pub(crate) counters: &'a mut SolverStatistics, pub(crate) proof_log: &'a mut ProofLog, pub(crate) should_minimise: bool, pub(crate) unit_nogood_inference_codes: &'a mut HashMap, - pub(crate) trailed_values: &'a mut TrailedValues, - pub(crate) variable_names: &'a VariableNames, pub(crate) rng: &'a mut dyn Random, pub(crate) restart_strategy: &'a mut RestartStrategy, + pub(crate) state: &'a mut State, } impl Debug for ConflictAnalysisContext<'_> { @@ -70,22 +54,14 @@ impl Debug for ConflictAnalysisContext<'_> { impl ConflictAnalysisContext<'_> { /// Returns the last decision which was made by the solver. pub(crate) fn find_last_decision(&mut self) -> Option { - self.assignments.find_last_decision() + self.state.assignments.find_last_decision() } /// Posts the predicate with reason an empty reason. pub(crate) fn enqueue_propagated_predicate(&mut self, predicate: Predicate) { - // This should only happen when we are not learning clauses. In that case, the proof log is - // also nonsensical. So we can supply a garbage inference code. - let garbage_inference_code = InferenceCode::create_from_index(0); - let update_occurred = self - .assignments - .post_predicate( - predicate, - Some((ReasonRef(0), garbage_inference_code)), - self.notification_engine, - ) + .state + .post(predicate) .expect("Expected enqueued predicate to not lead to conflict directly"); pumpkin_assert_simple!( @@ -97,14 +73,9 @@ impl ConflictAnalysisContext<'_> { /// Backtracks the solver to the provided backtrack level. pub(crate) fn backtrack(&mut self, backtrack_level: usize) { ConstraintSatisfactionSolver::backtrack( - self.notification_engine, - self.assignments, - self.reason_store, - self.propagator_queue, - self.propagators, + self.state, backtrack_level, self.brancher, - self.trailed_values, self.rng, ) } @@ -115,10 +86,11 @@ impl ConflictAnalysisContext<'_> { let conflict_nogood = match self.solver_state.get_conflict_info() { StoredConflictInfo::Propagator(conflict) => { let _ = self.proof_log.log_inference( + &self.state.inference_codes, conflict.inference_code, conflict.conjunction.iter().copied(), None, - self.variable_names, + self.state.variable_names(), ); conflict.conjunction @@ -134,20 +106,16 @@ impl ConflictAnalysisContext<'_> { for &predicate in conflict_nogood.iter() { let predicate_dl = self - .assignments - .get_decision_level_for_predicate(&predicate) + .state + .get_checkpoint_for_predicate(predicate) .expect("all predicates in the conflict nogood should be assigned to true"); if predicate_dl == 0 { explain_root_assignment( &mut RootExplanationContext { - propagators: self.propagators, proof_log: self.proof_log, unit_nogood_inference_codes: self.unit_nogood_inference_codes, - assignments: self.assignments, - reason_store: self.reason_store, - notification_engine: self.notification_engine, - variable_names: self.variable_names, + state: self.state, }, predicate, ); @@ -156,12 +124,7 @@ impl ConflictAnalysisContext<'_> { conflict_nogood .into_iter() - .filter(|p| { - self.assignments - .get_decision_level_for_predicate(p) - .unwrap() - > 0 - }) + .filter(|&p| self.state.get_checkpoint_for_predicate(p).unwrap() > 0) .collect() } @@ -169,73 +132,26 @@ impl ConflictAnalysisContext<'_> { /// `reason_buffer`. /// /// If `predicate` is not true, or it is a decision, then this function will panic. - #[allow( - clippy::too_many_arguments, - reason = "borrow checker complains either here or elsewhere" - )] pub(crate) fn get_propagation_reason( predicate: Predicate, - assignments: &Assignments, current_nogood: CurrentNogood<'_>, - reason_store: &mut ReasonStore, - propagators: &mut PropagatorStore, proof_log: &mut ProofLog, unit_nogood_inference_codes: &HashMap, reason_buffer: &mut (impl Extend + AsRef<[Predicate]>), - notification_engine: &mut NotificationEngine, - variable_names: &VariableNames, + state: &mut State, ) { - // TODO: this function could be put into the reason store - - // Note that this function can only be called with propagations, and never decision - // predicates. Furthermore only predicate from the current decision level will be - // considered. This is due to how the 1uip conflict analysis works: it scans the - // predicates in reverse order of assignment, and stops as soon as there is only one - // predicate from the current decision level in the learned nogood. - - // This means that the procedure would never ask for the reason of the decision predicate - // from the current decision level, because that would mean that all other predicates from - // the current decision level have been removed from the nogood, and the decision - // predicate is the only one left, but in that case, the 1uip would terminate since - // there would be only one predicate from the current decision level. For this - // reason, it is safe to assume that in the following, that any input predicate is - // indeed a propagated predicate. - if assignments.is_initial_bound(predicate) { - return; - } + let trail_index = state.get_propagation_reason(predicate, reason_buffer, current_nogood); - let trail_position = assignments - .get_trail_position(&predicate) - .expect("The predicate must be true during conflict analysis."); - - let trail_entry = assignments.get_trail_entry(trail_position); - - // We distinguish between three cases: - // 1) The predicate is explicitly present on the trail. - if trail_entry.predicate == predicate { + if let Some(trail_index) = trail_index { + let trail_entry = state.assignments.get_trail_entry(trail_index); let (reason_ref, inference_code) = trail_entry .reason .expect("Cannot be a null reason for propagation."); - let propagator_id = reason_store.get_propagator(reason_ref); - - let explanation_context = ExplanationContext::new( - assignments, - current_nogood, - trail_position, - notification_engine, - ); + let propagator_id = state.reason_store.get_propagator(reason_ref); - let reason_exists = reason_store.get_or_compute( - reason_ref, - explanation_context, - propagators, - reason_buffer, - ); - - assert!(reason_exists, "reason reference should not be stale"); - - if propagators + if state + .propagators .as_propagator_handle::(propagator_id) .is_some() && reason_buffer.as_ref().is_empty() @@ -258,248 +174,24 @@ impl ConflictAnalysisContext<'_> { }) .expect("Expected to be able to retrieve step id for unit nogood"); - let _ = - proof_log.log_inference(*inference_code, [], Some(predicate), variable_names); + let _ = proof_log.log_inference( + &state.inference_codes, + *inference_code, + [], + Some(predicate), + state.variable_names(), + ); } else { // Otherwise we log the inference which was used to derive the nogood let _ = proof_log.log_inference( + &state.inference_codes, inference_code, reason_buffer.as_ref().iter().copied(), Some(predicate), - variable_names, + state.variable_names(), ); } } - // 2) The predicate is true due to a propagation, and not explicitly on the trail. - // It is necessary to further analyse what was the reason for setting the predicate true. - else { - // The reason for propagation depends on: - // 1) The predicate on the trail at the moment the input predicate became true, and - // 2) The input predicate. - match ( - trail_entry.predicate.get_predicate_type(), - predicate.get_predicate_type(), - ) { - (PredicateType::LowerBound, PredicateType::LowerBound) => { - let trail_lower_bound = trail_entry.predicate.get_right_hand_side(); - let domain_id = predicate.get_domain(); - let input_lower_bound = predicate.get_right_hand_side(); - // Both the input predicate and the trail predicate are lower bound - // literals. Two cases to consider: - // 1) The trail predicate has a greater right-hand side, meaning - // the reason for the input predicate is true is because a stronger - // right-hand side predicate was posted. We can reuse the same - // reason as for the trail bound. - // todo: could consider lifting here, since the trail bound - // might be too strong. - if trail_lower_bound > input_lower_bound { - reason_buffer.extend(std::iter::once(trail_entry.predicate)); - } - // Otherwise, the input bound is strictly greater than the trailed - // bound. This means the reason is due to holes in the domain. - else { - // Note that the bounds cannot be equal. - // If the bound were equal, the predicate would be explicitly on the - // trail, so we would have detected this case earlier. - pumpkin_assert_simple!(trail_lower_bound < input_lower_bound); - - // The reason for the propagation of the input predicate [x >= a] is - // because [x >= a-1] & [x != a]. Conflict analysis will then - // recursively decompose these further. - - // Note that we do not need to worry about decreasing the lower - // bounds so much so that it reaches its root lower bound, for which - // there is no reason since it is given as input to the problem. - // We cannot reach the original lower bound since in the 1uip, we - // only look for reasons for predicates from the current decision - // level, and we never look for reasons at the root level. - - let one_less_bound_predicate = - predicate!(domain_id >= input_lower_bound - 1); - - let not_equals_predicate = predicate!(domain_id != input_lower_bound - 1); - reason_buffer.extend(std::iter::once(one_less_bound_predicate)); - reason_buffer.extend(std::iter::once(not_equals_predicate)); - } - } - (PredicateType::LowerBound, PredicateType::NotEqual) => { - let trail_lower_bound = trail_entry.predicate.get_right_hand_side(); - let not_equal_constant = predicate.get_right_hand_side(); - // The trail entry is a lower bound literal, - // and the input predicate is a not equals. - // Only one case to consider: - // The trail lower bound is greater than the not_equals_constant, - // so it safe to take the reason from the trail. - // todo: lifting could be used here - pumpkin_assert_simple!(trail_lower_bound > not_equal_constant); - reason_buffer.extend(std::iter::once(trail_entry.predicate)); - } - (PredicateType::LowerBound, PredicateType::Equal) => { - let domain_id = predicate.get_domain(); - let equality_constant = predicate.get_right_hand_side(); - // The input predicate is an equality predicate, and the trail predicate - // is a lower bound predicate. This means that the time of posting the - // trail predicate is when the input predicate became true. - - // Note that the input equality constant does _not_ necessarily equal - // the trail lower bound. This would be the - // case when the the trail lower bound is lower than the input equality - // constant, but due to holes in the domain, the lower bound got raised - // to just the value of the equality constant. - // For example, {1, 2, 3, 10}, then posting [x >= 5] will raise the - // lower bound to x >= 10. - - let predicate_lb = predicate!(domain_id >= equality_constant); - let predicate_ub = predicate!(domain_id <= equality_constant); - reason_buffer.extend(std::iter::once(predicate_lb)); - reason_buffer.extend(std::iter::once(predicate_ub)); - } - (PredicateType::UpperBound, PredicateType::UpperBound) => { - let trail_upper_bound = trail_entry.predicate.get_right_hand_side(); - let domain_id = predicate.get_domain(); - let input_upper_bound = predicate.get_right_hand_side(); - // Both the input and trail predicates are upper bound predicates. - // There are two scenarios to consider: - // 1) The input upper bound is greater than the trail upper bound, meaning that - // the reason for the input predicate is the propagation of a stronger upper - // bound. We can safely use the reason for of the trail predicate as the - // reason for the input predicate. - // todo: lifting could be applied here. - if trail_upper_bound < input_upper_bound { - reason_buffer.extend(std::iter::once(trail_entry.predicate)); - } else { - // I think it cannot be that the bounds are equal, since otherwise we - // would have found the predicate explicitly on the trail. - pumpkin_assert_simple!(trail_upper_bound > input_upper_bound); - - // The input upper bound is greater than the trail predicate, meaning - // that holes in the domain also played a rule in lowering the upper - // bound. - - // The reason of the input predicate [x <= a] is computed recursively as - // the reason for [x <= a + 1] & [x != a + 1]. - - let new_ub_predicate = predicate!(domain_id <= input_upper_bound + 1); - let not_equal_predicate = predicate!(domain_id != input_upper_bound + 1); - reason_buffer.extend(std::iter::once(new_ub_predicate)); - reason_buffer.extend(std::iter::once(not_equal_predicate)); - } - } - (PredicateType::UpperBound, PredicateType::NotEqual) => { - let trail_upper_bound = trail_entry.predicate.get_right_hand_side(); - let not_equal_constant = predicate.get_right_hand_side(); - // The input predicate is a not equal predicate, and the trail predicate is - // an upper bound predicate. This is only possible when the upper bound was - // pushed below the not equals value. Otherwise the hole would have been - // explicitly placed on the trail and we would have found it earlier. - pumpkin_assert_simple!(not_equal_constant > trail_upper_bound); - - // The bound was set past the not equals, so we can safely returns the trail - // reason. todo: can do lifting here. - reason_buffer.extend(std::iter::once(trail_entry.predicate)); - } - (PredicateType::UpperBound, PredicateType::Equal) => { - let domain_id = predicate.get_domain(); - let equality_constant = predicate.get_right_hand_side(); - // The input predicate is an equality predicate, and the trail predicate - // is an upper bound predicate. This means that the time of posting the - // trail predicate is when the input predicate became true. - - // Note that the input equality constant does _not_ necessarily equal - // the trail upper bound. This would be the - // case when the the trail upper bound is greater than the input equality - // constant, but due to holes in the domain, the upper bound got lowered - // to just the value of the equality constant. - // For example, x = {1, 2, 3, 8, 15}, setting [x <= 12] would lower the - // upper bound to x <= 8. - - // Note that it could be that one of the two predicates are decision - // predicates, so we need to use the substitute functions. - - let predicate_lb = predicate!(domain_id >= equality_constant); - let predicate_ub = predicate!(domain_id <= equality_constant); - reason_buffer.extend(std::iter::once(predicate_lb)); - reason_buffer.extend(std::iter::once(predicate_ub)); - } - (PredicateType::NotEqual, PredicateType::LowerBound) => { - let not_equal_constant = trail_entry.predicate.get_right_hand_side(); - let domain_id = predicate.get_domain(); - let input_lower_bound = predicate.get_right_hand_side(); - // The trail predicate is not equals, but the input predicate is a lower - // bound predicate. This means that creating the hole in the domain resulted - // in raising the lower bound. - - // I think this holds. The not_equals_constant cannot be greater, since that - // would not impact the lower bound. It can also not be the same, since - // creating a hole cannot result in the lower bound being raised to the - // hole, there must be some other reason for that to happen, which we would - // find earlier. - pumpkin_assert_simple!(input_lower_bound > not_equal_constant); - - // The reason for the input predicate [x >= a] is computed recursively as - // the reason for [x >= a - 1] & [x != a - 1]. - let new_lb_predicate = predicate!(domain_id >= input_lower_bound - 1); - let new_not_equals_predicate = predicate!(domain_id != input_lower_bound - 1); - - reason_buffer.extend(std::iter::once(new_lb_predicate)); - reason_buffer.extend(std::iter::once(new_not_equals_predicate)); - } - (PredicateType::NotEqual, PredicateType::UpperBound) => { - let not_equal_constant = trail_entry.predicate.get_right_hand_side(); - let domain_id = predicate.get_domain(); - let input_upper_bound = predicate.get_right_hand_side(); - // The trail predicate is not equals, but the input predicate is an upper - // bound predicate. This means that creating the hole in the domain resulted - // in lower the upper bound. - - // I think this holds. The not_equals_constant cannot be smaller, since that - // would not impact the upper bound. It can also not be the same, since - // creating a hole cannot result in the upper bound being lower to the - // hole, there must be some other reason for that to happen, which we would - // find earlier. - pumpkin_assert_simple!(input_upper_bound < not_equal_constant); - - // The reason for the input predicate [x <= a] is computed recursively as - // the reason for [x <= a + 1] & [x != a + 1]. - let new_ub_predicate = predicate!(domain_id <= input_upper_bound + 1); - let new_not_equals_predicate = predicate!(domain_id != input_upper_bound + 1); - - reason_buffer.extend(std::iter::once(new_ub_predicate)); - reason_buffer.extend(std::iter::once(new_not_equals_predicate)); - } - (PredicateType::NotEqual, PredicateType::Equal) => { - let domain_id = predicate.get_domain(); - let equality_constant = predicate.get_right_hand_side(); - // The trail predicate is not equals, but the input predicate is - // equals. The only time this could is when the not equals forces the - // lower/upper bounds to meet. So we simply look for the reasons for those - // bounds recursively. - - // Note that it could be that one of the two predicates are decision - // predicates, so we need to use the substitute functions. - - let predicate_lb = predicate!(domain_id >= equality_constant); - let predicate_ub = predicate!(domain_id <= equality_constant); - - reason_buffer.extend(std::iter::once(predicate_lb)); - reason_buffer.extend(std::iter::once(predicate_ub)); - } - ( - PredicateType::Equal, - PredicateType::LowerBound | PredicateType::UpperBound | PredicateType::NotEqual, - ) => { - // The trail predicate is equality, but the input predicate is either a - // lower-bound, upper-bound, or not equals. - // - // TODO: could consider lifting here - reason_buffer.extend(std::iter::once(trail_entry.predicate)) - } - _ => unreachable!( - "Unreachable combination of {} and {}", - trail_entry.predicate, predicate - ), - }; - } } fn compute_conflict_nogood( @@ -511,29 +203,30 @@ impl ConflictAnalysisContext<'_> { // Look up the reason for the bound that changed. // The reason for changing the bound cannot be a decision, so we can safely unwrap. let mut empty_domain_reason: Vec = vec![]; - let _ = self.reason_store.get_or_compute( + let _ = self.state.reason_store.get_or_compute( conflict.trigger_reason, ExplanationContext::without_working_nogood( - self.assignments, - self.assignments.num_trail_entries(), // Note that we do not do a + &self.state.assignments, + self.state.assignments.num_trail_entries(), // Note that we do not do a // `-1` here; the `Assignments` automatically undoes the last trail entry when an // empty domain is created meaning that the `-1` has already been applied. - self.notification_engine, + &mut self.state.notification_engine, ), - self.propagators, + &mut self.state.propagators, &mut empty_domain_reason, ); // We also need to log this last propagation to the proof log as an inference. let _ = self.proof_log.log_inference( + &self.state.inference_codes, conflict.trigger_inference_code, empty_domain_reason.iter().copied(), Some(conflict.trigger_predicate), - self.variable_names, + self.state.variable_names(), ); - let old_lower_bound = self.assignments.get_lower_bound(conflict_domain); - let old_upper_bound = self.assignments.get_upper_bound(conflict_domain); + let old_lower_bound = self.state.lower_bound(conflict_domain); + let old_upper_bound = self.state.upper_bound(conflict_domain); match conflict.trigger_predicate.get_predicate_type() { PredicateType::LowerBound => { diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs index ee9bf26f5..c44993c8c 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs @@ -7,6 +7,7 @@ use crate::engine::propagation::CurrentNogood; use crate::predicates::Predicate; use crate::proof::RootExplanationContext; use crate::proof::explain_root_assignment; +use crate::pumpkin_assert_eq_moderate; use crate::pumpkin_assert_moderate; use crate::pumpkin_assert_simple; @@ -40,7 +41,7 @@ impl RecursiveMinimiser { ) { let num_literals_before_minimisation = nogood.len(); - self.initialise_minimisation_data_structures(nogood, context.assignments); + self.initialise_minimisation_data_structures(nogood, &context.state.assignments); // Iterate over each predicate and check whether it is a dominated predicate. let mut end_position: usize = 0; @@ -78,7 +79,7 @@ impl RecursiveMinimiser { context: &mut ConflictAnalysisContext, current_nogood: &[Predicate], ) { - pumpkin_assert_moderate!(context.assignments.is_predicate_satisfied(input_predicate)); + pumpkin_assert_eq_moderate!(context.state.truth_value(input_predicate), Some(true)); self.current_depth += 1; @@ -98,7 +99,11 @@ impl RecursiveMinimiser { // If the predicate is a decision predicate, it cannot be a predicate from the original // learned nogood since those are labelled as part of initialisation. // Therefore the decision literal is labelled as poison and then return. - if context.assignments.is_decision_predicate(&input_predicate) { + if context + .state + .assignments + .is_decision_predicate(&input_predicate) + { self.assign_predicate_label(input_predicate, Label::Poison); self.current_depth -= 1; return; @@ -108,8 +113,8 @@ impl RecursiveMinimiser { // (levels from the original learned clause) cannot be removed. if !self.is_decision_level_allowed( context - .assignments - .get_decision_level_for_predicate(&input_predicate) + .state + .get_checkpoint_for_predicate(input_predicate) .unwrap(), ) { self.assign_predicate_label(input_predicate, Label::Poison); @@ -122,22 +127,18 @@ impl RecursiveMinimiser { let mut reason = vec![]; ConflictAnalysisContext::get_propagation_reason( input_predicate, - context.assignments, CurrentNogood::from(current_nogood), - context.reason_store, - context.propagators, context.proof_log, context.unit_nogood_inference_codes, &mut reason, - context.notification_engine, - context.variable_names, + context.state, ); for antecedent_predicate in reason.iter().copied() { // Root assignments can be safely ignored. if context - .assignments - .get_decision_level_for_predicate(&antecedent_predicate) + .state + .get_checkpoint_for_predicate(antecedent_predicate) .unwrap() == 0 { @@ -146,13 +147,9 @@ impl RecursiveMinimiser { // the proof is aware that that root-level assignment is used. explain_root_assignment( &mut RootExplanationContext { - propagators: context.propagators, proof_log: context.proof_log, unit_nogood_inference_codes: context.unit_nogood_inference_codes, - assignments: context.assignments, - reason_store: context.reason_store, - notification_engine: context.notification_engine, - variable_names: context.variable_names, + state: context.state, }, antecedent_predicate, ); @@ -244,9 +241,9 @@ impl RecursiveMinimiser { // Predicates from the current decision level are always kept. // This is the analogue of asserting literals. if assignments - .get_decision_level_for_predicate(&predicate) + .get_checkpoint_for_predicate(&predicate) .unwrap() - == assignments.get_decision_level() + == assignments.get_checkpoint() { let _ = self.label_assignments.insert(predicate, Some(Label::Keep)); continue; @@ -261,7 +258,7 @@ impl RecursiveMinimiser { self.mark_decision_level_as_allowed( assignments - .get_decision_level_for_predicate(&predicate) + .get_checkpoint_for_predicate(&predicate) .unwrap(), ); } diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/resolvers/no_learning_resolver.rs b/pumpkin-crates/core/src/engine/conflict_analysis/resolvers/no_learning_resolver.rs index c69a8b1f5..f7733f640 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/resolvers/no_learning_resolver.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/resolvers/no_learning_resolver.rs @@ -11,7 +11,7 @@ impl ConflictResolver for NoLearningResolver { .find_last_decision() .expect("the solver is not at decision level 0, so there exists a last decision"); - context.backtrack(context.assignments.get_decision_level() - 1); + context.backtrack(context.state.get_checkpoint() - 1); context.enqueue_propagated_predicate(!last_decision); } } diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/resolvers/resolution_resolver.rs b/pumpkin-crates/core/src/engine/conflict_analysis/resolvers/resolution_resolver.rs index 4f85187c3..57a51cd27 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/resolvers/resolution_resolver.rs @@ -1,19 +1,16 @@ use super::ConflictResolver; -use crate::PropagatorHandle; use crate::basic_types::PredicateId; use crate::basic_types::PredicateIdGenerator; use crate::basic_types::moving_averages::MovingAverage; use crate::branching::Brancher; use crate::containers::KeyValueHeap; use crate::containers::StorageKey; -use crate::engine::Assignments; use crate::engine::Lbd; use crate::engine::conflict_analysis::ConflictAnalysisContext; use crate::engine::conflict_analysis::Mode; use crate::engine::conflict_analysis::RecursiveMinimiser; use crate::engine::constraint_satisfaction_solver::NogoodLabel; use crate::engine::propagation::CurrentNogood; -use crate::engine::propagation::PropagationContextMut; use crate::predicates::Predicate; use crate::proof::InferenceCode; use crate::proof::RootExplanationContext; @@ -22,6 +19,7 @@ use crate::propagators::nogoods::NogoodPropagator; use crate::pumpkin_assert_advanced; use crate::pumpkin_assert_moderate; use crate::pumpkin_assert_simple; +use crate::state::PropagatorHandle; /// Resolve conflicts according to the CDCL procedure. /// @@ -71,16 +69,16 @@ impl ConflictResolver for ResolutionResolver { fn resolve_conflict(&mut self, context: &mut ConflictAnalysisContext) { let learned_nogood = self.learn_nogood(context); - let current_decision_level = context.assignments.get_decision_level(); + let current_checkpoint = context.state.get_checkpoint(); context .counters .learned_clause_statistics .average_backtrack_amount - .add_term((current_decision_level - learned_nogood.backjump_level) as u64); + .add_term((current_checkpoint - learned_nogood.backjump_level) as u64); context.counters.engine_statistics.sum_of_backjumps += - current_decision_level as u64 - 1 - learned_nogood.backjump_level as u64; - if current_decision_level - learned_nogood.backjump_level > 1 { + current_checkpoint as u64 - 1 - learned_nogood.backjump_level as u64; + if current_checkpoint - learned_nogood.backjump_level > 1 { context.counters.engine_statistics.num_backjumps += 1; } @@ -89,8 +87,8 @@ impl ConflictResolver for ResolutionResolver { // conflict happened context.restart_strategy.notify_conflict( self.lbd_helper - .compute_lbd(&learned_nogood.predicates, context.assignments), - context.assignments.get_pruned_value_count(), + .compute_lbd(&learned_nogood.predicates, &context.state.assignments), + context.state.assignments.get_pruned_value_count(), ); context.backtrack(learned_nogood.backjump_level); @@ -99,12 +97,12 @@ impl ConflictResolver for ResolutionResolver { .proof_log .log_deduction( learned_nogood.predicates.iter().copied(), - context.variable_names, + context.state.variable_names(), ) .expect("Failed to write proof log"); let inference_code = context - .proof_log + .state .create_inference_code(constraint_tag, NogoodLabel); if learned_nogood.predicates.len() == 1 { @@ -150,28 +148,19 @@ impl ResolutionResolver { let conflict_nogood = context.get_conflict_nogood(); - let mut root_explanation_context = if context.proof_log.is_logging_inferences() { - Some(RootExplanationContext { - propagators: context.propagators, - proof_log: context.proof_log, - unit_nogood_inference_codes: context.unit_nogood_inference_codes, - assignments: context.assignments, - reason_store: context.reason_store, - notification_engine: context.notification_engine, - variable_names: context.variable_names, - }) - } else { - None - }; - // Initialise the data structures with the conflict nogood. for predicate in conflict_nogood.iter() { + let should_explain = context.proof_log.is_logging_inferences(); self.add_predicate_to_conflict_nogood( *predicate, - context.assignments, context.brancher, self.mode, - root_explanation_context.as_mut(), + &mut RootExplanationContext { + proof_log: context.proof_log, + unit_nogood_inference_codes: context.unit_nogood_inference_codes, + state: context.state, + }, + should_explain, ); } @@ -211,42 +200,29 @@ impl ResolutionResolver { self.reason_buffer.clear(); ConflictAnalysisContext::get_propagation_reason( next_predicate, - context.assignments, CurrentNogood::new( &self.to_process_heap, &self.processed_nogood_predicates, &self.predicate_id_generator, ), - context.reason_store, - context.propagators, context.proof_log, context.unit_nogood_inference_codes, &mut self.reason_buffer, - context.notification_engine, - context.variable_names, + context.state, ); - let mut root_explanation_context = if context.proof_log.is_logging_inferences() { - Some(RootExplanationContext { - propagators: context.propagators, - proof_log: context.proof_log, - unit_nogood_inference_codes: context.unit_nogood_inference_codes, - assignments: context.assignments, - reason_store: context.reason_store, - notification_engine: context.notification_engine, - variable_names: context.variable_names, - }) - } else { - None - }; - for i in 0..self.reason_buffer.len() { + let should_explain = context.proof_log.is_logging_inferences(); self.add_predicate_to_conflict_nogood( self.reason_buffer[i], - context.assignments, context.brancher, self.mode, - root_explanation_context.as_mut(), + &mut RootExplanationContext { + proof_log: context.proof_log, + unit_nogood_inference_codes: context.unit_nogood_inference_codes, + state: context.state, + }, + should_explain, ); } } @@ -260,19 +236,11 @@ impl ResolutionResolver { learned_nogood: LearnedNogood, inference_code: InferenceCode, ) { - let mut propagation_context = PropagationContextMut::new( - context.trailed_values, - context.assignments, - context.reason_store, - context.semantic_minimiser, - context.notification_engine, - self.nogood_propagator_handle.propagator_id(), - ); - - let nogood_propagator = context - .propagators - .get_propagator_mut(self.nogood_propagator_handle) - .expect("nogood propagator handle should refer to nogood propagator"); + let (nogood_propagator, mut propagation_context) = context + .state + .get_propagator_mut_with_context(self.nogood_propagator_handle); + let nogood_propagator = + nogood_propagator.expect("nogood propagator handle should refer to nogood propagator"); nogood_propagator.add_asserting_nogood( learned_nogood.predicates, @@ -296,24 +264,32 @@ impl ResolutionResolver { fn add_predicate_to_conflict_nogood( &mut self, predicate: Predicate, - assignments: &Assignments, brancher: &mut dyn Brancher, mode: AnalysisMode, - root_explanation_context: Option<&mut RootExplanationContext>, + context: &mut RootExplanationContext, + should_explain: bool, ) { - let dec_level = assignments - .get_decision_level_for_predicate(&predicate) + let dec_level = context + .state + .assignments + .get_checkpoint_for_predicate(&predicate) .unwrap_or_else(|| { panic!( "Expected predicate {predicate} to be assigned but bounds were ({}, {})", - assignments.get_lower_bound(predicate.get_domain()), - assignments.get_upper_bound(predicate.get_domain()), + context + .state + .assignments + .get_lower_bound(predicate.get_domain()), + context + .state + .assignments + .get_upper_bound(predicate.get_domain()), ) }); // Ignore root level predicates. if dec_level == 0 { // do nothing, only possibly explain the predicate in the proof - if let Some(context) = root_explanation_context { + if should_explain { explain_root_assignment(context, predicate); } } @@ -325,8 +301,10 @@ impl ResolutionResolver { // If the variables are not decisions then we want to potentially add them to the heap, // otherwise we add it to the decision predicates which have been discovered previously else if match mode { - AnalysisMode::OneUIP => dec_level == assignments.get_decision_level(), - AnalysisMode::AllDecision => !assignments.is_decision_predicate(&predicate), + AnalysisMode::OneUIP => dec_level == context.state.assignments.get_checkpoint(), + AnalysisMode::AllDecision => { + !context.state.assignments.is_decision_predicate(&predicate) + } } { let predicate_id = self.predicate_id_generator.get_id(predicate); // The first time we encounter the predicate, we initialise its value in the @@ -354,7 +332,11 @@ impl ResolutionResolver { { brancher.on_appearance_in_conflict_predicate(predicate); - let trail_position = assignments.get_trail_position(&predicate).unwrap(); + let trail_position = context + .state + .assignments + .get_trail_position(&predicate) + .unwrap(); // The goal is to traverse predicate in reverse order of the trail. // @@ -373,11 +355,12 @@ impl ResolutionResolver { // by assigning explicitly set predicates the // value `2 * trail_position`, whereas implied predicates get `2 * // trail_position + 1`. - let heap_value = if assignments.trail[trail_position].predicate == predicate { - trail_position * 2 - } else { - trail_position * 2 + 1 - }; + let heap_value = + if context.state.assignments.trail[trail_position].predicate == predicate { + trail_position * 2 + } else { + trail_position * 2 + 1 + }; // We restore the key and since we know that the value is 0, we can safely // increment with `heap_value` @@ -424,7 +407,7 @@ impl ResolutionResolver { // recursive minimisation) let mut clean_nogood: Vec = context.semantic_minimiser.minimise( &self.processed_nogood_predicates, - context.assignments, + &context.state.assignments, if !context.should_minimise { // If we do not minimise then we do the equality // merging in the first iteration of removing @@ -445,7 +428,7 @@ impl ResolutionResolver { let size_before_semantic_minimisation = clean_nogood.len(); clean_nogood = context.semantic_minimiser.minimise( &clean_nogood, - context.assignments, + &context.state.assignments, Mode::EnableEqualityMerging, ); context @@ -463,11 +446,11 @@ impl ResolutionResolver { while index < clean_nogood.len() { let predicate = clean_nogood[index]; let dl = context - .assignments - .get_decision_level_for_predicate(&predicate) + .state + .get_checkpoint_for_predicate(predicate) .unwrap(); - if dl == context.assignments.get_decision_level() { + if dl == context.state.get_checkpoint() { clean_nogood.swap(0, index); index -= 1; } else if dl > highest_level_below_current { @@ -482,8 +465,8 @@ impl ResolutionResolver { // This is the backjump level. let backjump_level = if clean_nogood.len() > 1 { context - .assignments - .get_decision_level_for_predicate(&clean_nogood[1]) + .state + .get_checkpoint_for_predicate(clean_nogood[1]) .unwrap() } else { // For unit nogoods, the solver backtracks to the root level. @@ -494,7 +477,7 @@ impl ResolutionResolver { clean_nogood .iter() .skip(1) - .all(|p| context.assignments.is_predicate_satisfied(*p)) + .all(|p| context.state.truth_value(*p) == Some(true)) ); // TODO: asserting predicate may be bumped twice, probably not a problem. diff --git a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs index 3ef541e60..1f2a0fe08 100644 --- a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs +++ b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs @@ -3,6 +3,7 @@ use std::cmp::max; use std::collections::VecDeque; use std::fmt::Debug; +use std::sync::Arc; #[allow( clippy::disallowed_types, @@ -12,16 +13,11 @@ use rand::SeedableRng; use rand::rngs::SmallRng; use super::ResolutionResolver; -use super::TrailedValues; -use super::VariableNames; use super::conflict_analysis::AnalysisMode; use super::conflict_analysis::ConflictAnalysisContext; use super::conflict_analysis::NoLearningResolver; use super::conflict_analysis::SemanticMinimiser; -use super::notifications::NotificationEngine; -use super::propagation::PropagatorId; use super::propagation::constructor::PropagatorConstructor; -use super::propagation::store::PropagatorStore; use super::solver_statistics::SolverStatistics; use super::termination::TerminationCondition; use super::variables::IntegerVariable; @@ -30,8 +26,6 @@ use super::variables::Literal; use crate::Solver; use crate::basic_types::CSPSolverExecutionFlag; use crate::basic_types::ConstraintOperationError; -use crate::basic_types::EmptyDomainConflict; -use crate::basic_types::Inconsistency; use crate::basic_types::PredicateId; use crate::basic_types::Random; use crate::basic_types::SolutionReference; @@ -42,20 +36,13 @@ use crate::branching::SelectionContext; use crate::containers::HashMap; use crate::declare_inference_label; use crate::engine::Assignments; -use crate::engine::DebugHelper; use crate::engine::RestartOptions; use crate::engine::RestartStrategy; +use crate::engine::State; use crate::engine::conflict_analysis::ConflictResolver as Resolver; -use crate::engine::cp::PropagatorQueue; use crate::engine::predicates::predicate::Predicate; -use crate::engine::propagation::ExplanationContext; -use crate::engine::propagation::PropagationContext; -use crate::engine::propagation::PropagationContextMut; -use crate::engine::propagation::Propagator; -use crate::engine::propagation::constructor::PropagatorConstructorContext; use crate::engine::propagation::store::PropagatorHandle; -use crate::engine::reason::ReasonStore; -use crate::engine::variables::DomainId; +use crate::options::LearningOptions; use crate::proof::ConstraintTag; use crate::proof::FinalizingContext; use crate::proof::InferenceCode; @@ -63,15 +50,15 @@ use crate::proof::ProofLog; use crate::proof::RootExplanationContext; use crate::proof::explain_root_assignment; use crate::proof::finalize_proof; -use crate::propagators::nogoods::LearningOptions; use crate::propagators::nogoods::NogoodPropagator; -use crate::pumpkin_assert_advanced; +use crate::propagators::nogoods::NogoodPropagatorConstructor; use crate::pumpkin_assert_eq_simple; -use crate::pumpkin_assert_extreme; use crate::pumpkin_assert_moderate; +use crate::pumpkin_assert_ne_moderate; use crate::pumpkin_assert_simple; -use crate::statistics::statistic_logger::StatisticLogger; +use crate::statistics::StatisticLogger; use crate::statistics::statistic_logging::should_log_statistics; +use crate::variables::DomainId; /// A solver which attempts to find a solution to a Constraint Satisfaction Problem (CSP) using /// a Lazy Clause Generation (LCG [\[1\]](https://people.eng.unimelb.edu.au/pstuckey/papers/cp09-lc.pdf)) @@ -106,10 +93,8 @@ use crate::statistics::statistic_logging::should_log_statistics; pub struct ConstraintSatisfactionSolver { /// The solver continuously changes states during the search. /// The state helps track additional information and contributes to making the code clearer. - pub(crate) state: CSPSolverState, - /// The list of propagators. Propagators live here and are queried when events (domain changes) - /// happen. The list is only traversed during synchronisation for now. - propagators: PropagatorStore, + pub(crate) solver_state: CSPSolverState, + state: State, nogood_propagator_handle: PropagatorHandle, /// Tracks information about the restarts. Occassionally the solver will undo all its decisions @@ -119,28 +104,14 @@ pub struct ConstraintSatisfactionSolver { /// Holds the assumptions when the solver is queried to solve under assumptions. assumptions: Vec, semantic_minimiser: SemanticMinimiser, - /// Tracks information related to the assignments of integer variables. - pub(crate) assignments: Assignments, - /// Dictates the order in which propagators will be called to propagate. - propagator_queue: PropagatorQueue, - /// Handles storing information about propagation reasons, which are used later to construct - /// explanations during conflict analysis - pub(crate) reason_store: ReasonStore, /// A set of counters updated during the search. solver_statistics: SolverStatistics, /// Miscellaneous constant parameters used by the solver. internal_parameters: SatisfactionSolverOptions, - /// The names of the variables in the solver. - variable_names: VariableNames, /// A map from predicates that are propagated at the root to inference codes in the proof. unit_nogood_inference_codes: HashMap, /// The resolver which is used upon a conflict. conflict_resolver: Box, - /// Keep track of trailed values (i.e. values which automatically backtrack) - pub(crate) trailed_values: TrailedValues, - /// Component responsible for providing notifications for changes to the domains of variables - /// and/or the polarity [Predicate]s - notification_engine: NotificationEngine, } impl Default for ConstraintSatisfactionSolver { @@ -214,9 +185,13 @@ impl Default for SatisfactionSolverOptions { } impl ConstraintSatisfactionSolver { + pub(crate) fn assignments(&self) -> &Assignments { + &self.state.assignments + } + /// This is a temporary accessor to help refactoring. pub fn get_solution_reference(&self) -> SolutionReference<'_> { - SolutionReference::new(&self.assignments) + self.state.get_solution_reference() } /// Conclude the proof with the unsatisfiable claim. @@ -224,7 +199,7 @@ impl ConstraintSatisfactionSolver { /// This method will finish the proof. Any new operation will not be logged to the proof. pub fn conclude_proof_unsat(&mut self) -> std::io::Result<()> { let proof = std::mem::take(&mut self.internal_parameters.proof_log); - proof.unsat(&self.variable_names) + proof.unsat(self.state.variable_names()) } /// Conclude the proof with the optimality claim. @@ -232,7 +207,7 @@ impl ConstraintSatisfactionSolver { /// This method will finish the proof. Any new operation will not be logged to the proof. pub fn conclude_proof_optimal(&mut self, bound: Predicate) -> std::io::Result<()> { let proof = std::mem::take(&mut self.internal_parameters.proof_log); - proof.optimal(bound, &self.variable_names) + proof.optimal(bound, self.state.variable_names()) } fn complete_proof(&mut self) { @@ -249,35 +224,26 @@ impl ConstraintSatisfactionSolver { } let mut conflict_analysis_context = ConflictAnalysisContext { - assignments: &mut self.assignments, counters: &mut self.solver_statistics, - solver_state: &mut self.state, - reason_store: &mut self.reason_store, + solver_state: &mut self.solver_state, brancher: &mut DummyBrancher, semantic_minimiser: &mut self.semantic_minimiser, - propagators: &mut self.propagators, - notification_engine: &mut self.notification_engine, - propagator_queue: &mut self.propagator_queue, should_minimise: self.internal_parameters.learning_clause_minimisation, proof_log: &mut self.internal_parameters.proof_log, unit_nogood_inference_codes: &mut self.unit_nogood_inference_codes, - trailed_values: &mut self.trailed_values, - variable_names: &self.variable_names, rng: &mut self.internal_parameters.random_generator, restart_strategy: &mut self.restart_strategy, + + state: &mut self.state, }; let conflict = conflict_analysis_context.get_conflict_nogood(); let context = FinalizingContext { conflict: conflict.into(), - propagators: &mut self.propagators, proof_log: &mut self.internal_parameters.proof_log, unit_nogood_inference_codes: &self.unit_nogood_inference_codes, - assignments: &self.assignments, - reason_store: &mut self.reason_store, - notification_engine: &mut self.notification_engine, - variable_names: &self.variable_names, + state: &mut self.state, }; finalize_proof(context); @@ -291,57 +257,29 @@ impl ConstraintSatisfactionSolver { // methods that offer basic functionality impl ConstraintSatisfactionSolver { pub fn new(solver_options: SatisfactionSolverOptions) -> Self { - let mut propagators = PropagatorStore::default(); - - let nogood_propagator_slot = propagators.new_propagator(); - let nogood_propagator = NogoodPropagator::with_options( - nogood_propagator_slot.key(), - // 1_000_000 bytes in 1 MB + let mut state = State::default(); + let handle = state.add_propagator(NogoodPropagatorConstructor::new( (solver_options.memory_preallocated * 1_000_000) / size_of::(), solver_options.learning_options, - ); - - let nogood_propagator_handle = nogood_propagator_slot.populate(nogood_propagator); + )); - let mut csp_solver = ConstraintSatisfactionSolver { - state: CSPSolverState::default(), + ConstraintSatisfactionSolver { + solver_state: CSPSolverState::default(), assumptions: Vec::default(), - assignments: Assignments::default(), - propagator_queue: PropagatorQueue::new(5), - reason_store: ReasonStore::default(), restart_strategy: RestartStrategy::new(solver_options.restart_options), - propagators, - nogood_propagator_handle, + nogood_propagator_handle: handle, solver_statistics: SolverStatistics::default(), - variable_names: VariableNames::default(), semantic_minimiser: SemanticMinimiser::default(), unit_nogood_inference_codes: Default::default(), conflict_resolver: match solver_options.conflict_resolver { ConflictResolver::NoLearning => Box::new(NoLearningResolver), - ConflictResolver::UIP => Box::new(ResolutionResolver::new( - nogood_propagator_handle, - AnalysisMode::OneUIP, - )), + ConflictResolver::UIP => { + Box::new(ResolutionResolver::new(handle, AnalysisMode::OneUIP)) + } }, internal_parameters: solver_options, - trailed_values: TrailedValues::default(), - notification_engine: NotificationEngine::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 - // trivially true. We need to adjust other data structures to take this into account. - let dummy_id = Predicate::trivially_true().get_domain(); - - csp_solver - .variable_names - .add_integer(dummy_id, "Dummy".to_owned()); - - assert!(dummy_id.id() == 0); - assert!(csp_solver.assignments.get_lower_bound(dummy_id) == 1); - assert!(csp_solver.assignments.get_upper_bound(dummy_id) == 1); - - csp_solver + state, + } } pub fn solve( @@ -359,7 +297,7 @@ impl ConstraintSatisfactionSolver { termination: &mut impl TerminationCondition, brancher: &mut impl Brancher, ) -> CSPSolverExecutionFlag { - if self.state.is_inconsistent() { + if self.solver_state.is_inconsistent() { return CSPSolverExecutionFlag::Infeasible; } @@ -376,7 +314,7 @@ impl ConstraintSatisfactionSolver { } pub fn get_state(&self) -> &CSPSolverState { - &self.state + &self.solver_state } pub fn get_random_generator(&mut self) -> &mut impl Random { @@ -390,35 +328,27 @@ impl ConstraintSatisfactionSolver { return; } - self.solver_statistics.log( - &self.assignments, - &self.propagators, - StatisticLogger::default(), - verbose, - ); - if verbose { - for (index, propagator) in self.propagators.iter_propagators().enumerate() { - propagator.log_statistics(StatisticLogger::new([ - propagator.name(), - "number", - index.to_string().as_str(), - ])); - } - } + self.solver_statistics + .log(StatisticLogger::default(), verbose); + self.state.log_statistics(verbose); } - pub fn create_new_literal(&mut self, name: Option) -> Literal { - let domain_id = self.create_new_integer_variable(0, 1, name); - Literal::new(domain_id) + /// Create a new [`ConstraintTag`]. + pub fn new_constraint_tag(&mut self) -> ConstraintTag { + self.internal_parameters.proof_log.new_constraint_tag() + } + + pub fn create_new_literal(&mut self, name: Option>) -> Literal { + self.state.new_literal(name) } pub fn create_new_literal_for_predicate( &mut self, predicate: Predicate, - name: Option, + name: Option>, constraint_tag: ConstraintTag, ) -> Literal { - let literal = self.create_new_literal(name); + let literal = self.state.new_literal(name); self.internal_parameters .proof_log @@ -444,21 +374,15 @@ impl ConstraintSatisfactionSolver { &mut self, lower_bound: i32, upper_bound: i32, - name: Option, + name: Option>, ) -> DomainId { assert!( - !self.state.is_inconsistent(), + !self.solver_state.is_inconsistent(), "Variables cannot be created in an inconsistent state" ); - let domain_id = self.assignments.grow(lower_bound, upper_bound); - self.notification_engine.grow(); - - if let Some(name) = name { - self.variable_names.add_integer(domain_id, name); - } - - domain_id + self.state + .new_interval_variable(lower_bound, upper_bound, name) } /// Creates an integer variable with a domain containing only the values in `values` @@ -467,20 +391,7 @@ impl ConstraintSatisfactionSolver { values: Vec, name: Option, ) -> DomainId { - let domain_id = self.assignments.create_new_integer_variable_sparse(values); - - self.notification_engine.grow(); - - if let Some(name) = name { - self.variable_names.add_integer(domain_id, name); - } - - domain_id - } - - /// Create a new [`ConstraintTag`]. - pub fn new_constraint_tag(&mut self) -> ConstraintTag { - self.internal_parameters.proof_log.new_constraint_tag() + self.state.new_sparse_variable(values, name) } /// Returns an unsatisfiable core or an [`Err`] if the provided assumptions were conflicting @@ -549,7 +460,7 @@ impl ConstraintSatisfactionSolver { /// } /// ``` pub fn extract_clausal_core(&mut self, brancher: &mut impl Brancher) -> CoreExtractionResult { - if self.state.is_infeasible() { + if self.solver_state.is_infeasible() { return CoreExtractionResult::Core(vec![]); } @@ -569,22 +480,16 @@ impl ConstraintSatisfactionSolver { }) .unwrap_or_else(|| { let mut conflict_analysis_context = ConflictAnalysisContext { - assignments: &mut self.assignments, counters: &mut self.solver_statistics, - solver_state: &mut self.state, - reason_store: &mut self.reason_store, + solver_state: &mut self.solver_state, brancher, semantic_minimiser: &mut self.semantic_minimiser, - propagators: &mut self.propagators, - notification_engine: &mut self.notification_engine, - propagator_queue: &mut self.propagator_queue, should_minimise: self.internal_parameters.learning_clause_minimisation, proof_log: &mut self.internal_parameters.proof_log, unit_nogood_inference_codes: &mut self.unit_nogood_inference_codes, - trailed_values: &mut self.trailed_values, - variable_names: &self.variable_names, rng: &mut self.internal_parameters.random_generator, restart_strategy: &mut self.restart_strategy, + state: &mut self.state, }; let mut resolver = ResolutionResolver::new( @@ -599,63 +504,40 @@ impl ConstraintSatisfactionSolver { } pub fn get_literal_value(&self, literal: Literal) -> Option { - let literal_is_true = self - .assignments - .is_predicate_satisfied(literal.get_true_predicate()); - let opposite_literal_is_true = self - .assignments - .is_predicate_satisfied((!literal).get_true_predicate()); - - pumpkin_assert_moderate!(!(literal_is_true && opposite_literal_is_true)); - - // If both the literal is not true and its negation is not true then the literal is - // unassigned - if !literal_is_true && !opposite_literal_is_true { - None - } else { - Some(literal_is_true) - } + self.state.get_literal_value(literal) } /// Get the lower bound for the given variable. pub fn get_lower_bound(&self, variable: &impl IntegerVariable) -> i32 { - variable.lower_bound(&self.assignments) + self.state.lower_bound(variable.clone()) } /// Get the upper bound for the given variable. pub fn get_upper_bound(&self, variable: &impl IntegerVariable) -> i32 { - variable.upper_bound(&self.assignments) + self.state.upper_bound(variable.clone()) } /// Determine whether `value` is in the domain of `variable`. pub fn integer_variable_contains(&self, variable: &impl IntegerVariable, value: i32) -> bool { - variable.contains(&self.assignments, value) + self.state.contains(variable.clone(), value) } /// Get the assigned integer for the given variable. If it is not assigned, `None` is returned. pub fn get_assigned_integer_value(&self, variable: &impl IntegerVariable) -> Option { - let lb = self.get_lower_bound(variable); - let ub = self.get_upper_bound(variable); - - if lb == ub { Some(lb) } else { None } + self.state.fixed_value(variable.clone()) } pub fn restore_state_at_root(&mut self, brancher: &mut impl Brancher) { - if self.assignments.get_decision_level() != 0 { + if self.state.get_checkpoint() != 0 { ConstraintSatisfactionSolver::backtrack( - &mut self.notification_engine, - &mut self.assignments, - &mut self.reason_store, - &mut self.propagator_queue, - &mut self.propagators, + &mut self.state, 0, brancher, - &mut self.trailed_values, &mut self.internal_parameters.random_generator, ); - self.state.declare_ready(); - } else if self.state.internal_state == CSPSolverStateInternal::ContainsSolution { - self.state.declare_ready(); + self.solver_state.declare_ready(); + } else if self.solver_state.internal_state == CSPSolverStateInternal::ContainsSolution { + self.solver_state.declare_ready(); } } } @@ -664,11 +546,11 @@ impl ConstraintSatisfactionSolver { impl ConstraintSatisfactionSolver { fn initialise(&mut self, assumptions: &[Predicate]) { pumpkin_assert_simple!( - !self.state.is_infeasible_under_assumptions(), + !self.solver_state.is_infeasible_under_assumptions(), "Solver is not expected to be in the infeasible under assumptions state when initialising. Missed extracting the core?" ); - self.state.declare_solving(); + self.solver_state.declare_solving(); assumptions.clone_into(&mut self.assumptions); } @@ -679,19 +561,19 @@ impl ConstraintSatisfactionSolver { ) -> CSPSolverExecutionFlag { loop { if termination.should_stop() { - self.state.declare_timeout(); + self.solver_state.declare_timeout(); return CSPSolverExecutionFlag::Timeout; } self.propagate(); - if self.state.no_conflict() { + if self.solver_state.no_conflict() { // Restarts should only occur after a new decision level has been declared to // account for the fact that all assumptions should be assigned when restarts take // place. Since one assumption is posted per decision level, all assumptions are // assigned when the decision level is strictly larger than the number of // assumptions. - if self.get_decision_level() > self.assumptions.len() + if self.get_checkpoint() > self.assumptions.len() && self.restart_strategy.should_restart() { self.restart_during_search(brancher); @@ -701,7 +583,7 @@ impl ConstraintSatisfactionSolver { self.solver_statistics.engine_statistics.peak_depth = max( self.solver_statistics.engine_statistics.peak_depth, - self.assignments.get_decision_level() as u64, + self.state.get_checkpoint() as u64, ); match branching_result { @@ -710,7 +592,7 @@ impl ConstraintSatisfactionSolver { // that is inconsistent with the current assignment. We do not // have to declare a new state, as it will be done inside the // `make_next_decision` function. - pumpkin_assert_simple!(self.state.is_infeasible_under_assumptions()); + pumpkin_assert_simple!(self.solver_state.is_infeasible_under_assumptions()); self.complete_proof(); return CSPSolverExecutionFlag::Infeasible; @@ -724,9 +606,9 @@ impl ConstraintSatisfactionSolver { return flag; } } else { - if self.get_decision_level() == 0 { + if self.get_checkpoint() == 0 { self.complete_proof(); - self.state.declare_infeasible(); + self.solver_state.declare_infeasible(); return CSPSolverExecutionFlag::Infeasible; } @@ -740,10 +622,7 @@ impl ConstraintSatisfactionSolver { } fn decay_nogood_activities(&mut self) { - match self - .propagators - .get_propagator_mut(self.nogood_propagator_handle) - { + match self.state.get_propagator_mut(self.nogood_propagator_handle) { Some(nogood_propagator) => { nogood_propagator.decay_nogood_activities(); } @@ -759,23 +638,20 @@ impl ConstraintSatisfactionSolver { // Currently assumptions are implemented by adding an assumption predicate // at separate decision levels. if let Some(assumption_literal) = self.peek_next_assumption_predicate() { - self.declare_new_decision_level(); + self.new_checkpoint(); - let _ = self - .assignments - .post_predicate(assumption_literal, None, &mut self.notification_engine) - .map_err(|_| { - self.state - .declare_infeasible_under_assumptions(assumption_literal); - CSPSolverExecutionFlag::Infeasible - })?; + let _ = self.state.post(assumption_literal).map_err(|_| { + self.solver_state + .declare_infeasible_under_assumptions(assumption_literal); + CSPSolverExecutionFlag::Infeasible + })?; return Ok(()); } // Otherwise proceed with standard branching. let context = &mut SelectionContext::new( - &self.assignments, + &self.state.assignments, &mut self.internal_parameters.random_generator, ); @@ -784,35 +660,33 @@ impl ConstraintSatisfactionSolver { // Otherwise there are no more decisions to be made, // all predicates have been applied without a conflict, // meaning the problem is feasible. - self.state.declare_solution_found(); + self.solver_state.declare_solution_found(); return Err(CSPSolverExecutionFlag::Feasible); }; - self.declare_new_decision_level(); + self.new_checkpoint(); // Note: This also checks that the decision predicate is not already true. That is a // stronger check than the `.expect(...)` used later on when handling the result of // `Assignments::post_predicate`. - pumpkin_assert_moderate!( - !self.assignments.is_predicate_satisfied(decision_predicate), + pumpkin_assert_ne_moderate!( + self.state.truth_value(decision_predicate), + Some(true), "Decision should not already be assigned; double check the brancher" ); self.solver_statistics.engine_statistics.num_decisions += 1; let update_occurred = self - .assignments - .post_predicate(decision_predicate, None, &mut self.notification_engine) + .state + .post(decision_predicate) .expect("Decisions are expected not to fail."); pumpkin_assert_simple!(update_occurred); Ok(()) } - pub(crate) fn declare_new_decision_level(&mut self) { - self.assignments.increase_decision_level(); - self.notification_engine.increase_decision_level(); - self.trailed_values.increase_decision_level(); - self.reason_store.increase_decision_level(); + pub(crate) fn new_checkpoint(&mut self) { + self.state.new_checkpoint(); } /// Changes the state based on the conflict analysis. It performs the following: @@ -826,31 +700,25 @@ impl ConstraintSatisfactionSolver { /// # Note /// This method performs no propagation, this is left up to the solver afterwards. fn resolve_conflict_with_nogood(&mut self, brancher: &mut impl Brancher) { - pumpkin_assert_moderate!(self.state.is_conflicting()); + pumpkin_assert_moderate!(self.solver_state.is_conflicting()); let mut conflict_analysis_context = ConflictAnalysisContext { - assignments: &mut self.assignments, counters: &mut self.solver_statistics, - solver_state: &mut self.state, - reason_store: &mut self.reason_store, + solver_state: &mut self.solver_state, brancher, semantic_minimiser: &mut self.semantic_minimiser, - notification_engine: &mut self.notification_engine, - propagators: &mut self.propagators, - propagator_queue: &mut self.propagator_queue, should_minimise: self.internal_parameters.learning_clause_minimisation, proof_log: &mut self.internal_parameters.proof_log, unit_nogood_inference_codes: &mut self.unit_nogood_inference_codes, - trailed_values: &mut self.trailed_values, - variable_names: &self.variable_names, rng: &mut self.internal_parameters.random_generator, restart_strategy: &mut self.restart_strategy, + state: &mut self.state, }; self.conflict_resolver .resolve_conflict(&mut conflict_analysis_context); - self.state.declare_solving(); + self.solver_state.declare_solving(); } /// Performs a restart during the search process; it is only called when it has been determined @@ -864,12 +732,12 @@ impl ConstraintSatisfactionSolver { /// Returns true if a restart took place and false otherwise. fn restart_during_search(&mut self, brancher: &mut impl Brancher) { pumpkin_assert_simple!( - self.get_decision_level() > self.assumptions.len(), + self.get_checkpoint() > self.assumptions.len(), "Sanity check: restarts should not trigger whilst assigning assumptions" ); // no point backtracking past the assumption level - if self.get_decision_level() <= self.assumptions.len() { + if self.get_checkpoint() <= self.assumptions.len() { return; } @@ -882,14 +750,9 @@ impl ConstraintSatisfactionSolver { self.solver_statistics.engine_statistics.num_restarts += 1; ConstraintSatisfactionSolver::backtrack( - &mut self.notification_engine, - &mut self.assignments, - &mut self.reason_store, - &mut self.propagator_queue, - &mut self.propagators, + &mut self.state, 0, brancher, - &mut self.trailed_values, &mut self.internal_parameters.random_generator, ); @@ -901,151 +764,38 @@ impl ConstraintSatisfactionSolver { reason = "This method requires this many arguments, though a backtracking context could be considered; for now this function needs to be used by conflict analysis" )] pub(crate) fn backtrack( - notification_engine: &mut NotificationEngine, - assignments: &mut Assignments, - reason_store: &mut ReasonStore, - propagator_queue: &mut PropagatorQueue, - propagators: &mut PropagatorStore, + state: &mut State, backtrack_level: usize, brancher: &mut BrancherType, - trailed_values: &mut TrailedValues, rng: &mut dyn Random, ) { - pumpkin_assert_simple!(backtrack_level < assignments.get_decision_level()); + pumpkin_assert_simple!(backtrack_level < state.get_checkpoint()); brancher.on_backtrack(); - assignments - .synchronise(backtrack_level, notification_engine) - .iter() + state + .restore_to(backtrack_level) + .into_iter() .for_each(|(domain_id, previous_value)| { - brancher.on_unassign_integer(*domain_id, *previous_value) + brancher.on_unassign_integer(domain_id, previous_value) }); - trailed_values.synchronise(backtrack_level); - - reason_store.synchronise(backtrack_level); - propagator_queue.clear(); - // For now all propagators are called to synchronise, in the future this will be improved in - // two ways: - // + allow incremental synchronisation - // + only call the subset of propagators that were notified since last backtrack - for propagator in propagators.iter_propagators_mut() { - let context = PropagationContext::new(assignments); - propagator.synchronise(context); - } - - brancher.synchronise(&mut SelectionContext::new(assignments, rng)); - - let _ = notification_engine.process_backtrack_events(assignments, propagators); - notification_engine.clear_event_drain(); - - notification_engine.update_last_notified_index(assignments); - // Should be done after the assignments and trailed values have been synchronised - notification_engine.synchronise(backtrack_level, assignments, trailed_values); + brancher.synchronise(&mut SelectionContext::new(&state.assignments, rng)); } /// Main propagation loop. pub(crate) fn propagate(&mut self) { - // Record the number of predicates on the trail for statistics purposes. - let num_assigned_variables_old = self.assignments.num_trail_entries(); - // The initial domain events are due to the decision predicate. - self.notification_engine - .notify_propagators_about_domain_events( - &mut self.assignments, - &mut self.trailed_values, - &mut self.propagators, - self.nogood_propagator_handle, - &mut self.propagator_queue, - ); - // Keep propagating until there are unprocessed propagators, or a conflict is detected. - while let Some(propagator_id) = self.propagator_queue.pop() { - self.solver_statistics - .engine_statistics - .num_propagators_called += 1; - - let num_trail_entries_before = self.assignments.num_trail_entries(); - - let propagation_status = { - let propagator = &mut self.propagators[propagator_id]; - let context = PropagationContextMut::new( - &mut self.trailed_values, - &mut self.assignments, - &mut self.reason_store, - &mut self.semantic_minimiser, - &mut self.notification_engine, - propagator_id, - ); - propagator.propagate(context) - }; + let num_trail_entries_prev = self.state.trail_len(); - if self.assignments.get_decision_level() == 0 { - self.handle_root_propagation(num_trail_entries_before); - } - match propagation_status { - Ok(_) => { - // Notify other propagators of the propagations and continue. - self.notification_engine - .notify_propagators_about_domain_events( - &mut self.assignments, - &mut self.trailed_values, - &mut self.propagators, - self.nogood_propagator_handle, - &mut self.propagator_queue, - ); - } - Err(inconsistency) => match inconsistency { - // A propagator did a change that resulted in an empty domain. - Inconsistency::EmptyDomain => { - self.prepare_for_conflict_resolution(); - break; - } - // A propagator-specific reason for the current conflict. - Inconsistency::Conflict(conflict) => { - pumpkin_assert_advanced!(DebugHelper::debug_reported_failure( - &self.trailed_values, - &self.assignments, - &conflict.conjunction, - &self.propagators[propagator_id], - propagator_id, - &self.notification_engine - )); - - let stored_conflict_info = StoredConflictInfo::Propagator(conflict); - self.state.declare_conflict(stored_conflict_info); - break; - } - }, - } - pumpkin_assert_extreme!( - DebugHelper::debug_check_propagations( - num_trail_entries_before, - propagator_id, - &self.trailed_values, - &self.assignments, - &mut self.reason_store, - &mut self.propagators, - &self.notification_engine - ), - "Checking the propagations performed by the propagator led to inconsistencies!" - ); + let result = self.state.propagate_to_fixed_point(); + + if self.state.get_checkpoint() == 0 { + self.handle_root_propagation(num_trail_entries_prev); + } + + if let Err(conflict) = result { + self.solver_state.declare_conflict(conflict.into()); } - // Record statistics. - self.solver_statistics.engine_statistics.num_conflicts += - self.state.is_conflicting() as u64; - self.solver_statistics.engine_statistics.num_propagations += - self.assignments.num_trail_entries() as u64 - num_assigned_variables_old as u64; - // Only check fixed point propagation if there was no reported conflict, - // since otherwise the state may be inconsistent. - pumpkin_assert_extreme!( - self.state.is_conflicting() - || DebugHelper::debug_fixed_point_propagation( - &self.trailed_values, - &self.assignments, - &self.propagators, - &self.notification_engine - ) - ); } /// Introduces any root-level propagations to the proof by introducing them as @@ -1055,11 +805,11 @@ impl ConstraintSatisfactionSolver { /// 1. Infernce `R /\ ~l -> false` /// 2. Nogood (clause) `l` fn handle_root_propagation(&mut self, start_trail_index: usize) { - pumpkin_assert_eq_simple!(self.get_decision_level(), 0); + pumpkin_assert_eq_simple!(self.get_checkpoint(), 0); - for trail_idx in start_trail_index..self.assignments.num_trail_entries() { - let entry = self.assignments.get_trail_entry(trail_idx); - let (reason_ref, inference_code) = entry + for trail_idx in start_trail_index..self.state.trail_len() { + let entry = self.state.trail_entry(trail_idx); + let (_, inference_code) = entry .reason .expect("Added by a propagator and must therefore have a reason"); @@ -1075,26 +825,19 @@ impl ConstraintSatisfactionSolver { // Get the conjunction of predicates explaining the propagation. let mut reason = vec![]; - let _ = self.reason_store.get_or_compute( - reason_ref, - ExplanationContext::without_working_nogood( - &self.assignments, - trail_idx, - &mut self.notification_engine, - ), - &mut self.propagators, - &mut reason, - ); + self.state + .get_propagation_reason_trail_entry(trail_idx, &mut reason); let propagated = entry.predicate; // The proof inference for the propagation `R -> l` is `R /\ ~l -> false`. let inference_premises = reason.iter().copied().chain(std::iter::once(!propagated)); let _ = self.internal_parameters.proof_log.log_inference( + &self.state.inference_codes, inference_code, inference_premises, None, - &self.variable_names, + self.state.variable_names(), ); // Since inference steps are only related to the nogood they directly precede, @@ -1110,16 +853,16 @@ impl ConstraintSatisfactionSolver { let mut to_explain: VecDeque = reason.iter().copied().collect(); while let Some(premise) = to_explain.pop_front() { - pumpkin_assert_simple!(self.assignments.is_predicate_satisfied(premise)); + pumpkin_assert_simple!( + self.state + .truth_value(premise) + .expect("Expected predicate to hold") + ); let mut context = RootExplanationContext { - propagators: &mut self.propagators, proof_log: &mut self.internal_parameters.proof_log, unit_nogood_inference_codes: &self.unit_nogood_inference_codes, - assignments: &self.assignments, - reason_store: &mut self.reason_store, - notification_engine: &mut self.notification_engine, - variable_names: &self.variable_names, + state: &mut self.state, }; explain_root_assignment(&mut context, premise); @@ -1129,12 +872,11 @@ impl ConstraintSatisfactionSolver { let constraint_tag = self .internal_parameters .proof_log - .log_deduction([!propagated], &self.variable_names); + .log_deduction([!propagated], self.state.variable_names()); if let Ok(constraint_tag) = constraint_tag { let inference_code = self - .internal_parameters - .proof_log + .state .create_inference_code(constraint_tag, NogoodLabel); let _ = self @@ -1147,12 +889,12 @@ impl ConstraintSatisfactionSolver { fn peek_next_assumption_predicate(&self) -> Option { // The convention is that at decision level i, the (i-1)th assumption is posted. // Note that decisions start being posted start at 1, hence the minus one. - let next_assumption_index = self.get_decision_level(); + let next_assumption_index = self.get_checkpoint(); self.assumptions.get(next_assumption_index).copied() } } -// methods for adding constraints (propagators and clauses) +/// Methods for adding constraints (propagators and clauses) impl ConstraintSatisfactionSolver { /// See [`crate::Solver::add_propagator`] for documentation. pub(crate) fn add_propagator( @@ -1163,39 +905,19 @@ impl ConstraintSatisfactionSolver { Constructor: PropagatorConstructor, Constructor::PropagatorImpl: 'static, { - if self.state.is_inconsistent() { + if self.solver_state.is_inconsistent() { return Err(ConstraintOperationError::InfeasiblePropagator); } - let propagator_slot = self.propagators.new_propagator(); - - let constructor_context = PropagatorConstructorContext::new( - &mut self.notification_engine, - &mut self.trailed_values, - &mut self.internal_parameters.proof_log, - propagator_slot.key().propagator_id(), - &mut self.assignments, - ); - - let propagator = constructor.create(constructor_context); + let handle = self.state.add_propagator(constructor); + let result = self.state.propagate_to_fixed_point(); - pumpkin_assert_simple!( - propagator.priority() <= 3, - "The propagator priority exceeds 3. - Currently we only support values up to 3, - but this can easily be changed if there is a good reason." - ); - let new_propagator_id = propagator_slot.populate(propagator); - - let new_propagator = &mut self.propagators[new_propagator_id.propagator_id()]; - - self.propagator_queue - .enqueue_propagator(new_propagator_id.propagator_id(), new_propagator.priority()); - - self.propagate(); + if let Err(conflict) = result { + self.solver_state.declare_conflict(conflict.into()); + } - if self.state.no_conflict() { - Ok(new_propagator_id) + if self.solver_state.no_conflict() { + Ok(handle) } else { self.complete_proof(); let _ = self.conclude_proof_unsat(); @@ -1205,17 +927,14 @@ impl ConstraintSatisfactionSolver { pub fn post_predicate(&mut self, predicate: Predicate) -> Result<(), ConstraintOperationError> { assert!( - self.get_decision_level() == 0, + self.get_checkpoint() == 0, "Can only post predicates at the root level." ); - if self.state.is_infeasible() { + if self.solver_state.is_infeasible() { Err(ConstraintOperationError::InfeasibleState) } else { - match self - .assignments - .post_predicate(predicate, None, &mut self.notification_engine) - { + match self.state.post(predicate) { Ok(_) => Ok(()), Err(_) => Err(ConstraintOperationError::InfeasibleNogood), } @@ -1227,28 +946,23 @@ impl ConstraintSatisfactionSolver { nogood: Vec, inference_code: InferenceCode, ) -> Result<(), ConstraintOperationError> { - pumpkin_assert_eq_simple!(self.get_decision_level(), 0); - let num_trail_entries = self.assignments.num_trail_entries(); - - let mut propagation_context = PropagationContextMut::new( - &mut self.trailed_values, - &mut self.assignments, - &mut self.reason_store, - &mut self.semantic_minimiser, - &mut self.notification_engine, - self.nogood_propagator_handle.propagator_id(), - ); + pumpkin_assert_eq_simple!(self.get_checkpoint(), 0); + let num_trail_entries = self.state.trail_len(); + + let (nogood_propagator, mut context) = self + .state + .get_propagator_mut_with_context(self.nogood_propagator_handle); - let nogood_propagator = self - .propagators - .get_propagator_mut(self.nogood_propagator_handle) - .expect("nogood propagator handle should refer to nogood propagator"); + let nogood_propagator = + nogood_propagator.expect("Nogood propagator handle should refer to nogood propagator"); - let propagation_status = - nogood_propagator.add_nogood(nogood, inference_code, &mut propagation_context); + let addition_status = nogood_propagator.add_nogood(nogood, inference_code, &mut context); + + if addition_status.is_err() || self.solver_state.is_conflicting() { + if let Err(conflict) = addition_status { + self.solver_state.declare_conflict(conflict.into()); + } - if propagation_status.is_err() || self.state.is_conflicting() { - self.prepare_for_conflict_resolution(); self.handle_root_propagation(num_trail_entries); self.complete_proof(); return Err(ConstraintOperationError::InfeasibleNogood); @@ -1256,14 +970,16 @@ impl ConstraintSatisfactionSolver { self.handle_root_propagation(num_trail_entries); - // temporary hack for the nogood propagator that does propagation from scratch - self.propagator_queue.enqueue_propagator(PropagatorId(0), 0); - self.propagate(); + #[allow(deprecated, reason = "Will be refactored")] + self.state.enqueue_propagator(self.nogood_propagator_handle); + let result = self.state.propagate_to_fixed_point(); + if let Err(conflict) = result { + self.solver_state.declare_conflict(conflict.into()); + } self.handle_root_propagation(num_trail_entries); - if self.state.is_infeasible() { - self.prepare_for_conflict_resolution(); + if self.solver_state.is_infeasible() { self.complete_proof(); Err(ConstraintOperationError::InfeasibleState) } else { @@ -1271,26 +987,6 @@ impl ConstraintSatisfactionSolver { } } - fn prepare_for_conflict_resolution(&mut self) { - if self.state.is_conflicting() { - return; - } - - // TODO: As a temporary solution, we remove the last trail element. - // This way we guarantee that the assignment is consistent, which is needed - // for the conflict analysis data structures. The proper alternative would - // be to forbid the assignments from getting into an inconsistent state. - let (trigger_predicate, trigger_reason, trigger_inference_code) = - self.assignments.remove_last_trail_element(); - - let stored_conflict_info = StoredConflictInfo::EmptyDomain(EmptyDomainConflict { - trigger_predicate, - trigger_reason, - trigger_inference_code, - }); - self.state.declare_conflict(stored_conflict_info); - } - /// Creates a clause from `literals` and adds it to the current formula. /// /// If the formula becomes trivially unsatisfiable, a [`ConstraintOperationError`] will be @@ -1302,11 +998,11 @@ impl ConstraintSatisfactionSolver { constraint_tag: ConstraintTag, ) -> Result<(), ConstraintOperationError> { pumpkin_assert_simple!( - self.get_decision_level() == 0, + self.get_checkpoint() == 0, "Clauses can only be added in the root" ); - if self.state.is_inconsistent() { + if self.solver_state.is_inconsistent() { return Err(ConstraintOperationError::InfeasiblePropagator); } @@ -1318,7 +1014,7 @@ impl ConstraintSatisfactionSolver { let predicates = predicates .into_iter() .map(|predicate| { - are_all_falsified_at_root &= self.assignments.is_predicate_falsified(predicate); + are_all_falsified_at_root &= self.state.truth_value(predicate) == Some(false); !predicate }) .collect::>(); @@ -1326,7 +1022,7 @@ impl ConstraintSatisfactionSolver { if predicates.is_empty() { // This breaks the proof. If it occurs, we should fix up the proof logging. // The main issue is that nogoods are not tagged. In the proof that is problematic. - self.state + self.solver_state .declare_conflict(StoredConflictInfo::RootLevelConflict( ConstraintOperationError::InfeasibleClause, )); @@ -1336,15 +1032,11 @@ impl ConstraintSatisfactionSolver { if are_all_falsified_at_root { finalize_proof(FinalizingContext { conflict: predicates.into(), - propagators: &mut self.propagators, proof_log: &mut self.internal_parameters.proof_log, unit_nogood_inference_codes: &self.unit_nogood_inference_codes, - assignments: &self.assignments, - reason_store: &mut self.reason_store, - notification_engine: &mut self.notification_engine, - variable_names: &self.variable_names, + state: &mut self.state, }); - self.state + self.solver_state .declare_conflict(StoredConflictInfo::RootLevelConflict( ConstraintOperationError::InfeasibleClause, )); @@ -1352,13 +1044,12 @@ impl ConstraintSatisfactionSolver { } let inference_code = self - .internal_parameters - .proof_log + .state .create_inference_code(constraint_tag, NogoodLabel); if let Err(constraint_operation_error) = self.add_nogood(predicates, inference_code) { let _ = self.conclude_proof_unsat(); - self.state + self.solver_state .declare_conflict(StoredConflictInfo::RootLevelConflict( constraint_operation_error, )); @@ -1367,8 +1058,8 @@ impl ConstraintSatisfactionSolver { Ok(()) } - pub(crate) fn get_decision_level(&self) -> usize { - self.assignments.get_decision_level() + pub(crate) fn get_checkpoint(&self) -> usize { + self.state.get_checkpoint() } } @@ -1474,25 +1165,25 @@ impl CSPSolverState { self.internal_state = CSPSolverStateInternal::Solving; } - fn declare_infeasible(&mut self) { + pub fn declare_infeasible(&mut self) { self.internal_state = CSPSolverStateInternal::Infeasible; } - fn declare_conflict(&mut self, conflict_info: StoredConflictInfo) { + pub(crate) fn declare_conflict(&mut self, conflict_info: StoredConflictInfo) { self.internal_state = CSPSolverStateInternal::Conflict { conflict_info }; } - fn declare_solution_found(&mut self) { + pub fn declare_solution_found(&mut self) { pumpkin_assert_simple!(!self.is_infeasible()); self.internal_state = CSPSolverStateInternal::ContainsSolution; } - fn declare_timeout(&mut self) { + pub fn declare_timeout(&mut self) { pumpkin_assert_simple!(!self.is_infeasible()); self.internal_state = CSPSolverStateInternal::Timeout; } - fn declare_infeasible_under_assumptions(&mut self, violated_assumption: Predicate) { + pub fn declare_infeasible_under_assumptions(&mut self, violated_assumption: Predicate) { pumpkin_assert_simple!(!self.is_infeasible()); self.internal_state = CSPSolverStateInternal::InfeasibleUnderAssumptions { violated_assumption, @@ -1537,7 +1228,7 @@ mod tests { expected_flag: CSPSolverExecutionFlag, expected_result: CoreExtractionResult, ) { - let mut brancher = DefaultBrancher::default_over_all_variables(&solver.assignments); + let mut brancher = DefaultBrancher::default_over_all_variables(&solver.state.assignments); let flag = solver.solve_under_assumptions(&assumptions, &mut Indefinite, &mut brancher); assert_eq!(flag, expected_flag, "The flags do not match."); @@ -1739,12 +1430,13 @@ mod tests { let mut solver = ConstraintSatisfactionSolver::default(); let domain_id = solver.create_new_integer_variable(lb, ub, None); - assert_eq!(lb, solver.assignments.get_lower_bound(domain_id)); + assert_eq!(lb, solver.state.assignments.get_lower_bound(domain_id)); - assert_eq!(ub, solver.assignments.get_upper_bound(domain_id)); + assert_eq!(ub, solver.state.assignments.get_upper_bound(domain_id)); assert!( !solver + .state .assignments .is_predicate_satisfied(predicate![domain_id == lb]) ); @@ -1752,10 +1444,11 @@ mod tests { for value in (lb + 1)..ub { let predicate = predicate![domain_id >= value]; - assert!(!solver.assignments.is_predicate_satisfied(predicate)); + assert!(!solver.state.assignments.is_predicate_satisfied(predicate)); assert!( !solver + .state .assignments .is_predicate_satisfied(predicate![domain_id == value]) ); @@ -1763,6 +1456,7 @@ mod tests { assert!( !solver + .state .assignments .is_predicate_satisfied(predicate![domain_id == ub]) ); diff --git a/pumpkin-crates/core/src/engine/cp/assignments.rs b/pumpkin-crates/core/src/engine/cp/assignments.rs index 1aae1fde9..fa54b3065 100644 --- a/pumpkin-crates/core/src/engine/cp/assignments.rs +++ b/pumpkin-crates/core/src/engine/cp/assignments.rs @@ -45,25 +45,25 @@ impl Default for Assignments { } #[derive(Clone, Copy, Debug)] -pub(crate) struct EmptyDomain; +pub struct EmptyDomain; impl Assignments { #[allow(unused, reason = "Could be used in the future")] /// Returns all of the holes in the domain which were created at the provided decision level - pub(crate) fn get_holes_on_decision_level( + pub(crate) fn get_holes_at_checkpoint( &self, domain_id: DomainId, - decision_level: usize, + checkpoint: usize, ) -> impl Iterator + '_ { - self.domains[domain_id].get_holes_from_decision_level(decision_level) + self.domains[domain_id].get_holes_at_checkpoint(checkpoint) } /// Returns all of the holes in the domain which were created at the current decision level - pub(crate) fn get_holes_on_current_decision_level( + pub(crate) fn get_holes_at_current_checkpoint( &self, domain_id: DomainId, ) -> impl Iterator + '_ { - self.domains[domain_id].get_holes_from_current_decision_level(self.get_decision_level()) + self.domains[domain_id].get_holes_from_current_checkpoint(self.get_checkpoint()) } /// Returns all of the holes (currently) in the domain of `var` (including ones which were @@ -72,26 +72,25 @@ impl Assignments { self.domains[domain_id].get_holes() } - pub(crate) fn increase_decision_level(&mut self) { - self.trail.increase_decision_level() + pub(crate) fn new_checkpoint(&mut self) { + self.trail.new_checkpoint() } pub(crate) fn find_last_decision(&self) -> Option { - if self.get_decision_level() == 0 { + if self.get_checkpoint() == 0 { None } else { - let values_on_current_decision_level = self - .trail - .values_on_decision_level(self.get_decision_level()); - let entry = values_on_current_decision_level[0]; + let values_at_current_checkpoint = + self.trail.values_at_checkpoint(self.get_checkpoint()); + let entry = values_at_current_checkpoint[0]; pumpkin_assert_eq_simple!(None, entry.reason); Some(entry.predicate) } } - pub(crate) fn get_decision_level(&self) -> usize { - self.trail.get_decision_level() + pub(crate) fn get_checkpoint(&self) -> usize { + self.trail.get_checkpoint() } pub(crate) fn num_domains(&self) -> u32 { @@ -121,7 +120,7 @@ impl Assignments { // when values are removed at levels beyond the root, and then it becomes a tricky value to // update when a fresh domain needs to be considered. pumpkin_assert_simple!( - self.get_decision_level() == 0, + self.get_checkpoint() == 0, "can only create variables at the root" ); @@ -336,19 +335,19 @@ impl Assignments { // If the domain assigned at a nonroot level, this is just one predicate. if domain.lower_bound() == domain.upper_bound() - && domain.lower_bound_decision_level() > 0 - && domain.upper_bound_decision_level() > 0 + && domain.lower_bound_checkpoint() > 0 + && domain.checkpoint() > 0 { predicates.push(predicate![domain_id == domain.lower_bound()]); return predicates; } // Add bounds but avoid root assignments. - if domain.lower_bound_decision_level() > 0 { + if domain.lower_bound_checkpoint() > 0 { predicates.push(predicate![domain_id >= domain.lower_bound()]); } - if domain.upper_bound_decision_level() > 0 { + if domain.checkpoint() > 0 { predicates.push(predicate![domain_id <= domain.upper_bound()]); } @@ -358,7 +357,7 @@ impl Assignments { // that are not root assignments. // Since bound values cannot be in the holes, // we can use '<' or '>'. - if hole.1.decision_level > 0 + if hole.1.checkpoint > 0 && domain.lower_bound() < *hole.0 && *hole.0 < domain.upper_bound() { @@ -405,10 +404,10 @@ impl Assignments { /// If the predicate is assigned true, returns the decision level of the predicate. /// Otherwise returns None. - pub(crate) fn get_decision_level_for_predicate(&self, predicate: &Predicate) -> Option { + pub(crate) fn get_checkpoint_for_predicate(&self, predicate: &Predicate) -> Option { self.domains[predicate.get_domain()] .get_update_info(predicate) - .map(|u| u.decision_level) + .map(|u| u.checkpoint) } pub fn get_domain_descriptions(&self) -> Vec { @@ -421,7 +420,7 @@ impl Assignments { } } -type AssignmentReason = (ReasonRef, InferenceCode); +pub(crate) type AssignmentReason = (ReasonRef, InferenceCode); // methods to change the domains impl Assignments { @@ -451,11 +450,10 @@ impl Assignments { reason, }); - let decision_level = self.get_decision_level(); + let checkpoint = self.get_checkpoint(); let domain = &mut self.domains[domain_id]; - let update_took_place = - domain.set_lower_bound(new_lower_bound, decision_level, trail_position); + let update_took_place = domain.set_lower_bound(new_lower_bound, checkpoint, trail_position); self.bounds[domain_id].0 = domain.lower_bound(); @@ -492,11 +490,10 @@ impl Assignments { reason, }); - let decision_level = self.get_decision_level(); + let checkpoint = self.get_checkpoint(); let domain = &mut self.domains[domain_id]; - let update_took_place = - domain.set_upper_bound(new_upper_bound, decision_level, trail_position); + let update_took_place = domain.set_upper_bound(new_upper_bound, checkpoint, trail_position); self.bounds[domain_id].1 = domain.upper_bound(); @@ -534,19 +531,17 @@ impl Assignments { reason, }); - let decision_level = self.get_decision_level(); + let checkpoint = self.get_checkpoint(); let domain = &mut self.domains[domain_id]; if old_lower_bound < assigned_value { - update_took_place |= - domain.set_lower_bound(assigned_value, decision_level, trail_position); + update_took_place |= domain.set_lower_bound(assigned_value, checkpoint, trail_position); self.bounds[domain_id].0 = domain.lower_bound(); self.pruned_values += domain.lower_bound().abs_diff(old_lower_bound) as u64; } if old_upper_bound > assigned_value { - update_took_place |= - domain.set_upper_bound(assigned_value, decision_level, trail_position); + update_took_place |= domain.set_upper_bound(assigned_value, checkpoint, trail_position); self.bounds[domain_id].1 = domain.upper_bound(); self.pruned_values += domain.upper_bound().abs_diff(old_upper_bound) as u64; } @@ -582,10 +577,10 @@ impl Assignments { reason, }); - let decision_level = self.get_decision_level(); + let checkpoint = self.get_checkpoint(); let domain = &mut self.domains[domain_id]; - let _ = domain.remove_value(removed_value_from_domain, decision_level, trail_position); + let _ = domain.remove_value(removed_value_from_domain, checkpoint, trail_position); let changed_lower_bound = domain.lower_bound().abs_diff(old_lower_bound) as u64; let changed_upper_bound = old_upper_bound.abs_diff(domain.upper_bound()) as u64; @@ -708,25 +703,25 @@ impl Assignments { } /// Synchronises the internal structures of [`Assignments`] based on the fact that - /// backtracking to `new_decision_level` is taking place. This method returns the list of + /// backtracking to `new_checkpoint` is taking place. This method returns the list of /// [`DomainId`]s and their values which were fixed (i.e. domain of size one) before /// backtracking and are unfixed (i.e. domain of two or more values) after synchronisation. pub(crate) fn synchronise( &mut self, - new_decision_level: usize, + new_checkpoint: usize, notification_engine: &mut NotificationEngine, ) -> Vec<(DomainId, i32)> { let mut unfixed_variables = Vec::new(); let num_trail_entries_before_synchronisation = self.num_trail_entries(); pumpkin_assert_simple!( - new_decision_level <= self.trail.get_decision_level(), - "Expected the new decision level {new_decision_level} to be less than or equal to the current decision level {}", - self.trail.get_decision_level(), + new_checkpoint <= self.trail.get_checkpoint(), + "Expected the new decision level {new_checkpoint} to be less than or equal to the current decision level {}", + self.trail.get_checkpoint(), ); self.trail - .synchronise(new_decision_level) + .synchronise(new_checkpoint) .enumerate() .for_each(|(index, entry)| { // Calculate how many values are re-introduced into the domain. @@ -820,7 +815,7 @@ impl Assignments { #[derive(Clone, Copy, Debug)] pub(crate) struct ConstraintProgrammingTrailEntry { - pub(crate) predicate: Predicate, + pub predicate: Predicate, /// Explicitly store the bound before the predicate was applied so that it is easier later on /// to update the bounds when backtracking. pub(crate) old_lower_bound: i32, @@ -833,14 +828,14 @@ pub(crate) struct ConstraintProgrammingTrailEntry { #[derive(Clone, Copy, Debug)] struct PairDecisionLevelTrailPosition { - decision_level: usize, + checkpoint: usize, trail_position: usize, } #[derive(Clone, Debug)] struct BoundUpdateInfo { bound: i32, - decision_level: usize, + checkpoint: usize, trail_position: usize, } @@ -848,7 +843,7 @@ struct BoundUpdateInfo { struct HoleUpdateInfo { removed_value: i32, - decision_level: usize, + checkpoint: usize, triggered_lower_bound_update: bool, triggered_upper_bound_update: bool, @@ -888,13 +883,13 @@ impl IntegerDomain { let lower_bound_updates = vec![BoundUpdateInfo { bound: lower_bound, - decision_level: 0, + checkpoint: 0, trail_position: 0, }]; let upper_bound_updates = vec![BoundUpdateInfo { bound: upper_bound, - decision_level: 0, + checkpoint: 0, trail_position: 0, }]; @@ -917,11 +912,11 @@ impl IntegerDomain { .bound } - fn lower_bound_decision_level(&self) -> usize { + fn lower_bound_checkpoint(&self) -> usize { self.lower_bound_updates .last() .expect("Cannot be empty.") - .decision_level + .checkpoint } fn initial_lower_bound(&self) -> i32 { @@ -957,11 +952,11 @@ impl IntegerDomain { .bound } - fn upper_bound_decision_level(&self) -> usize { + fn checkpoint(&self) -> usize { self.upper_bound_updates .last() .expect("Cannot be empty.") - .decision_level + .checkpoint } fn initial_upper_bound(&self) -> i32 { @@ -1029,7 +1024,7 @@ impl IntegerDomain { fn remove_value( &mut self, removed_value: i32, - decision_level: usize, + checkpoint: usize, trail_position: usize, ) -> bool { if removed_value < self.lower_bound() @@ -1041,7 +1036,7 @@ impl IntegerDomain { self.hole_updates.push(HoleUpdateInfo { removed_value, - decision_level, + checkpoint, triggered_lower_bound_update: false, triggered_upper_bound_update: false, }); @@ -1050,7 +1045,7 @@ impl IntegerDomain { let old_none_entry = self.holes.insert( removed_value, PairDecisionLevelTrailPosition { - decision_level, + checkpoint, trail_position, }, ); @@ -1058,7 +1053,7 @@ impl IntegerDomain { // Check if removing a value triggers a lower bound update. if self.lower_bound() == removed_value { - let _ = self.set_lower_bound(removed_value + 1, decision_level, trail_position); + let _ = self.set_lower_bound(removed_value + 1, checkpoint, trail_position); self.hole_updates .last_mut() .expect("we just pushed a value, so must be present") @@ -1066,7 +1061,7 @@ impl IntegerDomain { } // Check if removing the value triggers an upper bound update. if self.upper_bound() == removed_value { - let _ = self.set_upper_bound(removed_value - 1, decision_level, trail_position); + let _ = self.set_upper_bound(removed_value - 1, checkpoint, trail_position); self.hole_updates .last_mut() .expect("we just pushed a value, so must be present") @@ -1078,22 +1073,22 @@ impl IntegerDomain { fn debug_is_valid_upper_bound_domain_update( &self, - decision_level: usize, + checkpoint: usize, trail_position: usize, ) -> bool { trail_position == 0 - || self.upper_bound_updates.last().unwrap().decision_level <= decision_level + || self.upper_bound_updates.last().unwrap().checkpoint <= checkpoint && self.upper_bound_updates.last().unwrap().trail_position < trail_position } fn set_upper_bound( &mut self, new_upper_bound: i32, - decision_level: usize, + checkpoint: usize, trail_position: usize, ) -> bool { pumpkin_assert_moderate!( - self.debug_is_valid_upper_bound_domain_update(decision_level, trail_position) + self.debug_is_valid_upper_bound_domain_update(checkpoint, trail_position) ); if new_upper_bound >= self.upper_bound() { @@ -1102,7 +1097,7 @@ impl IntegerDomain { self.upper_bound_updates.push(BoundUpdateInfo { bound: new_upper_bound, - decision_level, + checkpoint, trail_position, }); self.update_upper_bound_with_respect_to_holes(); @@ -1120,22 +1115,22 @@ impl IntegerDomain { fn debug_is_valid_lower_bound_domain_update( &self, - decision_level: usize, + checkpoint: usize, trail_position: usize, ) -> bool { trail_position == 0 - || self.lower_bound_updates.last().unwrap().decision_level <= decision_level + || self.lower_bound_updates.last().unwrap().checkpoint <= checkpoint && self.lower_bound_updates.last().unwrap().trail_position < trail_position } fn set_lower_bound( &mut self, new_lower_bound: i32, - decision_level: usize, + checkpoint: usize, trail_position: usize, ) -> bool { pumpkin_assert_moderate!( - self.debug_is_valid_lower_bound_domain_update(decision_level, trail_position) + self.debug_is_valid_lower_bound_domain_update(checkpoint, trail_position) ); if new_lower_bound <= self.lower_bound() { @@ -1144,7 +1139,7 @@ impl IntegerDomain { self.lower_bound_updates.push(BoundUpdateInfo { bound: new_lower_bound, - decision_level, + checkpoint, trail_position, }); self.update_lower_bound_with_respect_to_holes(); @@ -1265,7 +1260,7 @@ impl IntegerDomain { (position < self.lower_bound_updates.len()).then(|| { let u = &self.lower_bound_updates[position]; PairDecisionLevelTrailPosition { - decision_level: u.decision_level, + checkpoint: u.checkpoint, trail_position: u.trail_position, } }) @@ -1283,7 +1278,7 @@ impl IntegerDomain { (position < self.upper_bound_updates.len()).then(|| { let u = &self.upper_bound_updates[position]; PairDecisionLevelTrailPosition { - decision_level: u.decision_level, + checkpoint: u.checkpoint, trail_position: u.trail_position, } }) @@ -1347,25 +1342,25 @@ impl IntegerDomain { } /// Returns the holes which were created on the provided decision level. - pub(crate) fn get_holes_from_decision_level( + pub(crate) fn get_holes_at_checkpoint( &self, - decision_level: usize, + checkpoint: usize, ) -> impl Iterator + '_ { self.hole_updates .iter() - .filter(move |entry| entry.decision_level == decision_level) + .filter(move |entry| entry.checkpoint == checkpoint) .map(|entry| entry.removed_value) } /// Returns the holes which were created on the current decision level. - pub(crate) fn get_holes_from_current_decision_level( + pub(crate) fn get_holes_from_current_checkpoint( &self, - current_decision_level: usize, + current_checkpoint: usize, ) -> impl Iterator + '_ { self.hole_updates .iter() .rev() - .take_while(move |entry| entry.decision_level == current_decision_level) + .take_while(move |entry| entry.checkpoint == current_checkpoint) .map(|entry| entry.removed_value) } @@ -1434,7 +1429,7 @@ mod tests { let d1 = assignment.grow(1, 5); notification_engine.grow(); - assignment.increase_decision_level(); + assignment.new_checkpoint(); let _ = assignment .post_predicate(predicate!(d1 != 1), None, &mut notification_engine) @@ -1462,7 +1457,7 @@ mod tests { let d1 = assignment.grow(1, 5); notification_engine.grow(); - assignment.increase_decision_level(); + assignment.new_checkpoint(); let _ = assignment .post_predicate(predicate!(d1 != 2), None, &mut notification_engine) @@ -1500,7 +1495,7 @@ mod tests { let d1 = assignment.grow(1, 5); notification_engine.grow(); - assignment.increase_decision_level(); + assignment.new_checkpoint(); let _ = assignment .post_predicate(predicate!(d1 != 3), None, &mut notification_engine) @@ -1530,7 +1525,7 @@ mod tests { let d1 = assignment.grow(1, 5); notification_engine.grow(); - assignment.increase_decision_level(); + assignment.new_checkpoint(); let _ = assignment .remove_value_from_domain(d1, 3, None) @@ -1735,7 +1730,7 @@ mod tests { let d1 = assignment.grow(1, 5); notification_engine.grow(); - assignment.increase_decision_level(); + assignment.new_checkpoint(); let _ = assignment .post_predicate(predicate!(d1 != 5), None, &mut notification_engine) @@ -1877,7 +1872,7 @@ mod tests { notification_engine.grow(); // decision level 1 - assignment.increase_decision_level(); + assignment.new_checkpoint(); let _ = assignment .post_predicate(predicate!(domain_id1 >= 2), None, &mut notification_engine) .expect(""); @@ -1886,13 +1881,13 @@ mod tests { .expect(""); // decision level 2 - assignment.increase_decision_level(); + assignment.new_checkpoint(); let _ = assignment .post_predicate(predicate!(domain_id1 >= 5), None, &mut notification_engine) .expect(""); // decision level 3 - assignment.increase_decision_level(); + assignment.new_checkpoint(); let _ = assignment .post_predicate(predicate!(domain_id1 >= 7), None, &mut notification_engine) .expect(""); diff --git a/pumpkin-crates/core/src/engine/cp/mod.rs b/pumpkin-crates/core/src/engine/cp/mod.rs index 84ef1014c..e6dda5f9a 100644 --- a/pumpkin-crates/core/src/engine/cp/mod.rs +++ b/pumpkin-crates/core/src/engine/cp/mod.rs @@ -6,7 +6,8 @@ pub(crate) mod test_solver; mod trailed; pub(crate) use assignments::Assignments; -pub(crate) use assignments::EmptyDomain; +pub(crate) use assignments::ConstraintProgrammingTrailEntry; +pub use assignments::EmptyDomain; pub(crate) use propagator_queue::PropagatorQueue; pub(crate) use trailed::*; @@ -17,7 +18,6 @@ mod tests { use crate::conjunction; use crate::containers::StorageKey; use crate::engine::TrailedValues; - use crate::engine::conflict_analysis::SemanticMinimiser; use crate::engine::cp::assignments; use crate::engine::notifications::NotificationEngine; use crate::engine::propagation::PropagationContextMut; @@ -35,13 +35,11 @@ mod tests { let mut reason_store = ReasonStore::default(); assert_eq!(reason_store.len(), 0); { - let mut semantic_miniser = SemanticMinimiser::default(); let mut notification_engine = NotificationEngine::default(); let mut context = PropagationContextMut::new( &mut trailed_values, &mut assignments, &mut reason_store, - &mut semantic_miniser, &mut notification_engine, PropagatorId(0), ); @@ -66,13 +64,11 @@ mod tests { assert_eq!(reason_store.len(), 0); { - let mut semantic_miniser = SemanticMinimiser::default(); let mut notification_engine = NotificationEngine::default(); let mut context = PropagationContextMut::new( &mut trailed_values, &mut assignments, &mut reason_store, - &mut semantic_miniser, &mut notification_engine, PropagatorId(0), ); @@ -97,13 +93,11 @@ mod tests { assert_eq!(reason_store.len(), 0); { - let mut semantic_miniser = SemanticMinimiser::default(); let mut notification_engine = NotificationEngine::default(); let mut context = PropagationContextMut::new( &mut trailed_values, &mut assignments, &mut reason_store, - &mut semantic_miniser, &mut notification_engine, PropagatorId(0), ); diff --git a/pumpkin-crates/core/src/engine/cp/propagation/constructor.rs b/pumpkin-crates/core/src/engine/cp/propagation/constructor.rs index b83f4897d..bec94353b 100644 --- a/pumpkin-crates/core/src/engine/cp/propagation/constructor.rs +++ b/pumpkin-crates/core/src/engine/cp/propagation/constructor.rs @@ -8,13 +8,12 @@ use super::PropagatorId; use super::PropagatorVarId; use crate::engine::Assignments; use crate::engine::DomainEvents; +use crate::engine::State; use crate::engine::TrailedValues; -use crate::engine::notifications::NotificationEngine; use crate::engine::notifications::Watchers; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; use crate::proof::InferenceLabel; -use crate::proof::ProofLog; use crate::variables::IntegerVariable; /// A propagator constructor creates a fully initialized instance of a [`Propagator`]. @@ -24,7 +23,7 @@ use crate::variables::IntegerVariable; /// of the solver. pub(crate) trait PropagatorConstructor { /// The propagator that is produced by this constructor. - type PropagatorImpl: Propagator; + type PropagatorImpl: Propagator + Clone; /// Create the propagator instance from `Self`. fn create(self, context: PropagatorConstructorContext) -> Self::PropagatorImpl; @@ -37,42 +36,31 @@ pub(crate) trait PropagatorConstructor { /// of variables and to retrieve the current bounds of variables. #[derive(Debug)] pub(crate) struct PropagatorConstructorContext<'a> { - notification_engine: &'a mut NotificationEngine, - trailed_values: &'a mut TrailedValues, - propagator_id: PropagatorId, + state: &'a mut State, + pub(crate) propagator_id: PropagatorId, /// A [`LocalId`] that is guaranteed not to be used to register any variables yet. This is /// either a reference or an owned value, to support /// [`PropagatorConstructorContext::reborrow`]. next_local_id: RefOrOwned<'a, LocalId>, - - /// The proof log for which [`InferenceCode`]s can be created. - proof_log: &'a mut ProofLog, - - pub assignments: &'a mut Assignments, } impl PropagatorConstructorContext<'_> { pub(crate) fn new<'a>( - notification_engine: &'a mut NotificationEngine, - trailed_values: &'a mut TrailedValues, - proof_log: &'a mut ProofLog, propagator_id: PropagatorId, - assignments: &'a mut Assignments, + state: &'a mut State, ) -> PropagatorConstructorContext<'a> { PropagatorConstructorContext { - notification_engine, - trailed_values, - propagator_id, next_local_id: RefOrOwned::Owned(LocalId::from(0)), - proof_log, - - assignments, + propagator_id, + state, } } pub(crate) fn as_readonly(&self) -> PropagationContext<'_> { - PropagationContext::new(self.assignments) + PropagationContext { + assignments: &self.state.assignments, + } } /// Subscribes the propagator to the given [`DomainEvents`]. @@ -99,7 +87,7 @@ impl PropagatorConstructorContext<'_> { self.update_next_local_id(local_id); - let mut watchers = Watchers::new(propagator_var, self.notification_engine); + let mut watchers = Watchers::new(propagator_var, &mut self.state.notification_engine); var.watch_all(&mut watchers, domain_events.get_int_events()); } @@ -129,7 +117,7 @@ impl PropagatorConstructorContext<'_> { self.update_next_local_id(local_id); - let mut watchers = Watchers::new(propagator_var, self.notification_engine); + let mut watchers = Watchers::new(propagator_var, &mut self.state.notification_engine); var.watch_all_backtrack(&mut watchers, domain_events.get_int_events()); } @@ -140,7 +128,7 @@ impl PropagatorConstructorContext<'_> { constraint_tag: ConstraintTag, inference_label: impl InferenceLabel, ) -> InferenceCode { - self.proof_log + self.state .create_inference_code(constraint_tag, inference_label) } @@ -154,15 +142,12 @@ impl PropagatorConstructorContext<'_> { /// afterwards. pub(crate) fn reborrow(&mut self) -> PropagatorConstructorContext<'_> { PropagatorConstructorContext { - notification_engine: self.notification_engine, - trailed_values: self.trailed_values, propagator_id: self.propagator_id, - proof_log: self.proof_log, next_local_id: match &mut self.next_local_id { RefOrOwned::Ref(next_local_id) => RefOrOwned::Ref(next_local_id), RefOrOwned::Owned(next_local_id) => RefOrOwned::Ref(next_local_id), }, - assignments: self.assignments, + state: self.state, } } @@ -213,17 +198,17 @@ mod private { impl HasAssignments for PropagatorConstructorContext<'_> { fn assignments(&self) -> &Assignments { - self.assignments + &self.state.assignments } } impl HasTrailedValues for PropagatorConstructorContext<'_> { fn trailed_values(&self) -> &TrailedValues { - self.trailed_values + &self.state.trailed_values } fn trailed_values_mut(&mut self) -> &mut TrailedValues { - self.trailed_values + &mut self.state.trailed_values } } } @@ -236,20 +221,10 @@ mod tests { #[test] fn reborrowing_remembers_next_local_id() { - let mut notification_engine = NotificationEngine::default(); - notification_engine.grow(); - let mut trailed_values = TrailedValues::default(); - let mut proof_log = ProofLog::default(); - let propagator_id = PropagatorId(0); - let mut assignments = Assignments::default(); - - let mut c1 = PropagatorConstructorContext::new( - &mut notification_engine, - &mut trailed_values, - &mut proof_log, - propagator_id, - &mut assignments, - ); + let mut state = State::default(); + state.notification_engine.grow(); + + let mut c1 = PropagatorConstructorContext::new(PropagatorId(0), &mut state); let mut c2 = c1.reborrow(); c2.register(DomainId::new(0), DomainEvents::ANY_INT, LocalId::from(1)); diff --git a/pumpkin-crates/core/src/engine/cp/propagation/contexts/explanation_context.rs b/pumpkin-crates/core/src/engine/cp/propagation/contexts/explanation_context.rs index f244b99e7..030483f6b 100644 --- a/pumpkin-crates/core/src/engine/cp/propagation/contexts/explanation_context.rs +++ b/pumpkin-crates/core/src/engine/cp/propagation/contexts/explanation_context.rs @@ -95,7 +95,8 @@ static EMPTY_PREDICATE_IDS: LazyLock = static EMPTY_PREDICATES: [Predicate; 0] = []; -pub(crate) struct CurrentNogood<'a> { +#[derive(Debug)] +pub struct CurrentNogood<'a> { heap: &'a KeyValueHeap, visited: &'a [Predicate], ids: &'a PredicateIdGenerator, @@ -110,7 +111,7 @@ impl<'a> CurrentNogood<'a> { Self { heap, visited, ids } } - pub(crate) fn empty() -> CurrentNogood<'a> { + pub fn empty() -> CurrentNogood<'a> { // The variable here is necessary for lifetime coersion. let reference: &[Predicate] = &EMPTY_PREDICATES; Self::from(reference) diff --git a/pumpkin-crates/core/src/engine/cp/propagation/contexts/propagation_context.rs b/pumpkin-crates/core/src/engine/cp/propagation/contexts/propagation_context.rs index 71f1ce605..027c9675e 100644 --- a/pumpkin-crates/core/src/engine/cp/propagation/contexts/propagation_context.rs +++ b/pumpkin-crates/core/src/engine/cp/propagation/contexts/propagation_context.rs @@ -1,9 +1,9 @@ use crate::basic_types::PredicateId; use crate::engine::Assignments; use crate::engine::EmptyDomain; +use crate::engine::EmptyDomainConflict; use crate::engine::TrailedInteger; use crate::engine::TrailedValues; -use crate::engine::conflict_analysis::SemanticMinimiser; use crate::engine::notifications::NotificationEngine; use crate::engine::notifications::PredicateIdAssignments; use crate::engine::predicates::predicate::Predicate; @@ -67,7 +67,6 @@ pub(crate) struct PropagationContextMut<'a> { pub(crate) assignments: &'a mut Assignments, pub(crate) reason_store: &'a mut ReasonStore, pub(crate) propagator_id: PropagatorId, - pub(crate) semantic_minimiser: &'a mut SemanticMinimiser, pub(crate) notification_engine: &'a mut NotificationEngine, reification_literal: Option, } @@ -77,7 +76,6 @@ impl<'a> PropagationContextMut<'a> { trailed_values: &'a mut TrailedValues, assignments: &'a mut Assignments, reason_store: &'a mut ReasonStore, - semantic_minimiser: &'a mut SemanticMinimiser, notification_engine: &'a mut NotificationEngine, propagator_id: PropagatorId, ) -> Self { @@ -87,7 +85,6 @@ impl<'a> PropagationContextMut<'a> { reason_store, propagator_id, notification_engine, - semantic_minimiser, reification_literal: None, } } @@ -124,8 +121,8 @@ impl<'a> PropagationContextMut<'a> { } } - pub(crate) fn get_decision_level(&self) -> usize { - self.assignments.get_decision_level() + pub(crate) fn get_checkpoint(&self) -> usize { + self.assignments.get_checkpoint() } /// Returns whether the [`Predicate`] corresponding to the provided [`PredicateId`] is @@ -255,11 +252,11 @@ pub(crate) trait ReadDomains: HasAssignments { } /// Returns the holes which were created on the current decision level. - fn get_holes_on_current_decision_level( + fn get_holes_at_current_checkpoint( &self, var: &Var, ) -> impl Iterator { - var.get_holes_on_current_decision_level(self.assignments()) + var.get_holes_at_current_checkpoint(self.assignments()) } /// Returns all of the holes (currently) in the domain of `var` (including ones which were @@ -335,7 +332,7 @@ impl PropagationContextMut<'_> { predicate: Predicate, reason: impl Into, inference_code: InferenceCode, - ) -> Result<(), EmptyDomain> { + ) -> Result<(), EmptyDomainConflict> { let slot = self.reason_store.new_slot(); let modification_result = self.assignments.post_predicate( @@ -353,12 +350,19 @@ impl PropagationContextMut<'_> { ); Ok(()) } - Err(e) => { + Err(EmptyDomain) => { let _ = slot.populate( self.propagator_id, build_reason(reason, self.reification_literal), ); - Err(e) + let (trigger_predicate, trigger_reason, trigger_inference_code) = + self.assignments.remove_last_trail_element(); + + Err(EmptyDomainConflict { + trigger_predicate, + trigger_reason, + trigger_inference_code, + }) } } } diff --git a/pumpkin-crates/core/src/engine/cp/propagation/mod.rs b/pumpkin-crates/core/src/engine/cp/propagation/mod.rs index cead48708..84470c3ea 100644 --- a/pumpkin-crates/core/src/engine/cp/propagation/mod.rs +++ b/pumpkin-crates/core/src/engine/cp/propagation/mod.rs @@ -82,7 +82,7 @@ pub(crate) mod propagator_id; pub(crate) mod propagator_var_id; pub(crate) mod store; -pub(crate) use contexts::explanation_context::CurrentNogood; +pub use contexts::explanation_context::CurrentNogood; pub(crate) use contexts::explanation_context::ExplanationContext; pub(crate) use contexts::propagation_context::PropagationContext; pub(crate) use contexts::propagation_context::PropagationContextMut; @@ -90,7 +90,7 @@ pub(crate) use contexts::propagation_context::ReadDomains; pub(crate) use local_id::LocalId; pub(crate) use propagator::EnqueueDecision; pub(crate) use propagator::Propagator; -pub(crate) use propagator_id::PropagatorId; +pub use propagator_id::PropagatorId; pub(crate) use propagator_var_id::PropagatorVarId; #[cfg(doc)] diff --git a/pumpkin-crates/core/src/engine/cp/propagation/propagator.rs b/pumpkin-crates/core/src/engine/cp/propagation/propagator.rs index f4df173e4..1e0d584ae 100644 --- a/pumpkin-crates/core/src/engine/cp/propagation/propagator.rs +++ b/pumpkin-crates/core/src/engine/cp/propagation/propagator.rs @@ -1,12 +1,12 @@ use downcast_rs::Downcast; use downcast_rs::impl_downcast; +use dyn_clone::DynClone; +use dyn_clone::clone_trait_object; use super::ExplanationContext; use super::PropagationContext; use super::PropagationContextMut; use super::contexts::PropagationContextWithTrailedValues; -#[cfg(doc)] -use crate::basic_types::Inconsistency; use crate::basic_types::PredicateId; use crate::basic_types::PropagationStatusCP; use crate::basic_types::PropagatorConflict; @@ -21,12 +21,17 @@ use crate::predicates::Predicate; use crate::pumpkin_asserts::PUMPKIN_ASSERT_ADVANCED; #[cfg(doc)] use crate::pumpkin_asserts::PUMPKIN_ASSERT_EXTREME; +#[cfg(doc)] +use crate::state::Conflict; use crate::statistics::statistic_logger::StatisticLogger; // We need to use this to cast from `Box` to `NogoodPropagator`; rust inherently // does not allow downcasting from the trait definition to its concrete type. impl_downcast!(Propagator); +// To allow the State object to be cloneable, we need to allow `Box` to be cloned. +clone_trait_object!(Propagator); + /// All propagators implement the [`Propagator`] trait, which defines the main propagator logic with /// regards to propagation, detecting conflicts, and providing explanations. /// @@ -36,7 +41,7 @@ impl_downcast!(Propagator); /// enough, but a more mature implementation considers all functions in most cases. /// /// See the [`crate::engine::cp::propagation`] documentation for more details. -pub(crate) trait Propagator: Downcast { +pub(crate) trait Propagator: Downcast + DynClone { /// Return the name of the propagator, this is a convenience method that is used for printing. fn name(&self) -> &str; @@ -59,10 +64,10 @@ pub(crate) trait Propagator: Downcast { /// This method extends the current partial /// assignments with inferred domain changes found by the /// [`Propagator`]. In case no conflict has been detected it should return - /// [`Result::Ok`], otherwise it should return a [`Result::Err`] with an [`Inconsistency`] which + /// [`Result::Ok`], otherwise it should return a [`Result::Err`] with an [`Conflict`] which /// contains the reason for the failure; either because a propagation caused an - /// an empty domain ([`Inconsistency::EmptyDomain`]) or because the logic of the propagator - /// found the current state to be inconsistent ([`Inconsistency::Conflict`]). + /// an empty domain ([`Conflict::EmptyDomain`]) or because the logic of the propagator + /// found the current state to be inconsistent ([`Conflict::Propagator`]). /// /// Note that the failure (explanation) is given as a conjunction of predicates that lead to the /// failure diff --git a/pumpkin-crates/core/src/engine/cp/propagation/propagator_id.rs b/pumpkin-crates/core/src/engine/cp/propagation/propagator_id.rs index a02eec089..b108df215 100644 --- a/pumpkin-crates/core/src/engine/cp/propagation/propagator_id.rs +++ b/pumpkin-crates/core/src/engine/cp/propagation/propagator_id.rs @@ -4,7 +4,7 @@ use crate::containers::StorageKey; /// Each propagator is assigned a unique identifier at runtime. #[repr(transparent)] #[derive(Clone, Copy, Debug, Hash, PartialEq, Eq)] -pub(crate) struct PropagatorId(pub(crate) u32); +pub struct PropagatorId(pub(crate) u32); impl std::fmt::Display for PropagatorId { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { diff --git a/pumpkin-crates/core/src/engine/cp/propagation/store.rs b/pumpkin-crates/core/src/engine/cp/propagation/store.rs index a58e59d93..94275a43a 100644 --- a/pumpkin-crates/core/src/engine/cp/propagation/store.rs +++ b/pumpkin-crates/core/src/engine/cp/propagation/store.rs @@ -10,7 +10,7 @@ use crate::containers::Slot; use crate::engine::DebugDyn; /// A central store for propagators. -#[derive(Default)] +#[derive(Default, Clone)] pub(crate) struct PropagatorStore { propagators: KeyedVec>, } @@ -24,6 +24,13 @@ pub struct PropagatorHandle

{ } impl

PropagatorHandle

{ + pub(crate) fn new(propagator_id: PropagatorId) -> PropagatorHandle

{ + Self { + id: propagator_id, + propagator: PhantomData, + } + } + /// Get the type-erased [`PropagatorId`] of the propagator. pub(crate) fn propagator_id(self) -> PropagatorId { self.id @@ -60,6 +67,13 @@ impl PropagatorStore { } } + /// Get an exclusive reference to the propagator identified by the given handle. + /// + /// For more info, see [`Self::get_propagator`]. + pub(crate) fn get_propagator(&self, handle: PropagatorHandle

) -> Option<&P> { + self[handle.id].downcast_ref() + } + /// Get an exclusive reference to the propagator identified by the given handle. /// /// For more info, see [`Self::get_propagator`]. diff --git a/pumpkin-crates/core/src/engine/cp/propagator_queue.rs b/pumpkin-crates/core/src/engine/cp/propagator_queue.rs index f7ee624ee..f8f12eedf 100644 --- a/pumpkin-crates/core/src/engine/cp/propagator_queue.rs +++ b/pumpkin-crates/core/src/engine/cp/propagator_queue.rs @@ -6,13 +6,19 @@ use crate::containers::HashSet; use crate::engine::cp::propagation::PropagatorId; use crate::pumpkin_assert_moderate; -#[derive(Debug)] +#[derive(Debug, Clone)] pub(crate) struct PropagatorQueue { queues: Vec>, present_propagators: HashSet, present_priorities: BinaryHeap>, } +impl Default for PropagatorQueue { + fn default() -> Self { + Self::new(5) + } +} + impl PropagatorQueue { pub(crate) fn new(num_priority_levels: u32) -> PropagatorQueue { PropagatorQueue { @@ -22,6 +28,10 @@ impl PropagatorQueue { } } + pub(crate) fn is_empty(&self) -> bool { + self.present_propagators.is_empty() + } + #[cfg(test)] pub(crate) fn is_propagator_present(&self, propagator_id: PropagatorId) -> bool { self.present_propagators.contains(&propagator_id) diff --git a/pumpkin-crates/core/src/engine/cp/reason.rs b/pumpkin-crates/core/src/engine/cp/reason.rs index 6f989829c..05203a7e6 100644 --- a/pumpkin-crates/core/src/engine/cp/reason.rs +++ b/pumpkin-crates/core/src/engine/cp/reason.rs @@ -11,7 +11,7 @@ use crate::predicates::Predicate; use crate::pumpkin_assert_simple; /// The reason store holds a reason for each change made by a CP propagator on a trail. -#[derive(Default, Debug)] +#[derive(Default, Debug, Clone)] pub(crate) struct ReasonStore { trail: Trail<(PropagatorId, StoredReason)>, } @@ -63,8 +63,8 @@ impl ReasonStore { } } - pub(crate) fn increase_decision_level(&mut self) { - self.trail.increase_decision_level() + pub(crate) fn new_checkpoint(&mut self) { + self.trail.new_checkpoint() } pub(crate) fn synchronise(&mut self, level: usize) { @@ -102,7 +102,7 @@ pub(crate) enum Reason { } /// A reason for CP propagator to make a change -#[derive(Debug)] +#[derive(Debug, Clone)] pub(crate) enum StoredReason { /// An eager reason contains the propositional conjunction with the reason, without the /// propagated predicate. diff --git a/pumpkin-crates/core/src/engine/cp/test_solver.rs b/pumpkin-crates/core/src/engine/cp/test_solver.rs index 92053c1ee..f6d9d584a 100644 --- a/pumpkin-crates/core/src/engine/cp/test_solver.rs +++ b/pumpkin-crates/core/src/engine/cp/test_solver.rs @@ -2,75 +2,65 @@ //! This module exposes helpers that aid testing of CP propagators. The [`TestSolver`] allows //! setting up specific scenarios under which to test the various operations of a propagator. use std::fmt::Debug; +use std::num::NonZero; use super::PropagatorQueue; -use super::TrailedValues; use super::propagation::EnqueueDecision; use super::propagation::ExplanationContext; use super::propagation::constructor::PropagatorConstructor; -use super::propagation::constructor::PropagatorConstructorContext; -use super::propagation::store::PropagatorStore; -use crate::PropagatorHandle; -use crate::basic_types::Inconsistency; use crate::containers::KeyGenerator; -use crate::engine::Assignments; use crate::engine::EmptyDomain; -use crate::engine::conflict_analysis::SemanticMinimiser; -use crate::engine::notifications::NotificationEngine; +use crate::engine::State; use crate::engine::predicates::predicate::Predicate; use crate::engine::propagation::PropagationContext; use crate::engine::propagation::PropagationContextMut; use crate::engine::propagation::PropagatorId; -use crate::engine::reason::ReasonStore; use crate::engine::variables::DomainId; use crate::engine::variables::IntegerVariable; use crate::engine::variables::Literal; +use crate::options::LearningOptions; use crate::predicate; use crate::predicates::PropositionalConjunction; use crate::proof::ConstraintTag; use crate::proof::InferenceCode; -use crate::proof::ProofLog; +use crate::propagators::nogoods::NogoodPropagator; +use crate::propagators::nogoods::NogoodPropagatorConstructor; +use crate::state::Conflict; +use crate::state::PropagatorHandle; /// A container for CP variables, which can be used to test propagators. #[derive(Debug)] pub(crate) struct TestSolver { - pub assignments: Assignments, - pub propagator_store: PropagatorStore, - pub reason_store: ReasonStore, - pub semantic_minimiser: SemanticMinimiser, - pub trailed_values: TrailedValues, - pub notification_engine: NotificationEngine, + pub(crate) state: State, constraint_tags: KeyGenerator, - inference_codes: KeyGenerator, + pub(crate) nogood_handle: PropagatorHandle, } impl Default for TestSolver { fn default() -> Self { + let mut state = State::default(); + let handle = state.add_propagator(NogoodPropagatorConstructor::new( + 0, + LearningOptions::default(), + )); let mut solver = Self { - assignments: Default::default(), - reason_store: Default::default(), - propagator_store: Default::default(), - semantic_minimiser: Default::default(), - notification_engine: Default::default(), - trailed_values: Default::default(), + state, constraint_tags: Default::default(), - inference_codes: Default::default(), + nogood_handle: handle, }; // We allocate space for the zero-th dummy variable at the root level of the assignments. - solver.notification_engine.grow(); + solver.state.notification_engine.grow(); solver } } impl TestSolver { pub(crate) fn new_variable(&mut self, lb: i32, ub: i32) -> DomainId { - self.notification_engine.grow(); - self.assignments.grow(lb, ub) + self.state.new_interval_variable(lb, ub, None) } pub(crate) fn new_sparse_variable(&mut self, values: Vec) -> DomainId { - self.notification_engine.grow(); - self.assignments.create_new_integer_variable_sparse(values) + self.state.new_sparse_variable(values, None) } pub(crate) fn new_literal(&mut self) -> Literal { @@ -81,58 +71,23 @@ impl TestSolver { pub(crate) fn new_propagator( &mut self, constructor: Constructor, - ) -> Result + ) -> Result where Constructor: PropagatorConstructor, Constructor::PropagatorImpl: 'static, { - self.new_propagator_with_handle(move |_| constructor) - .map(|handle| handle.propagator_id()) - } - - pub(crate) fn new_propagator_with_handle( - &mut self, - constructor: impl FnOnce(PropagatorHandle) -> Constructor, - ) -> Result, Inconsistency> - where - Constructor: PropagatorConstructor, - Constructor::PropagatorImpl: 'static, - { - let propagator_slot = self.propagator_store.new_propagator(); - - let mut proof_log = ProofLog::default(); - - let constructor_context = PropagatorConstructorContext::new( - &mut self.notification_engine, - &mut self.trailed_values, - &mut proof_log, - propagator_slot.key().propagator_id(), - &mut self.assignments, - ); - - let propagator = constructor(propagator_slot.key()).create(constructor_context); - - let handle = propagator_slot.populate(propagator); - - let context = PropagationContextMut::new( - &mut self.trailed_values, - &mut self.assignments, - &mut self.reason_store, - &mut self.semantic_minimiser, - &mut self.notification_engine, - PropagatorId(0), - ); - self.propagator_store[handle.propagator_id()].propagate(context)?; - - Ok(handle) + let handle = self.state.add_propagator(constructor); + self.state + .propagate_to_fixed_point() + .map(|_| handle.propagator_id()) } pub(crate) fn contains(&self, var: Var, value: i32) -> bool { - var.contains(&self.assignments, value) + var.contains(&self.state.assignments, value) } pub(crate) fn lower_bound(&self, var: DomainId) -> i32 { - self.assignments.get_lower_bound(var) + self.state.assignments.get_lower_bound(var) } pub(crate) fn remove_and_notify( @@ -141,21 +96,18 @@ impl TestSolver { var: DomainId, value: i32, ) -> EnqueueDecision { - let result = self.assignments.post_predicate( - predicate!(var != value), - None, - &mut self.notification_engine, - ); + let result = self.state.post(predicate!(var != value)); assert!( result.is_ok(), "The provided value to `increase_lower_bound` caused an empty domain, generally the propagator should not be notified of this change!" ); let mut propagator_queue = PropagatorQueue::new(4); - self.notification_engine + self.state + .notification_engine .notify_propagators_about_domain_events_test( - &mut self.assignments, - &mut self.trailed_values, - &mut self.propagator_store, + &mut self.state.assignments, + &mut self.state.trailed_values, + &mut self.state.propagators, &mut propagator_queue, ); if propagator_queue.is_propagator_present(propagator) { @@ -172,21 +124,18 @@ impl TestSolver { var: DomainId, value: i32, ) -> EnqueueDecision { - let result = self.assignments.post_predicate( - predicate!(var >= value), - None, - &mut self.notification_engine, - ); + let result = self.state.post(predicate!(var >= value)); assert!( result.is_ok(), "The provided value to `increase_lower_bound` caused an empty domain, generally the propagator should not be notified of this change!" ); let mut propagator_queue = PropagatorQueue::new(4); - self.notification_engine + self.state + .notification_engine .notify_propagators_about_domain_events_test( - &mut self.assignments, - &mut self.trailed_values, - &mut self.propagator_store, + &mut self.state.assignments, + &mut self.state.trailed_values, + &mut self.state.propagators, &mut propagator_queue, ); if propagator_queue.is_propagator_present(propagator) { @@ -203,21 +152,18 @@ impl TestSolver { var: DomainId, value: i32, ) -> EnqueueDecision { - let result = self.assignments.post_predicate( - predicate!(var <= value), - None, - &mut self.notification_engine, - ); + let result = self.state.post(predicate!(var <= value)); assert!( result.is_ok(), "The provided value to `increase_lower_bound` caused an empty domain, generally the propagator should not be notified of this change!" ); let mut propagator_queue = PropagatorQueue::new(4); - self.notification_engine + self.state + .notification_engine .notify_propagators_about_domain_events_test( - &mut self.assignments, - &mut self.trailed_values, - &mut self.propagator_store, + &mut self.state.assignments, + &mut self.state.trailed_values, + &mut self.state.propagators, &mut propagator_queue, ); if propagator_queue.is_propagator_present(propagator) { @@ -228,21 +174,18 @@ impl TestSolver { } pub(crate) fn is_literal_false(&self, literal: Literal) -> bool { - self.assignments + self.state + .assignments .evaluate_predicate(literal.get_true_predicate()) .is_some_and(|truth_value| !truth_value) } pub(crate) fn upper_bound(&self, var: DomainId) -> i32 { - self.assignments.get_upper_bound(var) + self.state.assignments.get_upper_bound(var) } pub(crate) fn remove(&mut self, var: DomainId, value: i32) -> Result<(), EmptyDomain> { - let _ = self.assignments.post_predicate( - predicate!(var != value), - None, - &mut self.notification_engine, - )?; + let _ = self.state.post(predicate!(var != value))?; Ok(()) } @@ -253,84 +196,87 @@ impl TestSolver { truth_value: bool, ) -> Result<(), EmptyDomain> { let _ = match truth_value { - true => self.assignments.post_predicate( + true => self.state.assignments.post_predicate( literal.get_true_predicate(), None, - &mut self.notification_engine, + &mut self.state.notification_engine, )?, - false => self.assignments.post_predicate( + false => self.state.assignments.post_predicate( (!literal).get_true_predicate(), None, - &mut self.notification_engine, + &mut self.state.notification_engine, )?, }; Ok(()) } - pub(crate) fn propagate(&mut self, propagator: PropagatorId) -> Result<(), Inconsistency> { + pub(crate) fn propagate(&mut self, propagator: PropagatorId) -> Result<(), Conflict> { let context = PropagationContextMut::new( - &mut self.trailed_values, - &mut self.assignments, - &mut self.reason_store, - &mut self.semantic_minimiser, - &mut self.notification_engine, - PropagatorId(0), + &mut self.state.trailed_values, + &mut self.state.assignments, + &mut self.state.reason_store, + &mut self.state.notification_engine, + propagator, ); - self.propagator_store[propagator].propagate(context) + self.state.propagators[propagator].propagate(context) } pub(crate) fn propagate_until_fixed_point( &mut self, propagator: PropagatorId, - ) -> Result<(), Inconsistency> { - let mut num_trail_entries = self.assignments.num_trail_entries(); + ) -> Result<(), Conflict> { + let mut num_trail_entries = self.state.assignments.num_trail_entries(); self.notify_propagator(propagator); loop { { // Specify the life-times to be able to retrieve the trail entries let context = PropagationContextMut::new( - &mut self.trailed_values, - &mut self.assignments, - &mut self.reason_store, - &mut self.semantic_minimiser, - &mut self.notification_engine, - PropagatorId(0), + &mut self.state.trailed_values, + &mut self.state.assignments, + &mut self.state.reason_store, + &mut self.state.notification_engine, + propagator, ); - self.propagator_store[propagator].propagate(context)?; + self.state.propagators[propagator].propagate(context)?; self.notify_propagator(propagator); } - if self.assignments.num_trail_entries() == num_trail_entries { + if self.state.assignments.num_trail_entries() == num_trail_entries { break; } - num_trail_entries = self.assignments.num_trail_entries(); + num_trail_entries = self.state.assignments.num_trail_entries(); } Ok(()) } pub(crate) fn notify_propagator(&mut self, _propagator: PropagatorId) { - self.notification_engine + self.state + .notification_engine .notify_propagators_about_domain_events_test( - &mut self.assignments, - &mut self.trailed_values, - &mut self.propagator_store, + &mut self.state.assignments, + &mut self.state.trailed_values, + &mut self.state.propagators, &mut PropagatorQueue::new(4), ); } pub(crate) fn get_reason_int(&mut self, predicate: Predicate) -> PropositionalConjunction { let reason_ref = self + .state .assignments .get_reason_for_predicate_brute_force(predicate); let mut predicates = vec![]; - let _ = self.reason_store.get_or_compute( + let _ = self.state.reason_store.get_or_compute( reason_ref, ExplanationContext::without_working_nogood( - &self.assignments, - self.assignments.get_trail_position(&predicate).unwrap(), - &mut self.notification_engine, + &self.state.assignments, + self.state + .assignments + .get_trail_position(&predicate) + .unwrap(), + &mut self.state.notification_engine, ), - &mut self.propagator_store, + &mut self.state.propagators, &mut predicates, ); @@ -365,27 +311,35 @@ impl TestSolver { } pub(crate) fn new_inference_code(&mut self) -> InferenceCode { - self.inference_codes.next_key() + self.state.inference_codes.push(( + ConstraintTag::from_non_zero( + NonZero::try_from(1 + self.state.inference_codes.len() as u32).unwrap(), + ), + "label".into(), + )) } - pub(crate) fn increase_decision_level(&mut self) { - self.assignments.increase_decision_level(); - self.notification_engine.increase_decision_level(); - self.trailed_values.increase_decision_level(); + pub(crate) fn new_checkpoint(&mut self) { + self.state.new_checkpoint(); } pub(crate) fn synchronise(&mut self, level: usize) { let _ = self + .state .assignments - .synchronise(level, &mut self.notification_engine); - self.notification_engine - .synchronise(level, &self.assignments, &mut self.trailed_values); - self.trailed_values.synchronise(level); + .synchronise(level, &mut self.state.notification_engine); + self.state.notification_engine.synchronise( + level, + &self.state.assignments, + &mut self.state.trailed_values, + ); + self.state.trailed_values.synchronise(level); - self.propagator_store + self.state + .propagators .iter_propagators_mut() .for_each(|propagator| { - propagator.synchronise(PropagationContext::new(&self.assignments)) + propagator.synchronise(PropagationContext::new(&self.state.assignments)) }) } } diff --git a/pumpkin-crates/core/src/engine/cp/trailed/trailed_values.rs b/pumpkin-crates/core/src/engine/cp/trailed/trailed_values.rs index ec5f2f7ed..665719ca5 100644 --- a/pumpkin-crates/core/src/engine/cp/trailed/trailed_values.rs +++ b/pumpkin-crates/core/src/engine/cp/trailed/trailed_values.rs @@ -14,17 +14,17 @@ impl TrailedValues { self.values.push(initial_value) } - pub(crate) fn increase_decision_level(&mut self) { - self.trail.increase_decision_level() + pub(crate) fn new_checkpoint(&mut self) { + self.trail.new_checkpoint() } pub(crate) fn read(&self, trailed_integer: TrailedInteger) -> i64 { self.values[trailed_integer] } - pub(crate) fn synchronise(&mut self, new_decision_level: usize) { + pub(crate) fn synchronise(&mut self, new_checkpoint: usize) { self.trail - .synchronise(new_decision_level) + .synchronise(new_checkpoint) .for_each(|state_change| self.values[state_change.reference] = state_change.old_value) } @@ -52,7 +52,7 @@ impl TrailedValues { pub(crate) fn debug_create_empty_clone(&self) -> Self { let mut new_trail = self.trail.clone(); let mut new_values = self.values.clone(); - if new_trail.get_decision_level() > 0 { + if new_trail.get_checkpoint() > 0 { new_trail.synchronise(0).for_each(|state_change| { new_values[state_change.reference] = state_change.old_value }); @@ -75,7 +75,7 @@ mod tests { assert_eq!(assignments.read(trailed_integer), 0); - assignments.increase_decision_level(); + assignments.new_checkpoint(); assignments.add_assign(trailed_integer, 5); assert_eq!(assignments.read(trailed_integer), 5); @@ -83,7 +83,7 @@ mod tests { assignments.add_assign(trailed_integer, 5); assert_eq!(assignments.read(trailed_integer), 10); - assignments.increase_decision_level(); + assignments.new_checkpoint(); assignments.add_assign(trailed_integer, 1); assert_eq!(assignments.read(trailed_integer), 11); diff --git a/pumpkin-crates/core/src/engine/debug_helper.rs b/pumpkin-crates/core/src/engine/debug_helper.rs index bf51dfc97..fa81125fc 100644 --- a/pumpkin-crates/core/src/engine/debug_helper.rs +++ b/pumpkin-crates/core/src/engine/debug_helper.rs @@ -3,22 +3,20 @@ use std::fmt::Formatter; use std::iter::once; use log::debug; -use log::warn; use super::TrailedValues; -use super::conflict_analysis::SemanticMinimiser; use super::notifications::NotificationEngine; use super::predicates::predicate::Predicate; use super::propagation::ExplanationContext; use super::propagation::store::PropagatorStore; use super::reason::ReasonStore; -use crate::basic_types::Inconsistency; use crate::basic_types::PropositionalConjunction; use crate::engine::cp::Assignments; use crate::engine::propagation::PropagationContextMut; use crate::engine::propagation::Propagator; use crate::engine::propagation::PropagatorId; use crate::propagators::nogoods::NogoodPropagator; +use crate::state::Conflict; #[derive(Copy, Clone)] pub(crate) struct DebugDyn<'a> { @@ -79,24 +77,21 @@ impl DebugHelper { let num_entries_on_trail_before_propagation = assignments_clone.num_trail_entries(); let mut reason_store = Default::default(); - let mut semantic_minimiser = SemanticMinimiser::default(); let context = PropagationContextMut::new( &mut trailed_values_clone, &mut assignments_clone, &mut reason_store, - &mut semantic_minimiser, &mut notification_engine_clone, PropagatorId(propagator_id as u32), ); let propagation_status_cp = propagator.debug_propagate_from_scratch(context); if let Err(ref failure_reason) = propagation_status_cp { - warn!( + panic!( "Propagator '{}' with id '{propagator_id}' seems to have missed a conflict in its regular propagation algorithms! Aborting!\n Expected reason: {failure_reason:?}", propagator.name() ); - panic!(); } let num_missed_propagations = @@ -260,12 +255,10 @@ impl DebugHelper { if adding_predicates_was_successful { // Now propagate using the debug propagation method. let mut reason_store = Default::default(); - let mut semantic_minimiser = SemanticMinimiser::default(); let context = PropagationContextMut::new( &mut trailed_values_clone, &mut assignments_clone, &mut reason_store, - &mut semantic_minimiser, &mut notification_engine_clone, propagator_id, ); @@ -285,7 +278,7 @@ impl DebugHelper { assert!( { - let is_empty_domain = matches!(conflict, Inconsistency::EmptyDomain); + let is_empty_domain = matches!(conflict, Conflict::EmptyDomain(_)); let has_propagated_predicate = assignments.is_predicate_satisfied(propagated_predicate); if is_empty_domain && has_propagated_predicate { @@ -297,13 +290,13 @@ impl DebugHelper { // If this is not the case then we check whether the explanation is a // subset of the premises - if let Inconsistency::Conflict(ref found_inconsistency) = conflict { + if let Conflict::Propagator(ref found_inconsistency) = conflict { found_inconsistency .conjunction .iter() .all(|predicate| reason.contains(predicate)) || reason.iter().all(|predicate| { - found_inconsistency.conjunction.contains(*predicate) + found_inconsistency.conjunction.contains(predicate) }) } else { false @@ -366,7 +359,6 @@ impl DebugHelper { if adding_predicates_was_successful { // now propagate using the debug propagation method let mut reason_store = Default::default(); - let mut semantic_minimiser = SemanticMinimiser::default(); // Note that it might take multiple iterations before the conflict is reached due // to the assumption that some propagators make on that they are not idempotent! @@ -382,7 +374,6 @@ impl DebugHelper { &mut trailed_values_clone, &mut assignments_clone, &mut reason_store, - &mut semantic_minimiser, &mut notification_engine_clone, propagator_id, ); @@ -446,12 +437,10 @@ impl DebugHelper { if adding_predicates_was_successful { // now propagate using the debug propagation method let mut reason_store = Default::default(); - let mut semantic_minimiser = SemanticMinimiser::default(); let context = PropagationContextMut::new( &mut trailed_values_clone, &mut assignments_clone, &mut reason_store, - &mut semantic_minimiser, &mut notification_engine_clone, propagator_id, ); diff --git a/pumpkin-crates/core/src/engine/literal_block_distance.rs b/pumpkin-crates/core/src/engine/literal_block_distance.rs index 550e073bb..0863ace64 100644 --- a/pumpkin-crates/core/src/engine/literal_block_distance.rs +++ b/pumpkin-crates/core/src/engine/literal_block_distance.rs @@ -30,14 +30,12 @@ impl Lbd { ) -> u32 { self.lbd_helper.set_to_empty(); self.lbd_helper - .accommodate(&(assignments.get_decision_level() as u32)); + .accommodate(&(assignments.get_checkpoint() as u32)); for predicate in predicates { - let decision_level = assignments - .get_decision_level_for_predicate(predicate) - .unwrap(); + let checkpoint = assignments.get_checkpoint_for_predicate(predicate).unwrap(); - self.lbd_helper.insert(decision_level as u32); + self.lbd_helper.insert(checkpoint as u32); } self.lbd_helper.len() as u32 diff --git a/pumpkin-crates/core/src/engine/mod.rs b/pumpkin-crates/core/src/engine/mod.rs index 12b6d18c9..684c3570d 100644 --- a/pumpkin-crates/core/src/engine/mod.rs +++ b/pumpkin-crates/core/src/engine/mod.rs @@ -8,6 +8,7 @@ pub(crate) mod notifications; pub(crate) mod predicates; mod restart_strategy; mod solver_statistics; +pub(crate) mod state; pub(crate) mod termination; pub(crate) mod variable_names; pub(crate) mod variables; @@ -16,6 +17,7 @@ pub(crate) use conflict_analysis::ResolutionResolver; pub use constraint_satisfaction_solver::ConflictResolver; pub(crate) use constraint_satisfaction_solver::ConstraintSatisfactionSolver; pub use constraint_satisfaction_solver::SatisfactionSolverOptions; +pub use cp::EmptyDomain; pub(crate) use cp::*; pub(crate) use debug_helper::DebugDyn; pub(crate) use debug_helper::DebugHelper; @@ -23,6 +25,7 @@ pub(crate) use literal_block_distance::Lbd; pub use restart_strategy::RestartOptions; pub(crate) use restart_strategy::RestartStrategy; pub(crate) use solver_statistics::SolverStatistics; +pub use state::*; pub(crate) use variable_names::VariableNames; pub(crate) use crate::engine::notifications::DomainEvents; diff --git a/pumpkin-crates/core/src/engine/notifications/domain_event_notification/domain_event_watch_list.rs b/pumpkin-crates/core/src/engine/notifications/domain_event_notification/domain_event_watch_list.rs index ad150fab0..a71b6fc44 100644 --- a/pumpkin-crates/core/src/engine/notifications/domain_event_notification/domain_event_watch_list.rs +++ b/pumpkin-crates/core/src/engine/notifications/domain_event_notification/domain_event_watch_list.rs @@ -8,7 +8,7 @@ use crate::engine::notifications::NotificationEngine; use crate::engine::propagation::PropagatorVarId; use crate::engine::variables::DomainId; -#[derive(Default, Debug)] +#[derive(Default, Debug, Clone)] pub(crate) struct WatchListDomainEvents { /// Contains propagator ids of propagators that watch domain changes of the i-th integer /// variable @@ -113,14 +113,14 @@ impl<'a> Watchers<'a> { } } -#[derive(Default, Debug)] +#[derive(Default, Debug, Clone)] pub(crate) struct WatcherDomainEvents { // FIXME measure performance of these vectors, they are treated as sets pub(crate) forward_watcher: Watcher, pub(crate) backtrack_watcher: Watcher, } -#[derive(Debug, Default)] +#[derive(Debug, Default, Clone)] pub(crate) struct Watcher { pub(crate) lower_bound_watchers: Vec, pub(crate) upper_bound_watchers: Vec, diff --git a/pumpkin-crates/core/src/engine/notifications/mod.rs b/pumpkin-crates/core/src/engine/notifications/mod.rs index 2a4f4f533..3a851481e 100644 --- a/pumpkin-crates/core/src/engine/notifications/mod.rs +++ b/pumpkin-crates/core/src/engine/notifications/mod.rs @@ -13,7 +13,6 @@ pub(crate) use predicate_notification::PredicateNotifier; use super::propagation::PropagationContext; use super::propagation::PropagatorVarId; -use crate::PropagatorHandle; use crate::basic_types::PredicateId; use crate::engine::Assignments; use crate::engine::PropagatorQueue; @@ -28,9 +27,10 @@ use crate::predicates::Predicate; use crate::propagators::nogoods::NogoodPropagator; use crate::pumpkin_assert_extreme; use crate::pumpkin_assert_simple; +use crate::state::PropagatorHandle; use crate::variables::DomainId; -#[derive(Debug)] +#[derive(Debug, Clone)] pub(crate) struct NotificationEngine { /// Responsible for the notification of predicates becoming either falsified or satisfied. predicate_notifier: PredicateNotifier, @@ -497,10 +497,10 @@ impl NotificationEngine { self.predicate_notifier.predicate_to_id.num_predicate_ids() } - pub(crate) fn increase_decision_level(&mut self) { + pub(crate) fn new_checkpoint(&mut self) { self.predicate_notifier .predicate_id_assignments - .increase_decision_level(); + .new_checkpoint(); } pub(crate) fn debug_create_from_assignments(&mut self, assignments: &Assignments) { @@ -573,7 +573,7 @@ impl NotificationEngine { _trailed_values: &mut TrailedValues, ) { pumpkin_assert_simple!( - assignments.get_decision_level() == backtrack_level, + assignments.get_checkpoint() == backtrack_level, "Expected the assignments to have been backtracked previously" ); self.predicate_notifier diff --git a/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_assignments.rs b/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_assignments.rs index 4abbe9696..b79e1f049 100644 --- a/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_assignments.rs +++ b/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_assignments.rs @@ -80,8 +80,8 @@ impl PredicateIdAssignments { self.satisfied_predicates.drain(..) } - pub(crate) fn increase_decision_level(&mut self) { - self.trail.increase_decision_level() + pub(crate) fn new_checkpoint(&mut self) { + self.trail.new_checkpoint() } /// Stores a predicate in the [`PredicateIdAssignments`] with its corresponding @@ -175,14 +175,14 @@ impl PredicateIdAssignments { self.predicate_values[predicate_id].is_falsified() } - pub(crate) fn synchronise(&mut self, new_decision_level: usize) { + pub(crate) fn synchronise(&mut self, new_checkpoint: usize) { // We also need to clear the stored updated predicates; if this is not done, then it can be // the case that a predicate is erroneously said to be satisfied/falsified while it is not self.satisfied_predicates.clear(); self.falsified_predicates.clear(); self.trail - .synchronise(new_decision_level) + .synchronise(new_checkpoint) .for_each(|predicate_id| { // If the predicate id is unassigned then backtracking will not change anything; // this is more of a sanity check since it should not be on the trail if it is diff --git a/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_notifier.rs b/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_notifier.rs index e6d4cd5c9..d695c472c 100644 --- a/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_notifier.rs +++ b/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_notifier.rs @@ -21,7 +21,7 @@ use crate::variables::DomainId; /// /// It also contains the [`PredicateIdAssignments`] which serves as a (lazy) structure for /// retrieving the polarity of [`Predicate`]s (represented by [`PredicateId`]s). -#[derive(Default, Debug)] +#[derive(Default, Debug, Clone)] pub(crate) struct PredicateNotifier { /// Maps a [`Predicate`] to a [`PredicateId`] pub(crate) predicate_to_id: PredicateIdGenerator, diff --git a/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_tracker_for_domain.rs b/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_tracker_for_domain.rs index f643b73b8..82a8394e4 100644 --- a/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_tracker_for_domain.rs +++ b/pumpkin-crates/core/src/engine/notifications/predicate_notification/predicate_tracker_for_domain.rs @@ -108,7 +108,7 @@ impl PredicateTrackerForDomain { return; } - for removed_value in assignments.get_holes_on_current_decision_level(domain) { + for removed_value in assignments.get_holes_at_current_checkpoint(domain) { let predicate = predicate_type.into_predicate(domain, assignments, Some(removed_value)); if !self.disequality.is_empty() && !disequality_is_fixed { diff --git a/pumpkin-crates/core/src/engine/solver_statistics.rs b/pumpkin-crates/core/src/engine/solver_statistics.rs index b7f4eeef4..548ae878b 100644 --- a/pumpkin-crates/core/src/engine/solver_statistics.rs +++ b/pumpkin-crates/core/src/engine/solver_statistics.rs @@ -1,8 +1,6 @@ use crate::basic_types::moving_averages::CumulativeMovingAverage; use crate::basic_types::time::Duration; use crate::create_statistics_struct; -use crate::engine::Assignments; -use crate::engine::propagation::store::PropagatorStore; use crate::statistics::Statistic; use crate::statistics::StatisticLogger; use crate::statistics::log_statistic; @@ -18,34 +16,16 @@ pub(crate) struct SolverStatistics { } impl SolverStatistics { - pub(crate) fn log( - &self, - assignments: &Assignments, - propagators: &PropagatorStore, - statistic_logger: StatisticLogger, - verbose: bool, - ) { + pub(crate) fn log(&self, statistic_logger: StatisticLogger, verbose: bool) { log_statistic("nodes", self.engine_statistics.num_decisions); - log_statistic("failures", self.engine_statistics.num_conflicts); log_statistic("restarts", self.engine_statistics.num_restarts); - log_statistic("variables", assignments.num_domains()); - log_statistic("propagators", propagators.num_propagators()); - log_statistic( - "propagations", - self.engine_statistics.num_propagators_called, - ); log_statistic("peakDepth", self.engine_statistics.peak_depth); - log_statistic("nogoods", self.engine_statistics.num_conflicts); log_statistic("backjumps", self.engine_statistics.sum_of_backjumps); log_statistic( "solveTime", self.engine_statistics.time_spent_in_solver.as_secs_f64(), ); if verbose { - log_statistic( - "numAtomicConstraintsPropagated", - self.engine_statistics.num_propagations, - ); log_statistic("numberOfBackjumps", self.engine_statistics.num_backjumps); self.learned_clause_statistics.log(statistic_logger) } @@ -57,14 +37,8 @@ impl SolverStatistics { pub(crate) struct EngineStatistics { /// The number of decisions taken by the solver pub(crate) num_decisions: u64, - /// The number of conflicts encountered by the solver - pub(crate) num_conflicts: u64, /// The number of times the solver has restarted pub(crate) num_restarts: u64, - /// The number of (integer) propagations made by the solver - pub(crate) num_propagations: u64, - /// The number of times a propagator was called. - pub(crate) num_propagators_called: u64, /// The amount of time which is spent in the solver. pub(crate) time_spent_in_solver: Duration, /// The peak depth of the seach tree diff --git a/pumpkin-crates/core/src/engine/state.rs b/pumpkin-crates/core/src/engine/state.rs new file mode 100644 index 000000000..ebb4c5df2 --- /dev/null +++ b/pumpkin-crates/core/src/engine/state.rs @@ -0,0 +1,984 @@ +use std::sync::Arc; + +use crate::basic_types::PropagatorConflict; +use crate::containers::KeyedVec; +use crate::create_statistics_struct; +use crate::engine::Assignments; +use crate::engine::ConstraintProgrammingTrailEntry; +use crate::engine::DebugHelper; +use crate::engine::EmptyDomain; +use crate::engine::PropagatorQueue; +use crate::engine::TrailedValues; +use crate::engine::VariableNames; +use crate::engine::notifications::NotificationEngine; +use crate::engine::propagation::CurrentNogood; +use crate::engine::propagation::ExplanationContext; +use crate::engine::propagation::PropagationContext; +use crate::engine::propagation::PropagationContextMut; +use crate::engine::propagation::Propagator; +use crate::engine::propagation::PropagatorId; +use crate::engine::propagation::constructor::PropagatorConstructor; +use crate::engine::propagation::constructor::PropagatorConstructorContext; +use crate::engine::propagation::store::PropagatorStore; +use crate::engine::reason::ReasonRef; +use crate::engine::reason::ReasonStore; +use crate::predicate; +use crate::predicates::Predicate; +use crate::predicates::PredicateType; +use crate::proof::ConstraintTag; +use crate::proof::InferenceCode; +use crate::proof::InferenceLabel; +#[cfg(doc)] +use crate::proof::ProofLog; +use crate::pumpkin_assert_advanced; +use crate::pumpkin_assert_eq_simple; +use crate::pumpkin_assert_extreme; +use crate::pumpkin_assert_simple; +use crate::results::SolutionReference; +use crate::state::PropagatorHandle; +use crate::statistics::StatisticLogger; +use crate::statistics::log_statistic; +use crate::variables::DomainId; +use crate::variables::IntegerVariable; +use crate::variables::Literal; + +/// The [`State`] is the container of variables and propagators. +/// +/// [`State`] implements [`Clone`], and cloning the [`State`] will create a fresh copy of the +/// [`State`]. If the [`State`] is large, this may be extremely expensive. +#[derive(Debug, Clone)] +pub struct State { + /// The list of propagators; propagators live here and are queried when events (domain changes) + /// happen. + pub(crate) propagators: PropagatorStore, + /// Tracks information related to the assignments of integer variables. + pub(crate) assignments: Assignments, + /// Keep track of trailed values (i.e. values which automatically backtrack). + pub(crate) trailed_values: TrailedValues, + /// The names of the variables in the solver. + variable_names: VariableNames, + /// Dictates the order in which propagators will be called to propagate. + pub(crate) propagator_queue: PropagatorQueue, + /// Handles storing information about propagation reasons, which are used later to construct + /// explanations during conflict analysis. + pub(crate) reason_store: ReasonStore, + /// Component responsible for providing notifications for changes to the domains of variables + /// and/or the polarity [Predicate]s + pub(crate) notification_engine: NotificationEngine, + pub(crate) inference_codes: KeyedVec)>, + + statistics: StateStatistics, +} + +create_statistics_struct!(StateStatistics { + num_propagators_called: usize, + num_propagations: usize, + num_conflicts: usize, +}); + +/// Information concerning the conflict returned by [`State::propagate_to_fixed_point`]. +/// +/// Two (related) conflicts can happen: +/// 1) a propagator explicitly detects a conflict. +/// 2) a propagator post a domain change that results in a variable having an empty domain. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Conflict { + /// A conflict raised explicitly by a propagator. + Propagator(PropagatorConflict), + /// A conflict caused by an empty domain for a variable occurring. + EmptyDomain(EmptyDomainConflict), +} + +impl From for Conflict { + fn from(value: EmptyDomainConflict) -> Self { + Conflict::EmptyDomain(value) + } +} + +impl From for Conflict { + fn from(value: PropagatorConflict) -> Self { + Conflict::Propagator(value) + } +} + +/// A conflict because a domain became empty. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct EmptyDomainConflict { + /// The predicate that caused a domain to become empty. + pub trigger_predicate: Predicate, + /// The reason for [`EmptyDomainConflict::trigger_predicate`] to be true. + pub(crate) trigger_reason: ReasonRef, + /// The [`InferenceCode`] that accompanies [`EmptyDomainConflict::trigger_reason`]. + pub(crate) trigger_inference_code: InferenceCode, +} + +impl EmptyDomainConflict { + /// The domain that became empty. + pub fn domain(&self) -> DomainId { + self.trigger_predicate.get_domain() + } + + /// Returns the reason for the [`EmptyDomainConflict::trigger_predicate`] being propagated to + /// true while it is already false in the [`State`]. + pub fn get_reason( + &self, + state: &mut State, + reason_buffer: &mut (impl Extend + AsRef<[Predicate]>), + current_nogood: CurrentNogood, + ) { + let _ = state.reason_store.get_or_compute( + self.trigger_reason, + ExplanationContext::new( + &state.assignments, + current_nogood, + state.trail_len(), + &mut state.notification_engine, + ), + &mut state.propagators, + reason_buffer, + ); + } +} + +impl Default for State { + fn default() -> Self { + let mut result = Self { + assignments: Default::default(), + trailed_values: TrailedValues::default(), + variable_names: VariableNames::default(), + propagator_queue: PropagatorQueue::default(), + propagators: PropagatorStore::default(), + reason_store: ReasonStore::default(), + notification_engine: NotificationEngine::default(), + inference_codes: KeyedVec::default(), + statistics: StateStatistics::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 + // trivially true. We need to adjust other data structures to take this into account. + let dummy_id = Predicate::trivially_true().get_domain(); + + result.variable_names.add_integer(dummy_id, "Dummy".into()); + assert!(dummy_id.id() == 0); + assert!(result.assignments.get_lower_bound(dummy_id) == 1); + assert!(result.assignments.get_upper_bound(dummy_id) == 1); + + result + } +} + +impl State { + pub(crate) fn log_statistics(&self, verbose: bool) { + log_statistic("variables", self.assignments.num_domains()); + log_statistic("propagators", self.propagators.num_propagators()); + log_statistic("failures", self.statistics.num_conflicts); + log_statistic("propagations", self.statistics.num_propagators_called); + log_statistic("nogoods", self.statistics.num_conflicts); + if verbose { + log_statistic( + "numAtomicConstraintsPropagated", + self.statistics.num_propagations, + ); + for (index, propagator) in self.propagators.iter_propagators().enumerate() { + propagator.log_statistics(StatisticLogger::new([ + propagator.name(), + "number", + index.to_string().as_str(), + ])); + } + } + } +} + +/// Operations to create . +impl State { + /// Create a new [`InferenceCode`] for a [`ConstraintTag`] and [`InferenceLabel`] combination. + /// + /// The inference codes are required to log inferences with [`ProofLog::log_inference`]. + pub(crate) fn create_inference_code( + &mut self, + constraint_tag: ConstraintTag, + inference_label: impl InferenceLabel, + ) -> InferenceCode { + self.inference_codes + .push((constraint_tag, inference_label.to_str())) + } + + /// Creates a new Boolean (0-1) variable. + /// + /// The name is used in solver traces to identify individual domains. They are required to be + /// unique. If the state already contains a domain with the given name, then this function + /// will panic. + /// + /// Creation of new [`Literal`]s is not influenced by the current checkpoint of the state. + /// If a [`Literal`] is created at a non-zero checkpoint, then it will _not_ 'disappear' + /// when backtracking past the checkpoint where the domain was created. + pub fn new_literal(&mut self, name: Option>) -> Literal { + let domain_id = self.new_interval_variable(0, 1, name); + Literal::new(domain_id) + } + + /// Creates a new interval variable with the given lower and upper bound. + /// + /// The name is used in solver traces to identify individual domains. They are required to be + /// unique. If the state already contains a domain with the given name, then this function + /// will panic. + /// + /// Creation of new domains is not influenced by the current checkpoint of the state. If + /// a domain is created at a non-zero checkpoint, then it will _not_ 'disappear' when + /// backtracking past the checkpoint where the domain was created.) + pub fn new_interval_variable( + &mut self, + lower_bound: i32, + upper_bound: i32, + name: Option>, + ) -> DomainId { + let domain_id = self.assignments.grow(lower_bound, upper_bound); + + if let Some(name) = name { + self.variable_names.add_integer(domain_id, name); + } + + self.notification_engine.grow(); + + domain_id + } + + /// Creates a new sparse domain with the given values. + /// + /// Note that this is implemented as an interval domain with explicit holes in the domain. For + /// very sparse domains, this can result in a high memory overhead. + /// + /// For more information on creation of domains, see [`State::new_interval_variable`]. + pub fn new_sparse_variable(&mut self, values: Vec, name: Option) -> DomainId { + let domain_id = self.assignments.create_new_integer_variable_sparse(values); + + if let Some(name) = name { + self.variable_names.add_integer(domain_id, name.into()); + } + + self.notification_engine.grow(); + + domain_id + } +} + +/// Operations to retrieve information about values +impl State { + /// Returns the lower-bound of the given `variable`. + pub fn lower_bound(&self, variable: Var) -> i32 { + variable.lower_bound(&self.assignments) + } + + /// Returns the upper-bound of the given `variable`. + pub fn upper_bound(&self, variable: Var) -> i32 { + variable.upper_bound(&self.assignments) + } + + /// Returns whether the given `variable` contains the provided `value`. + pub fn contains(&self, variable: Var, value: i32) -> bool { + variable.contains(&self.assignments, value) + } + + /// If the given `variable` is fixed, then [`Some`] containing the assigned value is + /// returned. Otherwise, [`None`] is returned. + pub fn fixed_value(&self, variable: Var) -> Option { + (self.lower_bound(variable.clone()) == self.upper_bound(variable.clone())) + .then(|| self.lower_bound(variable)) + } + + /// Returns the truth value of the provided [`Predicate`]. + /// + /// If the [`Predicate`] is assigned in the current [`State`] then [`Some`] containing whether + /// the [`Predicate`] is satisfied or falsified is returned. Otherwise, [`None`] is returned. + pub fn truth_value(&self, predicate: Predicate) -> Option { + self.assignments.evaluate_predicate(predicate) + } + + /// If the provided [`Predicate`] is satisfied then it returns [`Some`] containing the + /// checkpoint at which the [`Predicate`] became satisfied. Otherwise, [`None`] is returned. + pub fn get_checkpoint_for_predicate(&self, predicate: Predicate) -> Option { + self.assignments.get_checkpoint_for_predicate(&predicate) + } + + /// Returns the truth value of the provided [`Literal`]. + /// + /// If the [`Literal`] is assigned in the current [`State`] then [`Some`] containing whether + /// the [`Literal`] is satisfied or falsified is returned. Otherwise, [`None`] is returned. + pub fn get_literal_value(&self, literal: Literal) -> Option { + self.truth_value(literal.get_true_predicate()) + } + + /// Returns the number of created checkpoints. + pub fn get_checkpoint(&self) -> usize { + self.assignments.get_checkpoint() + } +} + +/// Operations for retrieving information about trail +impl State { + /// Returns the length of the trail. + pub(crate) fn trail_len(&self) -> usize { + self.assignments.num_trail_entries() + } + + /// Returns the [`Predicate`] at the provided `trail_index`. + pub(crate) fn trail_entry(&self, trail_index: usize) -> ConstraintProgrammingTrailEntry { + self.assignments.get_trail_entry(trail_index) + } +} + +/// Operations for adding constraints. +impl State { + /// Enqueues the propagator with [`PropagatorHandle`] `handle` for propagation. + #[deprecated] + pub(crate) fn enqueue_propagator(&mut self, handle: PropagatorHandle

) { + let priority = self.propagators[handle.propagator_id()].priority(); + self.propagator_queue + .enqueue_propagator(handle.propagator_id(), priority); + } + + /// Add a new propagator to the [`State`]. The constructor for that propagator should + /// subscribe to the appropriate domain events so that the propagator is called when + /// necessary. + /// + /// While the propagator is added to the queue for propagation, this function does _not_ + /// trigger a round of propagation. An explicit call to [`State::propagate_to_fixed_point`] is + /// necessary to run the new propagator for the first time. + #[allow(private_bounds, reason = "Propagator will be part of public API")] + #[allow(private_interfaces, reason = "Constructor will be part of public API")] + pub fn add_propagator( + &mut self, + constructor: Constructor, + ) -> PropagatorHandle + where + Constructor: PropagatorConstructor, + Constructor::PropagatorImpl: 'static, + { + let original_handle: PropagatorHandle = + self.propagators.new_propagator().key(); + let constructor_context = + PropagatorConstructorContext::new(original_handle.propagator_id(), self); + let propagator = constructor.create(constructor_context); + + pumpkin_assert_simple!( + propagator.priority() <= 3, + "The propagator priority exceeds 3. + Currently we only support values up to 3, + but this can easily be changed if there is a good reason." + ); + + let slot = self.propagators.new_propagator(); + let handle = slot.populate(propagator); + + pumpkin_assert_eq_simple!(handle.propagator_id(), original_handle.propagator_id()); + + #[allow(deprecated, reason = "Will be refactored")] + self.enqueue_propagator(handle); + + handle + } +} + +/// Operations for retrieving propagators. +impl State { + /// Get a reference to the propagator identified by the given handle. + /// + /// For an exclusive reference, use [`State::get_propagator_mut`]. + #[allow( + private_bounds, + reason = "Propagator will be part of public interface in the future" + )] + pub fn get_propagator(&self, handle: PropagatorHandle

) -> Option<&P> { + self.propagators.get_propagator(handle) + } + + /// Get an exclusive reference to the propagator identified by the given handle. + #[allow( + private_bounds, + reason = "Propagator will be part of public interface in the future" + )] + pub fn get_propagator_mut( + &mut self, + handle: PropagatorHandle

, + ) -> Option<&mut P> { + self.propagators.get_propagator_mut(handle) + } + + /// Get an exclusive reference to the propagator identified by the given handle and a context + /// which can be used for propagation. + pub(crate) fn get_propagator_mut_with_context( + &mut self, + handle: PropagatorHandle

, + ) -> (Option<&mut P>, PropagationContextMut<'_>) { + ( + self.propagators.get_propagator_mut(handle), + PropagationContextMut::new( + &mut self.trailed_values, + &mut self.assignments, + &mut self.reason_store, + &mut self.notification_engine, + handle.propagator_id(), + ), + ) + } +} + +/// Operations for modifying the state. +impl State { + /// Apply a [`Predicate`] to the [`State`]. + /// + /// Returns `true` if a change to a domain occured, and `false` if the given [`Predicate`] was + /// already true. + /// + /// If a domain becomes empty due to this operation, an [`EmptyDomain`] error is returned. + /// + /// This method does _not_ perform any propagation. For that, an explicit call to + /// [`State::propagate_to_fixed_point`] is required. This allows the + /// posting of multiple predicates before the entire propagation engine is invoked. + /// + /// A call to [`State::restore_to`] that goes past the checkpoint at which a [`Predicate`] + /// was posted will undo the effect of that [`Predicate`]. See the documentation of + /// [`State::new_checkpoint`] and + /// [`State::restore_to`] for more information. + pub fn post(&mut self, predicate: Predicate) -> Result { + self.assignments + .post_predicate(predicate, None, &mut self.notification_engine) + } + + /// Create a checkpoint of the current [`State`], that can be returned to with + /// [`State::restore_to`]. + /// + /// The current checkpoint can be retrieved using the method [`State::get_checkpoint`]. + /// + /// If the state is not at fixed-point, then this method will panic. + /// + /// # Example + /// ``` + /// use pumpkin_core::predicate; + /// use pumpkin_core::state::State; + /// + /// let mut state = State::default(); + /// let variable = state.new_interval_variable(1, 10, Some("x1".into())); + /// + /// assert_eq!(state.get_checkpoint(), 0); + /// + /// state.new_checkpoint(); + /// + /// assert_eq!(state.get_checkpoint(), 1); + /// + /// state + /// .post(predicate![variable <= 5]) + /// .expect("The lower bound is 1 so no conflict"); + /// assert_eq!(state.upper_bound(variable), 5); + /// + /// state.restore_to(0); + /// + /// assert_eq!(state.get_checkpoint(), 0); + /// assert_eq!(state.upper_bound(variable), 10); + /// ``` + pub fn new_checkpoint(&mut self) { + pumpkin_assert_simple!( + self.propagator_queue.is_empty(), + "Can only create a new checkpoint when all propagation has occurred" + ); + self.assignments.new_checkpoint(); + self.notification_engine.new_checkpoint(); + self.trailed_values.new_checkpoint(); + self.reason_store.new_checkpoint(); + } + + /// Restore to the given checkpoint and return the [`DomainId`]s which were fixed before + /// restoring, with their assigned values. + /// + /// If the provided checkpoint is equal to the current checkpoint, this is a no-op. If + /// the provided checkpoint is larger than the current checkpoint, this method will + /// panic. + /// + /// See [`State::new_checkpoint`] for an example. + pub fn restore_to(&mut self, checkpoint: usize) -> Vec<(DomainId, i32)> { + pumpkin_assert_simple!(checkpoint <= self.get_checkpoint()); + + if checkpoint == self.get_checkpoint() { + return vec![]; + } + + let unfixed_after_backtracking = self + .assignments + .synchronise(checkpoint, &mut self.notification_engine); + self.trailed_values.synchronise(checkpoint); + self.reason_store.synchronise(checkpoint); + + self.propagator_queue.clear(); + // For now all propagators are called to synchronise, in the future this will be improved in + // two ways: + // + allow incremental synchronisation + // + only call the subset of propagators that were notified since last backtrack + for propagator in self.propagators.iter_propagators_mut() { + let context = PropagationContext::new(&self.assignments); + propagator.synchronise(context); + } + + let _ = self + .notification_engine + .process_backtrack_events(&mut self.assignments, &mut self.propagators); + self.notification_engine.clear_event_drain(); + + self.notification_engine + .update_last_notified_index(&mut self.assignments); + // Should be done after the assignments and trailed values have been synchronised + self.notification_engine.synchronise( + checkpoint, + &self.assignments, + &mut self.trailed_values, + ); + + unfixed_after_backtracking + } + + /// Performs a single call to [`Propagator::propagate`] for the propagator with the provided + /// [`PropagatorId`]. + /// + /// Other propagators could be enqueued as a result of the changes made by the propagated + /// propagator but a call to [`State::propagate_to_fixed_point`] is + /// required for further propagation to occur. + /// + /// It could be that the current [`State`] implies a conflict by propagation. In that case, an + /// [`Err`] with [`Conflict`] is returned. + /// + /// Once the [`State`] is conflicting, then the only operation that is defined is + /// [`State::restore_to`]. All other operations and queries on the state are undetermined. + fn propagate(&mut self, propagator_id: PropagatorId) -> Result<(), Conflict> { + self.statistics.num_propagators_called += 1; + + let num_trail_entries_before = self.assignments.num_trail_entries(); + + let propagation_status = { + let propagator = &mut self.propagators[propagator_id]; + let context = PropagationContextMut::new( + &mut self.trailed_values, + &mut self.assignments, + &mut self.reason_store, + &mut self.notification_engine, + propagator_id, + ); + propagator.propagate(context) + }; + + match propagation_status { + Ok(_) => { + // Notify other propagators of the propagations and continue. + self.notification_engine + .notify_propagators_about_domain_events( + &mut self.assignments, + &mut self.trailed_values, + &mut self.propagators, + PropagatorHandle::new(PropagatorId(0)), + &mut self.propagator_queue, + ); + pumpkin_assert_extreme!( + DebugHelper::debug_check_propagations( + num_trail_entries_before, + propagator_id, + &self.trailed_values, + &self.assignments, + &mut self.reason_store, + &mut self.propagators, + &self.notification_engine + ), + "Checking the propagations performed by the propagator led to inconsistencies!" + ); + } + Err(conflict) => { + self.statistics.num_conflicts += 1; + if let Conflict::Propagator(inner) = &conflict { + pumpkin_assert_advanced!(DebugHelper::debug_reported_failure( + &self.trailed_values, + &self.assignments, + &inner.conjunction, + &self.propagators[propagator_id], + propagator_id, + &self.notification_engine + )); + } + + return Err(conflict); + } + } + Ok(()) + } + + /// Performs fixed-point propagation using the propagators defined in the [`State`]. + /// + /// The posted [`Predicate`]s (using [`State::post`]) and added propagators (using + /// [`State::add_propagator`]) cause propagators to be enqueued when the events that + /// they have subscribed to are triggered. As propagation causes more changes to be made, + /// more propagators are enqueued. This continues until applying all (enqueued) + /// propagators leads to no more domain changes. + /// + /// It could be that the current [`State`] implies a conflict by propagation. In that case, an + /// error with [`Conflict`] is returned. + /// + /// Once the [`State`] is conflicting, then the only operation that is defined is + /// [`State::restore_to`]. All other operations and queries on the state are unspecified. + pub fn propagate_to_fixed_point(&mut self) -> Result<(), Conflict> { + // The initial domain events are due to the decision predicate. + self.notification_engine + .notify_propagators_about_domain_events( + &mut self.assignments, + &mut self.trailed_values, + &mut self.propagators, + PropagatorHandle::new(PropagatorId(0)), + &mut self.propagator_queue, + ); + + // Keep propagating until there are unprocessed propagators, or a conflict is detected. + while let Some(propagator_id) = self.propagator_queue.pop() { + self.propagate(propagator_id)?; + } + + // 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( + &self.trailed_values, + &self.assignments, + &self.propagators, + &self.notification_engine + )); + + Ok(()) + } +} + +impl State { + /// This is a temporary accessor to help refactoring. + pub(crate) fn get_solution_reference(&self) -> SolutionReference<'_> { + SolutionReference::new(&self.assignments) + } + + /// Returns a mapping of [`DomainId`] to variable name. + pub(crate) fn variable_names(&self) -> &VariableNames { + &self.variable_names + } + + pub(crate) fn get_propagation_reason_trail_entry( + &mut self, + trail_position: usize, + reason_buffer: &mut (impl Extend + AsRef<[Predicate]>), + ) { + let entry = self.trail_entry(trail_position); + let (reason_ref, _) = entry + .reason + .expect("Added by a propagator and must therefore have a reason"); + let _ = self.reason_store.get_or_compute( + reason_ref, + ExplanationContext::without_working_nogood( + &self.assignments, + trail_position, + &mut self.notification_engine, + ), + &mut self.propagators, + reason_buffer, + ); + } + /// Get the reason for a predicate being true and store it in `reason_buffer`; additionally, if + /// the provided [`Predicate`] is explicitly on the trail, this method will return the + /// corresponding trail index. + /// + /// The provided `current_nogood` can be used by the propagator to provide a different reason; + /// use [`CurrentNogood::empty`] otherwise. + /// + /// All the predicates in the returned slice will evaluate to `true`. + /// + /// If the provided predicate is not true, then this method will panic. + #[allow(unused, reason = "Will be part of public API")] + pub fn get_propagation_reason( + &mut self, + predicate: Predicate, + reason_buffer: &mut (impl Extend + AsRef<[Predicate]>), + current_nogood: CurrentNogood<'_>, + ) -> Option { + // TODO: this function could be put into the reason store + + // Note that this function can only be called with propagations, and never decision + // predicates. Furthermore only predicate from the current checkpoint will be + // considered. This is due to how the 1uip conflict analysis works: it scans the + // predicates in reverse order of assignment, and stops as soon as there is only one + // predicate from the current checkpoint in the learned nogood. + + // This means that the procedure would never ask for the reason of the decision predicate + // from the current checkpoint, because that would mean that all other predicates from + // the current checkpoint have been removed from the nogood, and the decision + // predicate is the only one left, but in that case, the 1uip would terminate since + // there would be only one predicate from the current checkpoint. For this + // reason, it is safe to assume that in the following, that any input predicate is + // indeed a propagated predicate. + if self.assignments.is_initial_bound(predicate) { + return None; + } + + let trail_position = self + .assignments + .get_trail_position(&predicate) + .unwrap_or_else(|| panic!("The predicate {predicate:?} must be true during conflict analysis. Bounds were {},{}", self.lower_bound(predicate.get_domain()), self.upper_bound(predicate.get_domain()))); + + let trail_entry = self.assignments.get_trail_entry(trail_position); + + // We distinguish between three cases: + // 1) The predicate is explicitly present on the trail. + if trail_entry.predicate == predicate { + let (reason_ref, inference_code) = trail_entry + .reason + .expect("Cannot be a null reason for propagation."); + + let explanation_context = ExplanationContext::new( + &self.assignments, + current_nogood, + trail_position, + &mut self.notification_engine, + ); + + let reason_exists = self.reason_store.get_or_compute( + reason_ref, + explanation_context, + &mut self.propagators, + reason_buffer, + ); + + assert!(reason_exists, "reason reference should not be stale"); + + Some(trail_position) + } + // 2) The predicate is true due to a propagation, and not explicitly on the trail. + // It is necessary to further analyse what was the reason for setting the predicate true. + else { + // The reason for propagation depends on: + // 1) The predicate on the trail at the moment the input predicate became true, and + // 2) The input predicate. + match ( + trail_entry.predicate.get_predicate_type(), + predicate.get_predicate_type(), + ) { + (PredicateType::LowerBound, PredicateType::LowerBound) => { + let trail_lower_bound = trail_entry.predicate.get_right_hand_side(); + let domain_id = predicate.get_domain(); + let input_lower_bound = predicate.get_right_hand_side(); + // Both the input predicate and the trail predicate are lower bound + // literals. Two cases to consider: + // 1) The trail predicate has a greater right-hand side, meaning + // the reason for the input predicate is true is because a stronger + // right-hand side predicate was posted. We can reuse the same + // reason as for the trail bound. + // todo: could consider lifting here, since the trail bound + // might be too strong. + if trail_lower_bound > input_lower_bound { + reason_buffer.extend(std::iter::once(trail_entry.predicate)); + } + // Otherwise, the input bound is strictly greater than the trailed + // bound. This means the reason is due to holes in the domain. + else { + // Note that the bounds cannot be equal. + // If the bound were equal, the predicate would be explicitly on the + // trail, so we would have detected this case earlier. + pumpkin_assert_simple!(trail_lower_bound < input_lower_bound); + + // The reason for the propagation of the input predicate [x >= a] is + // because [x >= a-1] & [x != a]. Conflict analysis will then + // recursively decompose these further. + + // Note that we do not need to worry about decreasing the lower + // bounds so much so that it reaches its root lower bound, for which + // there is no reason since it is given as input to the problem. + // We cannot reach the original lower bound since in the 1uip, we + // only look for reasons for predicates from the current decision + // level, and we never look for reasons at the root level. + + let one_less_bound_predicate = + predicate!(domain_id >= input_lower_bound - 1); + + let not_equals_predicate = predicate!(domain_id != input_lower_bound - 1); + reason_buffer.extend(std::iter::once(one_less_bound_predicate)); + reason_buffer.extend(std::iter::once(not_equals_predicate)); + } + } + (PredicateType::LowerBound, PredicateType::NotEqual) => { + let trail_lower_bound = trail_entry.predicate.get_right_hand_side(); + let not_equal_constant = predicate.get_right_hand_side(); + // The trail entry is a lower bound literal, + // and the input predicate is a not equals. + // Only one case to consider: + // The trail lower bound is greater than the not_equals_constant, + // so it safe to take the reason from the trail. + // todo: lifting could be used here + pumpkin_assert_simple!(trail_lower_bound > not_equal_constant); + reason_buffer.extend(std::iter::once(trail_entry.predicate)); + } + (PredicateType::LowerBound, PredicateType::Equal) => { + let domain_id = predicate.get_domain(); + let equality_constant = predicate.get_right_hand_side(); + // The input predicate is an equality predicate, and the trail predicate + // is a lower bound predicate. This means that the time of posting the + // trail predicate is when the input predicate became true. + + // Note that the input equality constant does _not_ necessarily equal + // the trail lower bound. This would be the + // case when the the trail lower bound is lower than the input equality + // constant, but due to holes in the domain, the lower bound got raised + // to just the value of the equality constant. + // For example, {1, 2, 3, 10}, then posting [x >= 5] will raise the + // lower bound to x >= 10. + + let predicate_lb = predicate!(domain_id >= equality_constant); + let predicate_ub = predicate!(domain_id <= equality_constant); + reason_buffer.extend(std::iter::once(predicate_lb)); + reason_buffer.extend(std::iter::once(predicate_ub)); + } + (PredicateType::UpperBound, PredicateType::UpperBound) => { + let trail_upper_bound = trail_entry.predicate.get_right_hand_side(); + let domain_id = predicate.get_domain(); + let input_upper_bound = predicate.get_right_hand_side(); + // Both the input and trail predicates are upper bound predicates. + // There are two scenarios to consider: + // 1) The input upper bound is greater than the trail upper bound, meaning that + // the reason for the input predicate is the propagation of a stronger upper + // bound. We can safely use the reason for of the trail predicate as the + // reason for the input predicate. + // todo: lifting could be applied here. + if trail_upper_bound < input_upper_bound { + reason_buffer.extend(std::iter::once(trail_entry.predicate)); + } else { + // I think it cannot be that the bounds are equal, since otherwise we + // would have found the predicate explicitly on the trail. + pumpkin_assert_simple!(trail_upper_bound > input_upper_bound); + + // The input upper bound is greater than the trail predicate, meaning + // that holes in the domain also played a rule in lowering the upper + // bound. + + // The reason of the input predicate [x <= a] is computed recursively as + // the reason for [x <= a + 1] & [x != a + 1]. + + let new_ub_predicate = predicate!(domain_id <= input_upper_bound + 1); + let not_equal_predicate = predicate!(domain_id != input_upper_bound + 1); + reason_buffer.extend(std::iter::once(new_ub_predicate)); + reason_buffer.extend(std::iter::once(not_equal_predicate)); + } + } + (PredicateType::UpperBound, PredicateType::NotEqual) => { + let trail_upper_bound = trail_entry.predicate.get_right_hand_side(); + let not_equal_constant = predicate.get_right_hand_side(); + // The input predicate is a not equal predicate, and the trail predicate is + // an upper bound predicate. This is only possible when the upper bound was + // pushed below the not equals value. Otherwise the hole would have been + // explicitly placed on the trail and we would have found it earlier. + pumpkin_assert_simple!(not_equal_constant > trail_upper_bound); + + // The bound was set past the not equals, so we can safely returns the trail + // reason. todo: can do lifting here. + reason_buffer.extend(std::iter::once(trail_entry.predicate)); + } + (PredicateType::UpperBound, PredicateType::Equal) => { + let domain_id = predicate.get_domain(); + let equality_constant = predicate.get_right_hand_side(); + // The input predicate is an equality predicate, and the trail predicate + // is an upper bound predicate. This means that the time of posting the + // trail predicate is when the input predicate became true. + + // Note that the input equality constant does _not_ necessarily equal + // the trail upper bound. This would be the + // case when the the trail upper bound is greater than the input equality + // constant, but due to holes in the domain, the upper bound got lowered + // to just the value of the equality constant. + // For example, x = {1, 2, 3, 8, 15}, setting [x <= 12] would lower the + // upper bound to x <= 8. + + // Note that it could be that one of the two predicates are decision + // predicates, so we need to use the substitute functions. + + let predicate_lb = predicate!(domain_id >= equality_constant); + let predicate_ub = predicate!(domain_id <= equality_constant); + reason_buffer.extend(std::iter::once(predicate_lb)); + reason_buffer.extend(std::iter::once(predicate_ub)); + } + (PredicateType::NotEqual, PredicateType::LowerBound) => { + let not_equal_constant = trail_entry.predicate.get_right_hand_side(); + let domain_id = predicate.get_domain(); + let input_lower_bound = predicate.get_right_hand_side(); + // The trail predicate is not equals, but the input predicate is a lower + // bound predicate. This means that creating the hole in the domain resulted + // in raising the lower bound. + + // I think this holds. The not_equals_constant cannot be greater, since that + // would not impact the lower bound. It can also not be the same, since + // creating a hole cannot result in the lower bound being raised to the + // hole, there must be some other reason for that to happen, which we would + // find earlier. + pumpkin_assert_simple!(input_lower_bound > not_equal_constant); + + // The reason for the input predicate [x >= a] is computed recursively as + // the reason for [x >= a - 1] & [x != a - 1]. + let new_lb_predicate = predicate!(domain_id >= input_lower_bound - 1); + let new_not_equals_predicate = predicate!(domain_id != input_lower_bound - 1); + + reason_buffer.extend(std::iter::once(new_lb_predicate)); + reason_buffer.extend(std::iter::once(new_not_equals_predicate)); + } + (PredicateType::NotEqual, PredicateType::UpperBound) => { + let not_equal_constant = trail_entry.predicate.get_right_hand_side(); + let domain_id = predicate.get_domain(); + let input_upper_bound = predicate.get_right_hand_side(); + // The trail predicate is not equals, but the input predicate is an upper + // bound predicate. This means that creating the hole in the domain resulted + // in lower the upper bound. + + // I think this holds. The not_equals_constant cannot be smaller, since that + // would not impact the upper bound. It can also not be the same, since + // creating a hole cannot result in the upper bound being lower to the + // hole, there must be some other reason for that to happen, which we would + // find earlier. + pumpkin_assert_simple!(input_upper_bound < not_equal_constant); + + // The reason for the input predicate [x <= a] is computed recursively as + // the reason for [x <= a + 1] & [x != a + 1]. + let new_ub_predicate = predicate!(domain_id <= input_upper_bound + 1); + let new_not_equals_predicate = predicate!(domain_id != input_upper_bound + 1); + + reason_buffer.extend(std::iter::once(new_ub_predicate)); + reason_buffer.extend(std::iter::once(new_not_equals_predicate)); + } + (PredicateType::NotEqual, PredicateType::Equal) => { + let domain_id = predicate.get_domain(); + let equality_constant = predicate.get_right_hand_side(); + // The trail predicate is not equals, but the input predicate is + // equals. The only time this could is when the not equals forces the + // lower/upper bounds to meet. So we simply look for the reasons for those + // bounds recursively. + + // Note that it could be that one of the two predicates are decision + // predicates, so we need to use the substitute functions. + + let predicate_lb = predicate!(domain_id >= equality_constant); + let predicate_ub = predicate!(domain_id <= equality_constant); + + reason_buffer.extend(std::iter::once(predicate_lb)); + reason_buffer.extend(std::iter::once(predicate_ub)); + } + ( + PredicateType::Equal, + PredicateType::LowerBound | PredicateType::UpperBound | PredicateType::NotEqual, + ) => { + // The trail predicate is equality, but the input predicate is either a + // lower-bound, upper-bound, or not equals. + // + // TODO: could consider lifting here + reason_buffer.extend(std::iter::once(trail_entry.predicate)) + } + _ => unreachable!( + "Unreachable combination of {} and {}", + trail_entry.predicate, predicate + ), + }; + None + } + } +} diff --git a/pumpkin-crates/core/src/engine/variable_names.rs b/pumpkin-crates/core/src/engine/variable_names.rs index 5c98f646f..035583404 100644 --- a/pumpkin-crates/core/src/engine/variable_names.rs +++ b/pumpkin-crates/core/src/engine/variable_names.rs @@ -1,21 +1,22 @@ +use std::sync::Arc; + use crate::containers::HashMap; use crate::engine::variables::DomainId; -#[derive(Debug, Default)] - +#[derive(Debug, Default, Clone)] pub(crate) struct VariableNames { - integers: HashMap, + integers: HashMap>, } impl VariableNames { /// Get the name associated with a domain id. pub(crate) fn get_int_name(&self, domain_id: DomainId) -> Option<&str> { - self.integers.get(&domain_id).map(|s| s.as_str()) + self.integers.get(&domain_id).map(|s| s.as_ref()) } /// Add a name to the integer variable. This will override existing the name if it /// exists. - pub(crate) fn add_integer(&mut self, integer: DomainId, name: String) { + pub(crate) fn add_integer(&mut self, integer: DomainId, name: Arc) { let _ = self.integers.insert(integer, name); } } diff --git a/pumpkin-crates/core/src/engine/variables/affine_view.rs b/pumpkin-crates/core/src/engine/variables/affine_view.rs index cee0f9460..aa60c4836 100644 --- a/pumpkin-crates/core/src/engine/variables/affine_view.rs +++ b/pumpkin-crates/core/src/engine/variables/affine_view.rs @@ -166,12 +166,12 @@ where } } - fn get_holes_on_current_decision_level( + fn get_holes_at_current_checkpoint( &self, assignments: &Assignments, ) -> impl Iterator { self.inner - .get_holes_on_current_decision_level(assignments) + .get_holes_at_current_checkpoint(assignments) .map(|value| self.map(value)) } diff --git a/pumpkin-crates/core/src/engine/variables/domain_id.rs b/pumpkin-crates/core/src/engine/variables/domain_id.rs index 3f5c05c7a..53014e6d2 100644 --- a/pumpkin-crates/core/src/engine/variables/domain_id.rs +++ b/pumpkin-crates/core/src/engine/variables/domain_id.rs @@ -84,11 +84,11 @@ impl IntegerVariable for DomainId { event.unwrap() } - fn get_holes_on_current_decision_level( + fn get_holes_at_current_checkpoint( &self, assignments: &Assignments, ) -> impl Iterator { - assignments.get_holes_on_current_decision_level(*self) + assignments.get_holes_at_current_checkpoint(*self) } fn get_holes(&self, assignments: &Assignments) -> impl Iterator { diff --git a/pumpkin-crates/core/src/engine/variables/integer_variable.rs b/pumpkin-crates/core/src/engine/variables/integer_variable.rs index e65da8c52..61f4791d7 100644 --- a/pumpkin-crates/core/src/engine/variables/integer_variable.rs +++ b/pumpkin-crates/core/src/engine/variables/integer_variable.rs @@ -53,7 +53,7 @@ pub trait IntegerVariable: fn unpack_event(&self, event: OpaqueDomainEvent) -> DomainEvent; /// Returns all of the holes in the domain which were created at the current decision level - fn get_holes_on_current_decision_level( + fn get_holes_at_current_checkpoint( &self, assignments: &Assignments, ) -> impl Iterator; diff --git a/pumpkin-crates/core/src/engine/variables/literal.rs b/pumpkin-crates/core/src/engine/variables/literal.rs index 15cb2a619..6ecee24b9 100644 --- a/pumpkin-crates/core/src/engine/variables/literal.rs +++ b/pumpkin-crates/core/src/engine/variables/literal.rs @@ -123,12 +123,12 @@ impl IntegerVariable for Literal { self.integer_variable.watch_all_backtrack(watchers, events) } - fn get_holes_on_current_decision_level( + fn get_holes_at_current_checkpoint( &self, assignments: &Assignments, ) -> impl Iterator { self.integer_variable - .get_holes_on_current_decision_level(assignments) + .get_holes_at_current_checkpoint(assignments) } fn get_holes(&self, assignments: &Assignments) -> impl Iterator { diff --git a/pumpkin-crates/core/src/lib.rs b/pumpkin-crates/core/src/lib.rs index f1df88a72..1e0107a3d 100644 --- a/pumpkin-crates/core/src/lib.rs +++ b/pumpkin-crates/core/src/lib.rs @@ -33,7 +33,6 @@ mod api; pub use api::*; pub use crate::api::solver::DefaultBrancher; -pub use crate::api::solver::PropagatorHandle; pub use crate::api::solver::Solver; pub use crate::basic_types::ConstraintOperationError; pub use crate::basic_types::Duration; diff --git a/pumpkin-crates/core/src/proof/finalizer.rs b/pumpkin-crates/core/src/proof/finalizer.rs index 25d70dca5..7115c90f8 100644 --- a/pumpkin-crates/core/src/proof/finalizer.rs +++ b/pumpkin-crates/core/src/proof/finalizer.rs @@ -5,25 +5,17 @@ use super::InferenceCode; use super::ProofLog; use crate::containers::HashMap; -use crate::engine::Assignments; -use crate::engine::VariableNames; +use crate::engine::State; use crate::engine::conflict_analysis::ConflictAnalysisContext; -use crate::engine::notifications::NotificationEngine; use crate::engine::propagation::CurrentNogood; -use crate::engine::propagation::store::PropagatorStore; -use crate::engine::reason::ReasonStore; use crate::predicates::Predicate; use crate::predicates::PropositionalConjunction; pub(crate) struct FinalizingContext<'a> { pub(crate) conflict: PropositionalConjunction, - pub(crate) propagators: &'a mut PropagatorStore, pub(crate) proof_log: &'a mut ProofLog, pub(crate) unit_nogood_inference_codes: &'a HashMap, - pub(crate) assignments: &'a Assignments, - pub(crate) reason_store: &'a mut ReasonStore, - pub(crate) notification_engine: &'a mut NotificationEngine, - pub(crate) variable_names: &'a VariableNames, + pub(crate) state: &'a mut State, } /// Finalizes the proof by introducing inferences used to derive root-level unsatisfiability. This @@ -40,13 +32,9 @@ pub(crate) fn finalize_proof(context: FinalizingContext<'_>) { .flat_map(|predicate| { get_required_assumptions( &mut RootExplanationContext { - propagators: context.propagators, proof_log: context.proof_log, unit_nogood_inference_codes: context.unit_nogood_inference_codes, - assignments: context.assignments, - reason_store: context.reason_store, - notification_engine: context.notification_engine, - variable_names: context.variable_names, + state: context.state, }, predicate, ) @@ -55,17 +43,13 @@ pub(crate) fn finalize_proof(context: FinalizingContext<'_>) { let _ = context .proof_log - .log_deduction(final_nogood, context.variable_names); + .log_deduction(final_nogood, context.state.variable_names()); } pub(crate) struct RootExplanationContext<'a> { - pub(crate) propagators: &'a mut PropagatorStore, pub(crate) proof_log: &'a mut ProofLog, pub(crate) unit_nogood_inference_codes: &'a HashMap, - pub(crate) assignments: &'a Assignments, - pub(crate) reason_store: &'a mut ReasonStore, - pub(crate) notification_engine: &'a mut NotificationEngine, - pub(crate) variable_names: &'a VariableNames, + pub(crate) state: &'a mut State, } /// Explain why a given predicate is true. We assume that `predicate` is true at the root. @@ -74,9 +58,7 @@ pub(crate) fn explain_root_assignment( predicate: Predicate, ) { assert_eq!( - context - .assignments - .get_decision_level_for_predicate(&predicate), + context.state.get_checkpoint_for_predicate(predicate), Some(0) ); @@ -98,25 +80,26 @@ fn get_required_assumptions( context: &mut RootExplanationContext<'_>, predicate: Predicate, ) -> Vec { - if context.assignments.is_decision_predicate(&predicate) { + if context.state.assignments.is_decision_predicate(&predicate) { return vec![predicate]; } // If the predicate is a root-level assignment, add the appropriate inference to the proof. - if context.assignments.is_initial_bound(predicate) { + if context.state.assignments.is_initial_bound(predicate) { let _ = context .proof_log - .log_domain_inference(predicate, context.variable_names); + .log_domain_inference(predicate, context.state.variable_names()); return vec![]; } // If the predicate is a unit-nogood, we explain the root-level assignment. if let Some(inference_code) = context.unit_nogood_inference_codes.get(&predicate) { let _ = context.proof_log.log_inference( + &context.state.inference_codes, *inference_code, [], Some(predicate), - context.variable_names, + context.state.variable_names(), ); return vec![]; } @@ -125,15 +108,11 @@ fn get_required_assumptions( let mut reason = vec![]; ConflictAnalysisContext::get_propagation_reason( predicate, - context.assignments, CurrentNogood::empty(), - context.reason_store, - context.propagators, context.proof_log, context.unit_nogood_inference_codes, &mut reason, - context.notification_engine, - context.variable_names, + context.state, ); // Here we combine all the required assumptions of recursive reasons. diff --git a/pumpkin-crates/core/src/proof/mod.rs b/pumpkin-crates/core/src/proof/mod.rs index a1a858ad4..2c7095825 100644 --- a/pumpkin-crates/core/src/proof/mod.rs +++ b/pumpkin-crates/core/src/proof/mod.rs @@ -64,7 +64,6 @@ impl ProofLog { writer, propagation_order_hint: if log_hints { Some(vec![]) } else { None }, logged_domain_inferences: HashMap::default(), - inference_codes: KeyedVec::default(), proof_atomics: ProofAtomics::default(), constraint_tags: KeyGenerator::default(), }), @@ -82,6 +81,7 @@ impl ProofLog { /// Log an inference to the proof. pub(crate) fn log_inference( &mut self, + inference_codes: &KeyedVec)>, inference_code: InferenceCode, premises: impl IntoIterator, propagated: Option, @@ -90,7 +90,6 @@ impl ProofLog { let Some(ProofImpl::CpProof { writer, propagation_order_hint: Some(propagation_sequence), - inference_codes, constraint_tags, proof_atomics, .. @@ -292,23 +291,6 @@ impl ProofLog { proof_atomics.reify_predicate(literal, predicate); } - /// Create a new [`InferenceCode`] for a [`ConstraintTag`] and [`InferenceLabel`] combination. - /// The inference codes are required to log inferences with [`Self::log_inference`]. - pub(crate) fn create_inference_code( - &mut self, - constraint_tag: ConstraintTag, - inference_label: impl InferenceLabel, - ) -> InferenceCode { - match &mut self.internal_proof { - Some(ProofImpl::CpProof { - inference_codes, .. - }) => inference_codes.push((constraint_tag, inference_label.to_str())), - - // If we are not logging a CP proof, then we do not care about this value. - _ => InferenceCode::create_from_index(0), - } - } - /// Create a new constraint tag. pub(crate) fn new_constraint_tag(&mut self) -> ConstraintTag { match self.internal_proof { @@ -363,7 +345,6 @@ impl Write for Sink { enum ProofImpl { CpProof { writer: ProofWriter, - inference_codes: KeyedVec)>, /// The [`ConstraintTag`]s generated for this proof. constraint_tags: KeyGenerator, // If propagation hints are enabled, this is a buffer used to record propagations in the diff --git a/pumpkin-crates/core/src/propagators/arithmetic/binary/binary_equals.rs b/pumpkin-crates/core/src/propagators/arithmetic/binary/binary_equals.rs index 4123be82d..eb977d8d2 100644 --- a/pumpkin-crates/core/src/propagators/arithmetic/binary/binary_equals.rs +++ b/pumpkin-crates/core/src/propagators/arithmetic/binary/binary_equals.rs @@ -10,7 +10,7 @@ use crate::conjunction; use crate::containers::HashSet; use crate::declare_inference_label; use crate::engine::DomainEvents; -use crate::engine::EmptyDomain; +use crate::engine::EmptyDomainConflict; use crate::engine::cp::propagation::ReadDomains; use crate::engine::notifications::DomainEvent; use crate::engine::notifications::OpaqueDomainEvent; @@ -120,7 +120,7 @@ where variable: Variable, predicate_type: PredicateType, value: i32, - ) -> Result<(), EmptyDomain> { + ) -> Result<(), EmptyDomainConflict> { use PredicateType::*; use Variable::*; @@ -195,7 +195,7 @@ where // If it is a removal then we need to make sure that all of the removed values // from `a` are also removed from `b` self.a_removed_values - .extend(context.get_holes_on_current_decision_level(&self.a)); + .extend(context.get_holes_at_current_checkpoint(&self.a)); } } 1 => { @@ -203,7 +203,7 @@ where // If it is a removal then we need to make sure that all of the removed values // from `b` are also removed from `a` self.b_removed_values - .extend(context.get_holes_on_current_decision_level(&self.b)); + .extend(context.get_holes_at_current_checkpoint(&self.b)); } } _ => panic!("Unexpected local id {local_id:?}"), diff --git a/pumpkin-crates/core/src/propagators/arithmetic/binary/binary_not_equals.rs b/pumpkin-crates/core/src/propagators/arithmetic/binary/binary_not_equals.rs index 1283e4c3f..ed28c28b8 100644 --- a/pumpkin-crates/core/src/propagators/arithmetic/binary/binary_not_equals.rs +++ b/pumpkin-crates/core/src/propagators/arithmetic/binary/binary_not_equals.rs @@ -230,7 +230,7 @@ mod tests { solver.assert_bounds(b, 1, 10); - solver.increase_decision_level(); + solver.new_checkpoint(); let should_enqueue = solver.decrease_upper_bound_and_notify(propagator, 1, b, 5); assert_eq!(should_enqueue, EnqueueDecision::Skip); diff --git a/pumpkin-crates/core/src/propagators/arithmetic/linear_not_equal.rs b/pumpkin-crates/core/src/propagators/arithmetic/linear_not_equal.rs index ecaa6b67f..a63908f3c 100644 --- a/pumpkin-crates/core/src/propagators/arithmetic/linear_not_equal.rs +++ b/pumpkin-crates/core/src/propagators/arithmetic/linear_not_equal.rs @@ -372,10 +372,10 @@ impl LinearNotEqualPropagator { #[cfg(test)] mod tests { use super::*; - use crate::basic_types::Inconsistency; use crate::conjunction; use crate::engine::test_solver::TestSolver; use crate::engine::variables::TransformableVariable; + use crate::state::Conflict; #[test] fn test_value_is_removed() { @@ -419,8 +419,8 @@ mod tests { let expected = conjunction!([x == 2] & [y == 2]); match err { - Inconsistency::EmptyDomain => panic!("expected an explicit conflict"), - Inconsistency::Conflict(conflict) => assert_eq!(expected, conflict.conjunction), + Conflict::EmptyDomain(_) => panic!("expected an explicit conflict"), + Conflict::Propagator(conflict) => assert_eq!(expected, conflict.conjunction), } } diff --git a/pumpkin-crates/core/src/propagators/arithmetic/maximum.rs b/pumpkin-crates/core/src/propagators/arithmetic/maximum.rs index 2089a6c86..13c65efed 100644 --- a/pumpkin-crates/core/src/propagators/arithmetic/maximum.rs +++ b/pumpkin-crates/core/src/propagators/arithmetic/maximum.rs @@ -149,7 +149,7 @@ impl Prop break; } } else { - propagation_reason.add(predicate![var <= rhs_lb - 1]); + propagation_reason.push(predicate![var <= rhs_lb - 1]); } } // If there is exactly one variable UB(a_i) >= LB(rhs, constraint_tag }, then the @@ -159,7 +159,7 @@ impl Prop if let Some(propagating_variable) = propagating_variable { let var_lb = context.lower_bound(propagating_variable); if var_lb < rhs_lb { - propagation_reason.add(predicate![self.rhs >= rhs_lb]); + propagation_reason.push(predicate![self.rhs >= rhs_lb]); context.post( predicate![propagating_variable >= rhs_lb], propagation_reason, diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/mod.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/mod.rs index be2b113e2..902beb439 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/mod.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/mod.rs @@ -100,7 +100,7 @@ pub(crate) fn add_propagating_task_predicate_lower_bound, time_point: Option, ) -> PropositionalConjunction { - explanation.add(create_predicate_propagating_task_lower_bound_propagation( + explanation.push(create_predicate_propagating_task_lower_bound_propagation( explanation_type, context, task, @@ -144,7 +144,7 @@ pub(crate) fn add_propagating_task_predicate_upper_bound, time_point: Option, ) -> PropositionalConjunction { - explanation.add(create_predicate_propagating_task_upper_bound_propagation( + explanation.push(create_predicate_propagating_task_upper_bound_propagation( explanation_type, context, task, diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/pointwise.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/pointwise.rs index 2348a9117..0b728c1bd 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/pointwise.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/explanations/pointwise.rs @@ -1,7 +1,7 @@ use std::rc::Rc; use crate::constraint_arguments::CumulativeExplanationType; -use crate::engine::EmptyDomain; +use crate::engine::EmptyDomainConflict; use crate::engine::propagation::PropagationContextMut; use crate::engine::propagation::ReadDomains; use crate::engine::propagation::contexts::propagation_context::HasAssignments; @@ -22,7 +22,7 @@ pub(crate) fn propagate_lower_bounds_with_pointwise_explanations], propagating_task: &Rc>, inference_code: InferenceCode, -) -> Result<(), EmptyDomain> { +) -> Result<(), EmptyDomainConflict> { // The time points should follow the following properties (based on `Improving // scheduling by learning - Andreas Schutt`): // 1. `t_0 = lb(s)` @@ -131,7 +131,7 @@ pub(crate) fn propagate_upper_bounds_with_pointwise_explanations], propagating_task: &Rc>, inference_code: InferenceCode, -) -> Result<(), EmptyDomain> { +) -> Result<(), EmptyDomainConflict> { // The time points should follow the following properties (based on `Improving // scheduling by learning - Andreas Schutt`): // 1. `t_0 = ub(s) + p` diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/synchronisation.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/synchronisation.rs index fa7dd3aa6..1da409f59 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/synchronisation.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/synchronisation.rs @@ -2,7 +2,6 @@ use std::rc::Rc; use super::debug::are_mergeable; use super::debug::merge_profiles; -use crate::basic_types::Inconsistency; use crate::basic_types::PropagationStatusCP; use crate::engine::propagation::PropagationContext; use crate::engine::propagation::ReadDomains; @@ -14,6 +13,7 @@ use crate::propagators::ResourceProfile; use crate::propagators::TimeTableOverIntervalPropagator; use crate::propagators::create_time_table_over_interval_from_scratch; use crate::propagators::cumulative::time_table::propagation_handler::create_conflict_explanation; +use crate::state::Conflict; use crate::variables::IntegerVariable; /// Finds the conflicting profile which would have been found by the @@ -64,7 +64,7 @@ pub(crate) fn check_synchronisation_conflict_explanation_over_interval< let error_from_scratch = create_time_table_over_interval_from_scratch(context, parameters, inference_code); if let Err(explanation_scratch) = error_from_scratch { - if let Err(Inconsistency::Conflict(explanation)) = &synchronised_conflict_explanation { + if let Err(Conflict::Propagator(explanation)) = &synchronised_conflict_explanation { // We check whether both inconsistencies are of the same type and then we check their // corresponding explanations explanation.conjunction == explanation_scratch.conjunction diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs index 671f56de6..372708cd0 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs @@ -4,7 +4,6 @@ use std::rc::Rc; use super::insertion; use super::removal; -use crate::basic_types::Inconsistency; use crate::basic_types::PropagationStatusCP; use crate::basic_types::PropagatorConflict; use crate::conjunction; @@ -53,6 +52,7 @@ use crate::propagators::UpdatableStructures; use crate::pumpkin_assert_advanced; use crate::pumpkin_assert_extreme; use crate::pumpkin_assert_simple; +use crate::state::Conflict; /// [`Propagator`] responsible for using time-table reasoning to propagate the [Cumulative](https://sofdem.github.io/gccat/gccat/Ccumulative.html) constraint /// where a time-table is a structure which stores the mandatory resource usage of the tasks at @@ -386,7 +386,7 @@ impl Propagator ); if self.parameters.is_infeasible { - return Err(Inconsistency::Conflict(PropagatorConflict { + return Err(Conflict::Propagator(PropagatorConflict { conjunction: conjunction!(), inference_code: self.inference_code.unwrap(), })); @@ -624,7 +624,6 @@ fn find_overlapping_profile( #[cfg(test)] mod tests { - use crate::basic_types::Inconsistency; use crate::conjunction; use crate::engine::predicates::predicate::Predicate; use crate::engine::propagation::EnqueueDecision; @@ -634,6 +633,7 @@ mod tests { use crate::propagators::CumulativeExplanationType; use crate::propagators::CumulativePropagatorOptions; use crate::propagators::TimeTableOverIntervalIncrementalPropagator; + use crate::state::Conflict; use crate::variables::DomainId; #[test] @@ -705,9 +705,9 @@ mod tests { constraint_tag, )); - assert!(matches!(result, Err(Inconsistency::Conflict(_)))); + assert!(matches!(result, Err(Conflict::Propagator(_)))); assert!(match result { - Err(Inconsistency::Conflict(conflict)) => { + Err(Conflict::Propagator(conflict)) => { let expected = [ predicate!(s1 <= 1), predicate!(s1 >= 1), diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs index 5dd863117..048ef6533 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs @@ -1,6 +1,5 @@ use std::rc::Rc; -use crate::basic_types::Inconsistency; use crate::basic_types::PropagationStatusCP; use crate::engine::propagation::PropagationContext; use crate::proof::InferenceCode; @@ -11,6 +10,7 @@ use crate::propagators::Task; use crate::propagators::create_time_table_per_point_from_scratch; use crate::propagators::cumulative::time_table::propagation_handler::create_conflict_explanation; use crate::pumpkin_assert_moderate; +use crate::state::Conflict; use crate::variables::IntegerVariable; /// Returns whether the synchronised conflict explanation created by @@ -27,7 +27,7 @@ pub(crate) fn check_synchronisation_conflict_explanation_per_point< let error_from_scratch = create_time_table_per_point_from_scratch(context, inference_code, parameters); if let Err(explanation_scratch) = error_from_scratch { - if let Err(Inconsistency::Conflict(conflict)) = &synchronised_conflict_explanation { + if let Err(Conflict::Propagator(conflict)) = &synchronised_conflict_explanation { // We check whether both inconsistencies are of the same type and then we check their // corresponding explanations conflict.conjunction == explanation_scratch.conjunction diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs index 183ced768..a98ae5839 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs @@ -3,7 +3,6 @@ use std::collections::btree_map::Entry; use std::fmt::Debug; use std::rc::Rc; -use crate::basic_types::Inconsistency; use crate::basic_types::PropagationStatusCP; use crate::basic_types::PropagatorConflict; use crate::conjunction; @@ -48,6 +47,7 @@ use crate::propagators::util::register_tasks; use crate::propagators::util::update_bounds_task; use crate::pumpkin_assert_advanced; use crate::pumpkin_assert_extreme; +use crate::state::Conflict; /// [`Propagator`] responsible for using time-table reasoning to propagate the [Cumulative](https://sofdem.github.io/gccat/gccat/Ccumulative.html) constraint /// where a time-table is a structure which stores the mandatory resource usage of the tasks at @@ -68,7 +68,7 @@ use crate::pumpkin_assert_extreme; /// /// \[1\] A. Schutt, Improving scheduling by learning. University of Melbourne, Department of /// Computer Science and Software Engineering, 2011. -#[derive(Debug)] +#[derive(Debug, Clone)] pub(crate) struct TimeTablePerPointIncrementalPropagator { /// The key `t` (representing a time-point) holds the mandatory resource consumption of @@ -415,7 +415,7 @@ impl Propagator ); if self.parameters.is_infeasible { - return Err(Inconsistency::Conflict(PropagatorConflict { + return Err(Conflict::Propagator(PropagatorConflict { conjunction: conjunction!(), inference_code: self.inference_code.unwrap(), })); @@ -621,7 +621,6 @@ mod debug { #[cfg(test)] mod tests { - use crate::basic_types::Inconsistency; use crate::conjunction; use crate::engine::predicates::predicate::Predicate; use crate::engine::propagation::EnqueueDecision; @@ -633,6 +632,7 @@ mod tests { use crate::propagators::CumulativePropagatorOptions; use crate::propagators::TimeTablePerPointIncrementalPropagator; use crate::propagators::TimeTablePerPointPropagator; + use crate::state::Conflict; use crate::variables::DomainId; #[test] @@ -703,7 +703,7 @@ mod tests { ), ); assert!(match result { - Err(Inconsistency::Conflict(x)) => { + Err(Conflict::Propagator(x)) => { let expected = [ predicate!(s1 <= 1), predicate!(s1 >= 1), @@ -1302,8 +1302,8 @@ mod tests { let result = solver.propagate(propagator); assert!( { - if let Err(Inconsistency::Conflict(conflict)) = &result { - if let Err(Inconsistency::Conflict(explanation_scratch)) = &result_scratch { + if let Err(Conflict::Propagator(conflict)) = &result { + if let Err(Conflict::Propagator(explanation_scratch)) = &result_scratch { conflict.conjunction.iter().collect::>() == explanation_scratch.conjunction.iter().collect::>() } else { @@ -1401,8 +1401,8 @@ mod tests { let result_scratch = solver_scratch.propagate(propagator_scratch); assert!(result_scratch.is_err()); assert!({ - if let Err(Inconsistency::Conflict(explanation)) = &result { - if let Err(Inconsistency::Conflict(explanation_scratch)) = &result_scratch { + if let Err(Conflict::Propagator(explanation)) = &result { + if let Err(Conflict::Propagator(explanation_scratch)) = &result_scratch { explanation.conjunction.iter().collect::>() == explanation_scratch.conjunction.iter().collect::>() } else { @@ -1496,8 +1496,8 @@ mod tests { let result = solver.propagate(propagator); let result_scratch = solver_scratch.propagate(propagator_scratch); assert!({ - if let Err(Inconsistency::Conflict(explanation)) = &result { - if let Err(Inconsistency::Conflict(explanation_scratch)) = &result_scratch { + if let Err(Conflict::Propagator(explanation)) = &result { + if let Err(Conflict::Propagator(explanation_scratch)) = &result_scratch { explanation.conjunction.iter().collect::>() != explanation_scratch.conjunction.iter().collect::>() } else { @@ -1793,8 +1793,8 @@ mod tests { let result = solver.propagate(propagator); assert!(result.is_err()); if let ( - Err(Inconsistency::Conflict(explanation)), - Err(Inconsistency::Conflict(explanation_scratch)), + Err(Conflict::Propagator(explanation)), + Err(Conflict::Propagator(explanation_scratch)), ) = (result, result_scratch) { assert_ne!(explanation, explanation_scratch); @@ -1907,8 +1907,8 @@ mod tests { let result = solver.propagate(propagator); assert!(result.is_err()); if let ( - Err(Inconsistency::Conflict(explanation)), - Err(Inconsistency::Conflict(explanation_scratch)), + Err(Conflict::Propagator(explanation)), + Err(Conflict::Propagator(explanation_scratch)), ) = (result, result_scratch) { assert_eq!( diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/propagation_handler.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/propagation_handler.rs index e490b14ed..f378c2c29 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/propagation_handler.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/propagation_handler.rs @@ -15,7 +15,7 @@ use super::explanations::naive::create_naive_propagation_explanation; use super::explanations::pointwise::create_pointwise_conflict_explanation; use super::explanations::pointwise::create_pointwise_propagation_explanation; use crate::basic_types::PropagatorConflict; -use crate::engine::EmptyDomain; +use crate::engine::EmptyDomainConflict; use crate::engine::propagation::PropagationContext; use crate::engine::propagation::PropagationContextMut; use crate::engine::propagation::ReadDomains; @@ -57,9 +57,9 @@ fn check_explanation( let at_least_one_element_from_current_level = explanation.iter().any(|&predicate| { context .assignments() - .get_decision_level_for_predicate(&predicate) + .get_checkpoint_for_predicate(&predicate) .unwrap() - == context.assignments().get_decision_level() + == context.assignments().get_checkpoint() }); if !at_least_one_element_from_current_level { eprintln!( @@ -89,7 +89,7 @@ impl CumulativePropagationHandler { context: &mut PropagationContextMut, profiles: &[&ResourceProfile], propagating_task: &Rc>, - ) -> Result<(), EmptyDomain> + ) -> Result<(), EmptyDomainConflict> where Var: IntegerVariable + 'static, { @@ -154,7 +154,7 @@ impl CumulativePropagationHandler { context: &mut PropagationContextMut, profiles: &[&ResourceProfile], propagating_task: &Rc>, - ) -> Result<(), EmptyDomain> + ) -> Result<(), EmptyDomainConflict> where Var: IntegerVariable + 'static, { @@ -219,7 +219,7 @@ impl CumulativePropagationHandler { context: &mut PropagationContextMut, profile: &ResourceProfile, propagating_task: &Rc>, - ) -> Result<(), EmptyDomain> + ) -> Result<(), EmptyDomainConflict> where Var: IntegerVariable + 'static, { @@ -250,7 +250,7 @@ impl CumulativePropagationHandler { )); let mut reason = (*explanation).clone(); - reason.add(lower_bound_predicate_propagating_task); + reason.push(lower_bound_predicate_propagating_task); context.post(predicate, reason, self.inference_code) } CumulativeExplanationType::Pointwise => { @@ -270,7 +270,7 @@ impl CumulativePropagationHandler { context: &mut PropagationContextMut, profile: &ResourceProfile, propagating_task: &Rc>, - ) -> Result<(), EmptyDomain> + ) -> Result<(), EmptyDomainConflict> where Var: IntegerVariable + 'static, { @@ -305,7 +305,7 @@ impl CumulativePropagationHandler { )); let mut reason = (*explanation).clone(); - reason.add(upper_bound_predicate_propagating_task); + reason.push(upper_bound_predicate_propagating_task); context.post(predicate, reason, self.inference_code) } CumulativeExplanationType::Pointwise => { @@ -326,7 +326,7 @@ impl CumulativePropagationHandler { context: &mut PropagationContextMut, profile: &ResourceProfile, propagating_task: &Rc>, - ) -> Result<(), EmptyDomain> + ) -> Result<(), EmptyDomainConflict> where Var: IntegerVariable + 'static, { @@ -485,7 +485,6 @@ pub(crate) mod test_propagation_handler { use crate::containers::StorageKey; use crate::engine::Assignments; use crate::engine::TrailedValues; - use crate::engine::conflict_analysis::SemanticMinimiser; use crate::engine::notifications::NotificationEngine; use crate::engine::propagation::ExplanationContext; use crate::engine::propagation::LocalId; @@ -594,7 +593,6 @@ pub(crate) mod test_propagation_handler { &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, - &mut SemanticMinimiser::default(), &mut self.notification_engine, PropagatorId(0), ), @@ -659,7 +657,6 @@ pub(crate) mod test_propagation_handler { &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, - &mut SemanticMinimiser::default(), &mut self.notification_engine, PropagatorId(0), ), @@ -710,7 +707,6 @@ pub(crate) mod test_propagation_handler { &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, - &mut SemanticMinimiser::default(), &mut self.notification_engine, PropagatorId(0), ), @@ -775,7 +771,6 @@ pub(crate) mod test_propagation_handler { &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, - &mut SemanticMinimiser::default(), &mut self.notification_engine, PropagatorId(0), ), diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_over_interval.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_over_interval.rs index b3141d9ec..7be88a250 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_over_interval.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_over_interval.rs @@ -3,7 +3,6 @@ use std::rc::Rc; use super::TimeTable; use super::time_table_util::propagate_based_on_timetable; use super::time_table_util::should_enqueue; -use crate::basic_types::Inconsistency; use crate::basic_types::PropagationStatusCP; use crate::basic_types::PropagatorConflict; use crate::conjunction; @@ -36,6 +35,7 @@ use crate::propagators::util::update_bounds_task; use crate::pumpkin_assert_extreme; use crate::pumpkin_assert_moderate; use crate::pumpkin_assert_simple; +use crate::state::Conflict; /// An event storing the start and end of mandatory parts used for creating the time-table #[derive(Debug)] @@ -59,7 +59,7 @@ pub(crate) struct Event { /// /// \[1\] A. Schutt, Improving scheduling by learning. University of Melbourne, Department of /// Computer Science and Software Engineering, 2011. -#[derive(Debug)] +#[derive(Debug, Clone)] pub(crate) struct TimeTableOverIntervalPropagator { /// Stores whether the time-table is empty is_time_table_empty: bool, @@ -119,7 +119,7 @@ impl PropagatorConstructor impl Propagator for TimeTableOverIntervalPropagator { fn propagate(&mut self, mut context: PropagationContextMut) -> PropagationStatusCP { if self.parameters.is_infeasible { - return Err(Inconsistency::Conflict(PropagatorConflict { + return Err(Conflict::Propagator(PropagatorConflict { conjunction: conjunction!(), inference_code: self.inference_code.unwrap(), })); @@ -213,7 +213,7 @@ impl Propagator for TimeTableOverIntervalPropaga /// /// The result of this method is either the time-table of type /// [`OverIntervalTimeTableType`] or the tasks responsible for the -/// conflict in the form of an [`Inconsistency`]. +/// conflict in the form of an [`PropagatorConflict`]. pub(crate) fn create_time_table_over_interval_from_scratch< Var: IntegerVariable + 'static, Context: ReadDomains + Copy, @@ -474,7 +474,6 @@ pub(crate) fn debug_propagate_from_scratch_time_table_interval { match e { - Inconsistency::EmptyDomain => false, - Inconsistency::Conflict(x) => { + Conflict::EmptyDomain(_) => false, + Conflict::Propagator(x) => { let expected = [ predicate!(s1 <= 1), predicate!(s1 >= 1), diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_per_point.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_per_point.rs index 62c87c32d..ca7a42353 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_per_point.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/time_table_per_point.rs @@ -8,7 +8,6 @@ use std::rc::Rc; use super::TimeTable; use super::time_table_util::propagate_based_on_timetable; use super::time_table_util::should_enqueue; -use crate::basic_types::Inconsistency; use crate::basic_types::PropagationStatusCP; use crate::basic_types::PropagatorConflict; use crate::conjunction; @@ -36,6 +35,7 @@ use crate::propagators::util::create_tasks; use crate::propagators::util::register_tasks; use crate::propagators::util::update_bounds_task; use crate::pumpkin_assert_extreme; +use crate::state::Conflict; /// [`Propagator`] responsible for using time-table reasoning to propagate the [Cumulative](https://sofdem.github.io/gccat/gccat/Ccumulative.html) constraint /// where a time-table is a structure which stores the mandatory resource usage of the tasks at @@ -49,8 +49,7 @@ use crate::pumpkin_assert_extreme; /// /// \[1\] A. Schutt, Improving scheduling by learning. University of Melbourne, Department of /// Computer Science and Software Engineering, 2011. -#[derive(Debug)] - +#[derive(Debug, Clone)] pub(crate) struct TimeTablePerPointPropagator { /// Stores whether the time-table is empty is_time_table_empty: bool, @@ -111,7 +110,7 @@ impl PropagatorConstructor for TimeTablePerPoint impl Propagator for TimeTablePerPointPropagator { fn propagate(&mut self, mut context: PropagationContextMut) -> PropagationStatusCP { if self.parameters.is_infeasible { - return Err(Inconsistency::Conflict(PropagatorConflict { + return Err(Conflict::Propagator(PropagatorConflict { conjunction: conjunction!(), inference_code: self.inference_code.unwrap(), })); @@ -205,7 +204,7 @@ impl Propagator for TimeTablePerPointPropagator< /// /// The result of this method is either the time-table of type /// [`PerPointTimeTableType`] or the tasks responsible for the -/// conflict in the form of an [`Inconsistency`]. +/// conflict in the form of an [`PropagatorConflict`]. pub(crate) fn create_time_table_per_point_from_scratch< Var: IntegerVariable + 'static, Context: ReadDomains + Copy, @@ -279,7 +278,6 @@ pub(crate) fn debug_propagate_from_scratch_time_table_point match e { - Inconsistency::EmptyDomain => false, - Inconsistency::Conflict(x) => { + Conflict::EmptyDomain(_) => false, + Conflict::Propagator(x) => { let expected = [ predicate!(s1 <= 1), predicate!(s1 >= 1), diff --git a/pumpkin-crates/core/src/propagators/disjunctive/disjunctive_propagator.rs b/pumpkin-crates/core/src/propagators/disjunctive/disjunctive_propagator.rs index 1cd9e32ae..3f535962b 100644 --- a/pumpkin-crates/core/src/propagators/disjunctive/disjunctive_propagator.rs +++ b/pumpkin-crates/core/src/propagators/disjunctive/disjunctive_propagator.rs @@ -4,7 +4,6 @@ use std::cmp::min; use super::disjunctive_task::ArgDisjunctiveTask; use super::disjunctive_task::DisjunctiveTask; use super::theta_lambda_tree::ThetaLambdaTree; -use crate::basic_types::Inconsistency; use crate::basic_types::PropagationStatusCP; use crate::basic_types::PropagatorConflict; use crate::containers::StorageKey; @@ -21,6 +20,7 @@ use crate::proof::ConstraintTag; use crate::proof::InferenceCode; use crate::propagators::disjunctive::DisjunctiveEdgeFinding; use crate::pumpkin_assert_simple; +use crate::state::Conflict; use crate::variables::IntegerVariable; /// [`Propagator`] responsible for using disjunctive reasoning to propagate the [Disjunctive](https://sofdem.github.io/gccat/gccat/Cdisjunctive.html) constraint. @@ -41,6 +41,7 @@ use crate::variables::IntegerVariable; /// Sciences, vol. 18, no. 2, pp. 159–202, 2008. /// - \[2\] R. A. Vasile, ‘Evaluating the Impact of Explanations on the Performance of an /// Edge-Finding Propagator’. +#[derive(Debug, Clone)] pub(crate) struct DisjunctivePropagator { /// The tasks which serve as the input to the disjunctive constraint tasks: Box<[DisjunctiveTask]>, @@ -167,7 +168,7 @@ fn edge_finding( // (which takes into account `j`) is larger than the LCT of `j` then we can report an // overflow if theta_lambda_tree.ect() > lct_j { - return Err(Inconsistency::Conflict(PropagatorConflict { + return Err(Conflict::Propagator(PropagatorConflict { conjunction: create_conflict_explanation(theta_lambda_tree, context, lct_j), inference_code, })); diff --git a/pumpkin-crates/core/src/propagators/disjunctive/theta_lambda_tree.rs b/pumpkin-crates/core/src/propagators/disjunctive/theta_lambda_tree.rs index 442674b00..7e9fd87fa 100644 --- a/pumpkin-crates/core/src/propagators/disjunctive/theta_lambda_tree.rs +++ b/pumpkin-crates/core/src/propagators/disjunctive/theta_lambda_tree.rs @@ -419,13 +419,16 @@ mod tests { let mut tree = ThetaLambdaTree::new(&tasks); tree.update(PropagationContext { - assignments: &solver.assignments, + assignments: &solver.state.assignments, }); for task in tasks.iter() { - tree.add_to_theta(task, PropagationContext::new(&solver.assignments)); + tree.add_to_theta(task, PropagationContext::new(&solver.state.assignments)); } tree.remove_from_theta(&tasks[2]); - tree.add_to_lambda(&tasks[2], PropagationContext::new(&solver.assignments)); + tree.add_to_lambda( + &tasks[2], + PropagationContext::new(&solver.state.assignments), + ); assert_eq!( tree.nodes[6], diff --git a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs index 4cbc3a49f..2fe6f0745 100644 --- a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs +++ b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs @@ -6,8 +6,6 @@ use log::warn; use super::LearningOptions; use super::NogoodId; use super::NogoodInfo; -use crate::PropagatorHandle; -use crate::basic_types::Inconsistency; use crate::basic_types::PredicateId; use crate::basic_types::PropagationStatusCP; use crate::basic_types::PropagatorConflict; @@ -19,7 +17,6 @@ use crate::engine::Assignments; use crate::engine::Lbd; use crate::engine::SolverStatistics; use crate::engine::TrailedValues; -use crate::engine::conflict_analysis::Mode; use crate::engine::notifications::NotificationEngine; use crate::engine::predicates::predicate::Predicate; use crate::engine::propagation::ExplanationContext; @@ -40,6 +37,8 @@ use crate::pumpkin_assert_advanced; use crate::pumpkin_assert_extreme; use crate::pumpkin_assert_moderate; use crate::pumpkin_assert_simple; +use crate::state::Conflict; +use crate::state::PropagatorHandle; /// A propagator which propagates nogoods (i.e. a list of [`Predicate`]s which cannot all be true /// at the same time). @@ -82,6 +81,44 @@ pub(crate) struct NogoodPropagator { handle: PropagatorHandle, } +/// [`PropagatorConstructor`] for constructing a new instance of the [`NogoodPropagator`] with the +/// provided [`LearningOptions`] and `capacity`. +pub(crate) struct NogoodPropagatorConstructor { + /// How many [`PredicateId`]s to preallocate to the [`ArenaAllocator`]. + capacity: usize, + parameters: LearningOptions, +} + +impl NogoodPropagatorConstructor { + pub(crate) fn new(capacity: usize, parameters: LearningOptions) -> Self { + Self { + capacity, + parameters, + } + } +} + +impl PropagatorConstructor for NogoodPropagatorConstructor { + type PropagatorImpl = NogoodPropagator; + + fn create(self, context: PropagatorConstructorContext) -> Self::PropagatorImpl { + NogoodPropagator { + handle: PropagatorHandle::new(context.propagator_id), + parameters: self.parameters, + nogood_predicates: ArenaAllocator::new(self.capacity), + nogood_info: Default::default(), + inference_codes: Default::default(), + permanent_nogood_ids: Default::default(), + learned_nogood_ids: Default::default(), + watch_lists: Default::default(), + updated_predicate_ids: Default::default(), + lbd_helper: Default::default(), + bumped_nogoods: Default::default(), + temp_nogood_reason: Default::default(), + } + } +} + /// Watcher for a single nogood. /// /// A watcher is a combination of a nogood ID and a cached predicate. If the nogood has a predicate @@ -119,34 +156,6 @@ struct LearnedNogoodIds { } impl NogoodPropagator { - /// Creates a new instance of the [`NogoodPropagator`] with the provided [`LearningOptions`] - /// and `capacity`. - /// - /// The `handle` should be the handle of the propagator used in the solver. - /// - /// The `capacity` indicates how many [`PredicateId`]s to preallocate to the - /// [`ArenaAllocator`]. - pub(crate) fn with_options( - handle: PropagatorHandle, - capacity: usize, - parameters: LearningOptions, - ) -> Self { - Self { - handle, - parameters, - nogood_predicates: ArenaAllocator::new(capacity), - nogood_info: Default::default(), - inference_codes: Default::default(), - permanent_nogood_ids: Default::default(), - learned_nogood_ids: Default::default(), - watch_lists: Default::default(), - updated_predicate_ids: Default::default(), - lbd_helper: Default::default(), - bumped_nogoods: Default::default(), - temp_nogood_reason: Default::default(), - } - } - /// Determines whether the nogood (pointed to by `id`) is propagating using the following /// reasoning: /// @@ -197,7 +206,7 @@ impl Propagator for NogoodPropagator { self.updated_predicate_ids.push(predicate_id); } - fn propagate(&mut self, mut context: PropagationContextMut) -> Result<(), Inconsistency> { + fn propagate(&mut self, mut context: PropagationContextMut) -> Result<(), Conflict> { pumpkin_assert_advanced!(self.debug_is_properly_watched()); // First we perform nogood management to ensure that the database does not grow excessively @@ -327,7 +336,7 @@ impl Propagator for NogoodPropagator { fn debug_propagate_from_scratch( &self, mut context: PropagationContextMut, - ) -> Result<(), Inconsistency> { + ) -> Result<(), Conflict> { // Very inefficient version! // The algorithm goes through every nogood explicitly @@ -426,7 +435,7 @@ impl NogoodPropagator { // root-level; this is essentially the same as adding a predicate at the root level if nogood.len() == 1 { pumpkin_assert_moderate!( - context.get_decision_level() == 0, + context.get_checkpoint() == 0, "A unit nogood should have backtracked to the root-level" ); self.add_permanent_nogood(nogood, inference_code, context) @@ -524,7 +533,7 @@ impl NogoodPropagator { context: &mut PropagationContextMut, ) -> PropagationStatusCP { pumpkin_assert_simple!( - context.get_decision_level() == 0, + context.get_checkpoint() == 0, "Only allowed to add nogoods permanently at the root for now." ); @@ -817,12 +826,12 @@ impl NogoodPropagator { let watcher2 = notification_engine.get_predicate(nogood[1]); assignments.is_predicate_falsified(watcher1) && assignments - .get_decision_level_for_predicate(&!watcher1) + .get_checkpoint_for_predicate(&!watcher1) .expect("Falsified predicates must have a decision level.") == 0 || assignments.is_predicate_falsified(watcher2) && assignments - .get_decision_level_for_predicate(&!watcher2) + .get_checkpoint_for_predicate(&!watcher2) .expect("Falsified predicates must have a decision level.") == 0 } @@ -889,7 +898,7 @@ impl NogoodPropagator { else if notification_engine .is_predicate_id_falsified(watcher.cached_predicate, assignments) && assignments - .get_decision_level_for_predicate( + .get_checkpoint_for_predicate( &!notification_engine.get_predicate(watcher.cached_predicate), ) .expect("Falsified predicates must have a decision level.") @@ -983,9 +992,7 @@ impl NogoodPropagator { id, notification_engine, ) && assignments - .get_decision_level_for_predicate( - &!notification_engine.get_predicate(nogoods[id][0]), - ) + .get_checkpoint_for_predicate(&!notification_engine.get_predicate(nogoods[id][0])) .expect("A propagating predicate must have a decision level.") > 0 { @@ -1112,7 +1119,7 @@ impl NogoodPropagator { /// to the empty nogood. /// 4. Conflicting predicates? fn preprocess_nogood(nogood: &mut Vec, context: &mut PropagationContextMut) { - pumpkin_assert_simple!(context.get_decision_level() == 0); + pumpkin_assert_simple!(context.get_checkpoint() == 0); // The code below is broken down into several parts // We opt for semantic minimisation upfront. This way we avoid the possibility of having @@ -1120,14 +1127,6 @@ impl NogoodPropagator { // change since the initial time the semantic minimiser recorded it, so it would not know // that a previously nonroot bound is now actually a root bound. - // Semantic minimisation will take care of removing duplicate predicates, conflicting - // nogoods, and may result in few predicates since it removes redundancies. - *nogood = context.semantic_minimiser.minimise( - nogood, - context.assignments, - Mode::EnableEqualityMerging, - ); - // Check if the nogood cannot be violated, i.e., it has a falsified predicate. if nogood.is_empty() || nogood.iter().any(|p| context.is_predicate_falsified(*p)) { *nogood = vec![Predicate::trivially_false()]; @@ -1153,7 +1152,7 @@ impl NogoodPropagator { &self, nogood_id: NogoodId, context: &mut PropagationContextMut, - ) -> Result<(), Inconsistency> { + ) -> Result<(), Conflict> { // This is an inefficient implementation for testing purposes let nogood = &self.nogood_predicates[nogood_id]; let info_id = self.nogood_predicates.get_nogood_index(&nogood_id); @@ -1288,9 +1287,7 @@ impl NogoodPropagator { mod tests { use super::NogoodPropagator; use crate::conjunction; - use crate::engine::propagation::PropagationContextMut; use crate::engine::test_solver::TestSolver; - use crate::options::LearningOptions; use crate::predicate; #[test] @@ -1302,44 +1299,30 @@ mod tests { let b = solver.new_variable(-4, 4); let c = solver.new_variable(-10, 20); - let handle = solver - .new_propagator_with_handle(|handle| { - NogoodPropagator::with_options(handle, 10, LearningOptions::default()) - }) - .expect("no empty domains"); + let id = solver.nogood_handle.propagator_id(); - let _ = - solver.increase_lower_bound_and_notify(handle.propagator_id(), dummy.id(), dummy, 1); + let _ = solver.increase_lower_bound_and_notify(id, dummy.id(), dummy, 1); let nogood = conjunction!([a >= 2] & [b >= 1] & [c >= 10]); { - let mut context = PropagationContextMut::new( - &mut solver.trailed_values, - &mut solver.assignments, - &mut solver.reason_store, - &mut solver.semantic_minimiser, - &mut solver.notification_engine, - handle.propagator_id(), - ); + let (nogood_propagator, mut context) = solver + .state + .get_propagator_mut_with_context(solver.nogood_handle); + let nogood_propagator: &mut NogoodPropagator = nogood_propagator.unwrap(); - solver - .propagator_store - .get_propagator_mut(handle) - .unwrap() + nogood_propagator .add_nogood(nogood.into(), inference_code, &mut context) .unwrap(); } - let _ = solver.increase_lower_bound_and_notify(handle.propagator_id(), a.id(), a, 3); - let _ = solver.increase_lower_bound_and_notify(handle.propagator_id(), b.id(), b, 0); + let _ = solver.increase_lower_bound_and_notify(id, a.id(), a, 3); + let _ = solver.increase_lower_bound_and_notify(id, b.id(), b, 0); - solver - .propagate_until_fixed_point(handle.propagator_id()) - .expect(""); + solver.propagate_until_fixed_point(id).expect(""); - let _ = solver.increase_lower_bound_and_notify(handle.propagator_id(), c.id(), c, 15); + let _ = solver.increase_lower_bound_and_notify(id, c.id(), c, 15); - solver.propagate(handle.propagator_id()).expect(""); + solver.propagate(id).expect(""); assert_eq!(solver.upper_bound(b), 0); @@ -1355,36 +1338,25 @@ mod tests { let b = solver.new_variable(-4, 4); let c = solver.new_variable(-10, 20); - let handle = solver - .new_propagator_with_handle(|handle| { - NogoodPropagator::with_options(handle, 10, LearningOptions::default()) - }) - .expect("no empty domains"); + let id = solver.nogood_handle.propagator_id(); let nogood = conjunction!([a >= 2] & [b >= 1] & [c >= 10]); { - let mut context = PropagationContextMut::new( - &mut solver.trailed_values, - &mut solver.assignments, - &mut solver.reason_store, - &mut solver.semantic_minimiser, - &mut solver.notification_engine, - handle.propagator_id(), - ); + let (nogood_propagator, mut context) = solver + .state + .get_propagator_mut_with_context(solver.nogood_handle); + let nogood_propagator: &mut NogoodPropagator = nogood_propagator.unwrap(); - solver - .propagator_store - .get_propagator_mut(handle) - .unwrap() + nogood_propagator .add_nogood(nogood.into(), inference_code, &mut context) .unwrap(); } - let _ = solver.increase_lower_bound_and_notify(handle.propagator_id(), a.id(), a, 3); - let _ = solver.increase_lower_bound_and_notify(handle.propagator_id(), b.id(), b, 1); - let _ = solver.increase_lower_bound_and_notify(handle.propagator_id(), c.id(), c, 15); + let _ = solver.increase_lower_bound_and_notify(id, a.id(), a, 3); + let _ = solver.increase_lower_bound_and_notify(id, b.id(), b, 1); + let _ = solver.increase_lower_bound_and_notify(id, c.id(), c, 15); - let result = solver.propagate_until_fixed_point(handle.propagator_id()); + let result = solver.propagate_until_fixed_point(id); assert!(result.is_err()); } } diff --git a/pumpkin-crates/core/src/propagators/reified_propagator.rs b/pumpkin-crates/core/src/propagators/reified_propagator.rs index 2555459ef..4bb1684c2 100644 --- a/pumpkin-crates/core/src/propagators/reified_propagator.rs +++ b/pumpkin-crates/core/src/propagators/reified_propagator.rs @@ -1,4 +1,3 @@ -use crate::basic_types::Inconsistency; use crate::basic_types::PropagationStatusCP; use crate::engine::DomainEvents; use crate::engine::notifications::OpaqueDomainEvent; @@ -14,6 +13,7 @@ use crate::engine::propagation::constructor::PropagatorConstructorContext; use crate::engine::propagation::contexts::PropagationContextWithTrailedValues; use crate::predicates::Predicate; use crate::pumpkin_assert_simple; +use crate::state::Conflict; use crate::variables::Literal; /// A [`PropagatorConstructor`] for the [`ReifiedPropagator`]. @@ -26,7 +26,7 @@ pub(crate) struct ReifiedPropagatorArgs { impl PropagatorConstructor for ReifiedPropagatorArgs where WrappedArgs: PropagatorConstructor, - WrappedPropagator: Propagator, + WrappedPropagator: Propagator + Clone, { type PropagatorImpl = ReifiedPropagator; @@ -78,7 +78,7 @@ pub(crate) struct ReifiedPropagator { reason_buffer: Vec, } -impl Propagator for ReifiedPropagator { +impl Propagator for ReifiedPropagator { fn notify( &mut self, context: PropagationContextWithTrailedValues, @@ -168,12 +168,12 @@ impl Propagator for ReifiedPropagator ReifiedPropagator { +impl ReifiedPropagator { fn map_propagation_status(&self, mut status: PropagationStatusCP) -> PropagationStatusCP { - if let Err(Inconsistency::Conflict(ref mut conflict)) = status { + if let Err(Conflict::Propagator(ref mut conflict)) = status { conflict .conjunction - .add(self.reification_literal.get_true_predicate()); + .push(self.reification_literal.get_true_predicate()); } status } @@ -231,7 +231,6 @@ impl ReifiedPropagator { #[cfg(test)] mod tests { use super::*; - use crate::basic_types::Inconsistency; use crate::basic_types::PropagatorConflict; use crate::conjunction; use crate::containers::StorageKey; @@ -346,7 +345,7 @@ mod tests { .expect_err("eagerly triggered the conflict"); match inconsistency { - Inconsistency::Conflict(conflict_nogood) => { + Conflict::Propagator(conflict_nogood) => { assert_eq!( conflict_nogood.conjunction, PropositionalConjunction::from(vec![ @@ -393,6 +392,7 @@ mod tests { assert!(matches!(enqueue, EnqueueDecision::Enqueue)) } + #[derive(Clone)] struct GenericPropagator { propagation: Propagation, consistency_check: ConsistencyCheck, @@ -402,9 +402,9 @@ mod tests { impl PropagatorConstructor for GenericPropagator where - Propagation: Fn(PropagationContextMut) -> PropagationStatusCP + 'static, + Propagation: Fn(PropagationContextMut) -> PropagationStatusCP + 'static + Clone, ConsistencyCheck: - Fn(PropagationContextWithTrailedValues) -> Option + 'static, + Fn(PropagationContextWithTrailedValues) -> Option + 'static + Clone, { type PropagatorImpl = Self; @@ -423,9 +423,9 @@ mod tests { impl Propagator for GenericPropagator where - Propagation: Fn(PropagationContextMut) -> PropagationStatusCP + 'static, + Propagation: Fn(PropagationContextMut) -> PropagationStatusCP + 'static + Clone, ConsistencyCheck: - Fn(PropagationContextWithTrailedValues) -> Option + 'static, + Fn(PropagationContextWithTrailedValues) -> Option + 'static + Clone, { fn name(&self) -> &str { "Generic Propagator"