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
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
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144

(datatype Math
  (Num BigRat)
  (Var String)
  (Add Math Math)
  (Div Math Math)
  (Mul Math Math))

(let $zero (Num (bigrat (bigint 0) (bigint 1))))
(let $one (Num (bigrat (bigint 1) (bigint 1))))
(let $two (Num (bigrat (bigint 2) (bigint 1))))

(rewrite (Add a b) (Add b a))
(rewrite (Add a $zero) a)
(rewrite (Add (Num r1) (Num r2))
         (Num (+ r1 r2)))

(let $one-two (Add $one $two))

(push)
(run 1)
;; yay, constant folding works
(check (= $one-two (Num (bigrat (bigint 3) (bigint 1)))))
;; also, commutativity works
(check (= (Add $two $one) $one-two))
(pop)

(push)
;; rule is like rewrite, but more general
;; the following rule doesn't union (Num r) with the result:
(rule ((Num r))
      ((union $one (Div (Num r) (Num r)))))
;; uh oh, division by zero!
(run 1)

(pop)

;; we need to detect when things are non-zero
(function lower-bound (Math) BigRat :merge (max old new))
(function upper-bound (Math) BigRat :merge (min old new))

(rule ((Num r))
      ((set (lower-bound (Num r)) r)
       (set (upper-bound (Num r)) r)))
(rule ((= e (Add a b)) (= x (lower-bound a)) (= y (lower-bound b)))
      ((set (lower-bound e) (+ x y))))
(rule ((= e (Add a b)) (= x (upper-bound a)) (= y (upper-bound b)))
      ((set (upper-bound e) (+ x y))))
(rule ((= e (Mul a b))
       (= lba (lower-bound a))
       (= lbb (lower-bound b))
       (= uba (upper-bound a))
       (= ubb (upper-bound b))
      )
      ((set (lower-bound e)
            (min (* lba lbb)
                 (min (* lba ubb)
                 (min (* uba lbb)
                      (* uba ubb)))))
       (set (upper-bound e)
            (min (* lba lbb)
                 (min (* lba ubb)
                 (min (* uba lbb)
                      (* uba ubb)))))))

(rule ((= e (Add a b))
       (> (lower-bound e) (bigrat (bigint 0) (bigint 1))))
      ((union $one (Div (Add a b) (Add a b)))))

(let $x (Var "x"))
(let $x1 (Add $x $one))

(push)
(set (lower-bound $x) (bigrat (bigint 0) (bigint 1)))
(set (upper-bound $x) (bigrat (bigint 1) (bigint 1)))

(run 3)

(extract (lower-bound $x1))
(extract (upper-bound $x1))
(check (= $one (Div $x1 $x1)))

(pop)


;; Set the variable $x to a particular input value 200/201
(set (lower-bound $x) (bigrat (bigint 200) (bigint 201)))
(set (upper-bound $x) (bigrat (bigint 200) (bigint 201)))

(run 3)

(extract (lower-bound $x1))
(extract (upper-bound $x1))

(function true-value (Math) f64 :no-merge)

(rule ((= (to-f64 (lower-bound e))
          (to-f64 (upper-bound e)))
       (= lbe (lower-bound e))
      )
      ((set (true-value e)
            (to-f64 lbe))))

(run 1)
(extract (true-value $x1))

(function best-error (Math) f64 :merge new)

(rule ((Num n))
      ((set (best-error (Num n)) (to-f64 n))))
(rule ((Add a b)) ((set (best-error (Add a b)) (to-f64 (bigrat (bigint 10000) (bigint 1))))))

;; finally, the mega rule for finding more accurate programs
(rule ((= expr (Add a b))
       (= (best-error a) va)
       (= (best-error b) vb)
       (= true-v (true-value (Add a b)))
       (= computed (+ va vb))
       (< (abs (- computed true-v))
          (best-error (Add a b))))
      ((set (best-error (Add a b)) computed)))



(push)

(let $target
  (Add 
    (Add (Num (bigrat (bigint 1) (bigint 100))) (Num (bigrat (bigint 1) (bigint 100))))
    (Num (bigrat (bigint -2) (bigint 100)))))

(run 1)

;; set a default
(set (best-error $target) (to-f64 (bigrat (bigint 10000) (bigint 1))))
;; error is bad, constant folding hasn't fired enough
(extract (best-error $target))

(run 1)

;; error is good, constant folding has fired enough
(extract (best-error $target))


(pop)