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/21 21:43]
david 		sav08:qe_for_presburger_arithmetic [2009/04/21 19:41]
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!
 +
 +
 +
 +
  
  
Line 110: Line 116:
 $\exists res, res',​i,​ i'. \neg F$ $\exists res, res',​i,​ i'. \neg F$
  
-We can eliminate quantifiers with equalities: $i'= i-1$+We can eliminate quantifiers with equalities: $i'= i-1$ and $res' = res + 2$
  
-$res' + 2i'$ becomes $res' ​+ 2(i-1)$, and $\exists i'$ can be removed+$res' + 2i'$ becomes $res + 2 + 2(i-1)$, and $\exists i', res' $ can be removed
  
 Finally : Finally :
  
-$\exists res, i. \neg (res + 2i = 2x \rightarrow res + 2 + 2(i-1) = 2x)$+$\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 =====
Line 123: Line 132:
  
 See Section 7.2 of the [[Calculus of Computation Textbook]]. See Section 7.2 of the [[Calculus of Computation Textbook]].
 +
  
 ===== References ===== ===== References =====
Line 130: Line 140:
 See Section 7.2 of the [[Calculus of Computation Textbook]] for a description of more efficient Cooper'​s algorithm. See Section 7.2 of the [[Calculus of Computation Textbook]] for a description of more efficient Cooper'​s algorithm.
  
-[[http://​doi.acm.org/​10.1145/​135226.135233|A practical algorithm for exact array dependence analysis]] ​(suitable for a project)+[[http://​doi.acm.org/​10.1145/​135226.135233|A practical algorithm for exact array dependence analysis]]