Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav08:fixed-width_bitvectors [2008/03/13 11:24] vkuncak |
sav08:fixed-width_bitvectors [2008/03/13 11:25] vkuncak |
||
---|---|---|---|
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 variable $x_1$ we initially introduce | + | For each bounded integer variable $x \in [0,2^B]$ we introduce propositional variables corresponding to its binary representation. |
- | These constructions correspond to implementing these operations in hardware circuits. | + | The constructions for operations correspond to implementing these operations in hardware circuits: |
* adder for + | * adder for + | ||
* shift for * | * shift for * | ||
* comparator for <, = | * comparator for <, = | ||
+ | |||
Note that subtraction can be expressed using addition, similarly for / and %. | Note that subtraction can be expressed using addition, similarly for / and %. | ||