refactor: InferenceCode wraps constraint tag and inference label directory

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,17 +175,15 @@ 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,
                 );
             } 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(),

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

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();
 

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

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());
         }

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();
     }

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<InferenceCode, (ConstraintTag, Arc<str>)>,
     /// The [`ConstraintTag`]s generated for this proof.
     pub(crate) constraint_tags: KeyGenerator<ConstraintTag>,
 
@@ -106,7 +103,7 @@ impl From<PropagatorConflict> 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()

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,

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<u32>);
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub struct InferenceCode(ConstraintTag, Arc<str>);
 
-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<str>`.
     fn to_str(&self) -> Arc<str>;
 }
+
+declare_inference_label!(pub Unknown);

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<InferenceCode, (ConstraintTag, Arc<str>)>,
         constraint_tags: &mut KeyGenerator<ConstraintTag>,
         inference_code: InferenceCode,
         premises: impl IntoIterator<Item = Predicate>,
@@ -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)?;

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()