Equality Saturation
\begin{algorithm}[H]
\caption{等式飽和}
\label{equality-saturation}
\begin{algorithmic}[1]
\Function{equality\_saturation}{$\mathrm{expr}, \mathrm{rewrites}$}
\State $\mathrm{egraph} = \mathrm{initial\_egraph}(\mathrm{expr})$
\While {$(\mathrm{\mathbf{not}}\ \mathrm{saturated})\ \mathrm{and}\ (\mathrm{not}\ \mathrm{timeout()})$}
\State $\mathrm{saturated} = \mathrm{true}$
\ForAll {$\ell \rightsquigarrow r\ \mathrm{\mathbf{in}}\ \mathrm{rewrites}$}
\ForAll {$(\mathrm{subst}, \mathrm{eclass})\ \mathrm{\mathbf{in}}\ \mathrm{egraph.search}(\ell)$}
\State $c_r = \mathrm{egraph.add}(\sigma(r))$
\EndFor
\EndFor
\EndWhile
\State \Return $\mathrm{egraph.extract\_best}(\mathrm{cost\_fun})$
\EndFunction
\end{algorithmic}
\end{algorithm}