pumpkin_core/checkers/
store.rs

1//! This module facilitates runtime verification in Pumpkin. It defines common types as well as the
2//! [`CheckerStore`] that owns the checkers that are active in the solver.
3
4use pumpkin_checking::BoxedChecker;
5#[cfg(doc)]
6use pumpkin_checking::InferenceChecker;
7
8use crate::containers::HashMap;
9use crate::predicates::Predicate;
10use crate::proof::InferenceCode;
11
12/// Owns the runtime checkers present in the solver.
13///
14/// The runtime checkers consist of:
15/// - inference checkers, which verify that propagations are sound.
16#[derive(Clone, Debug, Default)]
17pub struct CheckerStore {
18    /// For each inference code we associate possibly many inference checkers.
19    inference_checkers: HashMap<InferenceCode, Vec<BoxedChecker<Predicate>>>,
20}
21
22impl CheckerStore {
23    /// Get the [`InferenceChecker`]s for the given inference code.
24    pub fn for_inference_code(
25        &self,
26        inference_code: &InferenceCode,
27    ) -> impl ExactSizeIterator<Item = &BoxedChecker<Predicate>> {
28        self.inference_checkers
29            .get(inference_code)
30            .map(|checkers| itertools::Either::Left(checkers.iter()))
31            .unwrap_or(itertools::Either::Right(std::iter::empty()))
32    }
33
34    /// Add a new inference checker for the inference code.
35    ///
36    /// An inference code can have multiple checkers, so if an inference checker was already
37    /// registered for the given code, this new checker is simply added to the collection.
38    pub fn add_inference_checker(
39        &mut self,
40        inference_code: InferenceCode,
41        checker: BoxedChecker<Predicate>,
42    ) {
43        self.inference_checkers
44            .entry(inference_code.clone())
45            .or_default()
46            .push(checker);
47    }
48}
pumpkin_core/checkers/store.rs

pumpkin_core/checkers/
store.rs
