pumpkin-core 0.5.0

The core of the Pumpkin constraint programming solver.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48

//! This module facilitates runtime verification in Pumpkin. It defines common types as well as the
//! [`CheckerStore`] that owns the checkers that are active in the solver.

use pumpkin_checking::BoxedChecker;
#[cfg(doc)]
use pumpkin_checking::InferenceChecker;

use crate::containers::HashMap;
use crate::predicates::Predicate;
use crate::proof::InferenceCode;

/// Owns the runtime checkers present in the solver.
///
/// The runtime checkers consist of:
/// - inference checkers, which verify that propagations are sound.
#[derive(Clone, Debug, Default)]
pub struct CheckerStore {
    /// For each inference code we associate possibly many inference checkers.
    inference_checkers: HashMap<InferenceCode, Vec<BoxedChecker<Predicate>>>,
}

impl CheckerStore {
    /// Get the [`InferenceChecker`]s for the given inference code.
    pub fn for_inference_code(
        &self,
        inference_code: &InferenceCode,
    ) -> impl ExactSizeIterator<Item = &BoxedChecker<Predicate>> {
        self.inference_checkers
            .get(inference_code)
            .map(|checkers| itertools::Either::Left(checkers.iter()))
            .unwrap_or(itertools::Either::Right(std::iter::empty()))
    }

    /// Add a new inference checker for the inference code.
    ///
    /// An inference code can have multiple checkers, so if an inference checker was already
    /// registered for the given code, this new checker is simply added to the collection.
    pub fn add_inference_checker(
        &mut self,
        inference_code: InferenceCode,
        checker: BoxedChecker<Predicate>,
    ) {
        self.inference_checkers
            .entry(inference_code.clone())
            .or_default()
            .push(checker);
    }
}