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
; Binary Decision Diagrams are if-then-else trees/ compressed tries that hash cons their leaves
; This is easily expressible in the facilities provided. Everything in egglog is automatcally shared
; and Compression is easily expressible as a rule.
; They are a notion of first class set useful for certain classes of uniformly describable sets.
; https://en.wikipedia.org/wiki/Binary_decision_diagram
; https://www.lri.fr/~filliatr/ftp/publis/hash-consing2.pdf Type-Safe Modular Hash-Consing - Section 3.3
(datatype BDD
(ITE i64 BDD BDD) ; variables labelled by number
)
(constructor TrueConst () BDD)
(let $True (TrueConst))
(constructor FalseConst () BDD)
(let $False (FalseConst))
; compress unneeded nodes
(rewrite (ITE n a a) a)
(constructor bddand (BDD BDD) BDD)
(rewrite (bddand x y) (bddand y x))
(rewrite (bddand $False n) $False)
(rewrite (bddand $True x) x)
; We use an order where low variables are higher in tree
; Could go the other way.
(rewrite (bddand (ITE n a1 a2) (ITE m b1 b2))
(ITE n (bddand a1 (ITE m b1 b2)) (bddand a2 (ITE m b1 b2)))
:when ((< n m))
)
(rewrite (bddand (ITE n a1 a2) (ITE n b1 b2))
(ITE n (bddand a1 b1) (bddand a2 b2))
)
(constructor bddor (BDD BDD) BDD)
(rewrite (bddor x y) (bddor y x))
(rewrite (bddor $True n) $True)
(rewrite (bddor $False x) x)
(rewrite (bddor (ITE n a1 a2) (ITE m b1 b2))
(ITE n (bddor a1 (ITE m b1 b2)) (bddor a2 (ITE m b1 b2)))
:when ((< n m))
)
(rewrite (bddor (ITE n a1 a2) (ITE n b1 b2))
(ITE n (bddor a1 b1) (bddor a2 b2))
)
(constructor bddnot (BDD) BDD)
(rewrite (bddnot $True) $False)
(rewrite (bddnot $False) $True)
(rewrite (bddnot (ITE n a1 a2)) (ITE n (bddnot a1) (bddnot a2)))
(constructor bddxor (BDD BDD) BDD)
(rewrite (bddxor x y) (bddxor y x))
(rewrite (bddxor $True n) (bddnot n))
(rewrite (bddxor $False x) x)
(rewrite (bddxor (ITE n a1 a2) (ITE m b1 b2))
(ITE n (bddxor a1 (ITE m b1 b2)) (bddxor a2 (ITE m b1 b2)))
:when ((< n m))
)
(rewrite (bddxor (ITE n a1 a2) (ITE n b1 b2))
(ITE n (bddxor a1 b1) (bddxor a2 b2))
)
(push)
;;; Tests
(let $v0 (ITE 0 $True $False))
(let $v1 (ITE 1 $True $False))
(let $v2 (ITE 2 $True $False))
(let $t0 (bddnot (bddnot $v0)))
(let $t1 (bddor $v0 (bddnot $v0)))
(let $t2 (bddand $v0 (bddnot $v0)))
(let $t3 (bddand $v0 $v0))
(let $t4 (bddor $v0 $v0))
(let $t5 (bddxor (bddnot $v0) $v0))
(let $t6 (bddand (bddor $v1 $v2) $v2))
(let $t7a (bddxor (bddnot $v0) $v1))
(let $t7b (bddxor $v0 (bddnot $v1)))
(let $t7c (bddnot (bddxor $v0 $v1)))
(let $t8 (bddand $v1 $v2))
(let $t9 (bddand (bddnot $v1) (bddand (bddnot $v0) (bddxor $v0 $v1))))
(let $t10 (bddor (bddnot $v1) (bddor (bddnot $v0) (bddxor $v0 (bddnot $v1)))))
(run 30)
(check (= $t0 $v0)) ; bddnot cancels
(check (= $t1 $True))
(check (= $t2 $False))
(check (= $t3 $v0))
(check (= $t4 $v0))
(check (= $t5 $True))
(check (= $t6 $v2))
(check (= $t7a $t7b))
(check (= $t7a $t7c))
(check (= $t8 (ITE 1 (ITE 2 $True $False) $False)))
(check (= $t9 $False))
(check (= $t10 $True))
(pop)