1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68

//! Module containing type definitions for the elements of the BDD:
//! Nodes ([DDNode], [NodeID]) and Variables ([VarID])

use std::hash::{Hash, Hasher};

#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub struct NodeID(pub u32);

#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq, PartialOrd, Ord)]
pub struct VarID(pub u32);

/// Element of a BDD.
/// Note that the Node contains its own ID. This may be set to zero until it has been assigned,
/// and most importantly is not considered in hashing and equality testing.
#[derive(Debug, Copy, Clone)]
pub struct DDNode {
    /// Node ID. Special values: 0 and 1 for terminal nodes
    pub id: NodeID,
    /// Variable number. Special variable 0 == terminal nodes
    pub var: VarID,
    pub low: NodeID,
    pub high: NodeID,
}

/// Test equality of two nodes, not considering the ID!
impl PartialEq for DDNode {
    fn eq(&self, that: &Self) -> bool {
        self.var == that.var && self.low == that.low && self.high == that.high
    }
}

impl Eq for DDNode {}

impl DDNode {
    /// Returns the function resulting when setting the specified variable to the specified value.
    /// Note that this only implements the case of the node being at the exact level of the specified
    /// variable.
    pub fn restrict(&self, top: VarID, order: &[u32], val: bool) -> NodeID {
        if self.var == VarID(0) {
            return self.id;
        }

        if order[top.0 as usize] < order[self.var.0 as usize] {
            // Variable does not occur in current function
            return self.id;
        }

        if top == self.var {
            if val {
                return self.high;
            } else {
                return self.low;
            }
        }

        // Variable occurs further down in the function. This is not supported in this restrict().
        panic!("Restrict called with variable below current node");
    }
}

/// Hash a node, not considering the ID!
impl Hash for DDNode {
    fn hash<H: Hasher>(&self, state: &mut H) {
        self.var.hash(state);
        self.low.hash(state);
        self.high.hash(state);
    }
}