# 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:28] vkuncak |
sav08:fixed-width_bitvectors [2015/04/21 17:30] (current) |
||
---|---|---|---|

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, | ||

- | \[ | + | \begin{equation*} |

\exists x_1,\ldots,x_n.\ F | \exists x_1,\ldots,x_n.\ F | ||

- | \] | + | \end{equation*} |

is equivalent to | is equivalent to | ||

- | \[ | + | \begin{equation*} |

\exists p_1,\ldots,p_m.\ prop(F) | \exists p_1,\ldots,p_m.\ prop(F) | ||

- | \] | + | \end{equation*} |

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 %. |