2
$\begingroup$

I found a pseudo algorithm which describes bit blasting: click (page 156,157). I am trying to implement it in C, but I don't understand it yet completely. Let's make an example:

Assume our bit-vectors have only a length of 2 bits (for simplicity) and they are unsigned and out bit-vector formula looks as follows: $\phi = x \,\,\,\wedge\,\,\, y\mid 2 = z \,\,\,\wedge\,\,\, 1 < 3$.

Let's describe Boolean variables with $b_0, b_1,...$ ($x,y$ and $z$ are bit vectors).

The set of atoms would be $At(\phi) = \{ x,\,\,\, y\mid2=z,\,\,\, 1<3 \}$ and therefore the initially $\beta = e(\phi) = b_0 \,\,\,\wedge\,\,\, b_1 \,\,\,\wedge\,\,\, b_2$.

The set of terms would be $T(\phi) = \{ x,\,\,\, y, \,\,\, 2,\,\,\, z,\,\,\ 1,\,\,\,3 \}$.

Algorithm

Line 2: $\beta$ is already set.

Line 3-5: We set the $t \in T(\phi)$ to Boolean variables, hence $x \rightarrow b_3, b_4\,$ - (because we said our bit-vectors only have a length of 2 bits), the same with $y$ and $z$, but what happens with constants? I would guess: $2 \rightarrow 1,0$ or more precise $2 \rightarrow b_7=1, \, b_8=0$.

So after line 5, our $T(\phi) = \{ b_3, b_4,..., b_{14}\}$.

Then I stuck, how does it go on? And how would the equisatisfiable Boolean formula $\beta$ look like after the algorithm? Other references to other algorithms would be also nice.

$\endgroup$
  • 1
    $\begingroup$ x is not a boolean, so it doesn't make much sense to have a constraint "x is true" as you seem to have in your ϕ $\endgroup$ – harold Oct 4 '17 at 12:48
  • $\begingroup$ Sure, if it is not zero. $\endgroup$ – racc44 Oct 4 '17 at 15:14
  • $\begingroup$ Can you edit to provide a full citation for the paper/book you are referencing, so the question is still understandable if the link stops working, and so that others with a similar question about it will find this question via search? $\endgroup$ – D.W. Oct 4 '17 at 21:00
  • $\begingroup$ Can you make the question sef-contained? Can you provide a self-contained definition of your notation -- what is $\beta$? Do I need to know? What are the "lines"? $\endgroup$ – D.W. Oct 4 '17 at 21:08
4
$\begingroup$

I assume the formula is

$$(x \ne 0) \land (y|2 = z) \land (1<3).$$

We can handle each clause of the conjunction separately. If $x=(b_3,b_4)$, then $x \ne 0$ translates to

$$b_3 \lor b_4.$$

If $y=(b_5,b_6)$ and $z=(b_7,b_8)$, then $y|2$ translates to $(b_5|1,b_6)$, which simplifies to $(1,b_6)$ (if you are doing simplification). Now $(1,b_6) = (b_7,b_8)$ translates to

$$(b_7=1) \land (b_6 = b_8),$$

which in CNF form is

$$b_7 \land (b_6 \lor \neg b_8) \land (\neg b_6 \lor b_8).$$

Finally, $1<3$ translates to True, if you are doing simplification. So, the final result is the conjunction of those:

$$(b_3 \lor b_4) \land (b_7) \land (b_6 \lor \neg b_8) \land (\neg b_6 \lor b_8).$$

$\endgroup$
  • $\begingroup$ That makes it a lot clearer for me, thanks a lot. However, I don't actually understand what the given algorithm does from line 6-9, particularly line 8-9. And why we need $b_0 \,\,\wedge\,\, b_1 \,\,\wedge\,\, b_2$ as initialization (they call it the propositional skeleton of $\phi$). I will soon edit my question to make it self-containing. Can you also come up with a suggestion for something like $x + y = z$? $\endgroup$ – racc44 Oct 5 '17 at 11:25
  • 1
    $\begingroup$ @racc44, one standard approach would be to build a bitvector representation for each subexpression. So if $x=(b_3,b_4)$ and $y=(b_5,b_6)$ and $z=(b_7,b_8)$ and we use $(b_9,b_{10})$ to represent $x+y$, you first write CNF for $b_3,b_4,b_5,b_6,b_9,b_{10}$ that represents addition (this can be done using the Tseitin transform on an adder circuit), then add CNF to enforce $b_7=b_9$ and $b_8=b_{10}$. $\endgroup$ – D.W. Oct 5 '17 at 17:50
  • $\begingroup$ Nice! Do you know another paper or source which describes bit blasting? $\endgroup$ – racc44 Oct 5 '17 at 20:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.