propaga_core/
reason.rs

1use crate::{PropagatorId, VariableId};
2
3/// Kind of bound tightening applied to a domain.
4#[derive(Clone, Copy, Debug, PartialEq, Eq)]
5pub enum BoundKind {
6    /// Values strictly below the bound were removed.
7    Below,
8    /// Values strictly above the bound were removed.
9    Above,
10}
11
12/// Why a domain change occurred.
13#[derive(Clone, Debug, PartialEq, Eq)]
14pub enum ChangeReason {
15    /// Search assigned a value during branching.
16    Branch { variable: VariableId, value: i32 },
17    /// A propagator removed values or tightened bounds.
18    Propagator {
19        propagator: PropagatorId,
20        variable: VariableId,
21        removed_value: Option<i32>,
22        bound: Option<(BoundKind, i32)>,
23    },
24    /// A propagator detected infeasibility and recorded contributing assignments.
25    PropagatorConflict {
26        /// Branch literals that jointly caused the conflict.
27        literals: Vec<(VariableId, i32)>,
28    },
29}
30
31/// Collected explanation for the latest conflict or propagation round.
32#[derive(Clone, Debug, Default, PartialEq, Eq)]
33pub struct Explanation {
34    entries: Vec<ChangeReason>,
35}
36
37impl Explanation {
38    /// Creates an empty explanation.
39    #[must_use]
40    pub fn new() -> Self {
41        Self {
42            entries: Vec::new(),
43        }
44    }
45
46    /// Returns recorded change reasons.
47    #[must_use]
48    pub fn entries(&self) -> &[ChangeReason] {
49        &self.entries
50    }
51
52    /// Records a change reason.
53    pub fn record(&mut self, reason: ChangeReason) {
54        self.entries.push(reason);
55    }
56
57    /// Clears all recorded reasons.
58    pub fn reset(&mut self) {
59        self.entries.clear();
60    }
61
62    /// Truncates the log to the first `len` entries.
63    pub fn truncate(&mut self, len: usize) {
64        self.entries.truncate(len);
65    }
66}
67
68#[cfg(test)]
69mod tests {
70    use super::*;
71    use crate::VariableId;
72    use slotmap::SlotMap;
73
74    fn make_var() -> VariableId {
75        let mut sm: SlotMap<crate::VariableKey, ()> = SlotMap::with_key();
76        VariableId::from_key(sm.insert(()))
77    }
78
79    #[test]
80    fn records_and_resets_entries() {
81        let mut explanation = Explanation::new();
82        assert!(explanation.entries().is_empty());
83        explanation.record(ChangeReason::Branch {
84            variable: make_var(),
85            value: 1,
86        });
87        assert_eq!(explanation.entries().len(), 1);
88        explanation.reset();
89        assert!(explanation.entries().is_empty());
90    }
91
92    #[test]
93    fn truncates_to_prefix() {
94        let mut explanation = Explanation::new();
95        for value in 1..=3 {
96            explanation.record(ChangeReason::Branch {
97                variable: make_var(),
98                value,
99            });
100        }
101        explanation.truncate(2);
102        assert_eq!(explanation.entries().len(), 2);
103    }
104}
propaga_core/reason.rs

propaga_core/
reason.rs
