Project

General

Profile

Download (21.1 KB) Statistics
| Branch: | Tag: | Revision:
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
(*                    Instruction Printing functions                                        *)
27
(********************************************************************************************)
28

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

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

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

    
48
(* PL comment 2017/01/03: Useless code, the function existed before in typing.ml *)
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), *)
55
(* 				     get_type_cst (List.hd l))) *)
56
(*   | Const_tag(tag) -> new_ty Tbool *)
57
(*   | Const_string(str) ->  assert false(\* used only for annotations *\) *)
58
(*   | Const_struct(l) -> new_ty (Tstruct(List.map (fun (label, t) -> (label, get_type_cst t)) l)) *)
59

    
60
(* 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 *)
61

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

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

    
112

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
392
  fprintf fmt "@]@ )"
393

    
394

    
395

    
396
(**************************************************************)
397

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

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

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

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

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

    
453
	  pp_print_newline fmt ();
454

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

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

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

    
490

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

    
499

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

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

    
512

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

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

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

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

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

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

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

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

    
592
         end
593

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