boolean_expression/
bdd.rs

1// boolean_expression: a Rust crate for Boolean expressions and BDDs.
2//
3// Copyright (c) 2016 Chris Fallin <cfallin@c1f.net>. Released under the MIT
4// License.
5//
6
7use itertools::Itertools;
8use std::cmp;
9use std::collections::hash_map::Entry as HashEntry;
10use std::collections::{BTreeSet, HashMap, HashSet};
11use std::fmt;
12use std::fmt::Debug;
13use std::hash::Hash;
14use std::usize;
15
16use cubes::{Cube, CubeList, CubeVar};
17use idd::*;
18use Expr;
19
20/// A `BDDFunc` is a function index within a particular `BDD`. It must only
21/// be used with the `BDD` instance which produced it.
22pub type BDDFunc = usize;
23
24/// A special terminal `BDDFunc` which is constant `false` (zero).
25pub const BDD_ZERO: BDDFunc = usize::MAX;
26/// A special terminal `BDDFunc` which is constant `true` (one).
27pub const BDD_ONE: BDDFunc = usize::MAX - 1;
28
29pub(crate) type BDDLabel = usize;
30
31#[derive(Clone, PartialEq, Eq, Hash)]
32pub(crate) struct BDDNode {
33    pub label: BDDLabel,
34    pub lo: BDDFunc,
35    pub hi: BDDFunc,
36    pub varcount: usize,
37}
38
39fn bdd_func_str(b: BDDFunc) -> String {
40    if b == BDD_ZERO {
41        "ZERO".to_owned()
42    } else if b == BDD_ONE {
43        "ONE".to_owned()
44    } else {
45        format!("{}", b)
46    }
47}
48
49impl fmt::Debug for BDDNode {
50    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
51        write!(
52            f,
53            "BDDNode(label = {}, lo = {}, hi = {})",
54            self.label,
55            bdd_func_str(self.lo),
56            bdd_func_str(self.hi)
57        )
58    }
59}
60
61#[derive(Clone, Debug)]
62pub(crate) struct LabelBDD {
63    pub nodes: Vec<BDDNode>,
64    dedup_hash: HashMap<BDDNode, BDDFunc>,
65}
66
67impl LabelBDD {
68    pub fn new() -> LabelBDD {
69        LabelBDD {
70            nodes: Vec::new(),
71            dedup_hash: HashMap::new(),
72        }
73    }
74
75    fn get_node(&mut self, label: BDDLabel, lo: BDDFunc, hi: BDDFunc) -> BDDFunc {
76        if lo == hi {
77            return lo;
78        }
79        let n = BDDNode {
80            label: label,
81            lo: lo,
82            hi: hi,
83            varcount: cmp::min(self.sat_varcount(lo), self.sat_varcount(hi) + 1),
84        };
85        match self.dedup_hash.entry(n.clone()) {
86            HashEntry::Occupied(o) => *o.get(),
87            HashEntry::Vacant(v) => {
88                let idx = self.nodes.len() as BDDFunc;
89                self.nodes.push(n);
90                v.insert(idx);
91                idx
92            }
93        }
94    }
95
96    fn sat_varcount(&self, f: BDDFunc) -> usize {
97        if f == BDD_ZERO || f == BDD_ONE {
98            0
99        } else {
100            self.nodes[f].varcount
101        }
102    }
103
104    pub fn terminal(&mut self, label: BDDLabel) -> BDDFunc {
105        self.get_node(label, BDD_ZERO, BDD_ONE)
106    }
107
108    pub fn constant(&mut self, value: bool) -> BDDFunc {
109        if value {
110            BDD_ONE
111        } else {
112            BDD_ZERO
113        }
114    }
115
116    /// Restrict: fundamental building block of logical combinators. Takes a
117    /// Shannon cofactor: i.e., returns a new function based on `f` but with the
118    /// given label forced to the given value.
119    pub fn restrict(&mut self, f: BDDFunc, label: BDDLabel, val: bool) -> BDDFunc {
120        if f == BDD_ZERO {
121            return BDD_ZERO;
122        }
123        if f == BDD_ONE {
124            return BDD_ONE;
125        }
126
127        let node = self.nodes[f].clone();
128        if label < node.label {
129            f
130        } else if label == node.label {
131            if val {
132                node.hi
133            } else {
134                node.lo
135            }
136        } else {
137            let lo = self.restrict(node.lo, label, val);
138            let hi = self.restrict(node.hi, label, val);
139            self.get_node(node.label, lo, hi)
140        }
141    }
142
143    fn min_label(&self, f: BDDFunc) -> Option<BDDLabel> {
144        if f == BDD_ZERO || f == BDD_ONE {
145            None
146        } else {
147            Some(self.nodes[f].label)
148        }
149    }
150
151    /// If-then-else: fundamental building block of logical combinators. Works
152    /// by divide-and-conquer: split on the lowest appearing label, take Shannon
153    /// cofactors for the two cases, recurse, and recombine with a new node.
154    pub fn ite(&mut self, i: BDDFunc, t: BDDFunc, e: BDDFunc) -> BDDFunc {
155        if i == BDD_ONE {
156            t
157        } else if i == BDD_ZERO {
158            e
159        } else if t == e {
160            t
161        } else if t == BDD_ONE && e == BDD_ZERO {
162            i
163        } else {
164            let i_var = self.min_label(i).unwrap_or(usize::MAX);
165            let t_var = self.min_label(t).unwrap_or(usize::MAX);
166            let e_var = self.min_label(e).unwrap_or(usize::MAX);
167            let split = cmp::min(i_var, cmp::min(t_var, e_var));
168            assert!(split != usize::MAX);
169            let i_lo = self.restrict(i, split, false);
170            let t_lo = self.restrict(t, split, false);
171            let e_lo = self.restrict(e, split, false);
172            let i_hi = self.restrict(i, split, true);
173            let t_hi = self.restrict(t, split, true);
174            let e_hi = self.restrict(e, split, true);
175            let lo = self.ite(i_lo, t_lo, e_lo);
176            let hi = self.ite(i_hi, t_hi, e_hi);
177            self.get_node(split, lo, hi)
178        }
179    }
180
181    pub fn not(&mut self, n: BDDFunc) -> BDDFunc {
182        self.ite(n, BDD_ZERO, BDD_ONE)
183    }
184
185    pub fn and(&mut self, a: BDDFunc, b: BDDFunc) -> BDDFunc {
186        self.ite(a, b, BDD_ZERO)
187    }
188
189    pub fn or(&mut self, a: BDDFunc, b: BDDFunc) -> BDDFunc {
190        self.ite(a, BDD_ONE, b)
191    }
192
193    pub fn xor(&mut self, a: BDDFunc, b: BDDFunc) -> BDDFunc {
194        let not_b = self.not(b);
195        self.ite(a, not_b, b)
196    }
197
198    pub fn implies(&mut self, a: BDDFunc, b: BDDFunc) -> BDDFunc {
199        let not_a = self.not(a);
200        self.or(not_a, b)
201    }
202
203    pub fn evaluate(&self, func: BDDFunc, inputs: &[bool]) -> Option<bool> {
204        let mut f = func;
205        for (i, val) in inputs.iter().enumerate() {
206            if f == BDD_ZERO || f == BDD_ONE {
207                break;
208            }
209            let node = &self.nodes[f];
210            if node.label > i {
211                continue;
212            } else if node.label == i {
213                f = if *val { node.hi } else { node.lo };
214            }
215        }
216        match f {
217            BDD_ZERO => Some(false),
218            BDD_ONE => Some(true),
219            _ => None,
220        }
221    }
222
223    fn compute_cubelist(&self, memoize_vec: &mut Vec<Option<CubeList>>, n: BDDFunc, nvars: usize) {
224        if memoize_vec[n].is_some() {
225            return;
226        }
227        let label = self.nodes[n].label;
228        let lo = self.nodes[n].lo;
229        let hi = self.nodes[n].hi;
230        let lo_list = match lo {
231            BDD_ZERO => CubeList::new(),
232            BDD_ONE => CubeList::from_list(&[Cube::true_cube(nvars)])
233                .with_var(label as usize, CubeVar::False),
234            _ => {
235                self.compute_cubelist(memoize_vec, lo, nvars);
236                memoize_vec[lo]
237                    .as_ref()
238                    .unwrap()
239                    .with_var(label as usize, CubeVar::False)
240            }
241        };
242        let hi_list = match hi {
243            BDD_ZERO => CubeList::new(),
244            BDD_ONE => CubeList::from_list(&[Cube::true_cube(nvars)])
245                .with_var(label as usize, CubeVar::True),
246            _ => {
247                self.compute_cubelist(memoize_vec, hi, nvars);
248                memoize_vec[hi]
249                    .as_ref()
250                    .unwrap()
251                    .with_var(label as usize, CubeVar::True)
252            }
253        };
254        let new_list = lo_list.merge(&hi_list);
255        memoize_vec[n] = Some(new_list);
256    }
257
258    fn cube_to_expr(&self, c: &Cube) -> Expr<BDDLabel> {
259        c.vars()
260            .enumerate()
261            .flat_map(|(i, v)| match v {
262                &CubeVar::False => Some(Expr::not(Expr::Terminal(i))),
263                &CubeVar::True => Some(Expr::Terminal(i)),
264                &CubeVar::DontCare => None,
265            })
266            .fold1(|a, b| Expr::and(a, b))
267            .unwrap_or(Expr::Const(true))
268    }
269
270    fn cubelist_to_expr(&self, c: &CubeList) -> Expr<BDDLabel> {
271        c.cubes()
272            .map(|c| self.cube_to_expr(c))
273            .fold1(|a, b| Expr::or(a, b))
274            .unwrap_or(Expr::Const(false))
275    }
276
277    pub fn to_expr(&self, func: BDDFunc, nvars: usize) -> Expr<BDDLabel> {
278        if func == BDD_ZERO {
279            Expr::Const(false)
280        } else if func == BDD_ONE {
281            Expr::Const(true)
282        } else {
283            // At each node, we construct a cubelist, starting from the roots.
284            let mut cubelists: Vec<Option<CubeList>> = Vec::with_capacity(self.nodes.len());
285            cubelists.resize(self.nodes.len(), None);
286            self.compute_cubelist(&mut cubelists, func, nvars);
287            self.cubelist_to_expr(cubelists[func].as_ref().unwrap())
288        }
289    }
290
291    /// Returns a function that is true whenever the maximum number of
292    /// functions in `funcs` are true.
293    pub fn max_sat(&mut self, funcs: &[BDDFunc]) -> BDDFunc {
294        // First, construct an IDD function for each BDD function,
295        // with value 1 if true and 0 if false. Then add these
296        // together to obtain a single IDD function whose value is the
297        // number of satisfied (true) BDD functions.
298        let mut idd = LabelIDD::from_bdd(self);
299        let idd_funcs: Vec<_> = funcs.iter().map(|f| idd.from_bdd_func(*f)).collect();
300        let satisfied_count = idd_funcs
301            .iter()
302            .cloned()
303            .fold1(|a, b| idd.add(a.clone(), b.clone()))
304            .unwrap();
305
306        // Now, find the maximum reachable count.
307        let max_count = idd.max_value(satisfied_count.clone());
308
309        // Finally, return a boolean function that is true when the
310        // maximal number of functions are satisfied.
311        let c = idd.constant(max_count);
312        idd.eq(satisfied_count, c, self)
313    }
314}
315
316/// A `BDD` is a Binary Decision Diagram, an efficient way to represent a
317/// Boolean function in a canonical way. (It is actually a "Reduced Ordered
318/// Binary Decision Diagram", which gives it its canonicity assuming terminals
319/// are ordered consistently.)
320///
321/// A BDD is built up from terminals (free variables) and constants, combined
322/// with the logical combinators AND, OR, and NOT. It may be evaluated with
323/// certain terminal assignments.
324///
325/// The major advantage of a BDD is that its logical operations are performed,
326/// it will "self-simplify": i.e., taking the OR of `And(a, b)` and `And(a,
327/// Not(b))` will produce `a` without any further simplification step. Furthermore,
328/// the `BDDFunc` representing this value is canonical: if two different
329/// expressions are produced within the same BDD and they both result in
330/// (simplify down to) `a`, then the `BDDFunc` values will be equal. The
331/// tradeoff is that logical operations may be expensive: they are linear in
332/// BDD size, but BDDs may have exponential size (relative to terminal count)
333/// in the worst case.
334#[derive(Clone, Debug)]
335pub struct BDD<T>
336where
337    T: Clone + Debug + Eq + Hash,
338{
339    bdd: LabelBDD,
340    labels: HashMap<T, BDDLabel>,
341    rev_labels: Vec<T>,
342}
343
344impl<T> BDD<T>
345where
346    T: Clone + Debug + Eq + Hash,
347{
348    /// Produce a new, empty, BDD.
349    pub fn new() -> BDD<T> {
350        BDD {
351            bdd: LabelBDD::new(),
352            labels: HashMap::new(),
353            rev_labels: Vec::new(),
354        }
355    }
356
357    fn label(&mut self, t: T) -> BDDLabel {
358        match self.labels.entry(t.clone()) {
359            HashEntry::Occupied(o) => *o.get(),
360            HashEntry::Vacant(v) => {
361                let next_id = self.rev_labels.len() as BDDLabel;
362                v.insert(next_id);
363                self.rev_labels.push(t);
364                next_id
365            }
366        }
367    }
368
369    /// Produce a function within the BDD representing the terminal `t`. If
370    /// this terminal has been used in the BDD before, the same `BDDFunc` will be
371    /// returned.
372    pub fn terminal(&mut self, t: T) -> BDDFunc {
373        let l = self.label(t);
374        self.bdd.terminal(l)
375    }
376
377    /// Produce a function within the BDD representing the constant value `val`.
378    pub fn constant(&mut self, val: bool) -> BDDFunc {
379        self.bdd.constant(val)
380    }
381
382    /// Produce a function within the BDD representing the logical if-then-else
383    /// of the functions `i`, `t`, and `e`
384    pub fn ite(&mut self, i: BDDFunc, t: BDDFunc, e: BDDFunc) -> BDDFunc {
385        self.bdd.ite(i, t, e)
386    }
387
388    /// Produce a function within the BDD representing the logical complement
389    /// of the function `n`.
390    pub fn not(&mut self, n: BDDFunc) -> BDDFunc {
391        self.bdd.not(n)
392    }
393
394    /// Produce a function within the BDD representing the logical AND of the
395    /// functions `a` and `b`.
396    pub fn and(&mut self, a: BDDFunc, b: BDDFunc) -> BDDFunc {
397        self.bdd.and(a, b)
398    }
399
400    /// Produce a function within the BDD representing the logical OR of the
401    /// functions `a` and `b`.
402    pub fn or(&mut self, a: BDDFunc, b: BDDFunc) -> BDDFunc {
403        self.bdd.or(a, b)
404    }
405
406    /// Produce a function within the BDD representing the logical XOR of the
407    /// functions `a` and `b`.
408    pub fn xor(&mut self, a: BDDFunc, b: BDDFunc) -> BDDFunc {
409        self.bdd.xor(a, b)
410    }
411
412    /// Produce a function within the BDD representing the logical implication `a` -> `b`.
413    pub fn implies(&mut self, a: BDDFunc, b: BDDFunc) -> BDDFunc {
414        self.bdd.implies(a, b)
415    }
416
417    /// Check whether the function `f` within the BDD is satisfiable.
418    pub fn sat(&self, f: BDDFunc) -> bool {
419        match f {
420            BDD_ZERO => false,
421            _ => true,
422        }
423    }
424
425    /// Return a new function based on `f` but with the given label forced to the given value.
426    pub fn restrict(&mut self, f: BDDFunc, t: T, val: bool) -> BDDFunc {
427        self.bdd.restrict(f, self.labels[&t], val)
428    }
429
430    /// Produce a function within the BDD representing the given expression
431    /// `e`, which may contain ANDs, ORs, NOTs, terminals, and constants.
432    pub fn from_expr(&mut self, e: &Expr<T>) -> BDDFunc {
433        match e {
434            &Expr::Terminal(ref t) => self.terminal(t.clone()),
435            &Expr::Const(val) => self.constant(val),
436            &Expr::Not(ref x) => {
437                let xval = self.from_expr(&**x);
438                self.not(xval)
439            }
440            &Expr::And(ref a, ref b) => {
441                let aval = self.from_expr(&**a);
442                let bval = self.from_expr(&**b);
443                self.and(aval, bval)
444            }
445            &Expr::Or(ref a, ref b) => {
446                let aval = self.from_expr(&**a);
447                let bval = self.from_expr(&**b);
448                self.or(aval, bval)
449            }
450        }
451    }
452
453    /// Evaluate the function `f` in the BDD with the given terminal
454    /// assignments. Any terminals not specified in `values` default to `false`.
455    pub fn evaluate(&self, f: BDDFunc, values: &HashMap<T, bool>) -> bool {
456        let size = self.rev_labels.len();
457        let mut valarray = Vec::with_capacity(size);
458        valarray.resize(size, false);
459        for (t, l) in &self.labels {
460            valarray[*l as usize] = *values.get(t).unwrap_or(&false);
461        }
462        self.bdd.evaluate(f, &valarray).unwrap()
463    }
464
465    /// Compute an assignment for terminals which satisfies 'f'.  If
466    /// satisfiable, this function returns a HashMap with the
467    /// assignments (true, false) for terminals unless a terminal's
468    /// assignment does not matter for satisfiability. If 'f' is not
469    /// satisfiable, returns None.
470    ///
471    /// Example: for the boolean function "a or b", this function
472    /// could return one of the following two HashMaps: {"a" -> true}
473    /// or {"b" -> true}.
474    pub fn sat_one(&self, f: BDDFunc) -> Option<HashMap<T, bool>> {
475        let mut h = HashMap::new();
476        if self.sat_one_internal(f, &mut h) {
477            Some(h)
478        } else {
479            None
480        }
481    }
482
483    fn sat_one_internal(&self, f: BDDFunc, assignments: &mut HashMap<T, bool>) -> bool {
484        match f {
485            BDD_ZERO => false,
486            BDD_ONE => true,
487            _ => {
488                let hi = self.bdd.nodes[f].hi;
489                let lo = self.bdd.nodes[f].lo;
490                if hi != BDD_ZERO
491                    && (lo == BDD_ZERO || self.bdd.sat_varcount(hi) < self.bdd.sat_varcount(lo))
492                {
493                    assignments.insert(self.rev_labels[self.bdd.nodes[f].label].clone(), true);
494                    self.sat_one_internal(hi, assignments);
495                } else {
496                    assignments.insert(self.rev_labels[self.bdd.nodes[f].label].clone(), false);
497                    self.sat_one_internal(lo, assignments);
498                }
499                true
500            }
501        }
502    }
503
504    /// Convert the BDD to a minimized sum-of-products expression.
505    pub fn to_expr(&self, f: BDDFunc) -> Expr<T> {
506        self.bdd
507            .to_expr(f, self.rev_labels.len())
508            .map(|t: &BDDLabel| self.rev_labels[*t as usize].clone())
509    }
510
511    /// Export BDD to `dot` format (from the graphviz package) to enable visualization.
512    pub fn to_dot(&self, f: BDDFunc) -> String {
513        // the algorithm starts at the f BDDfunction and then recursively collects all BDDNodes
514        // until BDD_ZERO and BDD_ONE. The output for each node is straightforward: just a single
515        // `dot` node.
516        let mut out = String::from("digraph bdd {\n");
517
518        let mut nodes = BTreeSet::new();
519        self.reachable_nodes(f, &mut nodes);
520        for func in nodes {
521            if func <= f {
522                out.push_str(&format!(
523                    "n{} [label = {:?}];\n",
524                    func, self.rev_labels[self.bdd.nodes[func].label]
525                ));
526                out.push_str(&format!(
527                    "n{} -> n{} [style=dotted];\n",
528                    func, self.bdd.nodes[func].lo
529                ));
530                out.push_str(&format!("n{} -> n{};\n", func, self.bdd.nodes[func].hi));
531            }
532        }
533
534        out.push_str(&format!("n{} [label=\"0\"];\n", BDD_ZERO));
535        out.push_str(&format!("n{} [label=\"1\"];\n", BDD_ONE));
536
537        out.push_str("}");
538
539        out.to_string()
540    }
541
542    /// Produce an ordered set of nodes in the BDD function `f`: the transitive closure of
543    /// reachable nodes.
544    fn reachable_nodes(&self, f: BDDFunc, s: &mut BTreeSet<BDDFunc>) {
545        if f != BDD_ZERO && f != BDD_ONE {
546            // we use a BTreeSet instead of a HashSet since its order is stable.
547            if s.insert(f) {
548                self.reachable_nodes(self.bdd.nodes[f].hi, s);
549                self.reachable_nodes(self.bdd.nodes[f].lo, s);
550            }
551        }
552    }
553
554    /// Produce a function that is true when the maximal number of
555    /// given input functions are true.
556    pub fn max_sat(&mut self, funcs: &[BDDFunc]) -> BDDFunc {
557        self.bdd.max_sat(funcs)
558    }
559
560    /// Return a vector of all labels in the BDD.
561    pub fn labels(&self) -> Vec<T> {
562        self.labels.keys().cloned().collect()
563    }
564}
565
566/// The `BDDOutput` trait provides an interface to inform a listener about new
567/// BDD nodes that are created. It allows the user to persist a BDD to a stream
568/// (e.g., a log or trace file) as a long-running process executes. A
569/// `BDDOutput` instance may be provided to all BDD operations.
570pub trait BDDOutput<T, E> {
571    fn write_label(&self, label: T, label_id: u64) -> Result<(), E>;
572    fn write_node(
573        &self,
574        node_id: BDDFunc,
575        label_id: u64,
576        lo: BDDFunc,
577        hi: BDDFunc,
578    ) -> Result<(), E>;
579}
580
581/// A `PersistedBDD` is a wrapper around a `BDD` that provides a means to write
582/// BDD labels and nodes out to a `BDDOutput`. It tracks how much of the BDD
583/// has already been writen out, and writes out new nodes and labels as
584/// required when its `persist()` or `persist_all()` method is called.
585pub struct PersistedBDD<T>
586where
587    T: Clone + Debug + Eq + Hash,
588{
589    bdd: BDD<T>,
590    next_output_func: BDDFunc,
591    next_output_label: BDDLabel,
592}
593
594impl<T> PersistedBDD<T>
595where
596    T: Clone + Debug + Eq + Hash,
597{
598    /// Create a new `PersistedBDD`.
599    pub fn new() -> PersistedBDD<T> {
600        PersistedBDD {
601            bdd: BDD::new(),
602            next_output_func: 0,
603            next_output_label: 0,
604        }
605    }
606
607    /// Return the inner BDD.
608    pub fn bdd(&self) -> &BDD<T> {
609        &self.bdd
610    }
611
612    /// Return the inner BDD.
613    pub fn bdd_mut(&mut self) -> &mut BDD<T> {
614        &mut self.bdd
615    }
616
617    /// Persist (at least) all labels and nodes in the BDD necessary to fully
618    /// describe BDD function `f`. More records than strictly necessary may be
619    /// written out.
620    pub fn persist<E>(&mut self, f: BDDFunc, out: &dyn BDDOutput<T, E>) -> Result<(), E> {
621        if f == BDD_ZERO || f == BDD_ONE {
622            // No need to persist the terminal constant nodes!
623            return Ok(());
624        }
625        while self.next_output_label < self.bdd.rev_labels.len() {
626            let id = self.next_output_label;
627            let t = self.bdd.rev_labels[id].clone();
628            out.write_label(t, id as u64)?;
629            self.next_output_label += 1;
630        }
631        while self.next_output_func <= f {
632            let id = self.next_output_func;
633            let node = &self.bdd.bdd.nodes[id];
634            out.write_node(id, node.label as u64, node.lo, node.hi)?;
635            self.next_output_func += 1;
636        }
637        Ok(())
638    }
639
640    /// Persist all labels and nodes in the BDD.
641    pub fn persist_all<E>(&mut self, out: &dyn BDDOutput<T, E>) -> Result<(), E> {
642        if self.bdd.bdd.nodes.len() > 0 {
643            let last_f = self.bdd.bdd.nodes.len() - 1;
644            self.persist(last_f, out)
645        } else {
646            Ok(())
647        }
648    }
649}
650
651/// A `BDDLoader` provides a way to inject BDD nodes directly, as they were
652/// previously dumped by a `PersistedBDD` to a `BDDOutput`. The user should
653/// create a `BDDLoader` instance wrapped around a `BDD` and call
654/// `inject_label` and `inject_node` as appropriate to inject labels and nodes.
655pub struct BDDLoader<'a, T>
656where
657    T: Clone + Debug + Eq + Hash + 'a,
658{
659    bdd: &'a mut BDD<T>,
660}
661
662impl<'a, T> BDDLoader<'a, T>
663where
664    T: Clone + Debug + Eq + Hash + 'a,
665{
666    /// Create a new `BDDLoader` wrapping the given `bdd`. The `BDDLoader`
667    /// holds a mutable reference to `bdd` until destroyed. `bdd` must be empty
668    /// initially.
669    pub fn new(bdd: &'a mut BDD<T>) -> BDDLoader<'a, T> {
670        assert!(bdd.labels.len() == 0);
671        assert!(bdd.rev_labels.len() == 0);
672        assert!(bdd.bdd.nodes.len() == 0);
673        BDDLoader { bdd: bdd }
674    }
675
676    /// Inject a new label into the BDD. The `id` must be the next consecutive
677    /// `id`; i.e., labels must be injected in the order they were dumped to a
678    /// `BDDOutput`.
679    pub fn inject_label(&mut self, t: T, id: u64) {
680        assert!(id == self.bdd.rev_labels.len() as u64);
681        self.bdd.rev_labels.push(t.clone());
682        self.bdd.labels.insert(t, id as BDDLabel);
683    }
684
685    /// Inject a new node into the BDD. The `id` must be the next consecutive
686    /// `id`; i.e., nodes must be injected in the order they were dumped to a
687    /// `BDDOutput`.
688    pub fn inject_node(&mut self, id: BDDFunc, label_id: u64, lo: BDDFunc, hi: BDDFunc) {
689        assert!(id == self.bdd.bdd.nodes.len() as BDDFunc);
690        let n = BDDNode {
691            label: label_id as BDDLabel,
692            lo: lo,
693            hi: hi,
694            varcount: cmp::min(
695                self.bdd.bdd.sat_varcount(lo),
696                self.bdd.bdd.sat_varcount(hi) + 1,
697            ),
698        };
699        self.bdd.bdd.nodes.push(n.clone());
700        self.bdd.bdd.dedup_hash.insert(n, id);
701    }
702}
703
704#[cfg(test)]
705mod test {
706    use super::*;
707    use std::cell::RefCell;
708    use std::collections::HashMap;
709    use Expr;
710    extern crate rand;
711    extern crate rand_xorshift;
712    use self::rand::{Rng, SeedableRng};
713    use self::rand_xorshift::XorShiftRng;
714
715    fn term_hashmap(vals: &[bool], h: &mut HashMap<u32, bool>) {
716        h.clear();
717        for (i, v) in vals.iter().enumerate() {
718            h.insert(i as u32, *v);
719        }
720    }
721
722    fn test_bdd(
723        b: &BDD<u32>,
724        f: BDDFunc,
725        h: &mut HashMap<u32, bool>,
726        inputs: &[bool],
727        expected: bool,
728    ) {
729        term_hashmap(inputs, h);
730        assert!(b.evaluate(f, h) == expected);
731    }
732
733    #[test]
734    fn bdd_eval() {
735        let mut h = HashMap::new();
736        let mut b = BDD::new();
737        let expr = Expr::or(
738            Expr::and(Expr::Terminal(0), Expr::Terminal(1)),
739            Expr::and(Expr::not(Expr::Terminal(2)), Expr::not(Expr::Terminal(3))),
740        );
741        let f = b.from_expr(&expr);
742        test_bdd(&b, f, &mut h, &[false, false, true, true], false);
743        test_bdd(&b, f, &mut h, &[true, false, true, true], false);
744        test_bdd(&b, f, &mut h, &[true, true, true, true], true);
745        test_bdd(&b, f, &mut h, &[false, false, false, true], false);
746        test_bdd(&b, f, &mut h, &[false, false, false, false], true);
747    }
748
749    fn bits_to_hashmap(bits: usize, n: usize, h: &mut HashMap<u32, bool>) {
750        for b in 0..bits {
751            h.insert(b as u32, (n & (1 << b)) != 0);
752        }
753    }
754
755    fn test_bdd_expr(e: Expr<u32>, nterminals: usize) {
756        let mut b = BDD::new();
757        let f = b.from_expr(&e);
758        let mut terminal_values = HashMap::new();
759        let mut expected_satisfiable = false;
760        for v in 0..(1 << nterminals) {
761            bits_to_hashmap(nterminals, v, &mut terminal_values);
762            let expr_val = e.evaluate(&terminal_values);
763            let bdd_val = b.evaluate(f, &terminal_values);
764            assert!(expr_val == bdd_val);
765            if expr_val {
766                expected_satisfiable = true;
767            }
768        }
769        // test sat_one
770        let sat_result = b.sat_one(f);
771        assert!(sat_result.is_some() == expected_satisfiable);
772        if expected_satisfiable {
773            assert!(b.evaluate(f, &sat_result.unwrap()));
774        }
775    }
776
777    fn random_expr<R: Rng>(r: &mut R, nterminals: usize) -> Expr<u32> {
778        match r.gen_range(0, 5) {
779            0 => Expr::Terminal(r.gen_range(0, nterminals) as u32),
780            1 => Expr::Const(r.gen::<bool>()),
781            2 => Expr::Not(Box::new(random_expr(r, nterminals))),
782            3 => Expr::And(
783                Box::new(random_expr(r, nterminals)),
784                Box::new(random_expr(r, nterminals)),
785            ),
786            4 => Expr::Or(
787                Box::new(random_expr(r, nterminals)),
788                Box::new(random_expr(r, nterminals)),
789            ),
790            _ => unreachable!(),
791        }
792    }
793
794    #[test]
795    fn bdd_exhaustive_exprs() {
796        let mut rng = XorShiftRng::from_seed(rand::thread_rng().gen());
797        for _ in 0..100 {
798            let expr = random_expr(&mut rng, 6);
799            test_bdd_expr(expr, 6);
800        }
801    }
802
803    #[test]
804    fn bdd_to_expr() {
805        let mut b = BDD::new();
806        let f_true = b.constant(true);
807        assert!(b.to_expr(f_true) == Expr::Const(true));
808        let f_false = b.constant(false);
809        assert!(b.to_expr(f_false) == Expr::Const(false));
810        let f_0 = b.terminal(0);
811        let f_1 = b.terminal(1);
812        let f_and = b.and(f_0, f_1);
813        assert!(b.to_expr(f_and) == Expr::and(Expr::Terminal(0), Expr::Terminal(1)));
814        let f_or = b.or(f_0, f_1);
815        assert!(b.to_expr(f_or) == Expr::or(Expr::Terminal(1), Expr::Terminal(0)));
816        let f_not = b.not(f_0);
817        assert!(b.to_expr(f_not) == Expr::not(Expr::Terminal(0)));
818        let f_2 = b.terminal(2);
819        let f_1_or_2 = b.or(f_1, f_2);
820        let f_0_and_1_or_2 = b.and(f_0, f_1_or_2);
821        assert!(
822            b.to_expr(f_0_and_1_or_2)
823                == Expr::or(
824                    Expr::and(Expr::Terminal(0), Expr::Terminal(2)),
825                    Expr::and(Expr::Terminal(0), Expr::Terminal(1))
826                )
827        );
828    }
829
830    #[derive(Clone, Debug)]
831    struct InMemoryBDDLog {
832        labels: RefCell<Vec<(u64, String)>>,
833        nodes: RefCell<Vec<(BDDFunc, u64, BDDFunc, BDDFunc)>>,
834    }
835
836    impl InMemoryBDDLog {
837        pub fn new() -> InMemoryBDDLog {
838            InMemoryBDDLog {
839                labels: RefCell::new(Vec::new()),
840                nodes: RefCell::new(Vec::new()),
841            }
842        }
843    }
844
845    impl BDDOutput<String, ()> for InMemoryBDDLog {
846        fn write_label(&self, l: String, label_id: u64) -> Result<(), ()> {
847            let mut labels = self.labels.borrow_mut();
848            labels.push((label_id, l));
849            Ok(())
850        }
851
852        fn write_node(
853            &self,
854            node_id: BDDFunc,
855            label_id: u64,
856            lo: BDDFunc,
857            hi: BDDFunc,
858        ) -> Result<(), ()> {
859            let mut nodes = self.nodes.borrow_mut();
860            nodes.push((node_id, label_id, lo, hi));
861            Ok(())
862        }
863    }
864
865    #[test]
866    // the tests compare the dot output to a string which has been manually verified to be correct
867    fn dot_output() {
868        let mut bdd = BDD::new();
869        let a = bdd.terminal("a");
870        let b = bdd.terminal("b");
871        let b_and_a = bdd.and(a, b);
872        {
873            let dot = bdd.to_dot(b_and_a);
874            assert_eq!(
875                dot,
876                indoc!(
877                    "
878                            digraph bdd {
879                            n1 [label = \"b\"];
880                            n1 -> n18446744073709551615 [style=dotted];
881                            n1 -> n18446744073709551614;
882                            n2 [label = \"a\"];
883                            n2 -> n18446744073709551615 [style=dotted];
884                            n2 -> n1;
885                            n18446744073709551615 [label=\"0\"];
886                            n18446744073709551614 [label=\"1\"];
887                            }"
888                )
889            );
890        }
891        let c = bdd.terminal("c");
892        let c_or_a = bdd.or(c, a);
893        {
894            let dot = bdd.to_dot(c_or_a);
895            assert_eq!(
896                dot,
897                indoc!(
898                    "
899                            digraph bdd {
900                            n3 [label = \"c\"];
901                            n3 -> n18446744073709551615 [style=dotted];
902                            n3 -> n18446744073709551614;
903                            n4 [label = \"a\"];
904                            n4 -> n3 [style=dotted];
905                            n4 -> n18446744073709551614;
906                            n18446744073709551615 [label=\"0\"];
907                            n18446744073709551614 [label=\"1\"];
908                            }"
909                )
910            );
911        }
912        let not_c_and_b = bdd.not(b_and_a);
913        let c_or_a_and_not_b_and_a = bdd.and(c_or_a, not_c_and_b);
914        {
915            let dot = bdd.to_dot(c_or_a_and_not_b_and_a);
916            assert_eq!(
917                dot,
918                indoc!(
919                    "
920                            digraph bdd {
921                            n3 [label = \"c\"];
922                            n3 -> n18446744073709551615 [style=dotted];
923                            n3 -> n18446744073709551614;
924                            n5 [label = \"b\"];
925                            n5 -> n18446744073709551614 [style=dotted];
926                            n5 -> n18446744073709551615;
927                            n7 [label = \"a\"];
928                            n7 -> n3 [style=dotted];
929                            n7 -> n5;
930                            n18446744073709551615 [label=\"0\"];
931                            n18446744073709551614 [label=\"1\"];
932                            }"
933                )
934            );
935        }
936        {
937            let new_a = bdd.terminal("a");
938            let d = bdd.terminal("d");
939            let new_a_or_d = bdd.or(new_a, d);
940            let dot = bdd.to_dot(new_a_or_d);
941            assert_eq!(
942                dot,
943                indoc!(
944                    "
945                            digraph bdd {
946                            n8 [label = \"d\"];
947                            n8 -> n18446744073709551615 [style=dotted];
948                            n8 -> n18446744073709551614;
949                            n9 [label = \"a\"];
950                            n9 -> n8 [style=dotted];
951                            n9 -> n18446744073709551614;
952                            n18446744073709551615 [label=\"0\"];
953                            n18446744073709551614 [label=\"1\"];
954                            }"
955                )
956            );
957        }
958    }
959
960    #[test]
961    fn sat_one() {
962        let mut bdd = BDD::new();
963
964        // empty bdds
965        assert!(bdd.sat_one(BDD_ONE).is_some());
966        assert!(bdd.sat_one(BDD_ZERO).is_none());
967
968        let a = bdd.terminal("a");
969        let b = bdd.terminal("b");
970        let b_and_a = bdd.and(a, b);
971        let result = bdd.sat_one(b_and_a);
972        assert!(result.is_some());
973        assert!(bdd.evaluate(b_and_a, &result.unwrap()));
974
975        let c = bdd.terminal("c");
976        let not_c = bdd.not(c);
977        let b_and_a_or_not_c = bdd.or(b_and_a, not_c);
978        let result = bdd.sat_one(b_and_a_or_not_c);
979        assert!(result.is_some());
980        assert!(bdd.evaluate(b_and_a_or_not_c, &result.unwrap()));
981
982        // unsatisfiable formula
983        let c_and_not_c = bdd.and(c, not_c);
984        assert!(bdd.sat_one(c_and_not_c).is_none());
985    }
986
987    #[test]
988    fn max_sat() {
989        let mut bdd = BDD::new();
990        // Test: a, a+b, a+c, c', c, bd, ad, d'
991        let a = bdd.terminal(0);
992        let b = bdd.terminal(1);
993        let c = bdd.terminal(2);
994        let d = bdd.terminal(3);
995        let cnot = bdd.not(c);
996        let dnot = bdd.not(d);
997        let ab = bdd.and(a, b);
998        let ac = bdd.and(a, c);
999        let bd = bdd.and(b, d);
1000        let ad = bdd.and(a, d);
1001        let max_sat = bdd.max_sat(&[a, ab, ac, cnot, c, bd, ad, dnot]);
1002        let abc = bdd.and(ab, c);
1003        let abcd = bdd.and(abc, d);
1004        assert!(max_sat == abcd);
1005    }
1006
1007    #[test]
1008    fn max_sat_min_var() {
1009        let mut bdd = BDD::new();
1010        // Test: a, a+b, a+c, c', c, bd, d'
1011        let a = bdd.terminal(0);
1012        let b = bdd.terminal(1);
1013        let c = bdd.terminal(2);
1014        let d = bdd.terminal(3);
1015        let cnot = bdd.not(c);
1016        let dnot = bdd.not(d);
1017        let ab = bdd.and(a, b);
1018        let ac = bdd.and(a, c);
1019        let bd = bdd.and(b, d);
1020        let max_sat = bdd.max_sat(&[a, ab, ac, cnot, c, bd, dnot]);
1021        let abc = bdd.and(ab, c);
1022        assert!(max_sat == abc);
1023        let assn = bdd.sat_one(max_sat).unwrap();
1024        assert!(assn.get(&0) == Some(&true));
1025        assert!(assn.get(&1) == Some(&true));
1026        assert!(assn.get(&2) == Some(&true));
1027        assert!(assn.get(&3) == None);
1028    }
1029
1030    #[test]
1031    fn persist_bdd() {
1032        let out = InMemoryBDDLog::new();
1033        let mut p = PersistedBDD::new();
1034        let term_a = p.bdd_mut().terminal("A".to_owned());
1035        let term_b = p.bdd_mut().terminal("B".to_owned());
1036        let term_c = p.bdd_mut().terminal("C".to_owned());
1037        let ab = p.bdd_mut().and(term_a, term_b);
1038        let ab_or_c = p.bdd_mut().or(ab, term_c);
1039        p.persist(ab_or_c, &out).unwrap();
1040        assert!(
1041            *out.labels.borrow()
1042                == vec![
1043                    (0, "A".to_owned()),
1044                    (1, "B".to_owned()),
1045                    (2, "C".to_owned()),
1046                ]
1047        );
1048        assert!(
1049            *out.nodes.borrow()
1050                == vec![
1051                    (0, 0, BDD_ZERO, BDD_ONE),
1052                    (1, 1, BDD_ZERO, BDD_ONE),
1053                    (2, 2, BDD_ZERO, BDD_ONE),
1054                    (3, 0, BDD_ZERO, 1),
1055                    (4, 1, 2, BDD_ONE),
1056                    (5, 0, 2, 4),
1057                ]
1058        );
1059    }
1060
1061    #[test]
1062    fn load_bdd() {
1063        let mut bdd = BDD::new();
1064        {
1065            let mut loader = BDDLoader::new(&mut bdd);
1066            loader.inject_label("A".to_owned(), 0);
1067            loader.inject_label("B".to_owned(), 1);
1068            loader.inject_node(0, 1, BDD_ZERO, BDD_ONE);
1069            loader.inject_node(1, 0, BDD_ZERO, 0);
1070        }
1071        let mut h = HashMap::new();
1072        h.insert("A".to_owned(), true);
1073        h.insert("B".to_owned(), true);
1074        assert!(bdd.evaluate(1, &h) == true);
1075    }
1076
1077    #[test]
1078    fn persist_empty_bdd() {
1079        let out = InMemoryBDDLog::new();
1080        let mut p = PersistedBDD::new();
1081        p.persist(BDD_ZERO, &out).unwrap();
1082    }
1083}
boolean_expression/bdd.rs

boolean_expression/
bdd.rs
