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    /// constraint satisfaction solver. 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) -> &str {
73        self.1.as_ref()
74    }
75}
76
77/// Conveniently creates [`InferenceLabel`] for use in a propagator.
78///
79/// In case it is desirable, the exact string that is printed in the DRCP proof can be
80/// provided as a second parameter. Otherwise, the type name is converted to snake
81///
82/// # Example
83/// ```ignore
84/// declare_inference_label!(SomeInference);
85/// declare_inference_label!(OtherInference, "label");
86///
87/// // Now we can use `SomeInference` and `OtherInference` when creating an inference
88/// // code as it implements `InferenceLabel`.
89/// ```
90/// case.
91#[macro_export]
92macro_rules! declare_inference_label {
93    ($v:vis $name:ident) => {
94        declare_inference_label!($v $name, {
95            let ident_str = stringify!($name);
96            <&str as convert_case::Casing<&str>>::to_case(
97                &ident_str,
98                convert_case::Case::Snake,
99            )
100        });
101    };
102
103    ($v:vis $name:ident, $label:expr) => {
104        #[derive(Clone, Copy, Debug, PartialEq, Eq)]
105        $v struct $name;
106
107        declare_inference_label!(@impl_trait $name, $label);
108    };
109
110    (@impl_trait $name:ident, $label:expr) => {
111        impl $crate::proof::InferenceLabel for $name {
112            fn to_str(&self) -> std::sync::Arc<str> {
113                static LABEL: std::sync::OnceLock<std::sync::Arc<str>> = std::sync::OnceLock::new();
114
115                let label = LABEL.get_or_init(|| {
116                    std::sync::Arc::from($label)
117                });
118
119                std::sync::Arc::clone(label)
120            }
121        }
122    };
123}
124
125/// A label of the inference mechanism that identifies a particular inference. It is combined with a
126/// [`ConstraintTag`] to create an [`InferenceCode`].
127///
128/// There may be different inference algorithms for the same contraint that are incomparable in
129/// terms of propagation strength. To discriminate between these algorithms, the inference label is
130/// used.
131///
132/// Conceptually, the inference label is a string. To aid with auto-complete, we introduce
133/// this as a strongly-typed concept. For most cases, creating an inference label is done with the
134/// [`declare_inference_label`] macro.
135pub trait InferenceLabel {
136    /// Returns the string-representation of the inference label.
137    ///
138    /// Typically different instances of the same propagator will use the same inference label.
139    /// Users are encouraged to share the string allocation, which is why the return value is
140    /// `Arc<str>`.
141    fn to_str(&self) -> Arc<str>;
142}
143
144declare_inference_label!(pub Unknown);
pumpkin_core/proof/inference_code.rs

pumpkin_core/proof/
inference_code.rs
