Project

General

Profile

« Previous | Next » 

Revision 1d0fd52b

Added by Xavier Thirioux about 4 years ago

updated division for Horn clauses

View differences:

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