Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend_printers.ml @ e057dd08

History | View | Annotate | Download (20.7 KB)

1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

    
12
(* The compilation presented here was first defined in Garoche, Gurfinkel,
13
   Kahsai, HCSV'14.
14

    
15
   This is a modified version that handle reset
16
*)
17

    
18
open Format
19
open LustreSpec
20
open Corelang
21
open Machine_code
22

    
23
open Horn_backend_common
24
open Types
25

    
26
(********************************************************************************************)
27
(*                    Instruction Printing functions                                        *)
28
(********************************************************************************************)
29

    
30
let pp_horn_var m fmt id =
31
  (*if Types.is_array_type id.var_type
32
  then
33
    assert false (* no arrays in Horn output *)
34
  else*)
35
    fprintf fmt "%s" id.var_id
36

    
37
(* Used to print boolean constants *)
38
let pp_horn_tag fmt t =
39
  pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t)
40

    
41
(* Prints a constant value *)
42
let rec pp_horn_const fmt c =
43
  match c with
44
    | Const_int i    -> pp_print_int fmt i
45
    | Const_real (_,_,s)   -> pp_print_string fmt s
46
    | Const_tag t    -> pp_horn_tag fmt t
47
    | _              -> assert false
48

    
49
let rec get_type_cst c =
50
  match c with
51
  | Const_int(n) -> new_ty Tint
52
  | Const_real _ -> new_ty Treal
53
  (* | Const_float _ -> new_ty Treal *)
54
  | Const_array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), get_type_cst (List.hd l)))
55
  | Const_tag(tag) -> new_ty Tbool
56
  | Const_string(str) ->  assert false(* used only for annotations *)
57
  | Const_struct(l) -> new_ty (Tstruct(List.map (fun (label, t) -> (label, get_type_cst t)) l))
58

    
59
let rec get_type v =
60
  match v with
61
  | Cst c -> get_type_cst c
62
  | Access(tab, index) -> begin
63
      let rec remove_link ltype =
64
        match (dynamic_type ltype).tdesc with
65
        | Tlink t -> t
66
        | _ -> ltype
67
      in
68
      match (dynamic_type (remove_link (get_type tab))).tdesc with
69
      | Tarray(size, t) -> remove_link t
70
      | Tvar -> Format.eprintf "Type of access is a variable... "; assert false
71
      | Tunivar -> Format.eprintf "Type of access is a variable... "; assert false
72
      | _ -> Format.eprintf "Type of access is not an array "; assert false
73
                          end
74
  | Power(v, n) -> assert false
75
  | LocalVar v -> v.var_type
76
  | StateVar v -> v.var_type
77
  | Fun(n, vl) -> begin match n with
78
                  | "+"
79
                  | "-"
80
                  | "*" -> get_type (List.hd vl)
81
                  | _ -> Format.eprintf "Function undealt with : %s" n ;assert false
82
                  end
83
  | Array(l) -> new_ty (Tarray(Dimension.mkdim_int
84
                                 (Location.dummy_loc)
85
                                 (List.length l),
86
                               get_type (List.hd l)))
87
  | _ -> assert false
88

    
89

    
90
let rec default_val fmt t =
91
  match (dynamic_type t).tdesc with
92
  | Tint -> fprintf fmt "0"
93
  | Treal -> fprintf fmt "0"
94
  | Tbool -> fprintf fmt "true"
95
  | Tarray(dim, l) -> let valt = array_element_type t in
96
                      fprintf fmt "((as const (Array Int ";
97
                      begin try
98
                        pp_type fmt valt
99
                      with
100
                      | _ -> fprintf fmt "failed"; end;
101
                      fprintf fmt ")) ";
102
                      begin try
103
                        default_val fmt valt
104
                      with
105
                      | _ -> fprintf fmt "failed"; end;
106
                      fprintf fmt ")"
107
  | Tstruct(l) -> assert false
108
  | Ttuple(l) -> assert false
109
  |_ -> assert false
110

    
111

    
112
(* Prints a value expression [v], with internal function calls only.
113
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
114
   but an offset suffix may be added for array variables
115
*)
116
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
117
  match v.value_desc with
118
    | Cst c         -> pp_horn_const fmt c
119
    | Array initlist       -> (*Format.fprintf err_formatter "init %a" (pp_horn_val ~is_lhs:is_lhs self pp_var) (List.hd initlist);*)
120
                              let rec print tab x =
121
                                match tab with
122
                                | [] -> default_val fmt (get_type v)(*fprintf fmt "YAY"*)
123
                                | h::t -> fprintf fmt "(store "; print t (x+1); fprintf fmt " %i " x; pp_horn_val ~is_lhs:is_lhs self pp_var fmt h; fprintf fmt ")"
124
                              in
125
                              print initlist 0
126
    | Access(tab,index)      -> fprintf fmt "(select "; pp_horn_val ~is_lhs:is_lhs self pp_var fmt tab; fprintf fmt " "; pp_horn_val ~is_lhs:is_lhs self pp_var fmt index; fprintf fmt ")"
127
    | Power (v, n)  -> assert false
128
    | LocalVar v    -> pp_var fmt (rename_machine self v)
129
    | StateVar v    ->
130
      if Types.is_array_type v.var_type
131
      then begin assert false; eprintf "toto called\n";fprintf fmt "TOTO" end
132
      else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
133
    | Fun (n, vl)   -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
134

    
135
(* Prints a [value] indexed by the suffix list [loop_vars] *)
136
let rec pp_value_suffix self pp_value fmt value =
137
 match value.value_desc with
138
 | Fun (n, vl)  ->
139
   Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
140
 |  _            ->
141
   pp_horn_val self pp_value fmt value
142

    
143
(* type_directed assignment: array vs. statically sized type
144
   - [var_type]: type of variable to be assigned
145
   - [var_name]: name of variable to be assigned
146
   - [value]: assigned value
147
   - [pp_var]: printer for variables
148
*)
149
let pp_assign m pp_var fmt var_name value =
150
  let self = m.mname.node_id in
151
  fprintf fmt "(= %a %a)"
152
    (pp_horn_val ~is_lhs:true self pp_var) var_name
153
    (pp_value_suffix self pp_var) value
154

    
155

    
156
(* In case of no reset call, we define mid_mem = current_mem *)
157
let pp_no_reset machines m fmt i =
158
  let (n,_) = List.assoc i m.minstances in
159
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
160

    
161
  let m_list =
162
    rename_machine_list
163
      (concat m.mname.node_id i)
164
      (rename_mid_list (full_memory_vars machines target_machine))
165
  in
166
  let c_list =
167
    rename_machine_list
168
      (concat m.mname.node_id i)
169
      (rename_current_list (full_memory_vars machines target_machine))
170
  in
171
  match c_list, m_list with
172
  | [chd], [mhd] ->
173
    fprintf fmt "(= %a %a)"
174
      (pp_horn_var m) mhd
175
      (pp_horn_var m) chd
176

    
177
  | _ -> (
178
    fprintf fmt "@[<v 0>(and @[<v 0>";
179
    List.iter2 (fun mhd chd ->
180
      fprintf fmt "(= %a %a)@ "
181
      (pp_horn_var m) mhd
182
      (pp_horn_var m) chd
183
    )
184
      m_list
185
      c_list      ;
186
    fprintf fmt ")@]@ @]"
187
  )
188

    
189
let pp_instance_reset machines m fmt i =
190
  let (n,_) = List.assoc i m.minstances in
191
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
192

    
193
  fprintf fmt "(%a @[<v 0>%a)@]"
194
    pp_machine_reset_name (node_name n)
195
    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
196
    (
197
      (rename_machine_list
198
	 (concat m.mname.node_id i)
199
	 (rename_current_list (full_memory_vars machines target_machine))
200
      )
201
      @
202
	(rename_machine_list
203
	   (concat m.mname.node_id i)
204
	   (rename_mid_list (full_memory_vars machines target_machine))
205
	)
206
    )
207

    
208
let pp_instance_call machines reset_instances m fmt i inputs outputs =
209
  let self = m.mname.node_id in
210
  try (* stateful node instance *)
211
    begin
212
      let (n,_) = List.assoc i m.minstances in
213
      let target_machine = List.find (fun m  -> m.mname.node_id = node_name n) machines in
214
      (* Checking whether this specific instances has been reset yet *)
215
      if not (List.mem i reset_instances) then
216
	(* If not, declare mem_m = mem_c *)
217
	pp_no_reset machines m fmt i;
218

    
219
      let mems = full_memory_vars machines target_machine in
220
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
221
      let mid_mems = rename_mems rename_mid_list in
222
      let next_mems = rename_mems rename_next_list in
223

    
224
      match node_name n, inputs, outputs, mid_mems, next_mems with
225
      | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
226
	fprintf fmt "@[<v 5>(and ";
227
	fprintf fmt "(= %a (ite %a %a %a))"
228
	  (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *)
229
	  (pp_horn_var m) mem_m
230
	  (pp_horn_val self (pp_horn_var m)) i1
231
	  (pp_horn_val self (pp_horn_var m)) i2
232
	;
233
	fprintf fmt "@ ";
234
	fprintf fmt "(= %a false)" (pp_horn_var m) mem_x;
235
	fprintf fmt ")@]"
236
      end
237

    
238
      | node_name_n -> begin
239
	fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]"
240
	  pp_machine_step_name (node_name n)
241
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) inputs
242
	  (Utils.pp_final_char_if_non_empty "@ " inputs)
243
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
244
	  (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
245
	  (Utils.pp_final_char_if_non_empty "@ " outputs)
246
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)
247

    
248
      end
249
    end
250
  with Not_found -> ( (* stateless node instance *)
251
    let (n,_) = List.assoc i m.mcalls in
252
    fprintf fmt "(%s @[<v 0>%a%t%a)@]"
253
      (node_name n)
254
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
255
      inputs
256
      (Utils.pp_final_char_if_non_empty "@ " inputs)
257
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
258
      (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
259
  )
260

    
261

    
262
(* Print the instruction and update the set of reset instances *)
263
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =
264
  match instr with
265
  | MComment _ -> reset_instances
266
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
267
    pp_no_reset machines m fmt i;
268
    i::reset_instances
269
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
270
    pp_instance_reset machines m fmt i;
271
    i::reset_instances
272
  | MLocalAssign (i,v) ->
273
    pp_assign
274
      m (pp_horn_var m) fmt
275
      (mk_val (LocalVar i) i.var_type) v;
276
    reset_instances
277
  | MStateAssign (i,v) ->
278
    pp_assign
279
      m (pp_horn_var m) fmt
280
      (mk_val (StateVar i) i.var_type) v;
281
    reset_instances
282
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
283
    assert false (* This should not happen anymore *)
284
  | MStep (il, i, vl) ->
285
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
286
       mem_c and print the call to mem_m *)
287
    pp_instance_call machines reset_instances m fmt i vl il;
288
    reset_instances (* Since this instance call will only happen once, we
289
		       don't have to update reset_instances *)
290

    
291
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
292
			 should not be produced yet. Later, we will have to
293
			 compare the reset_instances of each branch and
294
			 introduced the mem_m = mem_c for branches to do not
295
			 address it while other did. Am I clear ? *)
296
    (* For each branch we obtain the logical encoding, and the information
297
       whether a sub node has been reset or not. If a node has been reset in one
298
       of the branch, then all others have to have the mem_m = mem_c
299
       statement. *)
300
    let self = m.mname.node_id in
301
    let pp_branch fmt (tag, instrs) =
302
      fprintf fmt
303
	"@[<v 3>(or (not (= %a %s))@ "
304
	(*"@[<v 3>(=> (= %a %s)@ "*)  (* Issues with some versions of Z3. It
305
					  seems that => within Horn predicate
306
					  may cause trouble. I have hard time
307
					  producing a MWE, so I'll just keep the
308
					  fix here as (not a) or b *)
309
	(pp_horn_val self (pp_horn_var m)) g
310
	tag;
311
      let rs = pp_machine_instrs machines reset_instances m fmt instrs in
312
      fprintf fmt "@])";
313
      () (* rs *)
314
    in
315
    pp_conj pp_branch fmt hl;
316
    reset_instances
317

    
318
and pp_machine_instrs machines reset_instances m fmt instrs =
319
  let ppi rs fmt i = pp_machine_instr machines rs m fmt i in
320
  match instrs with
321
  | [x] -> ppi reset_instances fmt x
322
  | _::_ ->
323
    fprintf fmt "(and @[<v 0>";
324
    let rs = List.fold_left (fun rs i ->
325
      let rs = ppi rs fmt i in
326
      fprintf fmt "@ ";
327
      rs
328
    )
329
      reset_instances instrs
330
    in
331
    fprintf fmt "@])";
332
    rs
333

    
334
  | [] -> fprintf fmt "true"; reset_instances
335

    
336
let pp_machine_reset machines fmt m =
337
  let locals = local_memory_vars machines m in
338
  fprintf fmt "@[<v 5>(and @ ";
339

    
340
  (* print "x_m = x_c" for each local memory *)
341
  (Utils.fprintf_list ~sep:"@ " (fun fmt v ->
342
    fprintf fmt "(= %a %a)"
343
      (pp_horn_var m) (rename_mid v)
344
      (pp_horn_var m) (rename_current v)
345
   )) fmt locals;
346
  fprintf fmt "@ ";
347

    
348
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
349
     Special treatment for _arrow: _first = true
350
  *)
351
  (Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) ->
352
    let name = node_name n in
353
    if name = "_arrow" then (
354
      fprintf fmt "(= %s._arrow._first_m true)"
355
	(concat m.mname.node_id id)
356
    ) else (
357
      let machine_n = get_machine machines name in
358
      fprintf fmt "(%s_reset @[<hov 0>%a@])"
359
	name
360
	(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
361
	(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
362
    )
363
   )) fmt m.minstances;
364

    
365
  fprintf fmt "@]@ )"
366

    
367

    
368

    
369
(**************************************************************)
370

    
371
let is_stateless m = m.minstances = [] && m.mmemory = []
372

    
373
(* Print the machine m:
374
   two functions: m_init and m_step
375
   - m_init is a predicate over m memories
376
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
377
   We first declare all variables then the two /rules/.
378
*)
379
let print_machine machines fmt m =
380
  if m.mname.node_id = arrow_id then
381
    (* We don't print arrow function *)
382
    ()
383
  else
384
    begin
385
      fprintf fmt "; %s@." m.mname.node_id;
386

    
387
      (* Printing variables *)
388
      Utils.fprintf_list ~sep:"@." pp_decl_var fmt
389
	(
390
	  (inout_vars machines m)@
391
	    (rename_current_list (full_memory_vars machines m)) @
392
	    (rename_mid_list (full_memory_vars machines m)) @
393
	    (rename_next_list (full_memory_vars machines m)) @
394
	    (rename_machine_list m.mname.node_id m.mstep.step_locals)
395
	);
396
      pp_print_newline fmt ();
397

    
398
      if is_stateless m then
399
	begin
400
	  (* Declaring single predicate *)
401
	  fprintf fmt "(declare-rel %a (%a))@."
402
	    pp_machine_stateless_name m.mname.node_id
403
	    (Utils.fprintf_list ~sep:" " pp_type)
404
	    (List.map (fun v -> v.var_type) (inout_vars machines m));
405

    
406
	  (* Rule for single predicate *)
407
	  fprintf fmt "@[<v 2>(rule (=> @ ";
408
	  ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);
409
	  fprintf fmt "@ (%a %a)@]@.))@.@."
410
	    pp_machine_stateless_name m.mname.node_id
411
	    (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m);
412
	end
413
      else
414
	begin
415
	  (* Declaring predicate *)
416
	  fprintf fmt "(declare-rel %a (%a))@."
417
	    pp_machine_reset_name m.mname.node_id
418
	    (Utils.fprintf_list ~sep:" " pp_type)
419
	    (List.map (fun v -> v.var_type) (reset_vars machines m));
420

    
421
	  fprintf fmt "(declare-rel %a (%a))@."
422
	    pp_machine_step_name m.mname.node_id
423
	    (Utils.fprintf_list ~sep:" " pp_type)
424
	    (List.map (fun v -> v.var_type) (step_vars machines m));
425

    
426
	  pp_print_newline fmt ();
427

    
428
	  (* Rule for reset *)
429
	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
430
	    (pp_machine_reset machines) m
431
	    pp_machine_reset_name m.mname.node_id
432
	    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);
433

    
434
          match m.mstep.step_asserts with
435
	  | [] ->
436
	    begin
437

    
438
	      (* Rule for step*)
439
	      fprintf fmt "@[<v 2>(rule (=> @ ";
440
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
441
	      fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
442
		pp_machine_step_name m.mname.node_id
443
		(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
444
	    end
445
	  | assertsl ->
446
	    begin
447
	      let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
448
	      (* print_string pp_val; *)
449
	      fprintf fmt "; with Assertions @.";
450

    
451
	      (*Rule for step*)
452
	      fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
453
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
454
	      fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
455
		pp_machine_step_name m.mname.node_id
456
		(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
457
	    end
458

    
459

    
460
	end
461
    end
462

    
463

    
464
let mk_flags arity =
465
  let b_range =
466
   let rec range i j =
467
     if i > arity then [] else i :: (range (i+1) j) in
468
   range 2 arity;
469
 in
470
 List.fold_left (fun acc x -> acc ^ " false") "true" b_range
471

    
472

    
473
  (*Get sfunction infos from command line*)
474
let get_sf_info() =
475
  let splitted = Str.split (Str.regexp "@") !Options.sfunction in
476
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. sfunction name: %s@," !Options.sfunction);
477
  let sf_name, flags, arity = match splitted with
478
      [h;flg;par] -> h, flg, par
479
    | _ -> failwith "Wrong Sfunction info"
480

    
481
  in
482
  Log.report ~level:1 (fun fmt -> fprintf fmt "... sf_name: %s@, .. flags: %s@ .. arity: %s@," sf_name flags arity);
483
  sf_name, flags, arity
484

    
485

    
486
    (*a function to print the rules in case we have an s-function*)
487
  let print_sfunction machines fmt m =
488
      if m.mname.node_id = arrow_id then
489
        (* We don't print arrow function *)
490
        ()
491
      else
492
        begin
493
          Format.fprintf fmt "; SFUNCTION@.";
494
          Format.fprintf fmt "; %s@." m.mname.node_id;
495
          Format.fprintf fmt "; EndPoint Predicate %s." !Options.sfunction;
496

    
497
          (* Check if there is annotation for s-function *)
498
          if m.mannot != [] then(
499
              Format.fprintf fmt "; @[%a@]@]@\n" (Utils.fprintf_list ~sep:"@ " Printers.pp_s_function) m.mannot;
500
            );
501

    
502
       (* Printing variables *)
503
          Utils.fprintf_list ~sep:"@." pp_decl_var fmt
504
                             ((step_vars machines m)@
505
    	                        (rename_machine_list m.mname.node_id m.mstep.step_locals));
506
          Format.pp_print_newline fmt ();
507
          let sf_name, flags, arity = get_sf_info() in
508

    
509
       if is_stateless m then
510
         begin
511
           (* Declaring single predicate *)
512
           Format.fprintf fmt "(declare-rel %a (%a))@."
513
    	                  pp_machine_stateless_name m.mname.node_id
514
    	                  (Utils.fprintf_list ~sep:" " pp_type)
515
    	                  (List.map (fun v -> v.var_type) (reset_vars machines m));
516
           Format.pp_print_newline fmt ();
517
           (* Rule for single predicate *)
518
           let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in
519
           Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@."
520
                          str_flags
521
                          (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m)
522
	                  pp_machine_stateless_name m.mname.node_id
523
	                  (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m);
524
         end
525
      else
526
         begin
527
           (* Declaring predicate *)
528
           Format.fprintf fmt "(declare-rel %a (%a))@."
529
    	                  pp_machine_reset_name m.mname.node_id
530
    	                  (Utils.fprintf_list ~sep:" " pp_type)
531
    	                  (List.map (fun v -> v.var_type) (inout_vars machines m));
532

    
533
           Format.fprintf fmt "(declare-rel %a (%a))@."
534
    	                  pp_machine_step_name m.mname.node_id
535
    	                  (Utils.fprintf_list ~sep:" " pp_type)
536
    	                  (List.map (fun v -> v.var_type) (step_vars machines m));
537

    
538
           Format.pp_print_newline fmt ();
539
          (* Adding assertions *)
540
           match m.mstep.step_asserts with
541
	  | [] ->
542
	    begin
543

    
544
	      (* Rule for step*)
545
	      fprintf fmt "@[<v 2>(rule (=> @ ";
546
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
547
	      fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
548
		pp_machine_step_name m.mname.node_id
549
		(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
550
	    end
551
	  | assertsl ->
552
	    begin
553
	      let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
554
	      (* print_string pp_val; *)
555
	      fprintf fmt "; with Assertions @.";
556

    
557
	      (*Rule for step*)
558
	      fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
559
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
560
	      fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
561
		pp_machine_step_name m.mname.node_id
562
		(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
563
	    end
564

    
565
         end
566

    
567
        end
568
(* Local Variables: *)
569
(* compile-command:"make -C ../../.." *)
570
(* End: *)