Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:fixed-width_bitvectors [2008/03/13 11:25] vkuncak |
sav08:fixed-width_bitvectors [2008/03/13 19:22] vkuncak |
||
---|---|---|---|
Line 23: | Line 23: | ||
K ::= 0 | 1 | 2 | ... | K ::= 0 | 1 | 2 | ... | ||
- | Suppose we are given bounds for all integer variables and that they belong to $[0,2^B]$. | + | Suppose we are given bounds for all integer variables and that they belong to $[0,2^B-1]$. |
We present translation from $F$ to equisatisfiable $prop(F)$ in propositional logic. That is, | We present translation from $F$ to equisatisfiable $prop(F)$ in propositional logic. That is, | ||
Line 35: | Line 35: | ||
Where $FV(F)=\{x_1,\ldots,x_n\}$ and $FV(prop(F)) = \{p_1,\ldots,p_m\}$. | 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. | + | For each bounded integer variable $x \in [0,2^B-1]$ we introduce propositional variables corresponding to its binary representation. |
The constructions for operations correspond to implementing these operations in hardware circuits: | The constructions for operations correspond to implementing these operations in hardware circuits: | ||
Line 41: | Line 41: | ||
* shift for * | * shift for * | ||
* comparator for <, = | * comparator for <, = | ||
+ | |||
+ | Example: propositional formula expressing $x + y = z$ when $x,y,z \in [0,2^B-1]$. | ||
Note that subtraction can be expressed using addition, similarly for / and %. | Note that subtraction can be expressed using addition, similarly for / and %. | ||
Line 46: | Line 48: | ||
++How to express inverse operations for nested terms?|Flat form of formulas.++ | ++How to express inverse operations for nested terms?|Flat form of formulas.++ | ||
- | Additional pre-processing is useful: | + | 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.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. | Later we will see how to prove that linear arithmetic holds for //all// bounds and not just given one. | ||