Project

General

Profile

Revision f19eb2fd src/horn_backend.ml

View differences:

src/horn_backend.ml
4 4
open Machine_code
5 5

  
6 6

  
7
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id
7
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id
8 8
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
9 9

  
10 10
let pp_type fmt t =
......
21 21
    
22 22

  
23 23
let pp_decl_var fmt id = 
24
  Format.fprintf fmt "(declare_var %s %a)"
24
  Format.fprintf fmt "(declare-var %s %a)"
25 25
    id.var_id
26 26
    pp_type id.var_type
27 27

  
......
186 186
     (Utils.fprintf_list ~sep:" " (pp_horn_var m)) outputs 
187 187
    )
188 188

  
189
let pp_machine_reset (m: machine_t) self fmt inst =
189
let pp_machine_init (m: machine_t) self fmt inst =
190 190
  let (node, static) = List.assoc inst m.minstances in
191 191
  fprintf fmt "(%a %a%t%s->%s)"
192
    pp_machine_reset_name (node_name node)
192
    pp_machine_init_name (node_name node)
193 193
    (Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static
194 194
    (Utils.pp_final_char_if_non_empty " " static)
195 195
    self inst
......
206 206
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
207 207
  match instr with 
208 208
  | MReset i ->
209
    pp_machine_reset m self fmt i
209
    pp_machine_init m self fmt i
210 210
  | MLocalAssign (i,v) ->
211 211
    pp_assign
212 212
      m self (pp_horn_var m) fmt
......
249 249
   Format.pp_print_newline fmt ();
250 250
   (* Declaring predicate *)
251 251
   Format.fprintf fmt "(declare-rel %a (%a))@."
252
     pp_machine_reset_name m.mname.node_id
252
     pp_machine_init_name m.mname.node_id
253 253
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (init_vars machines m));
254 254
   
255 255
   Format.fprintf fmt "(declare-rel %a (%a))@."

Also available in: Unified diff