Project

General

Profile

« Previous | Next » 

Revision 1d0fd52b

Added by Xavier Thirioux about 4 years ago

updated division for Horn clauses

View differences:

src/backends/C/c_backend_common.ml
121 121
let pp_div pp_val v1 v2 fmt =
122 122
  if !Options.integer_div_euclidean then
123 123
    (* (a - ((a mod_C b) + (a mod_C b < 0 ? abs(b) : 0))) div_C b *)
124
    Format.fprintf fmt "(%a - ((%a %% %a) + ((%a %% %a) < 0 ? abs(%a) : 0))) / %a"
124
    Format.fprintf fmt "(%a - %t) / %a"
125 125
      pp_val v1
126
      pp_val v1 pp_val v2
127
      pp_val v1 pp_val v2
128
      pp_val v2
126
      (pp_mod pp_val v1 v2)
129 127
      pp_val v2
130 128
  else (* Regular behavior: printing a / *)
131 129
    Format.fprintf fmt "(%a / %a)" pp_val v1 pp_val v2

Also available in: Unified diff