From c234c12a2741dad9446a2239bbbefc66d2ceb4b7 Mon Sep 17 00:00:00 2001 From: Hans-Joerg Schurr <commits@schurr.at> Date: Mon, 18 Mar 2024 19:47:28 -0500 Subject: [PATCH] Add bitvector rules list --- spec/rule_list.tex | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/spec/rule_list.tex b/spec/rule_list.tex index 868f23f..2152cda 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} -- GitLab