vivacity_resolver/
watch.rs

1//! Port of `RuleWatchGraph`, `RuleWatchNode`, `RuleWatchChain`: two watched
2//! literals per rule (all of them for a MultiConflictRule), one chain per
3//! literal, inserted at the head of the list (`unshift`).
4
5use crate::decisions::{Decisions, SolverBug};
6use crate::rule::{RuleKind, RuleSet};
7use std::collections::{HashMap, VecDeque};
8
9#[derive(Debug, Clone)]
10pub struct RuleWatchNode {
11    pub rule: usize,
12    pub watch1: i64,
13    pub watch2: i64,
14}
15
16impl RuleWatchNode {
17    pub fn new(rules: &RuleSet, rule: usize) -> RuleWatchNode {
18        let literals = &rules.rules[rule].literals;
19        RuleWatchNode {
20            rule,
21            watch1: literals.first().copied().unwrap_or(0),
22            watch2: literals.get(1).copied().unwrap_or(0),
23        }
24    }
25
26    /// `watch2OnHighest`.
27    pub fn watch2_on_highest(&mut self, rules: &RuleSet, decisions: &Decisions) {
28        let rule = &rules.rules[self.rule];
29        if rule.literals.len() < 3 || rule.kind == RuleKind::MultiConflict {
30            return;
31        }
32        let mut watch_level = 0;
33        for &literal in &rule.literals {
34            let level = decisions.decision_level(literal);
35            if level > watch_level {
36                self.watch2 = literal;
37                watch_level = level;
38            }
39        }
40    }
41
42    pub fn other_watch(&self, literal: i64) -> i64 {
43        if self.watch1 == literal {
44            self.watch2
45        } else {
46            self.watch1
47        }
48    }
49
50    pub fn move_watch(&mut self, from: i64, to: i64) {
51        if self.watch1 == from {
52            self.watch1 = to;
53        } else {
54            self.watch2 = to;
55        }
56    }
57}
58
59#[derive(Debug, Default)]
60pub struct RuleWatchGraph {
61    pub nodes: Vec<RuleWatchNode>,
62    /// literal -> nodes, head of the list first.
63    chains: HashMap<i64, VecDeque<usize>>,
64}
65
66impl RuleWatchGraph {
67    pub fn new() -> RuleWatchGraph {
68        RuleWatchGraph::default()
69    }
70
71    /// `insert`: nothing for an assertion.
72    pub fn insert(&mut self, rules: &RuleSet, node: RuleWatchNode) {
73        let rule = &rules.rules[node.rule];
74        if rule.is_assertion() {
75            return;
76        }
77        let node_id = self.nodes.len();
78        let literals: Vec<i64> = if rule.kind != RuleKind::MultiConflict {
79            vec![node.watch1, node.watch2]
80        } else {
81            rule.literals.clone()
82        };
83        self.nodes.push(node);
84        for literal in literals {
85            self.chains.entry(literal).or_default().push_front(node_id);
86        }
87    }
88
89    /// `propagateLiteral`: returns the conflicting rule, if any.
90    pub fn propagate_literal(
91        &mut self,
92        rules: &RuleSet,
93        decided_literal: i64,
94        level: i64,
95        decisions: &mut Decisions,
96    ) -> Result<Option<usize>, SolverBug> {
97        let literal = -decided_literal;
98        if !self.chains.contains_key(&literal) {
99            return Ok(None);
100        }
101        let mut cursor = 0;
102        while let Some(&node_id) = self.chains.get(&literal).and_then(|c| c.get(cursor)) {
103            let rule_id = self.nodes[node_id].rule;
104            let rule = &rules.rules[rule_id];
105            if rule.kind != RuleKind::MultiConflict {
106                let other_watch = self.nodes[node_id].other_watch(literal);
107                if !rule.disabled && !decisions.satisfy(other_watch) {
108                    let alternative = rule
109                        .literals
110                        .iter()
111                        .copied()
112                        .find(|&l| l != literal && l != other_watch && !decisions.conflict(l));
113                    if let Some(alternative) = alternative {
114                        self.move_watch(literal, alternative, node_id, cursor);
115                        // `continue` without `next()`: the next element has
116                        // taken this position.
117                        continue;
118                    }
119                    if decisions.conflict(other_watch) {
120                        return Ok(Some(rule_id));
121                    }
122                    decisions.decide(other_watch, level, rule_id)?;
123                }
124            } else {
125                for &other in &rule.literals {
126                    if literal != other && !decisions.satisfy(other) {
127                        if decisions.conflict(other) {
128                            return Ok(Some(rule_id));
129                        }
130                        decisions.decide(other, level, rule_id)?;
131                    }
132                }
133            }
134            cursor += 1;
135        }
136        Ok(None)
137    }
138
139    /// `moveWatch`: removes the node from the current chain (at the cursor
140    /// position) and puts it at the head of the target chain.
141    fn move_watch(&mut self, from: i64, to: i64, node_id: usize, cursor: usize) {
142        self.nodes[node_id].move_watch(from, to);
143        if let Some(chain) = self.chains.get_mut(&from) {
144            chain.remove(cursor);
145        }
146        self.chains.entry(to).or_default().push_front(node_id);
147    }
148}
vivacity_resolver/watch.rs

vivacity_resolver/
watch.rs
