# Fixed-Width Bitvectors

Bitvector: integer from some finite inteval of length Example: Logic on bitvectors.

• formulas for +.

We can reduce reasoning on bitvectors to reasoning in propositional logic.

Application:

• exact reasoning about Java integers
• finding counterexamples for formulas over unbounded integers

## Expressing Linear Arithmetic with Given Bounds

Consider formulas in our linear arithmetic language:

 T ::= K | V | (T + T) | (T - T) | (K * T) | (T / K) | (T % K)
F ::= (T=T) | (T < T) | (T > T) | (~F) | (F & F) | (F|F)
V ::= x | y | z | ...
K ::= 0 | 1 | 2 | ...

Suppose we are given bounds for all integer variables and that they belong to .

We present translation from to equisatisfiable in propositional logic. That is, is equivalent to Where and .

For each bounded integer variable we introduce propositional variables corresponding to its binary representation.

The constructions for operations correspond to implementing these operations in hardware circuits:

Example: propositional formula expressing when .