; 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
)
(function TrueConst () BDD)
(let True (TrueConst))
(function FalseConst () BDD)
(let False (FalseConst))

; compress unneeded nodes
(rewrite (ITE n a a) a)

(function 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))
)

(function 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))
)

(function bddnot (BDD) BDD)
(rewrite (bddnot True) False)
(rewrite (bddnot False) True)
(rewrite (bddnot (ITE n a1 a2)) (ITE n (bddnot a1) (bddnot a2)))


(function 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)