## lustrec / doc / integer_division.org @ 58d610e1

History | View | Annotate | Download (1.15 KB)

1 | a6e85cdc | ploc | 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 model-checker 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 | 8cc55e2c | xthirioux | a mod_M b = (a mod_C b) + (a mod_C b < 0 ? abs(b) : 0) |

30 | a6e85cdc | ploc | |

31 | a div_M b = (a - (a mod_M b)) div_C b |
||

32 | 8cc55e2c | xthirioux | = (a - ((a mod_C b) + (a mod_C b < 0 ? abs(b) : 0))) div_C b |

33 | a6e85cdc | ploc | |

34 | * From Euclidian to C |
||

35 | |||

36 | 58d610e1 | xthirioux | a mod_C b = a mod_M b - ((a mod_M b <> 0 && a <= 0) ? abs(b) : 0) |

37 | a6e85cdc | ploc | |

38 | a div_C b = (a - (a mod_C b)) div_M b |
||

39 | 58d610e1 | xthirioux | = (a mod_M b <> 0 && a <= 0)?((a - a mod_M b + abs(b)) div_M b) :((a - a mod_M b) div_M b) |