egglog 2.0.0

egglog is a language that combines the benefits of equality saturation and datalog. It can be used for analysis, optimization, and synthesis of programs. It is the successor to the popular rust library egg.
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

; proofs of connectivity are paths
(datatype Proof
  (Trans i64 Proof)
  (Edge i64 i64))

; We enhance the path relation to carry a proof field
(relation path (i64 i64 Proof))
(relation edge (i64 i64))

(edge 2 1)
(edge 3 2)
(edge 1 3)

(rule ((edge x y))  
      ((path x y (Edge x y))))
(rule ((edge x y) (path y z p))  
      ((path x z (Trans x p))))

; We consider equal all paths tha connect same points.
; Smallest Extraction will extract shortest path.
(rule ((path x y p1) (path x y p2))  
      ((union p1 p2)))

(run 3)
(check (path 3 1 (Trans 3 (Edge 2 1))))
; Would prefer being able to check
;(check (path 1 2 _))
; or extract
;(extract (path 1 4 ?p))
(print-function path 100)