V informatice je e-graf datová struktura, která ukládá relaci ekvivalence nad termy nějakého jazyka.
Nechť jsou f , g , … {\displaystyle f,g,\ldots } symboly funkcí v nějakém jazyce, a nechť jsou t 1 , … {\displaystyle t_{1},\ldots } termy v tomtéž jazyce. Nechť je i d {\displaystyle \mathbb {id} } 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 n {\displaystyle n} identifikátory e-tříd. E-třída je množina e-uzlů. E-graf obsahuje datovou strukturu disjunktních množin U {\displaystyle U} nad identifikátory e-tříd se standardními operacemi a d d {\displaystyle \mathrm {add} } , f i n d {\displaystyle \mathrm {find} } , a m e r g e {\displaystyle \mathrm {merge} } .
Identifikátor e-tříd e {\displaystyle e} je kanonický, pokud f i n d ( U , e ) = e {\displaystyle \mathrm {find} (U,e)=e} . E-uzel f ( i 1 , … , i n ) {\displaystyle f(i_{1},\ldots ,i_{n})} (kde i 1 , … , i n ∈ i d {\displaystyle i_{1},\ldots ,i_{n}\in \mathbb {id} } ) je kanonický, pokud je každý i j {\displaystyle i_{j}} kanonický (kde j {\displaystyle j} je v 1 , … , n {\displaystyle 1,\ldots ,n} ).
E-graf je kombinací: [1]
Kromě výše uvedené struktury vyhovuje platný e-graf několika datovým invariantám. [1] 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 f ( i 1 , … , i n ) , f ( j 1 , … , j n ) {\displaystyle f(i_{1},\ldots ,i_{n}),f(j_{1},\ldots ,j_{n})} jsou kongruentní, když f i n d ( U , i k ) = f i n d ( U , j k ) , k ∈ { 1 , … , n } {\displaystyle \mathrm {find} (U,i_{k})=\mathrm {find} (U,j_{k}),k\in \{1,\ldots ,n\}} . Invarianta hashcons postuluje, že hashcons mapuje kanonické e-uzly na identifikátor jejich e-třídy.
E-grafy poskytují abstrakci kolem operací a d d {\displaystyle \mathrm {add} } , f i n d {\displaystyle \mathrm {find} } , a m e r g e {\displaystyle \mathrm {merge} } 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í je technika vytváření optimalizujících překladačů pomocí e-grafů. [2] 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.
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 [3] a CVC4.
Saturace rovností se používá ve specializovaných optimalizujících kompilátorech, [4] např. pro hluboké učení [5] a lineární algebru. [6] Saturace rovností byla také použita při validaci překladu aplikovanou na sadu nástrojů LLVM. [7]
V tomto článku byl použit překlad textu z článku E-graph na anglické Wikipedii.