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.