From f8dcee1428eb0335959ee03ea1a90dd081afaec0 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Mon, 3 Jun 2024 11:35:07 -0500
Subject: [PATCH] Add list of rules that are only used by cvc5
---
spec/rule_list.tex | 11 +++++++++++
1 file changed, 11 insertions(+)
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 66d20af..663a4ef 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -243,6 +243,17 @@ simplifications.}
\ruleref{bitblast_add} & Bitblasting of $\lsymb{add}$. \\
\end{xltabular}
+\begin{xltabular}{\linewidth}{l X}
+\caption{Rules used by cvc5, but not by veriT.}
+\label{rule-tab:cvc5}\\
+ Rule & Description \\
+ \hline
+\ruleref{bitblast_extract} & Bitblasting of $\lsymb{extract}$. \\
+\ruleref{bitblast_ult} & Bitblasting of $\lsymb{ult}$. \\
+\ruleref{bitblast_add} & Bitblasting of $\lsymb{add}$. \\
+\ruleref{la_mult_pos} & Multiplication with a positive factor. \\
+\ruleref{la_mult_neg} & Multiplication with a negative factor.\\
+\end{xltabular}
\subsection{Rule List}
\label{sec:alethe:rules-list}
--
GitLab