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