• English only

# 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] (current) Both sides previous revision Previous revision 2008/03/13 19:22 vkuncak 2008/03/13 11:28 vkuncak 2008/03/13 11:25 vkuncak 2008/03/13 11:24 vkuncak 2008/03/12 22:12 vkuncak 2008/03/12 21:47 vkuncak 2008/03/12 21:47 vkuncak created Next revision Previous revision 2008/03/13 19:22 vkuncak 2008/03/13 11:28 vkuncak 2008/03/13 11:25 vkuncak 2008/03/13 11:24 vkuncak 2008/03/12 22:12 vkuncak 2008/03/12 21:47 vkuncak 2008/03/12 21:47 vkuncak created 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 %.