From 6b8582ba2b353b37ad0d6e4688716188ecad80dd Mon Sep 17 00:00:00 2001 From: Haniel Barbosa <hanielbbarbosa@gmail.com> Date: Thu, 19 Oct 2023 17:39:00 -0300 Subject: [PATCH] fixes --- spec/rule_list.tex | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/spec/rule_list.tex b/spec/rule_list.tex index a182005..f6dbed6 100644 --- a/spec/rule_list.tex +++ b/spec/rule_list.tex @@ -1532,16 +1532,23 @@ form and the reordering of equalities. \begin{RuleDescription}{bitblast_extract} \begin{AletheX} -$i$. & \ctxsep & $((\_\ \mathrm{extract}\ i\ j)\ x) \simeq (\mathrm{bbterm}\ x_j; \ldots; x_i)$ & (\currule) \\ +$i$. & \ctxsep & $((\_\ \mathrm{extract}\ j\ i)\ x) \simeq (\mathrm{bbterm}\ x[i]\ \ldots\ x[j])$ & (\currule) \\ \end{AletheX} -Each term $x_i$ corresponds to whether $i$-th bit of $x$ is true or not, which +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 +where the least significant bit is 1 if the first argument 1 is true, 0 otherwise, and so on. +% +Alternatively, we also have: + +\begin{AletheX} +$i$. & \ctxsep & $((\_\ \mathrm{extract}\ j\ i)\ (\mathrm{bbterm}\ x_0\ \ldots\ +x_i\ \ldots \ x_j\ \ldots\ x_n)) \simeq (\mathrm{bbterm}\ x_i\ \ldots\ x_j)$ & (\currule) \\ +\end{AletheX} \end{RuleDescription} -- GitLab