V informatice je e-graf datová struktura, která ukládá relaci ekvivalence nad termy nějakého jazyka.
Definice a operace Nechť jsou symboly funkcí v nějakém jazyce, a nechť jsou termy v tomtéž jazyce. Nechť je spočetná množina neprůhledných identifikátorů, u nichž lze ověřovat rovnost. Tuto množinu nazýváme identifikátory e-tříd. Potom e-uzel je symbol n-ární funkce společně s identifikátory e-tříd. E-třída je množina e-uzlů. E-graf obsahuje datovou strukturu disjunktních množin nad identifikátory e-tříd se standardními operacemi , , a .
Identifikátor e-tříd je kanonický, pokud . E-uzel (kde ) je kanonický, pokud je každý kanonický (kde je v ).
E-graf je kombinací: Willsey 2021
struktury disjunktních množin hashcons (tj. zobrazení) z kanonických e-uzlů na identifikátory e-tříd zobrazení e-tříd které zobrazuje identifikátory e-tříd na e-třídy tak, že přiřadí ekvivalentním identifikátorům stejnou množinu e-uzlů:
Invarianty Kromě výše uvedené struktury vyhovuje platný e-graf několika datovým invariantám. Dva e-uzly jsou ekvivalentní, pokud jsou ve stejné e-třídě. Invarianta kongruence uvádí, že e-graf musí zajistit, aby byla ekvivalence uzavřena v rámci kongruence, kde dva e-uzly jsou kongruentní, když . Invarianta hashcons postuluje, že hashcons mapuje kanonické e-uzly na identifikátor jejich e-třídy.
Operace E-grafy poskytují abstrakci kolem operací , , a ze struktury disjunktních množin, které zachovávají e-grafové invarianty. Další operací je e-párování. Ten mapuje „vzory“ (termy s proměnnými) na n-tice substitucí (od vzorů k identifikátorům e-tříd) a na identifikátory e-tříd tak, že vrácené e-třídy obsahují uzly, které odpovídají vstupnímu vzoru po aplikování substituce.
Saturace rovností Saturace rovností je technika vytváření optimalizujících překladačů pomocí e-grafů. Tate 2009 Funguje tak, že aplikuje sadu přepisovacích pravidel pomocí e-párování, dokud není e-graf nasycený, nevyprší časový limit, není dosaženo limitu velikosti e-grafu, není překročen určitý počet iterací nebo není dosaženo jiné zastavovací podmínky. Po přepisování se z e-grafu extrahuje optimální term podle nějaké nákladové funkce, obvykle související s velikostí AST nebo výkonem.
Použití E-grafy se používají v automatických důkazových systémech. Tvoří klíčovou součást moderních SMT solverů, jako jsou Z3 a CVC4.
Saturace rovností se používá ve specializovaných optimalizujících kompilátorech, např. pro hluboké učení a lineární algebru. Saturace rovností byla také použita při validaci překladu aplikovanou na sadu nástrojů LLVM.
Reference
Externí odkazy
The Egg Project Google Colab notebook vysvětlující e-grafy Kategorie:Datové struktury