Differences
This shows you the differences between two versions of the page.
sav08:fixed-width_bitvectors [2008/03/13 11:28] vkuncak |
sav08:fixed-width_bitvectors [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Fixed-Width Bitvectors ====== | ||
- | |||
- | Bitvector: integer from some finite inteval of length $2^n$ | ||
- | |||
- | Example: $[0,2^{32}-1]$ | ||
- | |||
- | 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 $[0,2^B]$. | ||
- | |||
- | We present translation from $F$ to equisatisfiable $prop(F)$ in propositional logic. That is, | ||
- | \[ | ||
- | \exists x_1,\ldots,x_n.\ F | ||
- | \] | ||
- | is equivalent to | ||
- | \[ | ||
- | \exists p_1,\ldots,p_m.\ prop(F) | ||
- | \] | ||
- | Where $FV(F)=\{x_1,\ldots,x_n\}$ and $FV(prop(F)) = \{p_1,\ldots,p_m\}$. | ||
- | |||
- | For each bounded integer variable $x \in [0,2^B]$ 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 <, = | ||
- | |||
- | Note that subtraction can be expressed using addition, similarly for / and %. | ||
- | |||
- | ++How to express inverse operations for nested terms?|Flat form of formulas.++ | ||
- | |||
- | Additional pre-processing is useful. Much more on such encodings we will see later, and can also be found here: | ||
- | |||
- | * [[http://www.springerlink.com/content/t57g3616p4756140/|Bitvectors and Arrays]] | ||
- | * [[http://www.decision-procedures.org/]] | ||
- | |||
- | Later we will see how to prove that linear arithmetic holds for //all// bounds and not just given one. | ||