Project

General

Profile

Revision 45f0f48d src/backends/Horn/horn_backend_printers.ml

View differences:

src/backends/Horn/horn_backend_printers.ml
42 42
let rec pp_horn_const fmt c =
43 43
  match c with
44 44
    | Const_int i    -> pp_print_int fmt i
45
    | Const_real (_,_s)   -> pp_print_string fmt s
45
    | Const_real (_,_,s)   -> pp_print_string fmt s
46 46
    | Const_tag t    -> pp_horn_tag fmt t
47 47
    | _              -> assert false
48 48

  
......
51 51
   but an offset suffix may be added for array variables
52 52
*)
53 53
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
54
  match v with
54
  match v.value_desc with
55 55
    | Cst c         -> pp_horn_const fmt c
56 56
    | Array _
57 57
    | Access _ -> assert false (* no arrays *)
......
65 65

  
66 66
(* Prints a [value] indexed by the suffix list [loop_vars] *)
67 67
let rec pp_value_suffix self pp_value fmt value =
68
 match value with
68
 match value.value_desc with
69 69
 | Fun (n, vl)  ->
70 70
   Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
71 71
 |  _            ->
......
77 77
   - [value]: assigned value
78 78
   - [pp_var]: printer for variables
79 79
*)
80
let pp_assign m pp_var fmt var_type var_name value =
80
let pp_assign m pp_var fmt var_name value =
81 81
  let self = m.mname.node_id in
82 82
  fprintf fmt "(= %a %a)" 
83 83
    (pp_horn_val ~is_lhs:true self pp_var) var_name
......
156 156
      | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
157 157
	fprintf fmt "@[<v 5>(and ";
158 158
	fprintf fmt "(= %a (ite %a %a %a))"
159
	  (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (LocalVar o) (* output var *)
159
	  (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *)
160 160
	  (pp_horn_var m) mem_m 
161 161
	  (pp_horn_val self (pp_horn_var m)) i1
162 162
	  (pp_horn_val self (pp_horn_var m)) i2
......
172 172
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) inputs
173 173
	  (Utils.pp_final_char_if_non_empty "@ " inputs)
174 174
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
175
	  (List.map (fun v -> LocalVar v) outputs)
175
	  (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
176 176
	  (Utils.pp_final_char_if_non_empty "@ " outputs)
177 177
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)
178 178
	
......
186 186
      inputs
187 187
      (Utils.pp_final_char_if_non_empty "@ " inputs)
188 188
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
189
      (List.map (fun v -> LocalVar v) outputs)
189
      (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
190 190
  )
191 191
    
192 192
    
......
202 202
  | MLocalAssign (i,v) ->
203 203
    pp_assign
204 204
      m (pp_horn_var m) fmt
205
      i.var_type (LocalVar i) v;
205
      (mk_val (LocalVar i) i.var_type) v;
206 206
    reset_instances
207 207
  | MStateAssign (i,v) ->
208 208
    pp_assign
209 209
      m (pp_horn_var m) fmt
210
      i.var_type (StateVar i) v;
210
      (mk_val (StateVar i) i.var_type) v;
211 211
    reset_instances
212
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
212
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
213 213
    assert false (* This should not happen anymore *)
214 214
  | MStep (il, i, vl) ->
215 215
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =

Also available in: Unified diff