rsdd/serialize/
ser_bdd.rs

1//! serializable representation of a BDD
2
3use std::collections::HashMap;
4
5use crate::repr::{BddNode, BddPtr, DDNNFPtr};
6
7#[derive(Clone, Debug, Serialize, Deserialize)]
8pub enum SerBDDPtr {
9    Ptr { index: usize, compl: bool },
10    True,
11    False,
12}
13
14#[derive(Clone, Debug, Serialize, Deserialize)]
15pub struct SerBDD {
16    topvar: usize,
17    low: SerBDDPtr,
18    high: SerBDDPtr,
19}
20
21#[derive(Clone, Debug, Serialize, Deserialize)]
22pub struct BDDSerializer {
23    /// list of nodes allocated in the BDD
24    /// `nodes[0]` is true, `nodes[1]` is false
25    nodes: Vec<SerBDD>,
26    /// list of all roots (to support multi-rooted BDD serialization with shared structure)
27    roots: Vec<SerBDDPtr>,
28}
29
30impl BDDSerializer {
31    fn serialize_helper<'a>(
32        bdd: BddPtr<'a>,
33        table: &mut HashMap<&'a BddNode<'a>, usize>,
34        nodes: &mut Vec<SerBDD>,
35    ) -> SerBDDPtr {
36        match bdd {
37            BddPtr::PtrTrue => SerBDDPtr::True,
38            BddPtr::PtrFalse => SerBDDPtr::False,
39            BddPtr::Reg(node) | BddPtr::Compl(node) => {
40                if table.contains_key(&node) {
41                    return SerBDDPtr::Ptr {
42                        index: *table.get(&node).unwrap(),
43                        compl: bdd.is_neg(),
44                    };
45                }
46
47                // new node, recurse
48                let l = BDDSerializer::serialize_helper(bdd.low_raw(), table, nodes);
49                let h = BDDSerializer::serialize_helper(bdd.high_raw(), table, nodes);
50                let new_node = SerBDD {
51                    topvar: node.var.value_usize(),
52                    low: l,
53                    high: h,
54                };
55                nodes.push(new_node);
56                let index = nodes.len() - 1;
57                let new_ptr = SerBDDPtr::Ptr {
58                    index,
59                    compl: bdd.is_neg(),
60                };
61                table.insert(node, index);
62                new_ptr
63            }
64        }
65    }
66
67    pub fn from_bdd(bdd: BddPtr) -> BDDSerializer {
68        let mut nodes = Vec::new();
69        #[allow(clippy::mutable_key_type)]
70        // this is a false positive, since BddNode's Hash/Ord ignore the scratch.
71        let mut table = HashMap::new();
72        let r = BDDSerializer::serialize_helper(bdd, &mut table, &mut nodes);
73        BDDSerializer {
74            nodes,
75            roots: vec![r],
76        }
77    }
78}
rsdd/serialize/ser_bdd.rs

rsdd/serialize/
ser_bdd.rs
