diff --git a/spec/rule_list.tex b/spec/rule_list.tex index 868f23f90a2da53da5fc64bde1bbcccb0c495a73..2152cdadc91a1af19450da1ea5f4d348fc9db219 100644 --- a/spec/rule_list.tex +++ b/spec/rule_list.tex @@ -229,6 +229,16 @@ simplifications.} \ruleref{qnt_simplify} & Simplification of constant quantified formulas. \\ \end{xltabular} +\begin{xltabular}{\linewidth}{l X} +\caption{Bitvector rules.} +\label{rule-tab:simplification}\\ + Rule & Description \\ + \hline +\ruleref{bitblast_extract} & Bitblasting of $\lsymb{extract}$. \\ +\ruleref{bitblast_ult} & Bitblasting of $\lsymb{ult}$. \\ +\ruleref{bitblast_add} & Bitblasting of $\lsymb{add}$. \\ +\end{xltabular} + \subsection{Rule List} \label{sec:alethe:rules-list}