pumpkin_core/proof/
inference_code.rs

1use std::num::NonZero;
2use std::sync::Arc;
3
4#[cfg(doc)]
5use crate::Solver;
6use crate::containers::StorageKey;
7
8/// An identifier for constraints, which is used to relate constraints from the model to steps in
9/// the proof. Under the hood, a tag is just a [`NonZero<u32>`]. The underlying integer can be
10/// obtained through the [`Into`] implementation.
11///
12/// Constraint tags only be created through [`Solver::new_constraint_tag()`]. This is a conscious
13/// decision, as learned constraints will also need to be tagged, which means the solver has to be
14/// responsible for maintaining their uniqueness.
15#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
16pub struct ConstraintTag(NonZero<u32>);
17
18impl From<ConstraintTag> for NonZero<u32> {
19    fn from(value: ConstraintTag) -> Self {
20        value.0
21    }
22}
23
24impl ConstraintTag {
25    /// Create a new tag directly.
26    ///
27    /// *Note*: Be careful when doing this. Regular construction should only be done through the
28    /// state. It is important that constraint tags remain unique.
29    pub(crate) fn from_non_zero(non_zero: NonZero<u32>) -> ConstraintTag {
30        ConstraintTag(non_zero)
31    }
32}
33
34impl StorageKey for ConstraintTag {
35    fn index(&self) -> usize {
36        self.0.get() as usize - 1
37    }
38
39    fn create_from_index(index: usize) -> Self {
40        Self::from_non_zero(
41            NonZero::new(index as u32 + 1).expect("the '+ 1' ensures the value is non-zero"),
42        )
43    }
44}
45
46/// An inference code is a combination of a constraint tag with an inference label. Propagators
47/// associate an inference code with every propagation to identify why that propagation happened
48/// in terms of the constraint and inference that identified it.
49#[derive(Clone, Debug, PartialEq, Eq, Hash)]
50pub struct InferenceCode(ConstraintTag, Arc<str>);
51
52impl InferenceCode {
53    /// Create a new inference code from a [`ConstraintTag`] and [`InferenceLabel`].
54    pub fn new(tag: ConstraintTag, label: impl InferenceLabel) -> Self {
55        InferenceCode(tag, label.to_str())
56    }
57
58    /// Create an inference label with the [`Unknown`] inference label.
59    ///
60    /// This should be avoided as much as possible. This is likely only useful for writing unit
61    /// tests.
62    pub fn unknown_label(tag: ConstraintTag) -> Self {
63        InferenceCode::new(tag, Unknown)
64    }
65
66    /// Get the constraint tag.
67    pub fn tag(&self) -> ConstraintTag {
68        self.0
69    }
70
71    /// Get the inference label.
72    pub fn label(&self) -> Arc<str> {
73        Arc::clone(&self.1)
74    }
75}
76
77#[doc(hidden)]
78pub fn convert_label_name(ident_str: &str) -> Arc<str> {
79    use convert_case::Casing;
80
81    ident_str.to_case(convert_case::Case::Snake).into()
82}
83
84/// Conveniently creates [`InferenceLabel`] for use in a propagator.
85///
86/// In case it is desirable, the exact string that is printed in the DRCP proof can be
87/// provided as a second parameter. Otherwise, the type name is converted to snake
88///
89/// # Example
90/// ```ignore
91/// declare_inference_label!(SomeInference);
92/// declare_inference_label!(OtherInference, "label");
93///
94/// // Now we can use `SomeInference` and `OtherInference` when creating an inference
95/// // code as it implements `InferenceLabel`.
96/// ```
97/// case.
98#[macro_export]
99macro_rules! declare_inference_label {
100    ($v:vis $name:ident) => {
101        declare_inference_label!($v $name, $crate::proof::convert_label_name(stringify!($name)));
102    };
103
104    ($v:vis $name:ident, $label:expr) => {
105        #[derive(Clone, Copy, Debug, PartialEq, Eq)]
106        $v struct $name;
107
108        declare_inference_label!(@impl_trait $name, std::sync::Arc::from($label));
109    };
110
111    (@impl_trait $name:ident, $label:expr) => {
112        impl $crate::proof::InferenceLabel for $name {
113            fn to_str(&self) -> std::sync::Arc<str> {
114                static LABEL: std::sync::OnceLock<std::sync::Arc<str>> = std::sync::OnceLock::new();
115
116                let label = LABEL.get_or_init(|| $label);
117
118                std::sync::Arc::clone(label)
119            }
120        }
121    };
122}
123
124/// A label of the inference mechanism that identifies a particular inference. It is combined with a
125/// [`ConstraintTag`] to create an [`InferenceCode`].
126///
127/// There may be different inference algorithms for the same contraint that are incomparable in
128/// terms of propagation strength. To discriminate between these algorithms, the inference label is
129/// used.
130///
131/// Conceptually, the inference label is a string. To aid with auto-complete, we introduce
132/// this as a strongly-typed concept. For most cases, creating an inference label is done with the
133/// [`declare_inference_label`] macro.
134pub trait InferenceLabel {
135    /// Returns the string-representation of the inference label.
136    ///
137    /// Typically different instances of the same propagator will use the same inference label.
138    /// Users are encouraged to share the string allocation, which is why the return value is
139    /// `Arc<str>`.
140    fn to_str(&self) -> Arc<str>;
141}
142
143declare_inference_label!(pub Unknown);
pumpkin_core/proof/inference_code.rs

pumpkin_core/proof/
inference_code.rs
