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 14f4643a1..ba47bb7b3 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 @@ -86,7 +86,6 @@ 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, &mut self.state.constraint_tags, conflict.inference_code, conflict.conjunction.iter().copied(), @@ -176,9 +175,8 @@ impl ConflictAnalysisContext<'_> { .expect("Expected to be able to retrieve step id for unit nogood"); let _ = proof_log.log_inference( - &state.inference_codes, &mut state.constraint_tags, - *inference_code, + inference_code.clone(), [], Some(predicate), &state.variable_names, @@ -186,7 +184,6 @@ impl ConflictAnalysisContext<'_> { } else { // Otherwise we log the inference which was used to derive the nogood let _ = proof_log.log_inference( - &state.inference_codes, &mut state.constraint_tags, inference_code, reason_buffer.as_ref().iter().copied(), @@ -221,7 +218,6 @@ impl ConflictAnalysisContext<'_> { // 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, &mut self.state.constraint_tags, conflict.trigger_inference_code, empty_domain_reason.iter().copied(), 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 69ef22095..3c9a77e57 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 @@ -106,14 +106,12 @@ impl ConflictResolver for ResolutionResolver { ) .expect("Failed to write proof log"); - let inference_code = context - .state - .create_inference_code(constraint_tag, NogoodLabel); + let inference_code = InferenceCode::new(constraint_tag, NogoodLabel); if learned_nogood.predicates.len() == 1 { let _ = context .unit_nogood_inference_codes - .insert(!learned_nogood.predicates[0], inference_code); + .insert(!learned_nogood.predicates[0], inference_code.clone()); } context diff --git a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs index 6fcffa158..828ed1de7 100644 --- a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs +++ b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs @@ -833,7 +833,6 @@ impl ConstraintSatisfactionSolver { // 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, &mut self.state.constraint_tags, inference_code, inference_premises, @@ -877,9 +876,7 @@ impl ConstraintSatisfactionSolver { ); if let Ok(constraint_tag) = constraint_tag { - let inference_code = self - .state - .create_inference_code(constraint_tag, NogoodLabel); + let inference_code = InferenceCode::new(constraint_tag, NogoodLabel); let _ = self .unit_nogood_inference_codes @@ -1045,9 +1042,7 @@ impl ConstraintSatisfactionSolver { return Err(ConstraintOperationError::InfeasibleClause); } - let inference_code = self - .state - .create_inference_code(constraint_tag, NogoodLabel); + let inference_code = InferenceCode::new(constraint_tag, NogoodLabel); if let Err(constraint_operation_error) = self.add_nogood(predicates, inference_code) { let _ = self.conclude_proof_unsat(); diff --git a/pumpkin-crates/core/src/engine/cp/assignments.rs b/pumpkin-crates/core/src/engine/cp/assignments.rs index 94fcccc40..8c130849d 100644 --- a/pumpkin-crates/core/src/engine/cp/assignments.rs +++ b/pumpkin-crates/core/src/engine/cp/assignments.rs @@ -82,7 +82,7 @@ impl Assignments { } else { let values_at_current_checkpoint = self.trail.values_at_checkpoint(self.get_checkpoint()); - let entry = values_at_current_checkpoint[0]; + let entry = &values_at_current_checkpoint[0]; pumpkin_assert_eq_simple!(None, entry.reason); Some(entry.predicate) @@ -108,7 +108,9 @@ impl Assignments { } pub(crate) fn get_trail_entry(&self, index: usize) -> ConstraintProgrammingTrailEntry { - self.trail[index] + // The clone is required because of InferenceCode is not copy. However, it is a + // reference-counted type, so cloning is cheap. + self.trail[index].clone() } // registers the domain of a new integer variable @@ -804,7 +806,7 @@ impl Assignments { .iter() .find_map(|entry| { if entry.predicate == predicate { - entry.reason.map(|(reason_ref, _)| reason_ref) + entry.reason.as_ref().map(|(reason_ref, _)| *reason_ref) } else { None } @@ -813,7 +815,7 @@ impl Assignments { } } -#[derive(Clone, Copy, Debug)] +#[derive(Clone, Debug)] pub(crate) struct ConstraintProgrammingTrailEntry { pub predicate: Predicate, /// Explicitly store the bound before the predicate was applied so that it is easier later on diff --git a/pumpkin-crates/core/src/engine/cp/mod.rs b/pumpkin-crates/core/src/engine/cp/mod.rs index e987703a0..2be12ab01 100644 --- a/pumpkin-crates/core/src/engine/cp/mod.rs +++ b/pumpkin-crates/core/src/engine/cp/mod.rs @@ -21,6 +21,7 @@ mod tests { use crate::engine::notifications::NotificationEngine; use crate::engine::reason::ReasonStore; use crate::predicate; + use crate::proof::ConstraintTag; use crate::proof::InferenceCode; use crate::propagation::PropagationContext; use crate::propagation::PropagatorId; @@ -46,7 +47,7 @@ mod tests { let result = context.post( predicate![domain >= 2], conjunction!(), - InferenceCode::create_from_index(0), + &InferenceCode::unknown_label(ConstraintTag::create_from_index(0)), ); assert!(result.is_ok()); } @@ -75,7 +76,7 @@ mod tests { let result = context.post( predicate![domain <= 15], conjunction!(), - InferenceCode::create_from_index(0), + &InferenceCode::unknown_label(ConstraintTag::create_from_index(0)), ); assert!(result.is_ok()); } @@ -104,7 +105,7 @@ mod tests { let result = context.post( predicate![domain != 15], conjunction!(), - InferenceCode::create_from_index(0), + &InferenceCode::unknown_label(ConstraintTag::create_from_index(0)), ); assert!(result.is_ok()); } diff --git a/pumpkin-crates/core/src/engine/cp/test_solver.rs b/pumpkin-crates/core/src/engine/cp/test_solver.rs index 8507c3c26..f7bfaeee1 100644 --- a/pumpkin-crates/core/src/engine/cp/test_solver.rs +++ b/pumpkin-crates/core/src/engine/cp/test_solver.rs @@ -1,7 +1,6 @@ //! 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 crate::containers::KeyGenerator; @@ -15,7 +14,6 @@ use crate::options::LearningOptions; use crate::predicate; use crate::predicates::PropositionalConjunction; use crate::proof::ConstraintTag; -use crate::proof::InferenceCode; use crate::propagation::Domains; use crate::propagation::EnqueueDecision; use crate::propagation::ExplanationContext; @@ -311,15 +309,6 @@ impl TestSolver { self.constraint_tags.next_key() } - pub fn new_inference_code(&mut self) -> InferenceCode { - self.state.inference_codes.push(( - ConstraintTag::from_non_zero( - NonZero::try_from(1 + self.state.inference_codes.len() as u32).unwrap(), - ), - "label".into(), - )) - } - pub fn new_checkpoint(&mut self) { self.state.new_checkpoint(); } diff --git a/pumpkin-crates/core/src/engine/state.rs b/pumpkin-crates/core/src/engine/state.rs index 11b67ab76..2e5b6b936 100644 --- a/pumpkin-crates/core/src/engine/state.rs +++ b/pumpkin-crates/core/src/engine/state.rs @@ -2,7 +2,6 @@ use std::sync::Arc; use crate::basic_types::PropagatorConflict; use crate::containers::KeyGenerator; -use crate::containers::KeyedVec; use crate::create_statistics_struct; use crate::engine::Assignments; use crate::engine::ConstraintProgrammingTrailEntry; @@ -19,7 +18,6 @@ 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::propagation::CurrentNogood; @@ -67,7 +65,6 @@ pub struct State { /// and/or the polarity [Predicate]s pub(crate) notification_engine: NotificationEngine, - pub(crate) inference_codes: KeyedVec)>, /// The [`ConstraintTag`]s generated for this proof. pub(crate) constraint_tags: KeyGenerator, @@ -106,7 +103,7 @@ impl From for Conflict { } /// A conflict because a domain became empty. -#[derive(Clone, Copy, Debug, PartialEq, Eq)] +#[derive(Clone, Debug, PartialEq, Eq)] pub struct EmptyDomainConflict { /// The predicate that caused a domain to become empty. pub trigger_predicate: Predicate, @@ -154,7 +151,6 @@ impl Default for State { propagators: PropagatorStore::default(), reason_store: ReasonStore::default(), notification_engine: NotificationEngine::default(), - inference_codes: KeyedVec::default(), statistics: StateStatistics::default(), constraint_tags: KeyGenerator::default(), }; @@ -197,18 +193,6 @@ impl State { /// 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())) - } - /// Create a new [`ConstraintTag`]. pub fn new_constraint_tag(&mut self) -> ConstraintTag { self.constraint_tags.next_key() diff --git a/pumpkin-crates/core/src/proof/finalizer.rs b/pumpkin-crates/core/src/proof/finalizer.rs index 1006aabd8..9f4687e39 100644 --- a/pumpkin-crates/core/src/proof/finalizer.rs +++ b/pumpkin-crates/core/src/proof/finalizer.rs @@ -99,9 +99,8 @@ fn get_required_assumptions( // 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, &mut context.state.constraint_tags, - *inference_code, + inference_code.clone(), [], Some(predicate), &context.state.variable_names, diff --git a/pumpkin-crates/core/src/proof/inference_code.rs b/pumpkin-crates/core/src/proof/inference_code.rs index 89eef8409..c0f75fdc6 100644 --- a/pumpkin-crates/core/src/proof/inference_code.rs +++ b/pumpkin-crates/core/src/proof/inference_code.rs @@ -46,16 +46,31 @@ impl StorageKey for ConstraintTag { /// An inference code is a combination of a constraint tag with an inference label. Propagators /// associate an inference code with every propagation to identify why that propagation happened /// in terms of the constraint and inference that identified it. -#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] -pub struct InferenceCode(NonZero); +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub struct InferenceCode(ConstraintTag, Arc); -impl StorageKey for InferenceCode { - fn index(&self) -> usize { - self.0.get() as usize - 1 +impl InferenceCode { + /// Create a new inference code from a [`ConstraintTag`] and [`InferenceLabel`]. + pub fn new(tag: ConstraintTag, label: impl InferenceLabel) -> Self { + InferenceCode(tag, label.to_str()) } - fn create_from_index(index: usize) -> Self { - Self(NonZero::new(index as u32 + 1).expect("the '+ 1' ensures the value is non-zero")) + /// Create an inference label with the [`Unknown`] inference label. + /// + /// This should be avoided as much as possible. This is likely only useful for writing unit + /// tests. + pub fn unknown_label(tag: ConstraintTag) -> Self { + InferenceCode::new(tag, Unknown) + } + + /// Get the constraint tag. + pub fn tag(&self) -> ConstraintTag { + self.0 + } + + /// Get the inference label. + pub fn label(&self) -> &str { + self.1.as_ref() } } @@ -75,8 +90,8 @@ impl StorageKey for InferenceCode { /// case. #[macro_export] macro_rules! declare_inference_label { - ($name:ident) => { - declare_inference_label!($name, { + ($v:vis $name:ident) => { + declare_inference_label!($v $name, { let ident_str = stringify!($name); <&str as convert_case::Casing<&str>>::to_case( &ident_str, @@ -125,3 +140,5 @@ pub trait InferenceLabel { /// `Arc`. fn to_str(&self) -> Arc; } + +declare_inference_label!(pub Unknown); diff --git a/pumpkin-crates/core/src/proof/mod.rs b/pumpkin-crates/core/src/proof/mod.rs index 091a660c0..284ac9617 100644 --- a/pumpkin-crates/core/src/proof/mod.rs +++ b/pumpkin-crates/core/src/proof/mod.rs @@ -12,7 +12,6 @@ mod proof_atomics; use std::fs::File; use std::io::Write; use std::path::Path; -use std::sync::Arc; use dimacs::DimacsProof; use drcp_format::Deduction; @@ -26,7 +25,6 @@ use proof_atomics::ProofAtomics; use crate::Solver; use crate::containers::HashMap; use crate::containers::KeyGenerator; -use crate::containers::KeyedVec; use crate::containers::StorageKey; use crate::engine::variable_names::VariableNames; use crate::predicates::Predicate; @@ -80,7 +78,6 @@ impl ProofLog { /// Log an inference to the proof. pub(crate) fn log_inference( &mut self, - inference_codes: &KeyedVec)>, constraint_tags: &mut KeyGenerator, inference_code: InferenceCode, premises: impl IntoIterator, @@ -97,8 +94,6 @@ impl ProofLog { return Ok(ConstraintTag::create_from_index(0)); }; - let (tag, label) = inference_codes[inference_code].clone(); - let inference_tag = constraint_tags.next_key(); let inference = Inference { @@ -110,8 +105,8 @@ impl ProofLog { consequent: propagated.map(|predicate| { proof_atomics.map_predicate_to_proof_atomic(predicate, variable_names) }), - generated_by: Some(tag.into()), - label: Some(label), + generated_by: Some(inference_code.tag().into()), + label: Some(inference_code.label()), }; writer.log_inference(inference)?; diff --git a/pumpkin-crates/core/src/propagation/constructor.rs b/pumpkin-crates/core/src/propagation/constructor.rs index 13b4e0c1f..b6e6652c5 100644 --- a/pumpkin-crates/core/src/propagation/constructor.rs +++ b/pumpkin-crates/core/src/propagation/constructor.rs @@ -18,9 +18,6 @@ use crate::engine::variables::AffineView; #[cfg(doc)] use crate::engine::variables::DomainId; use crate::predicates::Predicate; -use crate::proof::ConstraintTag; -use crate::proof::InferenceCode; -use crate::proof::InferenceLabel; #[cfg(doc)] use crate::propagation::DomainEvent; use crate::propagation::DomainEvents; @@ -157,17 +154,6 @@ impl PropagatorConstructorContext<'_> { var.watch_all_backtrack(&mut watchers, domain_events.events()); } - /// Create a new [`InferenceCode`]. These codes are required to identify specific propagations - /// in the solver and the proof. - pub fn create_inference_code( - &mut self, - constraint_tag: ConstraintTag, - inference_label: impl InferenceLabel, - ) -> InferenceCode { - self.state - .create_inference_code(constraint_tag, inference_label) - } - /// Get a new [`LocalId`] which is guaranteed to be unused. pub(crate) fn get_next_local_id(&self) -> LocalId { *self.next_local_id.deref() diff --git a/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs b/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs index dc9d6571a..c272742e3 100644 --- a/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs +++ b/pumpkin-crates/core/src/propagation/contexts/propagation_context.rs @@ -187,13 +187,13 @@ impl PropagationContext<'_> { &mut self, predicate: Predicate, reason: impl Into, - inference_code: InferenceCode, + inference_code: &InferenceCode, ) -> Result<(), EmptyDomainConflict> { let slot = self.reason_store.new_slot(); let modification_result = self.assignments.post_predicate( predicate, - Some((slot.reason_ref(), inference_code)), + Some((slot.reason_ref(), inference_code.clone())), self.notification_engine, ); diff --git a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs index 674296ad5..9bec2334e 100644 --- a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs +++ b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs @@ -316,7 +316,7 @@ impl Propagator for NogoodPropagator { let result = context.post( predicate, reason, - self.inference_codes + &self.inference_codes [self.nogood_predicates.get_nogood_index(&watcher.nogood_id)], ); // If the propagation lead to a conflict. @@ -491,7 +491,7 @@ impl NogoodPropagator { // asserting nogood such that we can re-create the reason when asked for it let reason = Reason::DynamicLazy(nogood_id.id as u64); let inference_code = - self.inference_codes[self.nogood_predicates.get_nogood_index(&nogood_id)]; + &self.inference_codes[self.nogood_predicates.get_nogood_index(&nogood_id)]; let predicate = !context .notification_engine @@ -613,7 +613,7 @@ impl NogoodPropagator { context.post( !nogood[0], PropositionalConjunction::from(input_nogood), - inference_code, + &inference_code, )?; Ok(()) } @@ -1154,7 +1154,7 @@ impl NogoodPropagator { // 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); - let inference_code = self.inference_codes[info_id]; + let inference_code = &self.inference_codes[info_id]; if self.nogood_info[info_id].is_deleted { // The nogood has already been deleted, meaning that it could be that the call to @@ -1191,7 +1191,7 @@ impl NogoodPropagator { .iter() .map(|predicate_id| context.get_predicate(*predicate_id)) .collect::(), - inference_code, + inference_code: inference_code.clone(), } .into()); } @@ -1286,13 +1286,16 @@ impl NogoodPropagator { mod tests { use super::NogoodPropagator; use crate::conjunction; + use crate::containers::StorageKey; use crate::engine::test_solver::TestSolver; use crate::predicate; + use crate::proof::ConstraintTag; + use crate::proof::InferenceCode; #[test] fn ternary_nogood_propagate() { let mut solver = TestSolver::default(); - let inference_code = solver.new_inference_code(); + let inference_code = InferenceCode::unknown_label(ConstraintTag::create_from_index(0)); let dummy = solver.new_variable(0, 1); let a = solver.new_variable(1, 3); let b = solver.new_variable(-4, 4); @@ -1332,7 +1335,7 @@ mod tests { #[test] fn unsat() { let mut solver = TestSolver::default(); - let inference_code = solver.new_inference_code(); + let inference_code = InferenceCode::unknown_label(ConstraintTag::create_from_index(0)); let a = solver.new_variable(1, 3); let b = solver.new_variable(-4, 4); let c = solver.new_variable(-10, 20); diff --git a/pumpkin-crates/core/src/propagators/reified_propagator.rs b/pumpkin-crates/core/src/propagators/reified_propagator.rs index 2cecbc1a8..8047addb9 100644 --- a/pumpkin-crates/core/src/propagators/reified_propagator.rs +++ b/pumpkin-crates/core/src/propagators/reified_propagator.rs @@ -183,7 +183,7 @@ impl ReifiedPropagator { context.post( self.reification_literal.get_false_predicate(), conflict.conjunction, - conflict.inference_code, + &conflict.inference_code, )?; } @@ -231,6 +231,7 @@ mod tests { use crate::engine::test_solver::TestSolver; use crate::predicate; use crate::predicates::PropositionalConjunction; + use crate::proof::ConstraintTag; use crate::proof::InferenceCode; use crate::variables::DomainId; @@ -246,7 +247,9 @@ mod tests { let t1 = triggered_conflict.clone(); let t2 = triggered_conflict.clone(); - let inference_code = solver.new_inference_code(); + let inference_code = InferenceCode::unknown_label(ConstraintTag::create_from_index(0)); + let i1 = inference_code.clone(); + let i2 = inference_code.clone(); let _ = solver .new_propagator(ReifiedPropagatorArgs { @@ -254,14 +257,14 @@ mod tests { move |_: PropagationContext| { Err(PropagatorConflict { conjunction: t1.clone(), - inference_code, + inference_code: i1.clone(), } .into()) }, move |_: Domains| { Some(PropagatorConflict { conjunction: t2.clone(), - inference_code, + inference_code: i2.clone(), }) }, ), @@ -289,7 +292,7 @@ mod tests { ctx.post( predicate![var >= 3], conjunction!(), - InferenceCode::create_from_index(0), + &InferenceCode::unknown_label(ConstraintTag::create_from_index(0)), )?; Ok(()) }, @@ -320,7 +323,7 @@ mod tests { let _ = solver.set_literal(reification_literal, true); let var = solver.new_variable(1, 1); - let inference_code = solver.new_inference_code(); + let inference_code = InferenceCode::unknown_label(ConstraintTag::create_from_index(0)); let inconsistency = solver .new_propagator(ReifiedPropagatorArgs { @@ -328,7 +331,7 @@ mod tests { move |_: PropagationContext| { Err(PropagatorConflict { conjunction: conjunction!([var >= 1]), - inference_code, + inference_code: inference_code.clone(), } .into()) }, @@ -360,7 +363,7 @@ mod tests { let reification_literal = solver.new_literal(); let var = solver.new_variable(1, 5); - let inference_code = solver.new_inference_code(); + let inference_code = InferenceCode::unknown_label(ConstraintTag::create_from_index(0)); let propagator = solver .new_propagator(ReifiedPropagatorArgs { @@ -370,7 +373,7 @@ mod tests { if context.is_fixed(&var) { Some(PropagatorConflict { conjunction: conjunction!([var == 5]), - inference_code, + inference_code: inference_code.clone(), }) } else { None diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs index 529bfedfc..eac1df128 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs @@ -40,7 +40,7 @@ where context.register(signed.clone(), DomainEvents::BOUNDS, LocalId::from(0)); context.register(absolute.clone(), DomainEvents::BOUNDS, LocalId::from(1)); - let inference_code = context.create_inference_code(constraint_tag, AbsoluteValue); + let inference_code = InferenceCode::new(constraint_tag, AbsoluteValue); AbsoluteValuePropagator { signed, @@ -80,7 +80,7 @@ where context.post( predicate![self.absolute >= 0], conjunction!(), - self.inference_code, + &self.inference_code, )?; // Propagating absolute value can be broken into a few cases: @@ -98,20 +98,20 @@ where context.post( predicate![self.absolute <= signed_absolute_ub], conjunction!([self.signed >= signed_lb] & [self.signed <= signed_ub]), - self.inference_code, + &self.inference_code, )?; if signed_lb > 0 { context.post( predicate![self.absolute >= signed_lb], conjunction!([self.signed >= signed_lb]), - self.inference_code, + &self.inference_code, )?; } else if signed_ub < 0 { context.post( predicate![self.absolute >= signed_ub.abs()], conjunction!([self.signed <= signed_ub]), - self.inference_code, + &self.inference_code, )?; } @@ -120,25 +120,25 @@ where context.post( predicate![self.signed >= -absolute_ub], conjunction!([self.absolute <= absolute_ub]), - self.inference_code, + &self.inference_code, )?; context.post( predicate![self.signed <= absolute_ub], conjunction!([self.absolute <= absolute_ub]), - self.inference_code, + &self.inference_code, )?; if signed_ub <= 0 { context.post( predicate![self.signed <= -absolute_lb], conjunction!([self.signed <= 0] & [self.absolute >= absolute_lb]), - self.inference_code, + &self.inference_code, )?; } else if signed_lb >= 0 { context.post( predicate![self.signed >= absolute_lb], conjunction!([self.signed >= 0] & [self.absolute >= absolute_lb]), - self.inference_code, + &self.inference_code, )?; } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs index e3abb42b3..56ee42373 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_equals.rs @@ -65,7 +65,7 @@ where a_removed_values: HashSet::default(), b_removed_values: HashSet::default(), - inference_code: context.create_inference_code(constraint_tag, BinaryEquals), + inference_code: InferenceCode::new(constraint_tag, BinaryEquals), has_backtracked: false, first_propagation_loop: true, @@ -141,7 +141,7 @@ where .with_predicate_type(predicate_type) .with_value(value) .into_bits(), - self.inference_code, + &self.inference_code, ) } } @@ -164,7 +164,7 @@ where // Note that we lift the conflict Some(PropagatorConflict { conjunction: conjunction!([self.a <= b_lb - 1] & [self.b >= b_lb]), - inference_code: self.inference_code, + inference_code: self.inference_code.clone(), }) } else if b_ub < a_lb { // If `b` is fully before `a` then we report a conflict @@ -172,7 +172,7 @@ where // Note that we lift the conflict Some(PropagatorConflict { conjunction: conjunction!([self.b <= a_lb - 1] & [self.a >= a_lb]), - inference_code: self.inference_code, + inference_code: self.inference_code.clone(), }) } else { None diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs index c10b6820f..e99bccac9 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/binary/binary_not_equals.rs @@ -48,7 +48,7 @@ where a, b, - inference_code: context.create_inference_code(constraint_tag, BinaryNotEquals), + inference_code: InferenceCode::new(constraint_tag, BinaryNotEquals), } } } @@ -78,7 +78,7 @@ where // If this is the case then we have detected a conflict Some(PropagatorConflict { conjunction: conjunction!([self.a == lb_a] & [self.b == lb_a]), - inference_code: self.inference_code, + inference_code: self.inference_code.clone(), }) } else { None @@ -117,7 +117,7 @@ where context.post( predicate!(self.b != a_lb), conjunction!([self.a == a_lb]), - self.inference_code, + &self.inference_code, )?; } @@ -126,7 +126,7 @@ where context.post( predicate!(self.a != b_lb), conjunction!([self.b == b_lb]), - self.inference_code, + &self.inference_code, )?; } @@ -152,7 +152,7 @@ where context.post( predicate!(self.b != a_lb), conjunction!([self.a == a_lb]), - self.inference_code, + &self.inference_code, )?; } @@ -160,7 +160,7 @@ where context.post( predicate!(self.a != b_lb), conjunction!([self.b == b_lb]), - self.inference_code, + &self.inference_code, )?; } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs index 5dd5365c0..4155a532a 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs @@ -55,7 +55,7 @@ where context.register(denominator.clone(), DomainEvents::BOUNDS, ID_DENOMINATOR); context.register(rhs.clone(), DomainEvents::BOUNDS, ID_RHS); - let inference_code = context.create_inference_code(constraint_tag, Division); + let inference_code = InferenceCode::new(constraint_tag, Division); DivisionPropagator { numerator, @@ -100,7 +100,7 @@ where &self.numerator, &self.denominator, &self.rhs, - self.inference_code, + &self.inference_code, ) } } @@ -110,7 +110,7 @@ fn perform_propagation PropagationStatusCP { if context.lower_bound(denominator) < 0 && context.upper_bound(denominator) > 0 { // For now we don't do anything in this case, note that this will not lead to incorrect @@ -194,7 +194,7 @@ fn propagate_positive_domains PropagationStatusCP { let rhs_min = context.lower_bound(rhs); let rhs_max = context.upper_bound(rhs); @@ -284,7 +284,7 @@ fn propagate_upper_bounds PropagationStatusCP { let rhs_max = context.upper_bound(rhs); let numerator_max = context.upper_bound(numerator); @@ -330,7 +330,7 @@ fn propagate_signs PropagationStatusCP { let rhs_min = context.lower_bound(rhs); let rhs_max = context.upper_bound(rhs); diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs index cfa34f2c4..d6cb8a456 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs @@ -51,7 +51,7 @@ where a, b, c, - inference_code: context.create_inference_code(constraint_tag, IntegerMultiplication), + inference_code: InferenceCode::new(constraint_tag, IntegerMultiplication), } } } @@ -87,7 +87,7 @@ where } fn propagate_from_scratch(&self, context: PropagationContext) -> PropagationStatusCP { - perform_propagation(context, &self.a, &self.b, &self.c, self.inference_code) + perform_propagation(context, &self.a, &self.b, &self.c, &self.inference_code) } } @@ -96,7 +96,7 @@ fn perform_propagation PropagationStatusCP { // First we propagate the signs propagate_signs(&mut context, a, b, c, inference_code)?; @@ -184,7 +184,7 @@ fn perform_propagation PropagationStatusCP { let a_min = context.lower_bound(a); let a_max = context.upper_bound(a); diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs index d42f37866..b2537cc02 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs @@ -66,7 +66,7 @@ where c, lower_bound_left_hand_side, current_bounds: current_bounds.into(), - inference_code: context.create_inference_code(constraint_tag, LinearBounds), + inference_code: InferenceCode::new(constraint_tag, LinearBounds), reason_buffer: Vec::default(), } } @@ -99,7 +99,7 @@ where .iter() .map(|var| predicate![var >= context.lower_bound(var)]) .collect(), - inference_code: self.inference_code, + inference_code: self.inference_code.clone(), } } } @@ -206,7 +206,7 @@ where let bound = self.c - (lower_bound_left_hand_side - context.lower_bound(x_i)); if context.upper_bound(x_i) > bound { - context.post(predicate![x_i <= bound], i, self.inference_code)?; + context.post(predicate![x_i <= bound], i, &self.inference_code)?; } } @@ -263,7 +263,7 @@ where }) .collect(); - context.post(predicate![x_i <= bound], reason, self.inference_code)?; + context.post(predicate![x_i <= bound], reason, &self.inference_code)?; } } diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs index 522a97ae4..3b01e76d2 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/linear_not_equal.rs @@ -67,7 +67,7 @@ where fixed_lhs: 0, unfixed_variable_has_been_updated: false, should_recalculate_lhs: false, - inference_code: context.create_inference_code(constraint_tag, LinearNotEquals), + inference_code: InferenceCode::new(constraint_tag, LinearNotEquals), }; propagator.recalculate_fixed_variables(context.domains()); @@ -208,7 +208,7 @@ where .filter(|&(i, _)| i != unfixed_x_i) .map(|(_, x_i)| predicate![x_i == context.lower_bound(x_i)]) .collect::(), - self.inference_code, + &self.inference_code, )?; } } else if self.number_of_fixed_terms == self.terms.len() { @@ -266,7 +266,7 @@ where .expect("Expected to be able to fit i64 into i32") ], reason, - self.inference_code, + &self.inference_code, )?; } else if num_fixed == self.terms.len() && lhs == self.rhs as i64 { let conjunction = self @@ -277,7 +277,7 @@ where return Err(PropagatorConflict { conjunction, - inference_code: self.inference_code, + inference_code: self.inference_code.clone(), } .into()); } @@ -322,7 +322,7 @@ impl LinearNotEqualPropagator { return Err(PropagatorConflict { conjunction, - inference_code: self.inference_code, + inference_code: self.inference_code.clone(), }); } Ok(()) diff --git a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs index 33d3ff38a..22c8b86a1 100644 --- a/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs +++ b/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs @@ -48,7 +48,7 @@ where LocalId::from(array.len() as u32), ); - let inference_code = context.create_inference_code(constraint_tag, Maximum); + let inference_code = InferenceCode::new(constraint_tag, Maximum); MaximumPropagator { array, @@ -92,7 +92,7 @@ impl Prop context.post( predicate![var <= rhs_ub], conjunction!([self.rhs <= rhs_ub]), - self.inference_code, + &self.inference_code, )?; let var_lb = context.lower_bound(var); @@ -112,7 +112,7 @@ impl Prop context.post( predicate![self.rhs >= max_lb], PropositionalConjunction::from(lb_reason), - self.inference_code, + &self.inference_code, )?; // Rule 3. @@ -128,7 +128,7 @@ impl Prop context.post( predicate![self.rhs <= max_ub], ub_reason, - self.inference_code, + &self.inference_code, )?; } @@ -161,7 +161,7 @@ impl Prop context.post( predicate![propagating_variable >= rhs_lb], propagation_reason, - self.inference_code, + &self.inference_code, )?; } } diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/explanations/pointwise.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/explanations/pointwise.rs index cdaec708b..b3e97857f 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/explanations/pointwise.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/explanations/pointwise.rs @@ -21,7 +21,7 @@ pub(crate) fn propagate_lower_bounds_with_pointwise_explanations], propagating_task: &Rc>, - inference_code: InferenceCode, + inference_code: &InferenceCode, ) -> Result<(), EmptyDomainConflict> { // The time points should follow the following properties (based on `Improving // scheduling by learning - Andreas Schutt`): @@ -130,7 +130,7 @@ pub(crate) fn propagate_upper_bounds_with_pointwise_explanations], propagating_task: &Rc>, - inference_code: InferenceCode, + inference_code: &InferenceCode, ) -> Result<(), EmptyDomainConflict> { // The time points should follow the following properties (based on `Improving // scheduling by learning - Andreas Schutt`): diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/debug.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/debug.rs index 84f9ed367..29e51c434 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/debug.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/debug.rs @@ -27,7 +27,7 @@ pub(crate) fn time_tables_are_the_same_interval< const SYNCHRONISE: bool, >( mut context: Domains, - inference_code: InferenceCode, + inference_code: &InferenceCode, time_table: &OverIntervalTimeTableType, parameters: &CumulativeParameters, ) -> bool { diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/synchronisation.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/synchronisation.rs index 3b53051b3..63002e4dc 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/synchronisation.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/synchronisation.rs @@ -58,7 +58,7 @@ pub(crate) fn check_synchronisation_conflict_explanation_over_interval< synchronised_conflict_explanation: &PropagationStatusCP, context: Domains, parameters: &CumulativeParameters, - inference_code: InferenceCode, + inference_code: &InferenceCode, ) -> bool { let error_from_scratch = create_time_table_over_interval_from_scratch(context, parameters, inference_code); @@ -81,7 +81,7 @@ pub(crate) fn check_synchronisation_conflict_explanation_over_interval< /// included in the profile and sorting them in the same order. pub(crate) fn create_synchronised_conflict_explanation( mut context: Domains, - inference_code: InferenceCode, + inference_code: &InferenceCode, conflicting_profile: &mut ResourceProfile, parameters: &CumulativeParameters, ) -> PropagationStatusCP { diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs index a426e0a16..fc6ff7f9c 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/over_interval_incremental_propagator/time_table_over_interval_incremental.rs @@ -123,7 +123,7 @@ impl PropagatorConstruc self.is_time_table_outdated = true; - self.inference_code = Some(context.create_inference_code(self.constraint_tag, TimeTable)); + self.inference_code = Some(InferenceCode::new(self.constraint_tag, TimeTable)); self } @@ -182,7 +182,7 @@ impl { conflict = Some(Err(create_conflict_explanation( context.reborrow(), - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), &conflict_tasks, self.parameters.options.explanation_type, ) @@ -243,7 +243,7 @@ impl self.time_table = create_time_table_over_interval_from_scratch( context.domains(), &self.parameters, - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), )?; // Then we note that the time-table is not outdated anymore @@ -304,7 +304,7 @@ impl let synchronised_conflict_explanation = create_synchronised_conflict_explanation( context.domains(), - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), &mut conflicting_profile, &self.parameters, ); @@ -313,7 +313,7 @@ impl &synchronised_conflict_explanation, context.domains(), &self.parameters, - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), ), "The conflict explanation was not the same as the conflict explanation from scratch!" ); @@ -335,7 +335,7 @@ impl create_time_table_over_interval_from_scratch( context.domains(), &self.parameters, - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), ) .is_err(), "Time-table from scratch could not find conflict" @@ -345,7 +345,7 @@ impl return Err(create_conflict_explanation( context.domains(), - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), conflicting_profile, self.parameters.options.explanation_type, ) @@ -390,7 +390,7 @@ impl Propagator if self.parameters.is_infeasible { return Err(Conflict::Propagator(PropagatorConflict { conjunction: conjunction!(), - inference_code: self.inference_code.unwrap(), + inference_code: self.inference_code.clone().unwrap(), })); } @@ -399,7 +399,7 @@ impl Propagator pumpkin_assert_extreme!( debug::time_tables_are_the_same_interval::( context.domains(), - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), &self.time_table, &self.parameters, ), @@ -412,7 +412,7 @@ impl Propagator // could cause another propagation by a profile which has not been updated propagate_based_on_timetable( &mut context, - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), self.time_table.iter(), &self.parameters, &mut self.updatable_structures, @@ -523,7 +523,7 @@ impl Propagator &mut context, &self.parameters, &self.updatable_structures, - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), ) } } diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs index 320abd00b..8d1a0e978 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/synchronisation.rs @@ -22,7 +22,7 @@ pub(crate) fn check_synchronisation_conflict_explanation_per_point< >( synchronised_conflict_explanation: &PropagationStatusCP, context: Domains, - inference_code: InferenceCode, + inference_code: &InferenceCode, parameters: &CumulativeParameters, ) -> bool { let error_from_scratch = @@ -112,7 +112,7 @@ fn get_minimum_set_of_tasks_which_overflow_capacity<'a, Var: IntegerVariable + ' /// profile and sorting them in the same order. pub(crate) fn create_synchronised_conflict_explanation( context: Domains, - inference_code: InferenceCode, + inference_code: &InferenceCode, conflicting_profile: &mut ResourceProfile, parameters: &CumulativeParameters, ) -> PropagationStatusCP { diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs index ae860f402..db3a00614 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/per_point_incremental_propagator/time_table_per_point_incremental.rs @@ -113,7 +113,7 @@ impl Propagator // Then we do normal propagation self.is_time_table_outdated = true; - self.inference_code = Some(context.create_inference_code(self.constraint_tag, TimeTable)); + self.inference_code = Some(InferenceCode::new(self.constraint_tag, TimeTable)); self } @@ -183,7 +183,7 @@ impl // The newly introduced mandatory part(s) caused an overflow of the resource conflict = Some(Err(create_conflict_explanation( context.reborrow(), - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), current_profile, self.parameters.options.explanation_type, ) @@ -260,7 +260,7 @@ impl // We create the time-table from scratch (and return an error if it overflows) self.time_table = create_time_table_per_point_from_scratch( context.domains(), - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), &self.parameters, )?; @@ -328,7 +328,7 @@ impl let synchronised_conflict_explanation = create_synchronised_conflict_explanation( context.domains(), - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), conflicting_profile, &self.parameters, ); @@ -337,7 +337,7 @@ impl check_synchronisation_conflict_explanation_per_point( &synchronised_conflict_explanation, context.domains(), - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), &self.parameters, ), "The conflict explanation was not the same as the conflict explanation from scratch!" @@ -363,7 +363,7 @@ impl pumpkin_assert_extreme!( create_time_table_per_point_from_scratch( context.domains(), - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), &self.parameters ) .is_err(), @@ -374,7 +374,7 @@ impl return Err(create_conflict_explanation( context.domains(), - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), conflicting_profile, self.parameters.options.explanation_type, ) @@ -419,7 +419,7 @@ impl Propagator if self.parameters.is_infeasible { return Err(Conflict::Propagator(PropagatorConflict { conjunction: conjunction!(), - inference_code: self.inference_code.unwrap(), + inference_code: self.inference_code.clone().unwrap(), })); } @@ -428,7 +428,7 @@ impl Propagator pumpkin_assert_extreme!(debug::time_tables_are_the_same_point::( context.domains(), - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), &self.time_table, &self.parameters )); @@ -439,7 +439,7 @@ impl Propagator // could cause another propagation by a profile which has not been updated propagate_based_on_timetable( &mut context, - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), self.time_table.values(), &self.parameters, &mut self.updatable_structures, @@ -546,7 +546,7 @@ impl Propagator // Use the same debug propagator from `TimeTablePerPoint` propagate_from_scratch_time_table_point( &mut context, - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), &self.parameters, &self.updatable_structures, ) @@ -577,7 +577,7 @@ mod debug { const SYNCHRONISE: bool, >( context: Domains, - inference_code: InferenceCode, + inference_code: &InferenceCode, time_table: &PerPointTimeTableType, parameters: &CumulativeParameters, ) -> bool { diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/propagation_handler.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/propagation_handler.rs index d1da49e9e..61fcc0203 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/propagation_handler.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/propagation_handler.rs @@ -132,14 +132,14 @@ impl CumulativePropagationHandler { &full_explanation, context.domains() )); - context.post(predicate, full_explanation, self.inference_code) + context.post(predicate, full_explanation, &self.inference_code) } CumulativeExplanationType::Pointwise => { pointwise::propagate_lower_bounds_with_pointwise_explanations( context, profiles, propagating_task, - self.inference_code, + &self.inference_code, ) } } @@ -198,14 +198,14 @@ impl CumulativePropagationHandler { &full_explanation, context.domains() )); - context.post(predicate, full_explanation, self.inference_code) + context.post(predicate, full_explanation, &self.inference_code) } CumulativeExplanationType::Pointwise => { pointwise::propagate_upper_bounds_with_pointwise_explanations( context, profiles, propagating_task, - self.inference_code, + &self.inference_code, ) } } @@ -249,14 +249,14 @@ impl CumulativePropagationHandler { let mut reason = (*explanation).clone(); reason.push(lower_bound_predicate_propagating_task); - context.post(predicate, reason, self.inference_code) + context.post(predicate, reason, &self.inference_code) } CumulativeExplanationType::Pointwise => { pointwise::propagate_lower_bounds_with_pointwise_explanations( context, &[profile], propagating_task, - self.inference_code, + &self.inference_code, ) } } @@ -304,14 +304,14 @@ impl CumulativePropagationHandler { let mut reason = (*explanation).clone(); reason.push(upper_bound_predicate_propagating_task); - context.post(predicate, reason, self.inference_code) + context.post(predicate, reason, &self.inference_code) } CumulativeExplanationType::Pointwise => { pointwise::propagate_upper_bounds_with_pointwise_explanations( context, &[profile], propagating_task, - self.inference_code, + &self.inference_code, ) } } @@ -370,7 +370,7 @@ impl CumulativePropagationHandler { &explanation, context.domains() )); - context.post(predicate, (*explanation).clone(), self.inference_code)?; + context.post(predicate, (*explanation).clone(), &self.inference_code)?; } CumulativeExplanationType::Pointwise => { // We split into two cases when determining the explanation of the profile @@ -403,7 +403,7 @@ impl CumulativePropagationHandler { &explanation, context.domains() )); - context.post(predicate, explanation, self.inference_code)?; + context.post(predicate, explanation, &self.inference_code)?; } } } @@ -448,7 +448,7 @@ impl CumulativePropagationHandler { /// `explanation_type`. pub(crate) fn create_conflict_explanation( context: Context, - inference_code: InferenceCode, + inference_code: &InferenceCode, conflict_profile: &ResourceProfile, explanation_type: CumulativeExplanationType, ) -> PropagatorConflict @@ -469,7 +469,7 @@ where PropagatorConflict { conjunction, - inference_code, + inference_code: inference_code.clone(), } } @@ -481,6 +481,7 @@ pub(crate) mod test_propagation_handler { use pumpkin_core::predicate; use pumpkin_core::predicates::Predicate; use pumpkin_core::predicates::PropositionalConjunction; + use pumpkin_core::proof::ConstraintTag; use pumpkin_core::proof::InferenceCode; use pumpkin_core::propagation::LocalId; use pumpkin_core::state::CurrentNogood; @@ -503,7 +504,7 @@ pub(crate) mod test_propagation_handler { pub(crate) fn new(explanation_type: CumulativeExplanationType) -> Self { let propagation_handler = CumulativePropagationHandler::new( explanation_type, - InferenceCode::create_from_index(0), + InferenceCode::unknown_label(ConstraintTag::create_from_index(0)), ); let state = State::default(); @@ -533,7 +534,7 @@ pub(crate) mod test_propagation_handler { let reason = create_conflict_explanation( self.state.get_domains(), - self.propagation_handler.inference_code, + &self.propagation_handler.inference_code, &profile, self.propagation_handler.explanation_type, ); diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs index fdbdb14cc..6bdf00a08 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_over_interval.rs @@ -112,7 +112,7 @@ impl PropagatorConstructor .initialise_bounds_and_remove_fixed(context.domains(), &self.parameters); register_tasks(&self.parameters.tasks, context.reborrow(), false); - self.inference_code = Some(context.create_inference_code(self.constraint_tag, TimeTable)); + self.inference_code = Some(InferenceCode::new(self.constraint_tag, TimeTable)); self } @@ -123,21 +123,21 @@ impl Propagator for TimeTableOverIntervalPropaga if self.parameters.is_infeasible { return Err(Conflict::Propagator(PropagatorConflict { conjunction: conjunction!(), - inference_code: self.inference_code.unwrap(), + inference_code: self.inference_code.clone().unwrap(), })); } let time_table = create_time_table_over_interval_from_scratch( context.domains(), &self.parameters, - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), )?; self.is_time_table_empty = time_table.is_empty(); // No error has been found -> Check for updates (i.e. go over all profiles and all tasks and // check whether an update can take place) propagate_based_on_timetable( &mut context, - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), time_table.iter(), &self.parameters, &mut self.updatable_structures, @@ -198,7 +198,7 @@ impl Propagator for TimeTableOverIntervalPropaga &mut context, &self.parameters, &self.updatable_structures, - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), ) } } @@ -216,7 +216,7 @@ impl Propagator for TimeTableOverIntervalPropaga pub(crate) fn create_time_table_over_interval_from_scratch( mut context: Domains, parameters: &CumulativeParameters, - inference_code: InferenceCode, + inference_code: &InferenceCode, ) -> Result, PropagatorConflict> { // First we create a list of all the events (i.e. start and ends of mandatory parts) let events = create_events(context.reborrow(), parameters); @@ -295,7 +295,7 @@ fn create_events( fn create_time_table_from_events( events: Vec>, context: Context, - inference_code: InferenceCode, + inference_code: &InferenceCode, parameters: &CumulativeParameters, ) -> Result, PropagatorConflict> { pumpkin_assert_extreme!( @@ -449,7 +449,7 @@ pub(crate) fn propagate_from_scratch_time_table_interval, updatable_structures: &UpdatableStructures, - inference_code: InferenceCode, + inference_code: &InferenceCode, ) -> PropagationStatusCP { // We first create a time-table over interval and return an error if there was // an overflow of the resource capacity while building the time-table diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs index 30890b922..1edfda6be 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_per_point.rs @@ -103,7 +103,7 @@ impl PropagatorConstructor for TimeTablePerPoint .initialise_bounds_and_remove_fixed(context.domains(), &self.parameters); register_tasks(&self.parameters.tasks, context.reborrow(), false); - self.inference_code = Some(context.create_inference_code(self.constraint_tag, TimeTable)); + self.inference_code = Some(InferenceCode::new(self.constraint_tag, TimeTable)); self } @@ -114,13 +114,13 @@ impl Propagator for TimeTablePerPointPropagator< if self.parameters.is_infeasible { return Err(Conflict::Propagator(PropagatorConflict { conjunction: conjunction!(), - inference_code: self.inference_code.unwrap(), + inference_code: self.inference_code.clone().unwrap(), })); } let time_table = create_time_table_per_point_from_scratch( context.domains(), - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), &self.parameters, )?; self.is_time_table_empty = time_table.is_empty(); @@ -128,7 +128,7 @@ impl Propagator for TimeTablePerPointPropagator< // check whether an update can take place) propagate_based_on_timetable( &mut context, - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), time_table.values(), &self.parameters, &mut self.updatable_structures, @@ -189,7 +189,7 @@ impl Propagator for TimeTablePerPointPropagator< fn propagate_from_scratch(&self, mut context: PropagationContext) -> PropagationStatusCP { propagate_from_scratch_time_table_point( &mut context, - self.inference_code.unwrap(), + self.inference_code.as_ref().unwrap(), &self.parameters, &self.updatable_structures, ) @@ -209,7 +209,7 @@ pub(crate) fn create_time_table_per_point_from_scratch< Context: ReadDomains, >( context: Context, - inference_code: InferenceCode, + inference_code: &InferenceCode, parameters: &CumulativeParameters, ) -> Result, PropagatorConflict> { let mut time_table: PerPointTimeTableType = PerPointTimeTableType::new(); @@ -254,7 +254,7 @@ pub(crate) fn create_time_table_per_point_from_scratch< pub(crate) fn propagate_from_scratch_time_table_point( context: &mut PropagationContext, - inference_code: InferenceCode, + inference_code: &InferenceCode, parameters: &CumulativeParameters, updatable_structures: &UpdatableStructures, ) -> PropagationStatusCP { diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_util.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_util.rs index 3f387fc9b..7da67427b 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_util.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/time_table_util.rs @@ -200,7 +200,7 @@ fn debug_check_whether_profiles_are_maximal_and_sorted<'a, Var: IntegerVariable /// cannot be increased or decreased, respectively). pub(crate) fn propagate_based_on_timetable<'a, Var: IntegerVariable + 'static>( context: &mut PropagationContext, - inference_code: InferenceCode, + inference_code: &InferenceCode, time_table: impl Iterator> + Clone, parameters: &CumulativeParameters, updatable_structures: &mut UpdatableStructures, @@ -255,14 +255,16 @@ pub(crate) fn propagate_based_on_timetable<'a, Var: IntegerVariable + 'static>( /// [`CumulativeExplanationType::Pointwise`]. fn propagate_single_profiles<'a, Var: IntegerVariable + 'static>( context: &mut PropagationContext, - inference_code: InferenceCode, + inference_code: &InferenceCode, time_table: impl Iterator> + Clone, updatable_structures: &mut UpdatableStructures, parameters: &CumulativeParameters, ) -> PropagationStatusCP { // We create the structure responsible for propagations and explanations - let mut propagation_handler = - CumulativePropagationHandler::new(parameters.options.explanation_type, inference_code); + let mut propagation_handler = CumulativePropagationHandler::new( + parameters.options.explanation_type, + inference_code.clone(), + ); // Then we go over all of the profiles in the time-table 'profile_loop: for profile in time_table { @@ -358,7 +360,7 @@ fn propagate_single_profiles<'a, Var: IntegerVariable + 'static>( /// beneficial. fn propagate_sequence_of_profiles<'a, Var: IntegerVariable + 'static>( context: &mut PropagationContext, - inference_code: InferenceCode, + inference_code: &InferenceCode, time_table: impl Iterator> + Clone, updatable_structures: &mut UpdatableStructures, parameters: &CumulativeParameters, @@ -373,8 +375,10 @@ fn propagate_sequence_of_profiles<'a, Var: IntegerVariable + 'static>( } // We create the structure responsible for propagations and explanations - let mut propagation_handler = - CumulativePropagationHandler::new(parameters.options.explanation_type, inference_code); + let mut propagation_handler = CumulativePropagationHandler::new( + parameters.options.explanation_type, + inference_code.clone(), + ); // Then we go over all the possible tasks for task in updatable_structures.get_unfixed_tasks() { diff --git a/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs b/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs index 27519eaa1..b34cf84fa 100644 --- a/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs +++ b/pumpkin-crates/propagators/src/propagators/disjunctive/disjunctive_propagator.rs @@ -91,8 +91,7 @@ impl PropagatorConstructor for DisjunctiveConstr .collect::>(); let theta_lambda_tree = ThetaLambdaTree::new(&tasks); - let inference_code = - context.create_inference_code(self.constraint_tag, DisjunctiveEdgeFinding); + let inference_code = InferenceCode::new(self.constraint_tag, DisjunctiveEdgeFinding); tasks.iter().for_each(|task| { context.register(task.start_time.clone(), DomainEvents::BOUNDS, task.id); @@ -119,7 +118,7 @@ impl Propagator for DisjunctivePropagator { &mut context, &self.tasks, &mut self.sorted_tasks, - self.inference_code, + &self.inference_code, ) } @@ -131,7 +130,7 @@ impl Propagator for DisjunctivePropagator { &mut context, &self.tasks, &mut sorted_tasks, - self.inference_code, + &self.inference_code, ) } } @@ -143,7 +142,7 @@ fn edge_finding( context: &mut PropagationContext, tasks: &[DisjunctiveTask], sorted_tasks: &mut [DisjunctiveTask], - inference_code: InferenceCode, + inference_code: &InferenceCode, ) -> PropagationStatusCP { // First we create our Theta-Lambda tree and add all of the tasks to Theta (Lambda is empty at // this point) @@ -169,7 +168,7 @@ fn edge_finding( if theta_lambda_tree.ect() > lct_j { return Err(Conflict::Propagator(PropagatorConflict { conjunction: create_conflict_explanation(theta_lambda_tree, context, lct_j), - inference_code, + inference_code: inference_code.clone(), })); } diff --git a/pumpkin-crates/propagators/src/propagators/element.rs b/pumpkin-crates/propagators/src/propagators/element.rs index 1f5e84838..074726a5b 100644 --- a/pumpkin-crates/propagators/src/propagators/element.rs +++ b/pumpkin-crates/propagators/src/propagators/element.rs @@ -59,7 +59,7 @@ where context.register(index.clone(), DomainEvents::ANY_INT, ID_INDEX); context.register(rhs.clone(), DomainEvents::ANY_INT, ID_RHS); - let inference_code = context.create_inference_code(constraint_tag, Element); + let inference_code = InferenceCode::new(constraint_tag, Element); ElementPropagator { array, @@ -158,12 +158,12 @@ where context.post( predicate![self.index >= 0], conjunction!(), - self.inference_code, + &self.inference_code, )?; context.post( predicate![self.index <= self.array.len() as i32 - 1], conjunction!(), - self.inference_code, + &self.inference_code, )?; Ok(()) } @@ -194,7 +194,7 @@ where .with_value(rhs_lb) .into_bits(), ), - self.inference_code, + &self.inference_code, )?; context.post( predicate![self.rhs <= rhs_ub], @@ -204,7 +204,7 @@ where .with_value(rhs_ub) .into_bits(), ), - self.inference_code, + &self.inference_code, )?; Ok(()) @@ -237,7 +237,7 @@ where } for (idx, reason) in to_remove.drain(..) { - context.post(predicate![self.index != idx], reason, self.inference_code)?; + context.post(predicate![self.index != idx], reason, &self.inference_code)?; } Ok(()) @@ -257,12 +257,12 @@ where context.post( predicate![lhs >= rhs_lb], conjunction!([self.rhs >= rhs_lb] & [self.index == index]), - self.inference_code, + &self.inference_code, )?; context.post( predicate![lhs <= rhs_ub], conjunction!([self.rhs <= rhs_ub] & [self.index == index]), - self.inference_code, + &self.inference_code, )?; Ok(()) }