resolvo/solver/
decision_tracker.rs

1use crate::internal::id::{ClauseId, VariableId};
2use crate::solver::{decision::Decision, decision_map::DecisionMap};
3
4/// Tracks the assignments to solvables, keeping a log that can be used to backtrack, and a map that
5/// can be used to query the current value assigned
6#[derive(Default)]
7pub(crate) struct DecisionTracker {
8    map: DecisionMap,
9    stack: Vec<Decision>,
10    propagate_index: usize,
11}
12
13impl DecisionTracker {
14    pub(crate) fn clear(&mut self) {
15        *self = Default::default();
16    }
17
18    #[cfg(feature = "diagnostics")]
19    pub(crate) fn len(&self) -> usize {
20        self.map.len()
21    }
22
23    #[inline(always)]
24    pub(crate) fn assigned_value(&self, variable_id: VariableId) -> Option<bool> {
25        self.map.value(variable_id)
26    }
27
28    pub(crate) fn map(&self) -> &DecisionMap {
29        &self.map
30    }
31
32    pub(crate) fn stack(&self) -> impl DoubleEndedIterator<Item = Decision> + '_ {
33        self.stack.iter().copied()
34    }
35
36    pub(crate) fn level(&self, variable_id: VariableId) -> u32 {
37        self.map.level(variable_id)
38    }
39
40    // Find the clause that caused the assignment of the specified solvable. If no assignment has
41    // been made to the solvable than `None` is returned.
42    pub(crate) fn find_clause_for_assignment(&self, variable_id: VariableId) -> Option<ClauseId> {
43        self.stack
44            .iter()
45            .find(|d| d.variable == variable_id)
46            .map(|d| d.derived_from)
47    }
48
49    /// Attempts to add a decision
50    ///
51    /// Returns true if the solvable was undecided, false if it was already decided to the same value
52    ///
53    /// Returns an error if the solvable was decided to a different value (which means there is a conflict)
54    pub(crate) fn try_add_decision(&mut self, decision: Decision, level: u32) -> Result<bool, ()> {
55        match self.map.value(decision.variable) {
56            None => {
57                self.map.set(decision.variable, decision.value, level);
58                self.stack.push(decision);
59                Ok(true)
60            }
61            Some(value) if value == decision.value => Ok(false),
62            _ => Err(()),
63        }
64    }
65
66    pub(crate) fn undo_until(&mut self, level: u32) {
67        if level == 0 {
68            self.clear();
69            return;
70        }
71
72        while let Some(decision) = self.stack.last() {
73            if self.level(decision.variable) <= level {
74                break;
75            }
76
77            self.undo_last();
78        }
79    }
80
81    pub(crate) fn undo_last(&mut self) -> (Decision, u32) {
82        let decision = self.stack.pop().unwrap();
83        self.map.reset(decision.variable);
84
85        self.propagate_index = self.stack.len();
86
87        let top_decision = self.stack.last().unwrap();
88        (decision, self.map.level(top_decision.variable))
89    }
90
91    /// Returns the next decision in the log for which unit propagation still needs to run
92    ///
93    /// Side-effect: the decision will be marked as propagated
94    pub(crate) fn next_unpropagated(&mut self) -> Option<Decision> {
95        let &decision = self.stack[self.propagate_index..].iter().next()?;
96        self.propagate_index += 1;
97        Some(decision)
98    }
99}
resolvo/solver/decision_tracker.rs

resolvo/solver/
decision_tracker.rs
