Revision a6e85cdc
doc/integer_division.org  

1 
Integer division in LustreC 

2  
3 
* Issue 

4  
5 
Integer division / and associated modulo mod 

6  
7 
a = (a / b) * b + (a mod b) 

8  
9 
Division between two integers can be interpreted in different ways 

10 
 a C like division where sign(a mod b) = sign a 

11 
 a euclidean division where 0 <= a mod b < b 

12 
In both cases they satisfy the above equation. 

13  
14 
Kind modelchecker or Horn encoding assumes the mathematical definition, ie. the 

15 
euclidean division, while lustreC or the Verimag compiler rely on the C 

16 
definition. 

17  
18 
In the following we deonote by div_C/mod_C and div_M/mod_M the functions in C 

19 
and math, respectively. 

20  
21 
As an example 4 div_C 3 = 1 while 4 div_M 3 = 2 

22  
23 
Some properties: 

24 
 we have a div_M b = a div_C b when a = b * k 

25 
 we have a mod_C b = 0 \equiv a mod_M b = 0. 

26  
27 
* From C to Euclidian 

28  
29 
a mod_M b = (a mod_C b) + (a < 0 ? abs(b) : 0) 

30  
31 
a div_M b = (a  (a mod_M b)) div_C b 

32 
= (a  ((a mod_C b) + (a < 0 ? abs(b) : 0))) div_C b 

33  
34 
* From Euclidian to C 

35  
36 
a mod_C b = (a >= 0 ? a mod_M b :  ((a) mod_M b)) 

37 
(using math def to ensure positiveness of remainder)) 

38 
= (a mod_M b)  (a < 0 ? abs(b) : 0) 

39 
(using the def of mod_M above) 

40  
41 
a div_C b = (a  (a mod_C b)) div_M b 

42 
= (a  ((a mod_M b)  (a < 0 ? abs(b) : 0))) div_M b 

43 


44 
Let's chosse the second, simpler, def of mod_C 

45 
Also available in: Unified diff