pumpkin_core/proof/
inference_code.rs

1use std::num::NonZero;
2use std::sync::Arc;
3
4use crate::containers::StorageKey;
5#[cfg(doc)]
6use crate::Solver;
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, Copy, Debug, PartialEq, Eq, Hash)]
50pub struct InferenceCode(NonZero<u32>);
51
52impl StorageKey for InferenceCode {
53    fn index(&self) -> usize {
54        self.0.get() as usize - 1
55    }
56
57    fn create_from_index(index: usize) -> Self {
58        Self(NonZero::new(index as u32 + 1).expect("the '+ 1' ensures the value is non-zero"))
59    }
60}
61
62/// Conveniently creates [`InferenceLabel`] for use in a propagator.
63///
64/// In case it is desirable, the exact string that is printed in the DRCP proof can be
65/// provided as a second parameter. Otherwise, the type name is converted to snake
66///
67/// # Example
68/// ```ignore
69/// declare_inference_label!(SomeInference);
70/// declare_inference_label!(OtherInference, "label");
71///
72/// // Now we can use `SomeInference` and `OtherInference` when creating an inference
73/// // code as it implements `InferenceLabel`.
74/// ```
75/// case.
76#[macro_export]
77macro_rules! declare_inference_label {
78    ($name:ident) => {
79        declare_inference_label!($name, {
80            let ident_str = stringify!($name);
81            <&str as convert_case::Casing<&str>>::to_case(
82                &ident_str,
83                convert_case::Case::Snake,
84            )
85        });
86    };
87
88    ($name:ident, $label:expr) => {
89        #[derive(Clone, Copy, Debug, PartialEq, Eq)]
90        struct $name;
91
92        declare_inference_label!(@impl_trait $name, $label);
93    };
94
95    (@impl_trait $name:ident, $label:expr) => {
96        impl $crate::proof::InferenceLabel for $name {
97            fn to_str(&self) -> std::sync::Arc<str> {
98                static LABEL: std::sync::OnceLock<std::sync::Arc<str>> = std::sync::OnceLock::new();
99
100                let label = LABEL.get_or_init(|| {
101                    std::sync::Arc::from($label)
102                });
103
104                std::sync::Arc::clone(label)
105            }
106        }
107    };
108}
109
110/// A label of the inference mechanism that identifies a particular inference. It is combined with a
111/// [`ConstraintTag`] to create an [`InferenceCode`].
112///
113/// There may be different inference algorithms for the same contraint that are incomparable in
114/// terms of propagation strength. To discriminate between these algorithms, the inference label is
115/// used.
116///
117/// Conceptually, the inference label is a string. To aid with auto-complete, we introduce
118/// this as a strongly-typed concept. For most cases, creating an inference label is done with the
119/// [`declare_inference_label`] macro.
120pub trait InferenceLabel {
121    /// Returns the string-representation of the inference label.
122    ///
123    /// Typically different instances of the same propagator will use the same inference label.
124    /// Users are encouraged to share the string allocation, which is why the return value is
125    /// `Arc<str>`.
126    fn to_str(&self) -> Arc<str>;
127}
pumpkin_core/proof/inference_code.rs

pumpkin_core/proof/
inference_code.rs
