;; computes "e-graph intersection"

(datatype Expr
    (Var String)
    (f Expr))

(function intersect (Expr Expr) Expr)

(rule (
    (= x3 (intersect x1 x2))
    (= f1 (f x1))
    (= f2 (f x2))
)(
    (union (intersect f1 f2) (f x3))
))

(let a1 (Var "a1")) (let a2 (Var "a2")) (let a3 (Var "a3"))
(let b1 (Var "b1")) (let b2 (Var "b2")) (let b3 (Var "b3"))

;; e-graph 1: f(a) = f(b), f(f(a))
(let t1 (f (f a1)))
(let fb1 (f b1))
(union (f a1) fb1)

;; e-graph 2: f(f(a)) = f(f(b))
(let t2  (f (f a2)))
(let t2p (f (f b2)))
(union t2 t2p)

(union (intersect a1 a2) a3)
(union (intersect b1 b2) b3)

(run 100)

(let t3 (f (f a3)))
(query-extract :variants 5 t3)

;; f(f(a)) = f(f(b)) is preserved
(check (= (f (f a3)) (f (f b3))))
;; but not f(a) = f(b), it was only in e-graph 1
(check (!= (f a3) (f b3)))