Bitvector: integer from some finite inteval of length
Logic on bitvectors.
- formulas for +.
We can reduce reasoning on bitvectors to reasoning in propositional logic.
- 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 %.
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.