aig 0.4.6

Aig library in Rust
Documentation 
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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121

use crate::{Aig, AigEdge};
use giputils::hash::GHashSet;
use logicrs::{DagCnf, LitVvec, Var};

impl Aig {
    #[inline]
    fn get_root_refs(&self) -> GHashSet<usize> {
        let mut refs = GHashSet::new();
        for l in self.latchs.iter() {
            refs.insert(l.next.node_id());
            if let Some(init) = &l.init {
                refs.insert(init.node_id());
            }
        }
        for l in self
            .constraints
            .iter()
            .chain(self.bads.iter())
            .chain(self.outputs.iter())
            .chain(self.justice.iter().flatten())
            .chain(self.fairness.iter())
        {
            refs.insert(l.node_id());
        }
        refs
    }

    fn is_xor(&self, n: usize) -> Option<(AigEdge, AigEdge)> {
        if !self.nodes[n].is_and() {
            return None;
        }
        let (fanin0, fanin1) = self.nodes[n].fanin();
        if !fanin0.compl()
            || !fanin1.compl()
            || !self.nodes[fanin0.node_id()].is_and()
            || !self.nodes[fanin1.node_id()].is_and()
        {
            return None;
        }
        let (fanin00, fanin01) = self.nodes[fanin0.node_id()].fanin();
        let (fanin10, fanin11) = self.nodes[fanin1.node_id()].fanin();
        if fanin00 == !fanin10 && fanin01 == !fanin11 {
            if fanin00.node_id() == fanin01.node_id() {
                return None;
            }
            return Some((fanin00, fanin01));
        }
        None
    }

    fn is_ite(&self, n: usize) -> Option<(AigEdge, AigEdge, AigEdge)> {
        if !self.nodes[n].is_and() {
            return None;
        }
        let (fanin0, fanin1) = self.nodes[n].fanin();
        if !fanin0.compl()
            || !fanin1.compl()
            || !self.nodes[fanin0.node_id()].is_and()
            || !self.nodes[fanin1.node_id()].is_and()
        {
            return None;
        }
        let (fanin00, fanin01) = self.nodes[fanin0.node_id()].fanin();
        let (fanin10, fanin11) = self.nodes[fanin1.node_id()].fanin();

        let (i, t, e) = if fanin00 == !fanin10 {
            (fanin00, !fanin01, !fanin11)
        } else if fanin00 == !fanin11 {
            (fanin00, !fanin01, !fanin10)
        } else if fanin01 == !fanin10 {
            (fanin01, !fanin00, !fanin11)
        } else if fanin01 == !fanin11 {
            (fanin01, !fanin00, !fanin10)
        } else {
            return None;
        };
        if i.node_id() == t.node_id() || i.node_id() == e.node_id() || t.node_id() == e.node_id() {
            return None;
        }
        Some((i, t, e))
    }

    pub fn cnf(&self, optimize: bool) -> DagCnf {
        let mut refs = self.get_root_refs();
        let mut ans = DagCnf::new();
        for node in self.nodes.iter().skip(1) {
            assert_eq!(Var::new(node.node_id()), ans.new_var());
        }
        for i in self.nodes_range().rev() {
            if self.nodes[i].is_and() && (refs.contains(&i)) {
                let n = Var::new(self.nodes[i].node_id()).lit();
                if optimize {
                    if let Some((xor0, xor1)) = self.is_xor(i) {
                        refs.insert(xor0.node_id());
                        refs.insert(xor1.node_id());
                        let xor0 = xor0.to_lit();
                        let xor1 = xor1.to_lit();
                        ans.add_rel(n.var(), &LitVvec::cnf_xor(n, xor0, xor1));
                        continue;
                    }
                    if let Some((c, t, e)) = self.is_ite(i) {
                        refs.insert(c.node_id());
                        refs.insert(t.node_id());
                        refs.insert(e.node_id());
                        let c = c.to_lit();
                        let t = t.to_lit();
                        let e = e.to_lit();
                        ans.add_rel(n.var(), &LitVvec::cnf_ite(n, c, t, e));
                        continue;
                    }
                }
                refs.insert(self.nodes[i].fanin0().id);
                refs.insert(self.nodes[i].fanin1().id);
                let fanin0 = self.nodes[i].fanin0().to_lit();
                let fanin1 = self.nodes[i].fanin1().to_lit();
                ans.add_rel(n.var(), &LitVvec::cnf_and(n, &[fanin0, fanin1]));
            }
        }
        ans
    }
}