Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend_printers.ml @ 990210f3

History | View | Annotate | Download (21.1 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

    
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
(* PL comment 2017/01/03: Useless code, the function existed before in typing.ml *)
50
(* let rec get_type_cst c = *)
51
(*   match c with *)
52
(*   | Const_int(n) -> new_ty Tint *)
53
(*   | Const_real _ -> new_ty Treal *)
54
(*   (\* | Const_float _ -> new_ty Treal *\) *)
55
(*   | Const_array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), *)
56
(* 				     get_type_cst (List.hd l))) *)
57
(*   | Const_tag(tag) -> new_ty Tbool *)
58
(*   | Const_string(str) ->  assert false(\* used only for annotations *\) *)
59
(*   | Const_struct(l) -> new_ty (Tstruct(List.map (fun (label, t) -> (label, get_type_cst t)) l)) *)
60

    
61
(* PL comment 2017/01/03: the following function get_type seems useless to me: it looks like computing the type of a machine code expression v while v.value_type should contain this information. The code is kept for the moment in case I missed something *)
62

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

    
95
(* Default value for each type, used when building arrays. Eg integer array
96
   [2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
97
   for the type integer (arrays).
98
*)
99
let rec pp_default_val fmt t =
100
  match (Types.dynamic_type t).Types.tdesc with
101
  | Types.Tint -> fprintf fmt "0"
102
  | Types.Treal -> fprintf fmt "0"
103
  | Types.Tbool -> fprintf fmt "true"
104
  | Types.Tarray(dim, l) -> (* TODO PL: this strange code has to be (heavily) checked *)
105
     let valt = Types.array_element_type t in
106
     fprintf fmt "((as const (Array Int %a)) %a)"
107
       pp_type valt 
108
       pp_default_val valt
109
  | Types.Tstruct(l) -> assert false
110
  | Types.Ttuple(l) -> assert false
111
  |_ -> assert false
112

    
113

    
114
(* Prints a value expression [v], with internal function calls only.
115
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
116
   but an offset suffix may be added for array variables
117
*)
118
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
119
  match v.value_desc with
120
  | Cst c       -> pp_horn_const fmt c
121

    
122
  (* Code specific for arrays *)
123
  | Array il    ->
124
     (* An array definition: 
125
	(store (
126
	  ...
127
 	    (store (
128
	       store (
129
	          default_val
130
	       ) 
131
	       idx_n val_n
132
	    ) 
133
	    idx_n-1 val_n-1)
134
	  ... 
135
	  idx_1 val_1
136
	) *)
137
     let rec print fmt (tab, x) =
138
       match tab with
139
       | [] -> pp_default_val fmt v.value_type(* (get_type v) *)
140
       | h::t ->
141
	  fprintf fmt "(store %a %i %a)"
142
	    print (t, (x+1))
143
	    x
144
	    (pp_horn_val ~is_lhs:is_lhs self pp_var) h
145
     in
146
     print fmt (il, 0)
147
       
148
  | Access(tab,index) ->
149
     fprintf fmt "(select %a %a)"
150
       (pp_horn_val ~is_lhs:is_lhs self pp_var) tab
151
       (pp_horn_val ~is_lhs:is_lhs self pp_var) index
152

    
153
  (* Code specific for arrays *)
154
    
155
  | Power (v, n)  -> assert false
156
  | LocalVar v    -> pp_var fmt (rename_machine self v)
157
  | StateVar v    ->
158
     if Types.is_array_type v.var_type
159
     then assert false
160
     else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
161
  | Fun (n, vl)   -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
162

    
163
(* Prints a [value] indexed by the suffix list [loop_vars] *)
164
let rec pp_value_suffix self pp_value fmt value =
165
 match value.value_desc with
166
 | Fun (n, vl)  ->
167
   Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
168
 |  _            ->
169
   pp_horn_val self pp_value fmt value
170

    
171
(* type_directed assignment: array vs. statically sized type
172
   - [var_type]: type of variable to be assigned
173
   - [var_name]: name of variable to be assigned
174
   - [value]: assigned value
175
   - [pp_var]: printer for variables
176
*)
177
let pp_assign m pp_var fmt var_name value =
178
  let self = m.mname.node_id in
179
  fprintf fmt "(= %a %a)" 
180
    (pp_horn_val ~is_lhs:true self pp_var) var_name
181
    (pp_value_suffix self pp_var) value
182
    
183

    
184
(* In case of no reset call, we define mid_mem = current_mem *)
185
let pp_no_reset machines m fmt i =
186
  let (n,_) = List.assoc i m.minstances in
187
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
188

    
189
  let m_list = 
190
    rename_machine_list
191
      (concat m.mname.node_id i)
192
      (rename_mid_list (full_memory_vars machines target_machine))
193
  in
194
  let c_list =
195
    rename_machine_list
196
      (concat m.mname.node_id i)
197
      (rename_current_list (full_memory_vars machines target_machine))
198
  in
199
  match c_list, m_list with
200
  | [chd], [mhd] ->
201
    fprintf fmt "(= %a %a)"
202
      (pp_horn_var m) mhd
203
      (pp_horn_var m) chd
204
  
205
  | _ -> (
206
    fprintf fmt "@[<v 0>(and @[<v 0>";
207
    List.iter2 (fun mhd chd -> 
208
      fprintf fmt "(= %a %a)@ "
209
      (pp_horn_var m) mhd
210
      (pp_horn_var m) chd
211
    )
212
      m_list
213
      c_list      ;
214
    fprintf fmt ")@]@ @]"
215
  )
216

    
217
let pp_instance_reset machines m fmt i =
218
  let (n,_) = List.assoc i m.minstances in
219
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
220
  
221
  fprintf fmt "(%a @[<v 0>%a)@]"
222
    pp_machine_reset_name (node_name n)
223
    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) 
224
    (
225
      (rename_machine_list
226
	 (concat m.mname.node_id i)
227
	 (rename_current_list (full_memory_vars machines target_machine))
228
      ) 
229
      @
230
	(rename_machine_list
231
	   (concat m.mname.node_id i)
232
	   (rename_mid_list (full_memory_vars machines target_machine))
233
	)
234
    )
235

    
236
let pp_instance_call machines reset_instances m fmt i inputs outputs =
237
  let self = m.mname.node_id in
238
  try (* stateful node instance *)
239
    begin
240
      let (n,_) = List.assoc i m.minstances in
241
      let target_machine = List.find (fun m  -> m.mname.node_id = node_name n) machines in
242
      (* Checking whether this specific instances has been reset yet *)
243
      if not (List.mem i reset_instances) then
244
	(* If not, declare mem_m = mem_c *)
245
	pp_no_reset machines m fmt i;
246
      
247
      let mems = full_memory_vars machines target_machine in
248
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
249
      let mid_mems = rename_mems rename_mid_list in
250
      let next_mems = rename_mems rename_next_list in
251

    
252
      match node_name n, inputs, outputs, mid_mems, next_mems with
253
      | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
254
	fprintf fmt "@[<v 5>(and ";
255
	fprintf fmt "(= %a (ite %a %a %a))"
256
	  (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *)
257
	  (pp_horn_var m) mem_m 
258
	  (pp_horn_val self (pp_horn_var m)) i1
259
	  (pp_horn_val self (pp_horn_var m)) i2
260
	;
261
	fprintf fmt "@ ";
262
	fprintf fmt "(= %a false)" (pp_horn_var m) mem_x;
263
	fprintf fmt ")@]"
264
      end
265

    
266
      | node_name_n -> begin
267
	fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]"
268
	  pp_machine_step_name (node_name n)
269
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) inputs
270
	  (Utils.pp_final_char_if_non_empty "@ " inputs)
271
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
272
	  (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
273
	  (Utils.pp_final_char_if_non_empty "@ " outputs)
274
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)
275
	
276
      end
277
    end
278
  with Not_found -> ( (* stateless node instance *)
279
    let (n,_) = List.assoc i m.mcalls in
280
    fprintf fmt "(%s @[<v 0>%a%t%a)@]"
281
      (node_name n)
282
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
283
      inputs
284
      (Utils.pp_final_char_if_non_empty "@ " inputs)
285
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
286
      (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
287
  )
288
    
289
    
290
(* Print the instruction and update the set of reset instances *)
291
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =
292
  match instr with
293
  | MComment _ -> reset_instances
294
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
295
    pp_no_reset machines m fmt i;
296
    i::reset_instances
297
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
298
    pp_instance_reset machines m fmt i;
299
    i::reset_instances
300
  | MLocalAssign (i,v) ->
301
    pp_assign
302
      m (pp_horn_var m) fmt
303
      (mk_val (LocalVar i) i.var_type) v;
304
    reset_instances
305
  | MStateAssign (i,v) ->
306
    pp_assign
307
      m (pp_horn_var m) fmt
308
      (mk_val (StateVar i) i.var_type) v;
309
    reset_instances
310
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
311
    assert false (* This should not happen anymore *)
312
  | MStep (il, i, vl) ->
313
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
314
       mem_c and print the call to mem_m *)
315
    pp_instance_call machines reset_instances m fmt i vl il;
316
    reset_instances (* Since this instance call will only happen once, we
317
		       don't have to update reset_instances *)
318

    
319
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
320
			 should not be produced yet. Later, we will have to
321
			 compare the reset_instances of each branch and
322
			 introduced the mem_m = mem_c for branches to do not
323
			 address it while other did. Am I clear ? *)
324
    (* For each branch we obtain the logical encoding, and the information
325
       whether a sub node has been reset or not. If a node has been reset in one
326
       of the branch, then all others have to have the mem_m = mem_c
327
       statement. *)
328
    let self = m.mname.node_id in
329
    let pp_branch fmt (tag, instrs) =
330
      fprintf fmt 
331
	"@[<v 3>(or (not (= %a %s))@ " 
332
	(*"@[<v 3>(=> (= %a %s)@ "*)  (* Issues with some versions of Z3. It
333
					  seems that => within Horn predicate
334
					  may cause trouble. I have hard time
335
					  producing a MWE, so I'll just keep the
336
					  fix here as (not a) or b *)
337
	(pp_horn_val self (pp_horn_var m)) g
338
	tag;
339
      let _ (* rs *) = pp_machine_instrs machines reset_instances m fmt instrs in 
340
      fprintf fmt "@])";
341
      () (* rs *)
342
    in
343
    pp_conj pp_branch fmt hl;
344
    reset_instances 
345

    
346
and pp_machine_instrs machines reset_instances m fmt instrs = 
347
  let ppi rs fmt i = pp_machine_instr machines rs m fmt i in
348
  match instrs with
349
  | [x] -> ppi reset_instances fmt x 
350
  | _::_ ->
351
    fprintf fmt "(and @[<v 0>";
352
    let rs = List.fold_left (fun rs i -> 
353
      let rs = ppi rs fmt i in
354
      fprintf fmt "@ ";
355
      rs
356
    )
357
      reset_instances instrs 
358
    in
359
    fprintf fmt "@])";
360
    rs
361

    
362
  | [] -> fprintf fmt "true"; reset_instances
363

    
364
let pp_machine_reset machines fmt m =
365
  let locals = local_memory_vars machines m in
366
  fprintf fmt "@[<v 5>(and @ ";
367

    
368
  (* print "x_m = x_c" for each local memory *)
369
  (Utils.fprintf_list ~sep:"@ " (fun fmt v -> 
370
    fprintf fmt "(= %a %a)"
371
      (pp_horn_var m) (rename_mid v)
372
      (pp_horn_var m) (rename_current v)
373
   )) fmt locals;
374
  fprintf fmt "@ ";
375

    
376
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
377
     Special treatment for _arrow: _first = true
378
  *)
379
  (Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) ->
380
    let name = node_name n in
381
    if name = "_arrow" then ( 
382
      fprintf fmt "(= %s._arrow._first_m true)"
383
	(concat m.mname.node_id id)  
384
    ) else (
385
      let machine_n = get_machine machines name in 
386
      fprintf fmt "(%s_reset @[<hov 0>%a@])" 
387
	name
388
	(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) 
389
	(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
390
    )
391
   )) fmt m.minstances;
392

    
393
  fprintf fmt "@]@ )"
394

    
395

    
396

    
397
(**************************************************************)
398

    
399
let is_stateless m = m.minstances = [] && m.mmemory = []
400

    
401
(* Print the machine m:
402
   two functions: m_init and m_step
403
   - m_init is a predicate over m memories
404
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
405
   We first declare all variables then the two /rules/.
406
*)
407
let print_machine machines fmt m =
408
  if m.mname.node_id = arrow_id then
409
    (* We don't print arrow function *)
410
    ()
411
  else
412
    begin
413
      fprintf fmt "; %s@." m.mname.node_id;
414
      
415
      (* Printing variables *)
416
      Utils.fprintf_list ~sep:"@." pp_decl_var fmt
417
	(
418
	  (inout_vars machines m)@
419
	    (rename_current_list (full_memory_vars machines m)) @
420
	    (rename_mid_list (full_memory_vars machines m)) @
421
	    (rename_next_list (full_memory_vars machines m)) @
422
	    (rename_machine_list m.mname.node_id m.mstep.step_locals)
423
	);
424
      pp_print_newline fmt ();
425

    
426
      if is_stateless m then
427
	begin
428
	  (* Declaring single predicate *)
429
	  fprintf fmt "(declare-rel %a (%a))@."
430
	    pp_machine_stateless_name m.mname.node_id
431
	    (Utils.fprintf_list ~sep:" " pp_type)
432
	    (List.map (fun v -> v.var_type) (inout_vars machines m));
433

    
434
	  (* Rule for single predicate *)
435
	  fprintf fmt "@[<v 2>(rule (=> @ ";
436
	  ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);
437
	  fprintf fmt "@ (%a %a)@]@.))@.@."
438
	    pp_machine_stateless_name m.mname.node_id
439
	    (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m);
440
	end
441
      else
442
	begin
443
	  (* Declaring predicate *)
444
	  fprintf fmt "(declare-rel %a (%a))@."
445
	    pp_machine_reset_name m.mname.node_id
446
	    (Utils.fprintf_list ~sep:" " pp_type)
447
	    (List.map (fun v -> v.var_type) (reset_vars machines m));
448

    
449
	  fprintf fmt "(declare-rel %a (%a))@."
450
	    pp_machine_step_name m.mname.node_id
451
	    (Utils.fprintf_list ~sep:" " pp_type)
452
	    (List.map (fun v -> v.var_type) (step_vars machines m));
453

    
454
	  pp_print_newline fmt ();
455

    
456
	  (* Rule for reset *)
457
	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
458
	    (pp_machine_reset machines) m 
459
	    pp_machine_reset_name m.mname.node_id
460
	    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);
461

    
462
          match m.mstep.step_asserts with
463
	  | [] ->
464
	    begin
465

    
466
	      (* Rule for step*)
467
	      fprintf fmt "@[<v 2>(rule (=> @ ";
468
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
469
	      fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
470
		pp_machine_step_name m.mname.node_id
471
		(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
472
	    end
473
	  | assertsl -> 
474
	    begin
475
	      let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
476
	      (* print_string pp_val; *)
477
	      fprintf fmt "; with Assertions @.";
478
	      
479
	      (*Rule for step*)
480
	      fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
481
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
482
	      fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
483
		pp_machine_step_name m.mname.node_id
484
		(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
485
	    end
486
	      
487
	      
488
	end
489
    end
490

    
491

    
492
let mk_flags arity =
493
  let b_range =
494
   let rec range i j =
495
     if i > arity then [] else i :: (range (i+1) j) in
496
   range 2 arity;
497
 in
498
 List.fold_left (fun acc x -> acc ^ " false") "true" b_range
499

    
500

    
501
  (*Get sfunction infos from command line*)
502
let get_sf_info() =
503
  let splitted = Str.split (Str.regexp "@") !Options.sfunction in
504
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. sfunction name: %s@," !Options.sfunction);
505
  let sf_name, flags, arity = match splitted with
506
      [h;flg;par] -> h, flg, par
507
    | _ -> failwith "Wrong Sfunction info"
508

    
509
  in
510
  Log.report ~level:1 (fun fmt -> fprintf fmt "... sf_name: %s@, .. flags: %s@ .. arity: %s@," sf_name flags arity);
511
  sf_name, flags, arity
512

    
513

    
514
    (*a function to print the rules in case we have an s-function*)
515
  let print_sfunction machines fmt m =
516
      if m.mname.node_id = arrow_id then
517
        (* We don't print arrow function *)
518
        ()
519
      else
520
        begin
521
          Format.fprintf fmt "; SFUNCTION@.";
522
          Format.fprintf fmt "; %s@." m.mname.node_id;
523
          Format.fprintf fmt "; EndPoint Predicate %s." !Options.sfunction;
524

    
525
          (* Check if there is annotation for s-function *)
526
          if m.mannot != [] then(
527
              Format.fprintf fmt "; @[%a@]@]@\n" (Utils.fprintf_list ~sep:"@ " Printers.pp_s_function) m.mannot;
528
            );
529

    
530
       (* Printing variables *)
531
          Utils.fprintf_list ~sep:"@." pp_decl_var fmt
532
                             ((step_vars machines m)@
533
    	                        (rename_machine_list m.mname.node_id m.mstep.step_locals));
534
          Format.pp_print_newline fmt ();
535
          let sf_name, flags, arity = get_sf_info() in
536

    
537
       if is_stateless m then
538
         begin
539
           (* Declaring single predicate *)
540
           Format.fprintf fmt "(declare-rel %a (%a))@."
541
    	                  pp_machine_stateless_name m.mname.node_id
542
    	                  (Utils.fprintf_list ~sep:" " pp_type)
543
    	                  (List.map (fun v -> v.var_type) (reset_vars machines m));
544
           Format.pp_print_newline fmt ();
545
           (* Rule for single predicate *)
546
           let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in
547
           Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@."
548
                          str_flags
549
                          (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m)
550
	                  pp_machine_stateless_name m.mname.node_id
551
	                  (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m);
552
         end
553
      else
554
         begin
555
           (* Declaring predicate *)
556
           Format.fprintf fmt "(declare-rel %a (%a))@."
557
    	                  pp_machine_reset_name m.mname.node_id
558
    	                  (Utils.fprintf_list ~sep:" " pp_type)
559
    	                  (List.map (fun v -> v.var_type) (inout_vars machines m));
560

    
561
           Format.fprintf fmt "(declare-rel %a (%a))@."
562
    	                  pp_machine_step_name m.mname.node_id
563
    	                  (Utils.fprintf_list ~sep:" " pp_type)
564
    	                  (List.map (fun v -> v.var_type) (step_vars machines m));
565

    
566
           Format.pp_print_newline fmt ();
567
          (* Adding assertions *)
568
           match m.mstep.step_asserts with
569
	  | [] ->
570
	    begin
571

    
572
	      (* Rule for step*)
573
	      fprintf fmt "@[<v 2>(rule (=> @ ";
574
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
575
	      fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
576
		pp_machine_step_name m.mname.node_id
577
		(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
578
	    end
579
	  | assertsl ->
580
	    begin
581
	      let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
582
	      (* print_string pp_val; *)
583
	      fprintf fmt "; with Assertions @.";
584

    
585
	      (*Rule for step*)
586
	      fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
587
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
588
	      fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
589
		pp_machine_step_name m.mname.node_id
590
		(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
591
	    end
592

    
593
         end
594

    
595
        end
596
(* Local Variables: *)
597
(* compile-command:"make -C ../../.." *)
598
(* End: *)