Home

Bit Blasting (BV-Flattening)

Reduce bit-vector arithmetic (QF_BV) to propositional logic — one Boolean variable per bit

QF_BV → SAT
Formula Input
Propositional: && || !   BV-ops: + - * & | ^ ~   Predicates: = !=   Constants: bv0001 (binary, MSB first) or decimal 1
BV-Flattening
φ Input
↓
Propositional
Skeleton e(φ)
↓
Bit Variables
e(t)ᵢ per term
↓
BV-Constraint
for each atom
↓
BV-Constraint
for each term
↓
Return B
Constraint Table — B grows here
Run a formula to see the bit-blasting steps.
Explanation

Enter a formula and click Run ▶ to start,
then step through the BV-Flattening algorithm.