Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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 %.
 
sav08/fixed-width_bitvectors.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice