biodivine_lib_bdd/
_impl_bdd_path_iterator.rs

1use crate::{Bdd, BddPartialValuation, BddPathIterator, BddPointer, OwnedBddPathIterator};
2
3impl BddPathIterator<'_> {
4    pub fn new(bdd: &Bdd) -> BddPathIterator<'_> {
5        if bdd.is_false() {
6            BddPathIterator {
7                bdd,
8                stack: Vec::new(),
9            }
10        } else {
11            let mut stack = vec![bdd.root_pointer()];
12            continue_path(bdd, &mut stack); // Compute the first valid path.
13            BddPathIterator { bdd, stack }
14        }
15    }
16}
17
18impl OwnedBddPathIterator {
19    pub fn new(bdd: Bdd) -> OwnedBddPathIterator {
20        if bdd.is_false() {
21            OwnedBddPathIterator {
22                bdd,
23                stack: Vec::new(),
24            }
25        } else {
26            let mut stack = vec![bdd.root_pointer()];
27            continue_path(&bdd, &mut stack); // Compute the first valid path.
28            OwnedBddPathIterator { bdd, stack }
29        }
30    }
31}
32
33impl From<Bdd> for OwnedBddPathIterator {
34    fn from(value: Bdd) -> Self {
35        OwnedBddPathIterator::new(value)
36    }
37}
38
39impl From<OwnedBddPathIterator> for Bdd {
40    fn from(value: OwnedBddPathIterator) -> Self {
41        value.bdd
42    }
43}
44
45impl Iterator for BddPathIterator<'_> {
46    type Item = BddPartialValuation;
47
48    fn next(&mut self) -> Option<Self::Item> {
49        if self.stack.is_empty() {
50            None
51        } else {
52            let item = make_clause(self.bdd, &self.stack);
53
54            // Now, we need to pop the path until we find a node with a valid successor,
55            // and then extend the path using `continue_path`.
56
57            let mut last_child = self.stack.pop().unwrap();
58
59            while let Some(top) = self.stack.last() {
60                if self.bdd.low_link_of(*top) == last_child {
61                    // Try to advance to the high link.
62                    if self.bdd.high_link_of(*top).is_zero() {
63                        // If high link is zero, we cannot advance and have to pop.
64                        last_child = *top;
65                        self.stack.pop();
66                    } else {
67                        // This is a sanity check which prevents the method from looping on
68                        // non-canonical BDDs.
69                        if self.bdd.low_link_of(*top) == self.bdd.high_link_of(*top) {
70                            panic!("The BDD is not canonical.");
71                        }
72
73                        let new_entry = self.bdd.high_link_of(*top);
74                        self.stack.push(new_entry);
75                        continue_path(self.bdd, &mut self.stack);
76                        break;
77                    }
78                } else if self.bdd.high_link_of(*top) == last_child {
79                    // Both low and high links have been processed,
80                    // so we can only pop to the next node.
81                    last_child = *top;
82                    self.stack.pop();
83                } else {
84                    // Just a sanity check. This should be unreachable.
85                    unreachable!("Invalid path data in iterator.");
86                }
87            }
88
89            // Here, either a path was found and extended, or the stack is empty and this was
90            // the last item.
91
92            Some(item)
93        }
94    }
95}
96
97/// This is just a copy of [BddPathIterator] code with adjusted ownership/references.
98impl Iterator for OwnedBddPathIterator {
99    type Item = BddPartialValuation;
100
101    fn next(&mut self) -> Option<Self::Item> {
102        if self.stack.is_empty() {
103            None
104        } else {
105            let item = make_clause(&self.bdd, &self.stack);
106
107            // Now, we need to pop the path until we find a node with a valid successor,
108            // and then extend the path using `continue_path`.
109
110            let mut last_child = self.stack.pop().unwrap();
111
112            while let Some(top) = self.stack.last() {
113                if self.bdd.low_link_of(*top) == last_child {
114                    // Try to advance to the high link.
115                    if self.bdd.high_link_of(*top).is_zero() {
116                        // If high link is zero, we cannot advance and have to pop.
117                        last_child = *top;
118                        self.stack.pop();
119                    } else {
120                        // This is a sanity check which prevents the method from looping on
121                        // non-canonical BDDs.
122                        if self.bdd.low_link_of(*top) == self.bdd.high_link_of(*top) {
123                            panic!("The BDD is not canonical.");
124                        }
125
126                        let new_entry = self.bdd.high_link_of(*top);
127                        self.stack.push(new_entry);
128                        continue_path(&self.bdd, &mut self.stack);
129                        break;
130                    }
131                } else if self.bdd.high_link_of(*top) == last_child {
132                    // Both low and high links have been processed,
133                    // so we can only pop to the next node.
134                    last_child = *top;
135                    self.stack.pop();
136                } else {
137                    // Just a sanity check. This should be unreachable.
138                    unreachable!("Invalid path data in iterator.");
139                }
140            }
141
142            // Here, either a path was found and extended, or the stack is empty and this was
143            // the last item.
144
145            Some(item)
146        }
147    }
148}
149
150/// **(internal)** Given a prefix of a path in a BDD, continue the prefix, always choosing
151/// the low link unless it leads to a false leaf.
152///
153/// The input path must be non-empty.
154fn continue_path(bdd: &Bdd, path: &mut Vec<BddPointer>) {
155    assert!(!path.is_empty());
156    loop {
157        let top = *path.last().unwrap();
158        if top.is_one() {
159            return;
160        }
161
162        if !bdd.low_link_of(top).is_zero() {
163            path.push(bdd.low_link_of(top));
164        } else if !bdd.high_link_of(top).is_zero() {
165            path.push(bdd.high_link_of(top));
166        } else {
167            panic!("The given BDD is not canonical.");
168        }
169    }
170}
171
172/// **(internal)** Convert a path in a `Bdd` saved as a stack into a clause.
173///
174/// The path must end with a pointer to the one-terminal node.
175fn make_clause(bdd: &Bdd, path: &[BddPointer]) -> BddPartialValuation {
176    let mut result = BddPartialValuation::empty();
177    for i in 0..(path.len() - 1) {
178        let this_node = path[i];
179        let next_node = path[i + 1];
180        let var = bdd.var_of(this_node);
181
182        if bdd.low_link_of(this_node) == next_node {
183            result.set_value(var, false);
184        } else if bdd.high_link_of(this_node) == next_node {
185            result.set_value(var, true);
186        } else {
187            panic!("Path {path:?} is not valid in BDD {bdd:?}");
188        }
189    }
190
191    result
192}
193
194#[cfg(test)]
195mod tests {
196    use crate::{Bdd, BddPartialValuation, BddPathIterator, BddVariable, BddVariableSet};
197
198    #[test]
199    fn bdd_path_iterator_trivial() {
200        let ff = Bdd::mk_false(10);
201        assert_eq!(0, BddPathIterator::new(&ff).count());
202
203        let tt = Bdd::mk_true(10);
204        assert_eq!(1, BddPathIterator::new(&tt).count());
205
206        let tt = Bdd::mk_true(0);
207        assert_eq!(1, BddPathIterator::new(&tt).count());
208
209        let clause =
210            BddPartialValuation::from_values(&[(BddVariable(1), true), (BddVariable(2), false)]);
211        let vars = BddVariableSet::new_anonymous(10);
212        assert_eq!(
213            1,
214            BddPathIterator::new(&vars.mk_conjunctive_clause(&clause)).count()
215        );
216        assert_eq!(
217            2,
218            BddPathIterator::new(&vars.mk_disjunctive_clause(&clause)).count()
219        );
220    }
221
222    #[test]
223    fn bdd_path_iterator() {
224        let vars = BddVariableSet::new_anonymous(5);
225        let v = vars.variables();
226
227        let c1 = BddPartialValuation::from_values(&[(v[0], true), (v[1], false)]);
228        let c2 = BddPartialValuation::from_values(&[(v[1], true), (v[3], false)]);
229        let c3 = BddPartialValuation::from_values(&[(v[2], false), (v[4], true)]);
230        let bdd = vars.mk_dnf(&[c1.clone(), c2.clone(), c3.clone()]);
231
232        // println!("{}", bdd.to_dot_string(&vars, true));
233        // Counted manually in the .dot graph:
234        assert_eq!(8, BddPathIterator::new(&bdd).count());
235
236        BddPathIterator::new(&bdd).for_each(|path| {
237            assert!(path.extends(&c1) || path.extends(&c2) || path.extends(&c3));
238        });
239    }
240}
biodivine_lib_bdd/_impl_bdd_path_iterator.rs

biodivine_lib_bdd/
_impl_bdd_path_iterator.rs
