# 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:

- adder for +
- shift for *
- comparator for <, =

Example: propositional formula expressing when .

Note that subtraction can be expressed using addition, similarly for / and %.

How to express inverse operations for nested terms?

Additional pre-processing is useful. Much more on such encodings we will see later, and can also be found here:

Later we will see how to prove that linear arithmetic holds for *all* bounds and not just given one.