Differences

This shows you the differences between two versions of the page.

--- sav08:fixed-width_bitvectors [2008/03/12 22:12]
vkuncak
+++ sav08:fixed-width_bitvectors [2008/03/13 11:25]
vkuncak
@@ Line 14: / Line 14: @@
   * 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:
   * [[http://www.springerlink.com/content/t57g3616p4756140/|Bitvectors and Arrays]]
+Later we will see how to prove that linear arithmetic holds for //all// bounds and not just given one.