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:25]
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 %.
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.