From 09f3e612bd9042b874fdb5089c4a03bd9f0f3aab Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 18 Oct 2023 15:41:21 -0300
Subject: [PATCH] defining bitblasting rules
---
spec/doc.tex | 5 +++++
spec/rule_list.tex | 15 +++++++++++++++
2 files changed, 20 insertions(+)
diff --git a/spec/doc.tex b/spec/doc.tex
index c0b26f1..c354011 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -1790,3 +1790,8 @@ standard.\footnote{See \url{https://smt-lib.github.io/theories-FixedSizeBitVecto
\bibliography{publications}
\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 0f1b08d..a182005 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -1530,6 +1530,21 @@ constants are unfolded during proof printing. Hence, the slightly strange
form and the reordering of equalities.
\end{RuleDescription}
+\begin{RuleDescription}{bitblast_extract}
+\begin{AletheX}
+$i$. & \ctxsep & $((\_\ \mathrm{extract}\ i\ j)\ x) \simeq (\mathrm{bbterm}\ x_j; \ldots; x_i)$ & (\currule) \\
+\end{AletheX}
+
+Each term $x_i$ corresponds to whether $i$-th bit of $x$ is true or not, which
+will be represented via an application of the operator ``bit\_of'', i.e.,
+$((\_\ bit\_of\ i)\ x)$, which has a Boolean return type.
+%
+The ``bbterm'' operator takes $n$ Booleans and yields a bit-vector of size $n$
+where the least significant bit is is 1 if the $n$-th argument is true, 0
+otherwise, and so on.
+
+\end{RuleDescription}
+
\clearpage
\subsection{Index of Rules}
\label{sec:alethe:rules-index}
--
GitLab