pumpkin_core/propagation/contexts/
explanation_context.rs

1use std::sync::LazyLock;
2
3use crate::basic_types::PredicateId;
4use crate::basic_types::PredicateIdGenerator;
5use crate::containers::KeyValueHeap;
6use crate::engine::Assignments;
7use crate::engine::TrailedValues;
8use crate::engine::notifications::NotificationEngine;
9use crate::predicates::Predicate;
10use crate::propagation::HasAssignments;
11#[cfg(doc)]
12use crate::propagation::Propagator;
13
14/// The context that is available when lazily explaining propagations.
15///
16/// See [`Propagator`] for more information.
17#[derive(Debug)]
18pub struct ExplanationContext<'a> {
19    assignments: &'a Assignments,
20    pub(crate) notification_engine: &'a mut NotificationEngine,
21    current_nogood: CurrentNogood<'a>,
22    trail_position: usize,
23}
24
25impl<'a> ExplanationContext<'a> {
26    #[cfg(test)]
27    pub(crate) fn test_new(
28        value: &'a Assignments,
29        notification_engine: &'a mut NotificationEngine,
30    ) -> Self {
31        ExplanationContext {
32            assignments: value,
33            notification_engine,
34            current_nogood: CurrentNogood::empty(),
35            trail_position: 0,
36        }
37    }
38
39    pub(crate) fn new(
40        assignments: &'a Assignments,
41        current_nogood: CurrentNogood<'a>,
42        trail_position: usize,
43        notification_engine: &'a mut NotificationEngine,
44    ) -> Self {
45        ExplanationContext {
46            assignments,
47            current_nogood,
48            trail_position,
49            notification_engine,
50        }
51    }
52
53    pub(crate) fn without_working_nogood(
54        assignments: &'a Assignments,
55        trail_position: usize,
56        notification_engine: &'a mut NotificationEngine,
57    ) -> Self {
58        ExplanationContext {
59            assignments,
60            current_nogood: CurrentNogood::empty(),
61            trail_position,
62            notification_engine,
63        }
64    }
65
66    pub fn get_predicate(&mut self, predicate_id: PredicateId) -> Predicate {
67        self.notification_engine.get_predicate(predicate_id)
68    }
69
70    /// Get the current working nogood.
71    ///
72    /// The working nogood does not necessarily contain the predicate that is being explained.
73    /// However, the explanation will be used to either resolve with the working nogood or minimize
74    /// it some other way.
75    pub fn working_nogood(&self) -> impl Iterator<Item = Predicate> + '_ {
76        self.current_nogood.iter()
77    }
78
79    /// Returns the trail position before which the propagation took place.
80    ///
81    /// For example, if the context is created for explaining a predicate `[x >= v]` at trail
82    /// position i, then this method will return `i - 1`
83    pub fn get_trail_position(&self) -> usize {
84        self.trail_position - 1
85    }
86}
87
88impl HasAssignments for ExplanationContext<'_> {
89    fn assignments(&self) -> &Assignments {
90        self.assignments
91    }
92
93    fn trailed_values(&self) -> &TrailedValues {
94        unimplemented!("Currently, this information cannot be retrieved using this structure")
95    }
96
97    fn trailed_values_mut(&mut self) -> &mut TrailedValues {
98        unimplemented!("Currently, this information cannot be retrieved using this structure")
99    }
100}
101
102static EMPTY_HEAP: KeyValueHeap<PredicateId, u32> = KeyValueHeap::new();
103
104static EMPTY_PREDICATE_IDS: LazyLock<PredicateIdGenerator> =
105    LazyLock::new(PredicateIdGenerator::default);
106
107static EMPTY_PREDICATES: [Predicate; 0] = [];
108
109/// The current nogood that is being analyzed.
110///
111/// Can be used by propagators to guide how they explain their propagations.
112#[derive(Debug)]
113pub struct CurrentNogood<'a> {
114    heap: &'a KeyValueHeap<PredicateId, u32>,
115    visited: &'a [Predicate],
116    ids: &'a PredicateIdGenerator,
117}
118
119impl<'a> CurrentNogood<'a> {
120    pub fn new(
121        heap: &'a KeyValueHeap<PredicateId, u32>,
122        visited: &'a [Predicate],
123        ids: &'a PredicateIdGenerator,
124    ) -> Self {
125        Self { heap, visited, ids }
126    }
127
128    pub fn empty() -> CurrentNogood<'a> {
129        // The variable here is necessary for lifetime coersion.
130        let reference: &[Predicate] = &EMPTY_PREDICATES;
131        Self::from(reference)
132    }
133
134    fn iter<'this, 'ids>(&'this self) -> impl Iterator<Item = Predicate> + 'this
135    where
136        'ids: 'this,
137    {
138        self.heap
139            .keys()
140            .map(|id| self.ids.get_predicate(id))
141            .chain(self.visited.iter().copied())
142    }
143}
144
145impl<'a> From<&'a [Predicate]> for CurrentNogood<'a> {
146    fn from(value: &'a [Predicate]) -> Self {
147        CurrentNogood {
148            heap: &EMPTY_HEAP,
149            visited: value,
150            ids: &EMPTY_PREDICATE_IDS,
151        }
152    }
153}
pumpkin_core/propagation/contexts/explanation_context.rs

pumpkin_core/propagation/contexts/
explanation_context.rs
