vivacity_resolver/
decisions.rs

1//! Port of `Composer\DependencyResolver\Decisions`: the decision map
2//! (package -> +/-level) and the decision queue with its rules.
3
4#[derive(Debug, thiserror::Error)]
5#[error("{0}")]
6pub struct SolverBug(pub String);
7
8#[derive(Debug, Clone, Copy)]
9pub struct Decision {
10    pub literal: i64,
11    /// Rule id (`DECISION_REASON`).
12    pub reason: usize,
13}
14
15#[derive(Debug, Clone)]
16pub struct Decisions {
17    /// Indexed by pool id (1-based; 0 unused): 0 = undecided, > 0 =
18    /// installed at that level, < 0 = rejected at that level.
19    map: Vec<i64>,
20    pub queue: Vec<Decision>,
21}
22
23impl Decisions {
24    pub fn new(pool_size: usize) -> Decisions {
25        Decisions {
26            map: vec![0; pool_size + 1],
27            queue: Vec::new(),
28        }
29    }
30
31    fn entry(&self, literal_or_id: i64) -> i64 {
32        let id = literal_or_id.unsigned_abs() as usize;
33        self.map.get(id).copied().unwrap_or(0)
34    }
35
36    pub fn decide(&mut self, literal: i64, level: i64, reason: usize) -> Result<(), SolverBug> {
37        self.add_decision(literal, level)?;
38        self.queue.push(Decision { literal, reason });
39        Ok(())
40    }
41
42    pub fn satisfy(&self, literal: i64) -> bool {
43        let d = self.entry(literal);
44        (literal > 0 && d > 0) || (literal < 0 && d < 0)
45    }
46
47    pub fn conflict(&self, literal: i64) -> bool {
48        let d = self.entry(literal);
49        (d > 0 && literal < 0) || (d < 0 && literal > 0)
50    }
51
52    pub fn decided(&self, literal_or_id: i64) -> bool {
53        self.entry(literal_or_id) != 0
54    }
55
56    pub fn undecided(&self, literal_or_id: i64) -> bool {
57        self.entry(literal_or_id) == 0
58    }
59
60    pub fn decided_install(&self, literal_or_id: i64) -> bool {
61        self.entry(literal_or_id) > 0
62    }
63
64    pub fn decision_level(&self, literal_or_id: i64) -> i64 {
65        self.entry(literal_or_id).abs()
66    }
67
68    /// `decisionRule`: the rule of the first decision on this package.
69    pub fn decision_rule(&self, literal_or_id: i64) -> Result<usize, SolverBug> {
70        let id = literal_or_id.abs();
71        self.queue
72            .iter()
73            .find(|d| d.literal.abs() == id)
74            .map(|d| d.reason)
75            .ok_or_else(|| {
76                SolverBug(format!(
77                    "Did not find a decision rule using {literal_or_id}"
78                ))
79            })
80    }
81
82    pub fn at_offset(&self, offset: usize) -> Decision {
83        self.queue[offset]
84    }
85
86    pub fn valid_offset(&self, offset: usize) -> bool {
87        offset < self.queue.len()
88    }
89
90    pub fn last_reason(&self) -> usize {
91        self.queue[self.queue.len() - 1].reason
92    }
93
94    pub fn last_literal(&self) -> i64 {
95        self.queue[self.queue.len() - 1].literal
96    }
97
98    /// `resetToOffset($offset)`: keeps `offset + 1` decisions.
99    pub fn reset_to_offset(&mut self, offset: i64) {
100        while (self.queue.len() as i64) > offset + 1 {
101            let d = self.queue.pop().expect("non-empty");
102            self.map[d.literal.unsigned_abs() as usize] = 0;
103        }
104    }
105
106    pub fn revert_last(&mut self) {
107        let last = self.last_literal();
108        self.map[last.unsigned_abs() as usize] = 0;
109        self.queue.pop();
110    }
111
112    pub fn len(&self) -> usize {
113        self.queue.len()
114    }
115
116    pub fn is_empty(&self) -> bool {
117        self.queue.is_empty()
118    }
119
120    fn add_decision(&mut self, literal: i64, level: i64) -> Result<(), SolverBug> {
121        let id = literal.unsigned_abs() as usize;
122        if id >= self.map.len() {
123            return Err(SolverBug(format!("literal {literal} out of pool")));
124        }
125        let previous = self.map[id];
126        if previous != 0 {
127            return Err(SolverBug(format!(
128                "Trying to decide {literal} on level {level}, even though package {id} was previously decided as {previous}."
129            )));
130        }
131        self.map[id] = if literal > 0 { level } else { -level };
132        Ok(())
133    }
134}
vivacity_resolver/decisions.rs

vivacity_resolver/
decisions.rs
