[alethe] Define pbblast_pbbconst

bernborgess · Dec 20, 2024 · d9468e5 · d9468e5
1 parent 74f0a06
commit d9468e5
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 1 deletion.
diff --git a/alethe/bit_blasting.tex b/alethe/bit_blasting.tex
@@ -169,9 +169,14 @@
         $i$. & \ctxsep & $b = \lsymb{pbbT} r \land \bigwedge_{i=0}^{n-1}{r_i = \lsymb{PB\_ZERO\_OR\_ONE}(b_{n-i-1})}$ & (\currule) \\
     \end{AletheX}
     % TODO: Explain PB_ZERO_OR_ONE := if b_i is 1 then b_i = 1 else b_i = 0
+    \noindent
+    In which we expand \textbf{PB\_ZERO\_OR\_ONE($b_i$)} into:
+    \begin{itemize}
+        \item $\left(b_i = 0\right)$ if $b_i$ is $0$
+        \item $\left(b_i = 1\right)$ if $b_i$ is $1$
+    \end{itemize}
 \end{RuleDescription}
 
-% CONST
 % XOR
 % ADD
 % AND

diff --git a/alethe/doc.pdf b/alethe/doc.pdf