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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99

use pumpkin_checking::BoxedChecker;
use pumpkin_checking::InferenceChecker;

use crate::predicates::Predicate;
use crate::proof::ConstraintTag;
use crate::proof::InferenceCode;
use crate::proof::InferenceLabel;
#[cfg(doc)]
use crate::propagation::PropagatorConstructor;

/// Holds the runtime checkers that are added by a propagator.
///
/// Used when creating a new propagator in [`PropagatorConstructor::create`].
#[derive(Clone, Debug)]
pub struct RuntimeCheckers {
    inference_checkers: Vec<(InferenceCode, BoxedChecker<Predicate>)>,
}

impl RuntimeCheckers {
    /// Create a [`RuntimeCheckers`] value which we accept may be empty.
    ///
    /// This is often not what you want. If it is expected that some checkers should be added,
    /// use [`RuntimeCheckers::builder`] instead to communicate that intention.
    pub fn empty() -> RuntimeCheckers {
        RuntimeCheckers {
            inference_checkers: vec![],
        }
    }

    /// Create a [`RuntimeCheckersBuilder`] to add runtime checkers.
    ///
    /// The [`RuntimeCheckersBuilder::build`] will panic if no checkers are added.
    pub fn builder() -> RuntimeCheckersBuilder {
        RuntimeCheckersBuilder {
            checkers: RuntimeCheckers {
                inference_checkers: vec![],
            },
        }
    }

    /// Add an [`InferenceChecker`] to verify the soundness of propagations.
    pub fn add_inference_checker(
        &mut self,
        constraint_tag: ConstraintTag,
        inference_label: impl InferenceLabel,
        checker: impl InferenceChecker<Predicate> + 'static,
    ) -> InferenceCode {
        let inference_code = InferenceCode::new(constraint_tag, inference_label);

        self.inference_checkers
            .push((inference_code.clone(), BoxedChecker::new(Box::new(checker))));

        inference_code
    }
}

impl IntoIterator for RuntimeCheckers {
    type Item = (InferenceCode, BoxedChecker<Predicate>);

    type IntoIter = std::vec::IntoIter<Self::Item>;

    fn into_iter(self) -> Self::IntoIter {
        self.inference_checkers.into_iter()
    }
}

/// A builder for the [`RuntimeCheckers`] that ensures at least one checker is added.
#[derive(Clone, Debug)]
pub struct RuntimeCheckersBuilder {
    checkers: RuntimeCheckers,
}

impl RuntimeCheckersBuilder {
    /// Add an [`InferenceChecker`] to verify the soundness of propagations.
    pub fn add_inference_checker(
        &mut self,
        constraint_tag: ConstraintTag,
        inference_label: impl InferenceLabel,
        checker: impl InferenceChecker<Predicate> + 'static,
    ) -> InferenceCode {
        self.checkers
            .add_inference_checker(constraint_tag, inference_label, checker)
    }

    /// Finish adding runtime checkers.
    ///
    /// Panics if runtime verification is enabled and no checkers are added. If it is expected
    /// behavior that no checkers are added, use [`RuntimeCheckers::empty`].
    pub fn build(self) -> RuntimeCheckers {
        if cfg!(feature = "check-propagations") {
            assert!(
                !self.checkers.inference_checkers.is_empty(),
                "did not register any inference checkers"
            );
        }

        self.checkers
    }
}