egglog 3.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
145
146
147
148
149
150
151
152
153
154
155
156
157

;; Example from  https://uwplse.org/2026/02/24/egglog-containers.html of factoring function bending graphics example
;; https://github.com/egraphs-good/egglog/issues/772#issuecomment-4309654823
;; https://github.com/egraphs-good/egglog-python/blob/8812ec9585f68342fb0e9817326ea84828accf56/python/egglog/exp/polynomials.py#L47-L51

;; x = egraph.let("x", symbolic_bending_examples()[0])
;; egraph.run(to_polynomial_ruleset.saturate() + factor_ruleset.saturate() + from_polynomial_ruleset.saturate())
;; egraph.extract(x)

(sort Value)
(constructor Value___mul__ (Value Value) Value)
(constructor Value_var (String) Value)
(let $__expr_0 (Value___mul__ (Value_var "q4") (Value_var "bp2")))
(let $__expr_1 (Value___mul__ (Value_var "q2") (Value_var "bp1")))
(let $__expr_2 (Value___mul__ (Value_var "q5") (Value_var "bp2")))
(let $__expr_3 (Value___mul__ (Value_var "q6") (Value_var "bpp2")))
(let $__expr_4 (Value___mul__ (Value_var "q3") (Value_var "bpp1")))
(let $__expr_5 (Value___mul__ (Value_var "q11") (Value_var "bp4")))
(let $__expr_6 (Value___mul__ (Value_var "q6") (Value_var "bp2")))
(let $__expr_7 (Value___mul__ (Value_var "q8") (Value_var "bp3")))
(let $__expr_8 (Value_var "bpp2"))
(let $__expr_9 (Value___mul__ (Value_var "q1") (Value_var "bpp1")))
(let $__expr_10 (Value___mul__ (Value_var "q2") (Value_var "bpp1")))
(sort Int)
(constructor Value_from_int (Int) Value)
(constructor Int___init__ (i64) Int)
(let $__expr_11 (Value_from_int (Int___init__ -1)))
(let $__expr_12 (Value___mul__ (Value_var "q9") (Value_var "bp3")))
(let $__expr_13 (Value_var "q6"))
(let $__expr_14 (Value___mul__ (Value_var "q1") (Value_var "bp1")))
(let $__expr_15 (Value___mul__ (Value_var "q5") (Value_var "bpp2")))
(let $__expr_16 (Value___mul__ (Value_var "q4") (Value_var "bpp2")))
(let $__expr_17 (Value___mul__ (Value_var "q7") (Value_var "bpp3")))
(let $__expr_18 (Value___mul__ (Value_var "q9") (Value_var "bpp3")))
(let $__expr_19 (Value___mul__ (Value_var "q12") (Value_var "bp4")))
(let $__expr_20 (Value___mul__ (Value_var "q7") (Value_var "bp3")))
(let $__expr_21 (Value_var "bpp1"))
(let $__expr_22 (Value___mul__ (Value_var "q8") (Value_var "bpp3")))
(let $__expr_23 (Value___mul__ (Value_var "q10") (Value_var "bp4")))
(let $__expr_24 (Value___mul__ (Value_var "q12") (Value_var "bpp4")))
(let $__expr_25 (Value___mul__ (Value_var "q3") (Value_var "bp1")))
(let $__expr_26 (Value___mul__ (Value_var "q11") (Value_var "bpp4")))
(let $__expr_27 (Value_var "q12"))
(let $__expr_28 (Value_var "q3"))
(let $__expr_29 (Value_var "bpp4"))
(let $__expr_30 (Value_var "q1"))
(let $__expr_31 (Value_var "q4"))
(let $__expr_32 (Value_var "q9"))
(let $__expr_33 (Value_var "bp2"))
(let $__expr_34 (Value___mul__ (Value_var "q10") (Value_var "bpp4")))
(let $__expr_35 (Value_var "bpp3"))
(let $__expr_36 (Value_var "q10"))
(let $__expr_37 (Value_var "bp1"))
(let $__expr_38 (Value_var "q11"))
(let $__expr_39 (Value_var "bp3"))
(let $__expr_40 (Value_from_int (Int___init__ 2)))
(sort NDArray)
(sort RecursiveValue)
(constructor NDArray___init__ (RecursiveValue) NDArray)
(constructor RecursiveValue___init__ (Value) RecursiveValue)
(let $__expr_41 (Value_var "q7"))
(let $__expr_42 (Value_var "q2"))
(let $__expr_43 (Value_var "bp4"))
(constructor Value___truediv__ (Value Value) Value)
(let $__expr_44 (Value_var "q5"))
(constructor Value___add__ (Value Value) Value)
(let $__expr_45 (Value_var "q8"))
(constructor Value___pow__ (Value Value) Value)
(let $x (NDArray___init__ (RecursiveValue___init__ (Value___truediv__ (Value___add__ (Value___add__ (Value___pow__ (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_1 $__expr_4) (Value___mul__ $__expr_1 $__expr_3)) (Value___mul__ $__expr_1 $__expr_18)) (Value___mul__ $__expr_1 $__expr_24)) (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_2 $__expr_4) (Value___mul__ $__expr_2 $__expr_3)) (Value___mul__ $__expr_2 $__expr_18)) (Value___mul__ $__expr_2 $__expr_24))) (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_7 $__expr_4) (Value___mul__ $__expr_7 $__expr_3)) (Value___mul__ $__expr_7 $__expr_18)) (Value___mul__ $__expr_7 $__expr_24))) (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_5 $__expr_4) (Value___mul__ $__expr_5 $__expr_3)) (Value___mul__ $__expr_5 $__expr_18)) (Value___mul__ $__expr_5 $__expr_24))) (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_11 (Value___mul__ $__expr_25 $__expr_10)) (Value___mul__ $__expr_11 (Value___mul__ $__expr_25 $__expr_15))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_25 $__expr_22))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_25 $__expr_26))) (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_11 (Value___mul__ $__expr_6 $__expr_10)) (Value___mul__ $__expr_11 (Value___mul__ $__expr_6 $__expr_15))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_6 $__expr_22))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_6 $__expr_26)))) (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_11 (Value___mul__ $__expr_12 $__expr_10)) (Value___mul__ $__expr_11 (Value___mul__ $__expr_12 $__expr_15))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_12 $__expr_22))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_12 $__expr_26)))) (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_11 (Value___mul__ $__expr_19 $__expr_10)) (Value___mul__ $__expr_11 (Value___mul__ $__expr_19 $__expr_15))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_19 $__expr_22))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_19 $__expr_26))))) $__expr_40) (Value___pow__ (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_25 $__expr_9) (Value___mul__ $__expr_25 $__expr_16)) (Value___mul__ $__expr_25 $__expr_17)) (Value___mul__ $__expr_25 $__expr_34)) (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_6 $__expr_9) (Value___mul__ $__expr_6 $__expr_16)) (Value___mul__ $__expr_6 $__expr_17)) (Value___mul__ $__expr_6 $__expr_34))) (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_12 $__expr_9) (Value___mul__ $__expr_12 $__expr_16)) (Value___mul__ $__expr_12 $__expr_17)) (Value___mul__ $__expr_12 $__expr_34))) (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_19 $__expr_9) (Value___mul__ $__expr_19 $__expr_16)) (Value___mul__ $__expr_19 $__expr_17)) (Value___mul__ $__expr_19 $__expr_34))) (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_11 (Value___mul__ $__expr_14 $__expr_4)) (Value___mul__ $__expr_11 (Value___mul__ $__expr_14 $__expr_3))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_14 $__expr_18))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_14 $__expr_24))) (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_11 (Value___mul__ $__expr_0 $__expr_4)) (Value___mul__ $__expr_11 (Value___mul__ $__expr_0 $__expr_3))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_0 $__expr_18))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_0 $__expr_24)))) (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_11 (Value___mul__ $__expr_20 $__expr_4)) (Value___mul__ $__expr_11 (Value___mul__ $__expr_20 $__expr_3))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_20 $__expr_18))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_20 $__expr_24)))) (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_11 (Value___mul__ $__expr_23 $__expr_4)) (Value___mul__ $__expr_11 (Value___mul__ $__expr_23 $__expr_3))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_23 $__expr_18))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_23 $__expr_24))))) $__expr_40)) (Value___pow__ (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_14 $__expr_10) (Value___mul__ $__expr_14 $__expr_15)) (Value___mul__ $__expr_14 $__expr_22)) (Value___mul__ $__expr_14 $__expr_26)) (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_0 $__expr_10) (Value___mul__ $__expr_0 $__expr_15)) (Value___mul__ $__expr_0 $__expr_22)) (Value___mul__ $__expr_0 $__expr_26))) (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_20 $__expr_10) (Value___mul__ $__expr_20 $__expr_15)) (Value___mul__ $__expr_20 $__expr_22)) (Value___mul__ $__expr_20 $__expr_26))) (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_23 $__expr_10) (Value___mul__ $__expr_23 $__expr_15)) (Value___mul__ $__expr_23 $__expr_22)) (Value___mul__ $__expr_23 $__expr_26))) (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_11 (Value___mul__ $__expr_1 $__expr_9)) (Value___mul__ $__expr_11 (Value___mul__ $__expr_1 $__expr_16))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_1 $__expr_17))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_1 $__expr_34))) (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_11 (Value___mul__ $__expr_2 $__expr_9)) (Value___mul__ $__expr_11 (Value___mul__ $__expr_2 $__expr_16))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_2 $__expr_17))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_2 $__expr_34)))) (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_11 (Value___mul__ $__expr_7 $__expr_9)) (Value___mul__ $__expr_11 (Value___mul__ $__expr_7 $__expr_16))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_7 $__expr_17))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_7 $__expr_34)))) (Value___add__ (Value___add__ (Value___add__ (Value___mul__ $__expr_11 (Value___mul__ $__expr_5 $__expr_9)) (Value___mul__ $__expr_11 (Value___mul__ $__expr_5 $__expr_16))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_5 $__expr_17))) (Value___mul__ $__expr_11 (Value___mul__ $__expr_5 $__expr_34))))) $__expr_40)) (Value___pow__ (Value___add__ (Value___add__ (Value___pow__ (Value___add__ (Value___add__ (Value___add__ $__expr_14 $__expr_0) $__expr_20) $__expr_23) $__expr_40) (Value___pow__ (Value___add__ (Value___add__ (Value___add__ $__expr_1 $__expr_2) $__expr_7) $__expr_5) $__expr_40)) (Value___pow__ (Value___add__ (Value___add__ (Value___add__ $__expr_25 $__expr_6) $__expr_12) $__expr_19) $__expr_40)) (Value_from_int (Int___init__ 3)))))))
(ruleset egglog.exp.array_api.to_polynomial_ruleset)
(sort MultiSet[Value] (MultiSet Value))
(sort MultiSet[MultiSet[Value]] (MultiSet MultiSet[Value]))
(constructor polynomial (MultiSet[MultiSet[Value]]) Value)
(function get_sole_polynomial (MultiSet[Value]) MultiSet[MultiSet[Value]] :merge new)
(rule ((= _n3 (Value___add__ _n1 _n2))
       (= _mss (multiset-of (multiset-of _n1) (multiset-of _n2))))
      ((union _n3 (polynomial _mss))
       (set (get_sole_polynomial (multiset-of (polynomial _mss))) _mss)
       (delete (Value___add__ _n1 _n2)))
        :ruleset egglog.exp.array_api.to_polynomial_ruleset :name "add")
(function get_monomial (Value) MultiSet[Value] :merge new)
(rule ((= _n3 (Value___mul__ _n1 _n2))
       (= _ms (multiset-of _n1 _n2)))
      ((union _n3 (polynomial (multiset-of _ms)))
       (set (get_monomial (polynomial (multiset-of _ms))) _ms)
       (delete (Value___mul__ _n1 _n2)))
        :ruleset egglog.exp.array_api.to_polynomial_ruleset :name "mul")
(rule ((= _n3 (Value___pow__ _n1 (Value_from_int (Int___init__ _i))))
       (>= _i 0)
       (= _ms (multiset-single _n1 _i)))
      ((union _n3 (polynomial (multiset-of _ms)))
       (set (get_monomial (polynomial (multiset-of _ms))) _ms)
       (delete (Value___pow__ _n1 (Value_from_int (Int___init__ _i)))))
        :ruleset egglog.exp.array_api.to_polynomial_ruleset :name "pow")
(sort UnstableFn[MultiSet[Value],MultiSet[Value]] (UnstableFn (MultiSet[Value]) MultiSet[Value]))
(sort UnstableFn[MultiSet[Value],Value] (UnstableFn (Value) MultiSet[Value]))
(rule ((= _n1 (polynomial _mss))
       (= _mss1 (unstable-multiset-map (unstable-fn "unstable-multiset-flat-map" (unstable-fn "get_monomial")) _mss))
       (!= _mss _mss1))
      ((union _n1 (polynomial _mss1))
       (delete (polynomial _mss))
       (set (get_sole_polynomial (multiset-of _n1)) _mss1))
        :ruleset egglog.exp.array_api.to_polynomial_ruleset :name "unwrap monomial" :naive)
(sort UnstableFn[MultiSet[MultiSet[Value]],MultiSet[Value]] (UnstableFn (MultiSet[Value]) MultiSet[MultiSet[Value]]))
(rule ((= _n1 (polynomial _mss))
       (= _mss1 (unstable-multiset-flat-map (unstable-fn "get_sole_polynomial") _mss))
       (!= _mss _mss1))
      ((union _n1 (polynomial _mss1))
       (delete (polynomial _mss))
       (set (get_sole_polynomial (multiset-of _n1)) _mss1))
        :ruleset egglog.exp.array_api.to_polynomial_ruleset :name "unwrap polynomial" :naive)
(ruleset egglog.exp.array_api.factor_ruleset)
(sort UnstableFn[Unit,MultiSet[Value]] (UnstableFn (MultiSet[Value]) Unit))
(sort UnstableFn[MultiSet[Value],MultiSet[Value],MultiSet[Value]] (UnstableFn (MultiSet[Value] MultiSet[Value]) MultiSet[Value]))
(rule ((= _n (polynomial _mss))
       (= _counts (multiset-sum-multisets (unstable-multiset-map (unstable-fn "multiset-reset-counts") _mss)))
       (= _picked_term (multiset-pick-max _counts))
       (> (multiset-count _counts _picked_term) 1)
       (= _picked (unstable-multiset-filter (unstable-fn "multiset-contains-swapped" _picked_term) _mss))
       (= _factor (unstable-multiset-reduce (unstable-fn "multiset-intersection") (multiset-pick _picked) _picked))
       (= _divided (unstable-multiset-map (unstable-fn "multiset-subtract-swapped" _factor) _picked))
       (= _remainder (unstable-multiset-filter (unstable-fn "multiset-not-contains-swapped" _picked_term) _mss)))
      ((union _n (polynomial (multiset-sum (multiset-of (multiset-insert _factor (polynomial _divided))) _remainder)))
       (delete (polynomial _mss)))
        :ruleset egglog.exp.array_api.factor_ruleset :name "factor")
(ruleset egglog.exp.array_api.from_polynomial_ruleset)
(sort UnstableFn[Value,Value,Value] (UnstableFn (Value Value) Value))
(sort UnstableFn[Value,MultiSet[Value]] (UnstableFn (MultiSet[Value]) Value))
(rule ((= _n (polynomial _mss)))
      ((union _n (unstable-multiset-reduce (unstable-fn "Value___add__") (Value_from_int (Int___init__ 0)) (unstable-multiset-map (unstable-fn "unstable-multiset-reduce" (unstable-fn "Value___mul__") (Value_from_int (Int___init__ 1))) _mss)))
       (delete (polynomial _mss)))
        :ruleset egglog.exp.array_api.from_polynomial_ruleset )
(rule ((= _n1 (Value___mul__ _n _n)))
      ((union _n1 (Value___pow__ _n (Value_from_int (Int___init__ 2))))
       (delete (Value___mul__ _n _n)))
        :ruleset egglog.exp.array_api.from_polynomial_ruleset )
(rule ((= _n1 (Value___mul__ (Value___pow__ _n (Value_from_int (Int___init__ _i))) _n)))
      ((union _n1 (Value___pow__ _n (Value_from_int (Int___init__ (+ _i 1)))))
       (delete (Value___mul__ (Value___pow__ _n (Value_from_int (Int___init__ _i))) _n)))
        :ruleset egglog.exp.array_api.from_polynomial_ruleset )
(rule ((= _n1 (Value___mul__ _n (Value___pow__ _n (Value_from_int (Int___init__ _i))))))
      ((union _n1 (Value___pow__ _n (Value_from_int (Int___init__ (+ _i 1)))))
       (delete (Value___mul__ _n (Value___pow__ _n (Value_from_int (Int___init__ _i))))))
        :ruleset egglog.exp.array_api.from_polynomial_ruleset )
(rule ((= _n1 (Value___add__ _n _n)))
      ((union _n1 (Value___mul__ (Value_from_int (Int___init__ 2)) _n))
       (delete (Value___add__ _n _n)))
        :ruleset egglog.exp.array_api.from_polynomial_ruleset )
(rule ((= _n1 (Value___add__ (Value___mul__ (Value_from_int (Int___init__ _i)) _n) _n)))
      ((union _n1 (Value___mul__ (Value_from_int (Int___init__ (+ _i 1))) _n))
       (delete (Value___add__ (Value___mul__ (Value_from_int (Int___init__ _i)) _n) _n)))
        :ruleset egglog.exp.array_api.from_polynomial_ruleset )
(rule ((= _n1 (Value___add__ _n (Value___mul__ (Value_from_int (Int___init__ _i)) _n))))
      ((union _n1 (Value___mul__ (Value_from_int (Int___init__ (+ _i 1))) _n))
       (delete (Value___add__ _n (Value___mul__ (Value_from_int (Int___init__ _i)) _n))))
        :ruleset egglog.exp.array_api.from_polynomial_ruleset )
(run-schedule (seq (seq (saturate (run egglog.exp.array_api.to_polynomial_ruleset)) (saturate (run egglog.exp.array_api.factor_ruleset))) (saturate (run egglog.exp.array_api.from_polynomial_ruleset))))
(extract $x 0)