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}