3352:
2464:
1154:
3906:
3926:
3916:
2497:
is a technique for building optimizing compilers using e-graphs. It operates by applying a set of rewrites using e-matching until the e-graph is saturated, a timeout is reached, an e-graph size limit is reached, a fixed number of iterations is exceeded, or some other halting condition is reached.
891:
1135:
1708:
1588:
1510:
1013:
268:
1794:
2319:
1451:
2916:
Wang, Yisu Remy; Hutchison, Shana; Leang, Jonathan; Howe, Bill; Suciu, Dan (2020-12-22). "SPORES: Sum-Product
Optimization via Relational Equality Saturation for Large Scale Linear Algebra".
2230:
336:
3031:
Cao, David; Kunkel, Rose; Nandi, Chandrakana; Willsey, Max; Tatlock, Zachary; Polikarpova, Nadia (2023-01-09). "babble: Learning Better
Abstractions with E-Graphs and Anti-Unification".
1976:
1915:
1399:
1349:
2031:
599:
544:
2775:. 18th International Conference, LPAR-18, Merida, Venezuela, March 11–15, 2012. Lecture Notes in Computer Science. Vol. 7180. Berlin, Heidelberg: Springer. pp. 359–374.
2895:
Yang, Yichen; Phothilimtha, Phitchaya Mangpo; Wang, Yisu Remy; Willsey, Max; Roy, Sudip; Pienaar, Jacques (2021-03-17). "Equality
Saturation for Tensor Graph Superoptimization".
2370:
1621:
1275:
762:
468:
198:
1241:
406:
1210:
434:
161:
2282:
2172:
678:
96:
2399:
116:
65:
2120:
626:
2057:
2419:
2339:
2250:
2140:
2093:
1854:
1834:
1814:
1739:
1303:
757:
737:
711:
646:
488:
375:
136:
2538:(also known as non-chronological backtracking), e-graphs are extended to produce proof certificates. E-graphs are also used in the Simplify theorem prover of
1018:
3273:
2972:
2937:
Stepp, Michael; Tate, Ross; Lerner, Sorin (2011). "Equality-Based
Translation Validator for LLVM". In Gopalakrishnan, Ganesh; Qadeer, Shaz (eds.).
3217:
3178:
3104:
2956:
2788:
2755:
1626:
3351:
1515:
3528:
2426:
1456:
922:
3627:
203:
2535:
1747:
3950:
3788:
3642:
3336:
3301:
2515:
3878:
2287:
2736:
de Moura, Leonardo; Bjørner, Nikolaj (2008). "Z3: An
Efficient SMT Solver". In Ramakrishnan, C. R.; Rehof, Jakob (eds.).
1404:
1277:
operations from the union-find that preserve the e-graph invariants. The last operation, e-matching, is described below.
3841:
3360:
3311:
3246:
3010:
Coward, Samuel; Constantinides, George A.; Drane, Theo (2022-05-30). "Combining E-Graphs with
Abstract Interpretation".
3816:
3735:
354:
2183:
3266:
3846:
3566:
3114:
Willsey, Max; Nandi, Chandrakana; Wang, Yisu Remy; Flatt, Oliver; Tatlock, Zachary; Panchekha, Pavel (2021-01-04).
2498:
After rewriting, an optimal term is extracted from the e-graph according to some cost function, usually related to
3929:
2530:
by computing the congruence closure of a set of equalities, and e-matching is used to instantiate quantifiers. In
273:
3919:
3909:
3437:
3259:
2511:
1920:
1859:
1358:
1308:
3760:
3558:
3491:
3720:
3476:
3468:
2996:
Coward, Samuel; Constantinides, George A.; Drane, Theo (2022-03-17). "Abstract
Interpretation on E-Graphs".
2817:
Detlefs, David; Nelson, Greg; Saxe, James B. (May 2005). "Simplify: a theorem prover for program checking".
1981:
904:
549:
497:
3863:
3858:
3661:
3380:
2558:
68:
3689:
3588:
886:{\displaystyle \forall i,j\in \mathbb {id} ,M=M\Leftrightarrow \mathrm {find} (U,i)=\mathrm {find} (U,j)}
3486:
3392:
3385:
2771:
Rümmer, Philipp (2012). "E-Matching with Free
Variables". In Bjørner, Nikolaj; Voronkov, Andrei (eds.).
2344:
1593:
1246:
439:
170:
3656:
3651:
3538:
3414:
3402:
3331:
3091:. Lecture Notes in Computer Science. Vol. 4603. Berlin, Heidelberg: Springer. pp. 183–198.
2941:. Lecture Notes in Computer Science. Vol. 6806. Berlin, Heidelberg: Springer. pp. 737–742.
2740:. Lecture Notes in Computer Science. Vol. 4963. Berlin, Heidelberg: Springer. pp. 337–340.
2499:
1215:
380:
32:
3571:
2860:
Joshi, Rajeev; Nelson, Greg; Randall, Keith (2002-05-17). "Denali: a goal-directed superoptimizer".
1355:), includes the variables, and is closed under application of the function symbols. In other words,
1187:
411:
3668:
3503:
3375:
2546:
141:
3163:
Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on
Principles of programming languages
3637:
3578:
3548:
3533:
3498:
3397:
3341:
3296:
3223:
3184:
3145:
3127:
3084:
3066:
3040:
3011:
2997:
2917:
2896:
2842:
2692:
2255:
2145:
651:
74:
3196:
Flatt, Oliver; Coward, Samuel; Willsey, Max; Tatlock, Zachary; Panchekha, Pavel (October 2022).
2375:
3752:
3326:
3213:
3209:
3174:
3100:
3058:
2952:
2877:
2834:
2784:
2751:
2651:
2636:. Proceedings of the 5th International Workshop on Satisfiability Modulo Theories (SMT 2007).
2519:
101:
50:
3699:
3598:
3523:
3432:
3282:
3205:
3166:
3137:
3092:
3050:
2942:
2869:
2826:
2776:
2741:
2682:
2641:
2569:
20:
2098:
604:
3803:
3593:
3513:
3422:
3202:
Proceedings of the 22nd
Conference on Formal Methods in Computer-Aided Design – FMCAD 2022
2036:
3197:
3821:
3780:
3704:
3632:
3612:
3518:
3481:
3447:
3316:
2554:
2404:
2324:
2235:
2125:
2062:
1839:
1819:
1799:
1724:
1288:
742:
722:
696:
631:
473:
360:
121:
28:
3165:. POPL '09. Savannah, GA, USA: Association for Computing Machinery. pp. 264–276.
2463:
1153:
1130:{\displaystyle \mathrm {find} (U,i_{k})=\mathrm {find} (U,j_{k}),k\in \{1,\ldots ,n\}}
3944:
3508:
3442:
3306:
3227:
3149:
3070:
2973:"Wasm-mutate: Fuzzing WebAssembly Compilers with E-Graphs (EGRAPHS 2022) - PLDI 2022"
2696:
2550:
349:
then represents equivalence classes of e-nodes, using the following data structures:
3868:
3851:
3694:
3321:
3188:
2846:
2527:
691:
163:
be a countable set of opaque identifiers that may be compared for equality, called
36:
3096:
2947:
2780:
2746:
3684:
3543:
2646:
2629:
3770:
3765:
3062:
2881:
2838:
2669:
Zhang, Yihong; Wang, Yisu Remy; Willsey, Max; Tatlock, Zachary (2022-01-12).
2655:
3831:
3647:
3427:
3170:
2830:
1351:
be the smallest set that includes the 0-arity function symbols (also called
377:
representing equivalence classes of e-class IDs, with the usual operations
3158:
3157:
Tate, Ross; Stepp, Michael; Tatlock, Zachary; Lerner, Sorin (2009-01-21).
2873:
2773:
Logic for Programming, Artificial Intelligence, and Reasoning. Proceedings
3730:
2539:
903:
In addition to the above structure, a valid e-graph conforms to several
3583:
2531:
1141:
states that the hashcons maps canonical e-nodes to their e-class ID.
3141:
3054:
2687:
2670:
2628:
Moskal, Michał; Łopuszański, Jakub; Kiniry, Joseph R. (2008-05-06).
2572:, including fuzzing, abstract interpretation, and library learning.
1703:{\displaystyle f(x_{1},\ldots ,x_{n})\in \mathrm {Term} (\Sigma ,V)}
915:
states that an e-graph must ensure that equivalence is closed under
3793:
3251:
3132:
3045:
3016:
3002:
2922:
2901:
3883:
3873:
3241:
3115:
2738:
Tools and Algorithms for the Construction and Analysis of Systems
1583:{\displaystyle x_{1},\ldots ,x_{n}\in \mathrm {Term} (\Sigma ,V)}
3836:
3811:
2562:
2523:
3255:
2458:
1148:
1505:{\displaystyle \Sigma _{0}\subset \mathrm {Term} (\Sigma ,V)}
1008:{\displaystyle f(i_{1},\ldots ,i_{n}),f(j_{1},\ldots ,j_{n})}
3826:
713:(i.e. a mapping) from canonical e-nodes to e-class IDs, and
683:
An association of e-class IDs with sets of e-nodes, called
263:{\displaystyle i_{1},i_{2},\ldots ,i_{n}\in \mathbb {id} }
2804:
2710:
2421:. There are several known algorithms for e-matching, the
1789:{\displaystyle t\in \mathrm {Term} (\Sigma ,\emptyset )}
2475:
1165:
2723:
2602:
2589:
2407:
2378:
2347:
2327:
2290:
2258:
2238:
2186:
2148:
2128:
2101:
2065:
2039:
1984:
1923:
1862:
1842:
1822:
1802:
1750:
1727:
1629:
1596:
1518:
1459:
1407:
1361:
1311:
1291:
1249:
1218:
1190:
1021:
925:
765:
745:
725:
699:
654:
634:
607:
552:
500:
476:
442:
414:
383:
363:
276:
206:
173:
144:
124:
104:
77:
53:
2314:{\displaystyle \sigma \subset V\times \mathbb {id} }
3802:
3779:
3751:
3744:
3713:
3677:
3620:
3611:
3557:
3467:
3460:
3413:
3368:
3359:
3289:
1446:{\displaystyle V\subset \mathrm {Term} (\Sigma ,V)}
2568:E-graphs have been applied to several problems in
2413:
2393:
2364:
2333:
2313:
2276:
2244:
2224:
2166:
2134:
2114:
2087:
2051:
2025:
1970:
1909:
1848:
1828:
1808:
1788:
1733:
1702:
1615:
1582:
1504:
1445:
1393:
1343:
1297:
1269:
1235:
1204:
1129:
1007:
885:
751:
731:
705:
672:
640:
620:
593:
538:
482:
462:
428:
400:
369:
330:
262:
192:
155:
130:
110:
90:
59:
2634:Electronic Notes in Theoretical Computer Science
759:maps equivalent IDs to the same set of e-nodes:
3120:Proceedings of the ACM on Programming Languages
3033:Proceedings of the ACM on Programming Languages
2675:Proceedings of the ACM on Programming Languages
2615:
2225:{\displaystyle p\in \mathrm {Term} (\Sigma ,V)}
3116:"egg: Fast and extensible equality saturation"
739:that maps e-class IDs to e-classes, such that
3267:
3083:de Moura, Leonardo; Bjørner, Nikolaj (2007).
2557:. Equality saturation has also been used for
8:
1124:
1106:
331:{\displaystyle f(i_{1},i_{2},\ldots ,i_{n})}
2545:Equality saturation is used in specialized
2321:is a substitution mapping the variables in
1971:{\displaystyle f(i_{1},\ldots ,i_{n})\in C}
1910:{\displaystyle f(i_{1},\ldots ,i_{n})\in C}
3925:
3915:
3748:
3617:
3464:
3365:
3274:
3260:
3252:
3204:. TU Wien Academic Press. pp. 75–83.
1710:. A term containing variables is called a
1394:{\displaystyle \mathrm {Term} (\Sigma ,V)}
1344:{\displaystyle \mathrm {Term} (\Sigma ,V)}
3131:
3044:
3015:
3001:
2946:
2921:
2900:
2745:
2686:
2645:
2406:
2377:
2358:
2355:
2354:
2346:
2326:
2307:
2304:
2303:
2289:
2257:
2237:
2193:
2185:
2147:
2127:
2106:
2100:
2076:
2064:
2038:
2014:
1995:
1983:
1953:
1934:
1922:
1892:
1873:
1861:
1841:
1821:
1801:
1757:
1749:
1726:
1671:
1659:
1640:
1628:
1607:
1595:
1551:
1542:
1523:
1517:
1473:
1464:
1458:
1414:
1406:
1362:
1360:
1312:
1310:
1290:
1250:
1248:
1219:
1217:
1191:
1189:
1088:
1061:
1049:
1022:
1020:
996:
977:
955:
936:
924:
854:
822:
785:
782:
781:
764:
744:
724:
698:
653:
633:
612:
606:
582:
563:
551:
501:
499:
475:
443:
441:
415:
413:
384:
382:
362:
319:
300:
287:
275:
256:
253:
252:
243:
224:
211:
205:
184:
172:
149:
146:
145:
143:
123:
103:
82:
76:
52:
3210:10.34727/2022/isbn.978-3-85448-053-2_13
2581:
3198:"Small Proofs from Congruence Closure"
3085:"Efficient E-Matching for SMT Solvers"
2026:{\displaystyle g(j_{1},\ldots ,j_{n})}
594:{\displaystyle f(i_{1},\ldots ,i_{n})}
539:{\displaystyle \mathrm {find} (U,e)=e}
2372:is an e-class ID such that each term
2180:is an operation that takes a pattern
1714:, a term without variables is called
911:if they are in the same e-class. The
7:
3247:A Colab notebook explaining e-graphs
2526:, where they are used to decide the
2514:. They are a crucial part of modern
2502:size or performance considerations.
1184:E-graphs expose wrappers around the
3200:. In A. Griggio; N. Rungta (eds.).
2442:equalities can be constructed in O(
1796:if one of its e-classes represents
2365:{\displaystyle C\in \mathbb {id} }
2210:
2203:
2200:
2197:
2194:
1780:
1774:
1767:
1764:
1761:
1758:
1688:
1681:
1678:
1675:
1672:
1604:
1568:
1561:
1558:
1555:
1552:
1490:
1483:
1480:
1477:
1474:
1461:
1431:
1424:
1421:
1418:
1415:
1379:
1372:
1369:
1366:
1363:
1329:
1322:
1319:
1316:
1313:
1263:
1260:
1257:
1254:
1251:
1229:
1226:
1223:
1220:
1198:
1195:
1192:
1071:
1068:
1065:
1062:
1032:
1029:
1026:
1023:
864:
861:
858:
855:
832:
829:
826:
823:
766:
511:
508:
505:
502:
456:
453:
450:
447:
444:
422:
419:
416:
394:
391:
388:
385:
181:
105:
79:
54:
14:
118:consisting of functions of arity
3924:
3914:
3905:
3904:
3350:
2462:
1616:{\displaystyle f\in \Sigma _{n}}
1270:{\displaystyle \mathrm {merge} }
1152:
463:{\displaystyle \mathrm {merge} }
193:{\displaystyle f\in \Sigma _{n}}
2630:"E-matching for Fun and Profit"
2536:conflict-driven clause learning
1236:{\displaystyle \mathrm {find} }
401:{\displaystyle \mathrm {find} }
2388:
2382:
2271:
2259:
2219:
2207:
2082:
2069:
2020:
1988:
1959:
1927:
1898:
1866:
1783:
1771:
1697:
1685:
1665:
1633:
1577:
1565:
1499:
1487:
1440:
1428:
1401:is the smallest set such that
1388:
1376:
1338:
1326:
1305:be a set of variables and let
1205:{\displaystyle \mathrm {add} }
1094:
1075:
1055:
1036:
1002:
970:
961:
929:
880:
868:
848:
836:
819:
816:
810:
801:
795:
588:
556:
527:
515:
429:{\displaystyle \mathrm {add} }
325:
280:
1:
3089:Automated Deduction – CADE-21
156:{\displaystyle \mathbb {id} }
3097:10.1007/978-3-540-73595-3_13
3087:. In Pfenning, Frank (ed.).
2948:10.1007/978-3-642-22110-1_59
2781:10.1007/978-3-642-28717-6_28
2747:10.1007/978-3-540-78800-3_24
3628:Curry–Howard correspondence
2939:Computer Aided Verification
2647:10.1016/j.entcs.2008.04.078
2616:de Moura & Bjørner 2007
2429:and is worst-case optimal.
2277:{\displaystyle (\sigma ,C)}
2167:{\displaystyle 1,\ldots ,n}
673:{\displaystyle 1,\ldots ,n}
91:{\displaystyle \Sigma _{n}}
3967:
2394:{\displaystyle \sigma (p)}
3900:
3348:
2512:automated theorem proving
905:data structure invariants
43:Definition and operations
2534:-based solvers that use
2427:worst-case optimal joins
3477:Abstract interpretation
3171:10.1145/1480881.1480915
2831:10.1145/1066100.1066102
2671:"Relational e-matching"
2252:, and yields all pairs
111:{\displaystyle \Sigma }
69:uninterpreted functions
60:{\displaystyle \Sigma }
2559:translation validation
2425:algorithm is based on
2415:
2395:
2366:
2335:
2315:
2278:
2246:
2226:
2168:
2136:
2116:
2089:
2053:
2027:
1972:
1911:
1850:
1830:
1810:
1790:
1735:
1704:
1617:
1584:
1506:
1447:
1395:
1345:
1299:
1271:
1237:
1206:
1131:
1009:
887:
753:
733:
707:
674:
642:
622:
595:
540:
484:
464:
430:
402:
371:
332:
264:
194:
157:
132:
112:
92:
61:
3951:Graph data structures
3386:Categorical semantics
3159:"Equality saturation"
2874:10.1145/543552.512566
2510:E-graphs are used in
2423:relational e-matching
2416:
2396:
2367:
2336:
2316:
2279:
2247:
2227:
2169:
2137:
2117:
2115:{\displaystyle j_{k}}
2090:
2054:
2028:
1973:
1912:
1851:
1831:
1811:
1791:
1736:
1705:
1618:
1585:
1507:
1448:
1396:
1346:
1300:
1272:
1238:
1207:
1132:
1010:
888:
754:
734:
708:
675:
643:
623:
621:{\displaystyle i_{j}}
601:is canonical if each
596:
541:
485:
465:
431:
403:
372:
333:
265:
195:
167:. The application of
158:
133:
113:
93:
62:
3332:Runtime verification
3126:(POPL): 23:1–23:29.
2681:(POPL): 35:1–35:22.
2547:optimizing compilers
2405:
2376:
2345:
2325:
2288:
2256:
2236:
2184:
2146:
2126:
2099:
2095:represents the term
2063:
2037:
1982:
1921:
1860:
1840:
1820:
1800:
1748:
1725:
1627:
1594:
1516:
1457:
1405:
1359:
1309:
1289:
1247:
1216:
1188:
1019:
923:
919:, where two e-nodes
913:congruence invariant
763:
743:
723:
697:
652:
632:
605:
550:
498:
474:
440:
412:
381:
361:
274:
204:
171:
142:
122:
102:
75:
51:
33:equivalence relation
16:Graph data structure
3589:Invariant inference
3337:Safety and liveness
2862:ACM SIGPLAN Notices
2603:Willsey et al. 2021
2590:Willsey et al. 2021
2495:Equality saturation
2455:Equality saturation
2341:to e-class IDs and
2052:{\displaystyle f=g}
1015:are congruent when
687:. This consists of
3753:Constraint solvers
3579:Concolic execution
3534:Symbolic execution
3342:Undefined behavior
3297:Control-flow graph
2977:pldi22.sigplan.org
2819:Journal of the ACM
2474:. You can help by
2411:
2401:is represented by
2391:
2362:
2331:
2311:
2274:
2242:
2222:
2164:
2132:
2112:
2085:
2049:
2023:
1978:represents a term
1968:
1907:
1846:
1826:
1806:
1786:
1731:
1700:
1613:
1580:
1502:
1443:
1391:
1341:
1295:
1267:
1233:
1202:
1164:. You can help by
1139:hashcons invariant
1127:
1005:
907:. Two e-nodes are
883:
749:
729:
703:
670:
638:
618:
591:
536:
480:
460:
426:
398:
367:
328:
260:
190:
153:
128:
108:
88:
57:
39:of some language.
3938:
3937:
3896:
3895:
3892:
3891:
3607:
3606:
3456:
3455:
3219:978-3-85448-053-2
3180:978-1-60558-379-2
3106:978-3-540-73595-3
3039:(POPL): 396–424.
2958:978-3-642-22110-1
2805:Flatt et al. 2022
2790:978-3-642-28717-6
2757:978-3-540-78800-3
2711:Flatt et al. 2022
2492:
2491:
2414:{\displaystyle C}
2334:{\displaystyle p}
2245:{\displaystyle E}
2135:{\displaystyle k}
2088:{\displaystyle M}
2059:and each e-class
1849:{\displaystyle t}
1829:{\displaystyle C}
1809:{\displaystyle t}
1734:{\displaystyle E}
1298:{\displaystyle V}
1182:
1181:
752:{\displaystyle M}
732:{\displaystyle M}
706:{\displaystyle H}
641:{\displaystyle j}
483:{\displaystyle e}
370:{\displaystyle U}
131:{\displaystyle n}
98:is the subset of
3958:
3928:
3927:
3918:
3917:
3908:
3907:
3804:Proof assistants
3749:
3618:
3465:
3438:Rewriting system
3433:Process calculus
3366:
3354:
3283:Program analysis
3276:
3269:
3262:
3253:
3231:
3192:
3153:
3135:
3110:
3075:
3074:
3048:
3028:
3022:
3021:
3019:
3007:
3005:
2993:
2987:
2986:
2984:
2983:
2969:
2963:
2962:
2950:
2934:
2928:
2927:
2925:
2913:
2907:
2906:
2904:
2892:
2886:
2885:
2857:
2851:
2850:
2814:
2808:
2801:
2795:
2794:
2768:
2762:
2761:
2749:
2733:
2727:
2724:Tate et al. 2009
2720:
2714:
2707:
2701:
2700:
2690:
2666:
2660:
2659:
2649:
2625:
2619:
2612:
2606:
2599:
2593:
2586:
2570:program analysis
2487:
2484:
2466:
2459:
2438:An e-graph with
2420:
2418:
2417:
2412:
2400:
2398:
2397:
2392:
2371:
2369:
2368:
2363:
2361:
2340:
2338:
2337:
2332:
2320:
2318:
2317:
2312:
2310:
2283:
2281:
2280:
2275:
2251:
2249:
2248:
2243:
2231:
2229:
2228:
2223:
2206:
2173:
2171:
2170:
2165:
2141:
2139:
2138:
2133:
2121:
2119:
2118:
2113:
2111:
2110:
2094:
2092:
2091:
2086:
2081:
2080:
2058:
2056:
2055:
2050:
2032:
2030:
2029:
2024:
2019:
2018:
2000:
1999:
1977:
1975:
1974:
1969:
1958:
1957:
1939:
1938:
1917:does. An e-node
1916:
1914:
1913:
1908:
1897:
1896:
1878:
1877:
1855:
1853:
1852:
1847:
1835:
1833:
1832:
1827:
1815:
1813:
1812:
1807:
1795:
1793:
1792:
1787:
1770:
1740:
1738:
1737:
1732:
1709:
1707:
1706:
1701:
1684:
1664:
1663:
1645:
1644:
1622:
1620:
1619:
1614:
1612:
1611:
1589:
1587:
1586:
1581:
1564:
1547:
1546:
1528:
1527:
1511:
1509:
1508:
1503:
1486:
1469:
1468:
1452:
1450:
1449:
1444:
1427:
1400:
1398:
1397:
1392:
1375:
1350:
1348:
1347:
1342:
1325:
1304:
1302:
1301:
1296:
1276:
1274:
1273:
1268:
1266:
1242:
1240:
1239:
1234:
1232:
1211:
1209:
1208:
1203:
1201:
1177:
1174:
1156:
1149:
1136:
1134:
1133:
1128:
1093:
1092:
1074:
1054:
1053:
1035:
1014:
1012:
1011:
1006:
1001:
1000:
982:
981:
960:
959:
941:
940:
892:
890:
889:
884:
867:
835:
788:
758:
756:
755:
750:
738:
736:
735:
730:
712:
710:
709:
704:
679:
677:
676:
671:
647:
645:
644:
639:
627:
625:
624:
619:
617:
616:
600:
598:
597:
592:
587:
586:
568:
567:
545:
543:
542:
537:
514:
489:
487:
486:
481:
470:. An e-class ID
469:
467:
466:
461:
459:
435:
433:
432:
427:
425:
407:
405:
404:
399:
397:
376:
374:
373:
368:
337:
335:
334:
329:
324:
323:
305:
304:
292:
291:
269:
267:
266:
261:
259:
248:
247:
229:
228:
216:
215:
199:
197:
196:
191:
189:
188:
162:
160:
159:
154:
152:
137:
135:
134:
129:
117:
115:
114:
109:
97:
95:
94:
89:
87:
86:
66:
64:
63:
58:
21:computer science
3966:
3965:
3961:
3960:
3959:
3957:
3956:
3955:
3941:
3940:
3939:
3934:
3888:
3798:
3775:
3740:
3714:Data structures
3709:
3673:
3603:
3594:Program slicing
3553:
3452:
3423:Lambda calculus
3409:
3355:
3346:
3307:Hyperproperties
3285:
3280:
3242:The Egg Project
3238:
3220:
3195:
3181:
3156:
3142:10.1145/3434304
3113:
3107:
3082:
3079:
3078:
3055:10.1145/3571207
3030:
3029:
3025:
3009:
3008:
2995:
2994:
2990:
2981:
2979:
2971:
2970:
2966:
2959:
2936:
2935:
2931:
2915:
2914:
2910:
2894:
2893:
2889:
2859:
2858:
2854:
2816:
2815:
2811:
2802:
2798:
2791:
2770:
2769:
2765:
2758:
2735:
2734:
2730:
2721:
2717:
2708:
2704:
2688:10.1145/3498696
2668:
2667:
2663:
2627:
2626:
2622:
2613:
2609:
2600:
2596:
2587:
2583:
2578:
2561:applied to the
2508:
2488:
2482:
2479:
2472:needs expansion
2457:
2435:
2403:
2402:
2374:
2373:
2343:
2342:
2323:
2322:
2286:
2285:
2254:
2253:
2234:
2233:
2232:and an e-graph
2182:
2181:
2144:
2143:
2124:
2123:
2102:
2097:
2096:
2072:
2061:
2060:
2035:
2034:
2010:
1991:
1980:
1979:
1949:
1930:
1919:
1918:
1888:
1869:
1858:
1857:
1856:if some e-node
1838:
1837:
1818:
1817:
1798:
1797:
1746:
1745:
1723:
1722:
1655:
1636:
1625:
1624:
1603:
1592:
1591:
1538:
1519:
1514:
1513:
1460:
1455:
1454:
1403:
1402:
1357:
1356:
1307:
1306:
1287:
1286:
1283:
1245:
1244:
1214:
1213:
1186:
1185:
1178:
1172:
1169:
1162:needs expansion
1147:
1084:
1045:
1017:
1016:
992:
973:
951:
932:
921:
920:
901:
761:
760:
741:
740:
721:
720:
695:
694:
650:
649:
630:
629:
608:
603:
602:
578:
559:
548:
547:
496:
495:
472:
471:
438:
437:
410:
409:
379:
378:
359:
358:
315:
296:
283:
272:
271:
239:
220:
207:
202:
201:
200:to e-class IDs
180:
169:
168:
140:
139:
120:
119:
100:
99:
78:
73:
72:
49:
48:
45:
31:that stores an
17:
12:
11:
5:
3964:
3962:
3954:
3953:
3943:
3942:
3936:
3935:
3933:
3932:
3922:
3912:
3901:
3898:
3897:
3894:
3893:
3890:
3889:
3887:
3886:
3881:
3876:
3871:
3866:
3861:
3856:
3855:
3854:
3844:
3839:
3834:
3829:
3824:
3819:
3814:
3808:
3806:
3800:
3799:
3797:
3796:
3791:
3785:
3783:
3777:
3776:
3774:
3773:
3768:
3763:
3757:
3755:
3746:
3742:
3741:
3739:
3738:
3733:
3728:
3723:
3717:
3715:
3711:
3710:
3708:
3707:
3702:
3697:
3692:
3687:
3681:
3679:
3675:
3674:
3672:
3671:
3666:
3665:
3664:
3654:
3645:
3640:
3635:
3633:Loop invariant
3630:
3624:
3622:
3615:
3613:Formal methods
3609:
3608:
3605:
3604:
3602:
3601:
3596:
3591:
3586:
3581:
3576:
3575:
3574:
3572:Taint tracking
3563:
3561:
3555:
3554:
3552:
3551:
3546:
3541:
3536:
3531:
3526:
3521:
3519:Model checking
3516:
3511:
3506:
3501:
3496:
3495:
3494:
3484:
3479:
3473:
3471:
3462:
3458:
3457:
3454:
3453:
3451:
3450:
3448:Turing machine
3445:
3440:
3435:
3430:
3425:
3419:
3417:
3411:
3410:
3408:
3407:
3406:
3405:
3400:
3390:
3389:
3388:
3378:
3372:
3370:
3363:
3357:
3356:
3349:
3347:
3345:
3344:
3339:
3334:
3329:
3327:Rice's theorem
3324:
3319:
3317:Path explosion
3314:
3309:
3304:
3299:
3293:
3291:
3287:
3286:
3281:
3279:
3278:
3271:
3264:
3256:
3250:
3249:
3244:
3237:
3236:External links
3234:
3233:
3232:
3218:
3193:
3179:
3154:
3111:
3105:
3077:
3076:
3023:
2988:
2964:
2957:
2929:
2908:
2887:
2868:(5): 304–314.
2852:
2825:(3): 365–473.
2809:
2796:
2789:
2763:
2756:
2728:
2715:
2702:
2661:
2620:
2607:
2594:
2580:
2579:
2577:
2574:
2555:linear algebra
2507:
2504:
2490:
2489:
2469:
2467:
2456:
2453:
2452:
2451:
2434:
2431:
2410:
2390:
2387:
2384:
2381:
2360:
2357:
2353:
2350:
2330:
2309:
2306:
2302:
2299:
2296:
2293:
2273:
2270:
2267:
2264:
2261:
2241:
2221:
2218:
2215:
2212:
2209:
2205:
2202:
2199:
2196:
2192:
2189:
2163:
2160:
2157:
2154:
2151:
2131:
2109:
2105:
2084:
2079:
2075:
2071:
2068:
2048:
2045:
2042:
2022:
2017:
2013:
2009:
2006:
2003:
1998:
1994:
1990:
1987:
1967:
1964:
1961:
1956:
1952:
1948:
1945:
1942:
1937:
1933:
1929:
1926:
1906:
1903:
1900:
1895:
1891:
1887:
1884:
1881:
1876:
1872:
1868:
1865:
1845:
1825:
1805:
1785:
1782:
1779:
1776:
1773:
1769:
1766:
1763:
1760:
1756:
1753:
1744:a ground term
1730:
1699:
1696:
1693:
1690:
1687:
1683:
1680:
1677:
1674:
1670:
1667:
1662:
1658:
1654:
1651:
1648:
1643:
1639:
1635:
1632:
1610:
1606:
1602:
1599:
1579:
1576:
1573:
1570:
1567:
1563:
1560:
1557:
1554:
1550:
1545:
1541:
1537:
1534:
1531:
1526:
1522:
1501:
1498:
1495:
1492:
1489:
1485:
1482:
1479:
1476:
1472:
1467:
1463:
1442:
1439:
1436:
1433:
1430:
1426:
1423:
1420:
1417:
1413:
1410:
1390:
1387:
1384:
1381:
1378:
1374:
1371:
1368:
1365:
1340:
1337:
1334:
1331:
1328:
1324:
1321:
1318:
1315:
1294:
1282:
1279:
1265:
1262:
1259:
1256:
1253:
1231:
1228:
1225:
1222:
1200:
1197:
1194:
1180:
1179:
1159:
1157:
1146:
1143:
1126:
1123:
1120:
1117:
1114:
1111:
1108:
1105:
1102:
1099:
1096:
1091:
1087:
1083:
1080:
1077:
1073:
1070:
1067:
1064:
1060:
1057:
1052:
1048:
1044:
1041:
1038:
1034:
1031:
1028:
1025:
1004:
999:
995:
991:
988:
985:
980:
976:
972:
969:
966:
963:
958:
954:
950:
947:
944:
939:
935:
931:
928:
900:
897:
896:
895:
894:
893:
882:
879:
876:
873:
870:
866:
863:
860:
857:
853:
850:
847:
844:
841:
838:
834:
831:
828:
825:
821:
818:
815:
812:
809:
806:
803:
800:
797:
794:
791:
787:
784:
780:
777:
774:
771:
768:
748:
728:
714:
702:
681:
669:
666:
663:
660:
657:
637:
628:is canonical (
615:
611:
590:
585:
581:
577:
574:
571:
566:
562:
558:
555:
535:
532:
529:
526:
523:
520:
517:
513:
510:
507:
504:
479:
458:
455:
452:
449:
446:
424:
421:
418:
396:
393:
390:
387:
366:
338:and called an
327:
322:
318:
314:
311:
308:
303:
299:
295:
290:
286:
282:
279:
258:
255:
251:
246:
242:
238:
235:
232:
227:
223:
219:
214:
210:
187:
183:
179:
176:
151:
148:
127:
107:
85:
81:
56:
44:
41:
29:data structure
15:
13:
10:
9:
6:
4:
3:
2:
3963:
3952:
3949:
3948:
3946:
3931:
3923:
3921:
3913:
3911:
3903:
3902:
3899:
3885:
3882:
3880:
3877:
3875:
3872:
3870:
3867:
3865:
3862:
3860:
3857:
3853:
3850:
3849:
3848:
3845:
3843:
3840:
3838:
3835:
3833:
3830:
3828:
3825:
3823:
3820:
3818:
3815:
3813:
3810:
3809:
3807:
3805:
3801:
3795:
3792:
3790:
3787:
3786:
3784:
3782:
3778:
3772:
3769:
3767:
3764:
3762:
3759:
3758:
3756:
3754:
3750:
3747:
3743:
3737:
3734:
3732:
3729:
3727:
3724:
3722:
3719:
3718:
3716:
3712:
3706:
3703:
3701:
3698:
3696:
3693:
3691:
3690:Incorrectness
3688:
3686:
3683:
3682:
3680:
3676:
3670:
3667:
3663:
3660:
3659:
3658:
3657:Specification
3655:
3653:
3649:
3646:
3644:
3641:
3639:
3636:
3634:
3631:
3629:
3626:
3625:
3623:
3619:
3616:
3614:
3610:
3600:
3597:
3595:
3592:
3590:
3587:
3585:
3582:
3580:
3577:
3573:
3570:
3569:
3568:
3565:
3564:
3562:
3560:
3556:
3550:
3547:
3545:
3542:
3540:
3537:
3535:
3532:
3530:
3527:
3525:
3522:
3520:
3517:
3515:
3512:
3510:
3509:Effect system
3507:
3505:
3502:
3500:
3497:
3493:
3490:
3489:
3488:
3485:
3483:
3480:
3478:
3475:
3474:
3472:
3470:
3466:
3463:
3459:
3449:
3446:
3444:
3443:State machine
3441:
3439:
3436:
3434:
3431:
3429:
3426:
3424:
3421:
3420:
3418:
3416:
3412:
3404:
3401:
3399:
3396:
3395:
3394:
3391:
3387:
3384:
3383:
3382:
3379:
3377:
3374:
3373:
3371:
3367:
3364:
3362:
3358:
3353:
3343:
3340:
3338:
3335:
3333:
3330:
3328:
3325:
3323:
3320:
3318:
3315:
3313:
3310:
3308:
3305:
3303:
3300:
3298:
3295:
3294:
3292:
3288:
3284:
3277:
3272:
3270:
3265:
3263:
3258:
3257:
3254:
3248:
3245:
3243:
3240:
3239:
3235:
3229:
3225:
3221:
3215:
3211:
3207:
3203:
3199:
3194:
3190:
3186:
3182:
3176:
3172:
3168:
3164:
3160:
3155:
3151:
3147:
3143:
3139:
3134:
3129:
3125:
3121:
3117:
3112:
3108:
3102:
3098:
3094:
3090:
3086:
3081:
3080:
3072:
3068:
3064:
3060:
3056:
3052:
3047:
3042:
3038:
3034:
3027:
3024:
3018:
3013:
3004:
2999:
2992:
2989:
2978:
2974:
2968:
2965:
2960:
2954:
2949:
2944:
2940:
2933:
2930:
2924:
2919:
2912:
2909:
2903:
2898:
2891:
2888:
2883:
2879:
2875:
2871:
2867:
2863:
2856:
2853:
2848:
2844:
2840:
2836:
2832:
2828:
2824:
2820:
2813:
2810:
2806:
2800:
2797:
2792:
2786:
2782:
2778:
2774:
2767:
2764:
2759:
2753:
2748:
2743:
2739:
2732:
2729:
2725:
2719:
2716:
2712:
2706:
2703:
2698:
2694:
2689:
2684:
2680:
2676:
2672:
2665:
2662:
2657:
2653:
2648:
2643:
2639:
2635:
2631:
2624:
2621:
2617:
2611:
2608:
2604:
2598:
2595:
2591:
2585:
2582:
2575:
2573:
2571:
2566:
2564:
2560:
2556:
2552:
2551:deep learning
2548:
2543:
2541:
2537:
2533:
2529:
2525:
2521:
2517:
2513:
2505:
2503:
2501:
2496:
2486:
2477:
2473:
2470:This section
2468:
2465:
2461:
2460:
2454:
2449:
2445:
2441:
2437:
2436:
2432:
2430:
2428:
2424:
2408:
2385:
2379:
2351:
2348:
2328:
2300:
2297:
2294:
2291:
2268:
2265:
2262:
2239:
2216:
2213:
2190:
2187:
2179:
2175:
2161:
2158:
2155:
2152:
2149:
2129:
2107:
2103:
2077:
2073:
2066:
2046:
2043:
2040:
2015:
2011:
2007:
2004:
2001:
1996:
1992:
1985:
1965:
1962:
1954:
1950:
1946:
1943:
1940:
1935:
1931:
1924:
1904:
1901:
1893:
1889:
1885:
1882:
1879:
1874:
1870:
1863:
1843:
1823:
1816:. An e-class
1803:
1777:
1754:
1751:
1743:
1728:
1719:
1717:
1713:
1694:
1691:
1668:
1660:
1656:
1652:
1649:
1646:
1641:
1637:
1630:
1608:
1600:
1597:
1574:
1571:
1548:
1543:
1539:
1535:
1532:
1529:
1524:
1520:
1496:
1493:
1470:
1465:
1437:
1434:
1411:
1408:
1385:
1382:
1354:
1335:
1332:
1292:
1280:
1278:
1176:
1167:
1163:
1160:This section
1158:
1155:
1151:
1150:
1144:
1142:
1140:
1121:
1118:
1115:
1112:
1109:
1103:
1100:
1097:
1089:
1085:
1081:
1078:
1058:
1050:
1046:
1042:
1039:
997:
993:
989:
986:
983:
978:
974:
967:
964:
956:
952:
948:
945:
942:
937:
933:
926:
918:
914:
910:
906:
898:
877:
874:
871:
851:
845:
842:
839:
813:
807:
804:
798:
792:
789:
778:
775:
772:
769:
746:
726:
719:
715:
700:
693:
689:
688:
686:
682:
667:
664:
661:
658:
655:
635:
613:
609:
583:
579:
575:
572:
569:
564:
560:
553:
533:
530:
524:
521:
518:
493:
477:
364:
356:
352:
351:
350:
348:
343:
341:
320:
316:
312:
309:
306:
301:
297:
293:
288:
284:
277:
249:
244:
240:
236:
233:
230:
225:
221:
217:
212:
208:
185:
177:
174:
166:
125:
83:
70:
42:
40:
38:
34:
30:
26:
22:
3852:Isabelle/HOL
3725:
3669:Verification
3652:completeness
3544:Type systems
3487:Control flow
3381:Denotational
3322:Polyvariance
3290:Key concepts
3201:
3162:
3123:
3119:
3088:
3036:
3032:
3026:
2991:
2980:. Retrieved
2976:
2967:
2938:
2932:
2911:
2890:
2865:
2861:
2855:
2822:
2818:
2812:
2807:, p. 2)
2799:
2772:
2766:
2737:
2731:
2718:
2713:, p. 2)
2705:
2678:
2674:
2664:
2640:(2): 19–35.
2637:
2633:
2623:
2610:
2597:
2584:
2567:
2544:
2528:empty theory
2509:
2506:Applications
2494:
2493:
2480:
2476:adding to it
2471:
2447:
2443:
2439:
2422:
2177:
2176:
1741:
1720:
1715:
1711:
1352:
1284:
1183:
1170:
1166:adding to it
1161:
1138:
916:
912:
908:
902:
717:
684:
546:; an e-node
491:
346:
344:
339:
164:
67:be a set of
46:
24:
18:
3781:Lightweight
3643:Side effect
3539:Termination
3393:Operational
3302:Correctness
2565:toolchain.
2549:, e.g. for
2516:SMT solvers
1836:represents
1721:An e-graph
1512:, and when
718:e-class map
270:is denoted
165:e-class IDs
3736:Union-find
3700:Separation
3638:Refinement
3504:Dependence
3403:Small-step
3312:Invariants
3133:2004.03082
3046:2212.04596
3017:2205.14989
3003:2203.09191
2982:2023-02-03
2923:2002.07951
2902:2101.01332
2576:References
2433:Complexity
2178:e-matching
1742:represents
1281:E-matching
1145:Operations
917:congruence
909:equivalent
899:Invariants
357:structure
355:union-find
3832:HOL Light
3662:Languages
3648:Soundness
3567:Data-flow
3549:Typestate
3499:Data-flow
3428:Petri net
3376:Axiomatic
3361:Semantics
3228:252118847
3150:226282597
3071:254536022
3063:2475-1421
2882:0362-1340
2839:0004-5411
2697:236924583
2656:1571-0661
2483:June 2021
2380:σ
2352:∈
2301:×
2295:⊂
2292:σ
2263:σ
2211:Σ
2191:∈
2156:…
2005:…
1963:∈
1944:…
1902:∈
1883:…
1781:∅
1775:Σ
1755:∈
1689:Σ
1669:∈
1650:…
1605:Σ
1601:∈
1569:Σ
1549:∈
1533:…
1491:Σ
1471:⊂
1462:Σ
1432:Σ
1412:⊂
1380:Σ
1353:constants
1330:Σ
1173:June 2021
1116:…
1104:∈
987:…
946:…
820:⇔
779:∈
767:∀
685:e-classes
662:…
573:…
492:canonical
310:…
250:∈
234:…
182:Σ
178:∈
106:Σ
80:Σ
55:Σ
3945:Category
3930:Glossary
3910:Category
3847:Isabelle
3731:Hashcons
3705:Temporal
3621:Concepts
3461:Analyses
3398:Big-step
2540:ESC/Java
2518:such as
692:hashcons
71:, where
3920:Outline
3726:E-graph
3599:Testing
3584:Fuzzing
3559:Dynamic
3524:Pointer
3189:2138086
2847:9613854
2532:DPLL(T)
2450:) time.
1712:pattern
1623:, then
347:e-graph
25:e-graph
3695:Linear
3678:Logics
3514:Escape
3469:Static
3415:Models
3226:
3216:
3187:
3177:
3148:
3103:
3069:
3061:
2955:
2880:
2845:
2837:
2787:
2754:
2695:
2654:
2284:where
1716:ground
1243:, and
1137:. The
340:e-node
138:. Let
3884:Twelf
3874:NuPRL
3869:Mizar
3842:Idris
3789:Alloy
3745:Tools
3685:Hoare
3529:Shape
3482:Alias
3369:Types
3224:S2CID
3185:S2CID
3146:S2CID
3128:arXiv
3067:S2CID
3041:arXiv
3012:arXiv
2998:arXiv
2918:arXiv
2897:arXiv
2843:S2CID
2693:S2CID
37:terms
35:over
27:is a
23:, an
3864:LEGO
3859:Lean
3837:HOL4
3817:Agda
3812:ACL2
3794:TLA+
3650:and
3492:kCFA
3214:ISBN
3175:ISBN
3101:ISBN
3059:ISSN
2953:ISBN
2878:ISSN
2835:ISSN
2785:ISBN
2752:ISBN
2652:ISSN
2563:LLVM
2553:and
2524:CVC4
2522:and
2446:log
1590:and
1285:Let
436:and
345:The
47:Let
3879:PVS
3822:Coq
3771:SMT
3766:SAT
3761:CHC
3721:BDD
3206:doi
3167:doi
3138:doi
3093:doi
3051:doi
2943:doi
2870:doi
2827:doi
2777:doi
2742:doi
2683:doi
2642:doi
2638:198
2500:AST
2478:.
2174:).
2142:in
2033:if
1168:.
716:an
648:in
494:if
490:is
19:In
3947::
3827:F*
3222:.
3212:.
3183:.
3173:.
3161:.
3144:.
3136:.
3122:.
3118:.
3099:.
3065:.
3057:.
3049:.
3035:.
2975:.
2951:.
2876:.
2866:37
2864:.
2841:.
2833:.
2823:52
2821:.
2783:.
2750:.
2691:.
2677:.
2673:.
2650:.
2632:.
2542:.
2520:Z3
1718:.
1453:,
1212:,
690:a
680:).
408:,
353:A
342:.
3275:e
3268:t
3261:v
3230:.
3208::
3191:.
3169::
3152:.
3140::
3130::
3124:5
3109:.
3095::
3073:.
3053::
3043::
3037:7
3020:.
3014::
3006:.
3000::
2985:.
2961:.
2945::
2926:.
2920::
2905:.
2899::
2884:.
2872::
2849:.
2829::
2803:(
2793:.
2779::
2760:.
2744::
2726:)
2722:(
2709:(
2699:.
2685::
2679:6
2658:.
2644::
2618:)
2614:(
2605:)
2601:(
2592:)
2588:(
2485:)
2481:(
2448:n
2444:n
2440:n
2409:C
2389:)
2386:p
2383:(
2359:d
2356:i
2349:C
2329:p
2308:d
2305:i
2298:V
2272:)
2269:C
2266:,
2260:(
2240:E
2220:)
2217:V
2214:,
2208:(
2204:m
2201:r
2198:e
2195:T
2188:p
2162:n
2159:,
2153:,
2150:1
2130:k
2122:(
2108:k
2104:j
2083:]
2078:k
2074:i
2070:[
2067:M
2047:g
2044:=
2041:f
2021:)
2016:n
2012:j
2008:,
2002:,
1997:1
1993:j
1989:(
1986:g
1966:C
1960:)
1955:n
1951:i
1947:,
1941:,
1936:1
1932:i
1928:(
1925:f
1905:C
1899:)
1894:n
1890:i
1886:,
1880:,
1875:1
1871:i
1867:(
1864:f
1844:t
1824:C
1804:t
1784:)
1778:,
1772:(
1768:m
1765:r
1762:e
1759:T
1752:t
1729:E
1698:)
1695:V
1692:,
1686:(
1682:m
1679:r
1676:e
1673:T
1666:)
1661:n
1657:x
1653:,
1647:,
1642:1
1638:x
1634:(
1631:f
1609:n
1598:f
1578:)
1575:V
1572:,
1566:(
1562:m
1559:r
1556:e
1553:T
1544:n
1540:x
1536:,
1530:,
1525:1
1521:x
1500:)
1497:V
1494:,
1488:(
1484:m
1481:r
1478:e
1475:T
1466:0
1441:)
1438:V
1435:,
1429:(
1425:m
1422:r
1419:e
1416:T
1409:V
1389:)
1386:V
1383:,
1377:(
1373:m
1370:r
1367:e
1364:T
1339:)
1336:V
1333:,
1327:(
1323:m
1320:r
1317:e
1314:T
1293:V
1264:e
1261:g
1258:r
1255:e
1252:m
1230:d
1227:n
1224:i
1221:f
1199:d
1196:d
1193:a
1175:)
1171:(
1125:}
1122:n
1119:,
1113:,
1110:1
1107:{
1101:k
1098:,
1095:)
1090:k
1086:j
1082:,
1079:U
1076:(
1072:d
1069:n
1066:i
1063:f
1059:=
1056:)
1051:k
1047:i
1043:,
1040:U
1037:(
1033:d
1030:n
1027:i
1024:f
1003:)
998:n
994:j
990:,
984:,
979:1
975:j
971:(
968:f
965:,
962:)
957:n
953:i
949:,
943:,
938:1
934:i
930:(
927:f
881:)
878:j
875:,
872:U
869:(
865:d
862:n
859:i
856:f
852:=
849:)
846:i
843:,
840:U
837:(
833:d
830:n
827:i
824:f
817:]
814:j
811:[
808:M
805:=
802:]
799:i
796:[
793:M
790:,
786:d
783:i
776:j
773:,
770:i
747:M
727:M
701:H
668:n
665:,
659:,
656:1
636:j
614:j
610:i
589:)
584:n
580:i
576:,
570:,
565:1
561:i
557:(
554:f
534:e
531:=
528:)
525:e
522:,
519:U
516:(
512:d
509:n
506:i
503:f
478:e
457:e
454:g
451:r
448:e
445:m
423:d
420:d
417:a
395:d
392:n
389:i
386:f
365:U
326:)
321:n
317:i
313:,
307:,
302:2
298:i
294:,
289:1
285:i
281:(
278:f
257:d
254:i
245:n
241:i
237:,
231:,
226:2
222:i
218:,
213:1
209:i
186:n
175:f
150:d
147:i
126:n
84:n
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
