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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46

(datatype expr 
    (Num i64)
    (Add expr expr)
    (Max expr expr))
(rewrite (Add (Num a) (Num b)) (Num (+ a b)))
(rewrite (Max (Num a) (Num b)) (Num (max a b)))

; List of (weight, value) pairs
(datatype objects
    (Cons i64 i64 objects))
(constructor NilConst () objects)
(let $Nil (NilConst))

; Given a capacity and a list of objects, finds the maximum value of a
; collection of objects whose total weight does not exceed the capacity.
(constructor Knap (i64 objects) expr)

(rule ((= f (Knap capacity (Cons weight val rest))) (<= weight capacity))
      ((union (Knap capacity (Cons weight val rest))
            (Max
                (Add (Num val) (Knap (- capacity weight) rest))
                (Knap capacity rest)))))

(rule ((= f (Knap capacity (Cons weight val rest))) (> weight capacity))
      ((union (Knap capacity (Cons weight val rest))
            (Knap capacity rest))))

(rule ((= f (Knap capacity $Nil)))
      ((union (Knap capacity $Nil) (Num 0))))

(let $test1 (Knap 13 (Cons 5 5 (Cons 3 3 (Cons 12 12 (Cons 5 5 $Nil))))))

(let $test2 (Knap 5 (Cons 6 6 $Nil)))

(let $test3 (Knap 5 (Cons 1 1 (Cons 1 1 (Cons 1 1 $Nil)))))

(let $test4 (Knap 15 (Cons 12 40 (Cons 2 20 (Cons 1 20 (Cons 1 10 (Cons 4 100 $Nil)))))))

; turn a (Num n) into n
(function Unwrap (expr) i64 :no-merge)
(rule ((= x (Num n))) ((set (Unwrap (Num n)) n)))

(run 100)

(check (= $test1 (Num 13)))