lustrec / doc / integer_division.org @ 8cc55e2c
History  View  Annotate  Download (1.32 KB)
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 mod_C b < 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 mod_C b < 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 mod_C < 0 ? abs(b) : 0) 
39 
= a mod_M b  ((a mod_M b <> 0 && a <= 0) ? abs(b) : 0) 
40 
(using the def of mod_M above) 
41  
42 
a div_C b = (a  (a mod_C b)) div_M b 
43 

44 
Let's choose the second, simpler, def of mod_C 
45 