pumpkin_core/propagation/
runtime_checkers.rs

1use pumpkin_checking::BoxedChecker;
2use pumpkin_checking::InferenceChecker;
3
4use crate::predicates::Predicate;
5use crate::proof::ConstraintTag;
6use crate::proof::InferenceCode;
7use crate::proof::InferenceLabel;
8#[cfg(doc)]
9use crate::propagation::PropagatorConstructor;
10
11/// Holds the runtime checkers that are added by a propagator.
12///
13/// Used when creating a new propagator in [`PropagatorConstructor::create`].
14#[derive(Clone, Debug)]
15pub struct RuntimeCheckers {
16    inference_checkers: Vec<(InferenceCode, BoxedChecker<Predicate>)>,
17}
18
19impl RuntimeCheckers {
20    /// Create a [`RuntimeCheckers`] value which we accept may be empty.
21    ///
22    /// This is often not what you want. If it is expected that some checkers should be added,
23    /// use [`RuntimeCheckers::builder`] instead to communicate that intention.
24    pub fn empty() -> RuntimeCheckers {
25        RuntimeCheckers {
26            inference_checkers: vec![],
27        }
28    }
29
30    /// Create a [`RuntimeCheckersBuilder`] to add runtime checkers.
31    ///
32    /// The [`RuntimeCheckersBuilder::build`] will panic if no checkers are added.
33    pub fn builder() -> RuntimeCheckersBuilder {
34        RuntimeCheckersBuilder {
35            checkers: RuntimeCheckers {
36                inference_checkers: vec![],
37            },
38        }
39    }
40
41    /// Add an [`InferenceChecker`] to verify the soundness of propagations.
42    pub fn add_inference_checker(
43        &mut self,
44        constraint_tag: ConstraintTag,
45        inference_label: impl InferenceLabel,
46        checker: impl InferenceChecker<Predicate> + 'static,
47    ) -> InferenceCode {
48        let inference_code = InferenceCode::new(constraint_tag, inference_label);
49
50        self.inference_checkers
51            .push((inference_code.clone(), BoxedChecker::new(Box::new(checker))));
52
53        inference_code
54    }
55}
56
57impl IntoIterator for RuntimeCheckers {
58    type Item = (InferenceCode, BoxedChecker<Predicate>);
59
60    type IntoIter = std::vec::IntoIter<Self::Item>;
61
62    fn into_iter(self) -> Self::IntoIter {
63        self.inference_checkers.into_iter()
64    }
65}
66
67/// A builder for the [`RuntimeCheckers`] that ensures at least one checker is added.
68#[derive(Clone, Debug)]
69pub struct RuntimeCheckersBuilder {
70    checkers: RuntimeCheckers,
71}
72
73impl RuntimeCheckersBuilder {
74    /// Add an [`InferenceChecker`] to verify the soundness of propagations.
75    pub fn add_inference_checker(
76        &mut self,
77        constraint_tag: ConstraintTag,
78        inference_label: impl InferenceLabel,
79        checker: impl InferenceChecker<Predicate> + 'static,
80    ) -> InferenceCode {
81        self.checkers
82            .add_inference_checker(constraint_tag, inference_label, checker)
83    }
84
85    /// Finish adding runtime checkers.
86    ///
87    /// Panics if runtime verification is enabled and no checkers are added. If it is expected
88    /// behavior that no checkers are added, use [`RuntimeCheckers::empty`].
89    pub fn build(self) -> RuntimeCheckers {
90        if cfg!(feature = "check-propagations") {
91            assert!(
92                !self.checkers.inference_checkers.is_empty(),
93                "did not register any inference checkers"
94            );
95        }
96
97        self.checkers
98    }
99}
pumpkin_core/propagation/runtime_checkers.rs

pumpkin_core/propagation/
runtime_checkers.rs
