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
Next revision Both sides next revision
sav08:qe_for_presburger_arithmetic [2008/04/17 10:42]
david 		sav08:qe_for_presburger_arithmetic [2009/04/21 19:39]
vkuncak
Line 4: Line 4:
  
 We consider elimination of a quantifier from a conjunction of literals (because [[QE from Conjunction of Literals Suffices]]). We consider elimination of a quantifier from a conjunction of literals (because [[QE from Conjunction of Literals Suffices]]).
 +
 +
  
 ===== Normalizing Conjunctions of Literals ===== ===== Normalizing Conjunctions of Literals =====
Line 29: Line 31:
 $t_1 < t_2$ becomes ++| $0 < t_2 - t_1$++ $t_1 < t_2$ becomes ++| $0 < t_2 - t_1$++
  
-We obtain a disjunction of conjunctions of literals of the form $0 < t$ and $K \mid t$ where $t$ are +We obtain a disjunction of conjunctions of literals of the form $0 < t$ and $K \mid t$ where $t$ are of the form $K_0 + \sum_{i=1}^n K_i \cdot x_i$
  
  
Line 94: Line 96:
  
 That's it! That's it!
 +
 +
 +
 +
 +
  
 ===== Example ===== ===== Example =====
Line 100: Line 107:
  
 How can we prove such verification condition? How can we prove such verification condition?
 +
 +The invariant of this code example is : $F = (res + 2i = 2x \wedge i' = i - 1 \wedge res' = res + 2) \rightarrow res' + 2i' = 2x$
 +
 +We have to find out if 
 +$\neg F$ 
 +is satisfiable.
 +
 +$\exists res, res',​i,​ i'. \neg F$
 +
 +We can eliminate quantifiers with equalities: $i'= i-1$ and $res' = res + 2$
 +
 +$res' + 2i'$ becomes $res + 2 + 2(i-1)$, and $\exists i', res' $ can be removed
 +
 +Finally :
 +
 +$\exists res, i. \neg (res + 2i = 2x \rightarrow res + 2 + 2(i-1) = 2x)$\\
 +$\exists res, i. \neg (res + 2i = 2x \rightarrow res + 2i = 2x)$\\
 +$\exists res, i. \neg true$\\
 +$false$
  
 ===== Some Improvements ===== ===== Some Improvements =====