For example, I have a simple function:

int4_t add(int4_t a, int4_t b) {
    return a + b;
}

I need to eliminate integer arithmetic operations and use boolean operations instead (A.K.A., bit-blasting).

int4_t add(int4_t a, int4_t b) {
    // Extract individual bits of a and b
    bool a0 = a & 1;
    bool a1 = (a >> 1) & 1;
    bool a2 = (a >> 2) & 1;
    bool a3 = (a >> 3) & 1;

    bool b0 = b & 1;
    bool b1 = (b >> 1) & 1;
    bool b2 = (b >> 2) & 1;
    bool b3 = (b >> 3) & 1;

    // Compute sum and carry for each bit using full adder logic
    bool s0 = a0 ^ b0;
    bool c1 = a0 & b0;

    bool s1 = a1 ^ b1 ^ c1;
    bool c2 = (a1 & b1) | (a1 & c1) | (b1 & c1);

    bool s2 = a2 ^ b2 ^ c2;
    bool c3 = (a2 & b2) | (a2 & c2) | (b2 & c2);

    bool s3 = a3 ^ b3 ^ c3;
    bool c4 = (a3 & b3) | (a3 & c3) | (b3 & c3);

    // Reassemble the result
    int4_t result = (s0) | (s1 << 1) | (s2 << 2) | (s3 << 3);

    return result;
}

A possible way I can think is to implement “soft circuits” in C/C++, including full-adders for addition ops and multipliers for multiplication ops.

However I want to utilize existing tools, like Z3:

from z3 import *

x1 = BitVec('x1', 4)
x2 = BitVec('x2', 4)
out = BitVec('out', 4)

g = Goal()

bitmap = {}
for i in range(4):
    mask = BitVecSort(4).cast(math.pow(2,i))

    bitmap[(x1,i)] = Bool('x1#'+str(i))
    g.add(bitmap[(x1,i)] == ((x1 & mask) == mask))

    bitmap[(x2,i)] = Bool('x2#'+str(i))
    g.add(bitmap[(x2,i)] == ((x2 & mask) == mask))

    bitmap[(out,i)] = Bool('out#'+str(i))
    g.add(bitmap[(out,i)] == ((out & mask) == mask))

g.add(x1 + x2 == out)

simplify = Then('simplify','bit-blast','simplify')
final = simplify(g)

print(final.sexpr())

This will give simplified bit-blasted constriants, where I can recover a new program:

(goals
(goal
  (= k!0 |x1#0|)
  (= k!4 |x2#0|)
  (= k!8 |out#0|)
  (= k!1 |x1#1|)
  (= k!5 |x2#1|)
  (= k!9 |out#1|)
  (= k!2 |x1#2|)
  (= k!6 |x2#2|)
  (= k!10 |out#2|)
  (= k!3 |x1#3|)
  (= k!7 |x2#3|)
  (= k!11 |out#3|)
  (let ((a!1 (= k!1 (= k!5 (or (not k!0) (not k!4))))))
    (not (= a!1 k!9)))
  (let ((a!1 (or (not (or (not k!1) (not k!5)))
                 (not (or (not k!4) (not k!1) (not k!0)))
                 (not (or (not k!4) (not k!5) (not k!0))))))
    (= (= k!2 (= k!6 a!1)) k!10))
  (let ((a!1 (or (not (or (not k!1) (not k!5)))
                 (not (or (not k!4) (not k!1) (not k!0)))
                 (not (or (not k!4) (not k!5) (not k!0))))))
  (let ((a!2 (or (not (or (not k!2) (not k!6)))
                 (not (or (not k!2) (not a!1)))
                 (not (or (not k!6) (not a!1))))))
    (= (= k!3 (= k!7 a!2)) k!11)))
  (not (= (= k!0 k!4) k!8)))
)

But this is kind of dirty, right? Since we need to generate a C/C++ program from the output of the Z3 solver. Which is trivial.

So I am wondering what is the better way to do this.

Edit:

I must convert them into boolean variables, so I cannot use something like bitset. The process to extract each bit in an integer may be improved, and the int4_t type may not exist, but this are not closely related to the core problem 🙂
My question is mainly about “how to do bit-blasting correctly”.