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.