Revision 1d0fd52b
Added by Xavier Thirioux about 4 years ago
| src/backends/Horn/horn_backend_printers.ml | ||
|---|---|---|
| 67 | 67 |
|
| 68 | 68 |
let pp_mod pp_val v1 v2 fmt = |
| 69 | 69 |
if Types.is_int_type v1.value_type && not !Options.integer_div_euclidean then |
| 70 |
(* C semantics: converting it to Euclidian operators
|
|
| 71 |
(a mod_M b) - (a < 0 ? abs(b) : 0)
|
|
| 70 |
(* C semantics: converting it from Euclidean operators
|
|
| 71 |
(a mod_M b) - ((a mod_M b > 0 && a < 0) ? abs(b) : 0)
|
|
| 72 | 72 |
*) |
| 73 |
Format.fprintf fmt "(- (mod %a %a) (ite (< %a 0) (abs %a) 0))" |
|
| 74 |
pp_val v1 pp_val v2 pp_val v1 pp_val v2 |
|
| 73 |
Format.fprintf fmt "(- (mod %a %a) (ite (and (> (mod %a %a) 0) (< %a 0)) (abs %a) 0))" |
|
| 74 |
pp_val v1 pp_val v2 |
|
| 75 |
pp_val v1 pp_val v2 |
|
| 76 |
pp_val v1 |
|
| 77 |
pp_val v2 |
|
| 75 | 78 |
else |
| 76 | 79 |
Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2 |
| 77 | 80 |
|
| 78 | 81 |
let pp_div pp_val v1 v2 fmt = |
| 79 | 82 |
if Types.is_int_type v1.value_type && not !Options.integer_div_euclidean then |
| 80 |
(* C semantics: converting it to Euclidian operators
|
|
| 81 |
(a - ((a mod_M b) - (a < 0 ? abs(b) : 0))) div_M b
|
|
| 83 |
(* C semantics: converting it from Euclidean operators
|
|
| 84 |
(a - (a mod_C b)) div_M b
|
|
| 82 | 85 |
*) |
| 83 |
Format.fprintf fmt "(div (- %a (- (mod %a %a) (ite (< %a 0) (abs %a) 0))) %a)" |
|
| 84 |
pp_val v1 pp_val v1 pp_val v2 |
|
| 85 |
pp_val v1 pp_val v2 pp_val v2 |
|
| 86 |
Format.fprintf fmt "(div (- %a %t) %a)" |
|
| 87 |
pp_val v1 |
|
| 88 |
(pp_mod pp_val v1 v2) |
|
| 89 |
pp_val v2 |
|
| 86 | 90 |
else |
| 87 | 91 |
Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2 |
| 88 | 92 |
|
Also available in: Unified diff
updated division for Horn clauses