Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend_printers.ml @ 212d6eff

History | View | Annotate | Download (26.5 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
(*                    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 "(%a @[<v 0>%a%t%a)@]"
280
      pp_machine_stateless_name (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 get_instr_desc 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 %a))@ " 
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
	pp_horn_tag 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
          match m.mstep.step_asserts with
434
	  | [] ->
435
	     begin
436

    
437
	       (* Rule for single predicate *)
438
	       fprintf fmt "; Stateless step rule @.";
439
	       fprintf fmt "@[<v 2>(rule (=> @ ";
440
	       ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);
441
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
442
		 pp_machine_stateless_name m.mname.node_id
443
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_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
	       
449
	       fprintf fmt "; Stateless step rule with Assertions @.";
450
	       (*Rule for step*)
451
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
452
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
453
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
454
		 pp_machine_stateless_name m.mname.node_id
455
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
456
	  
457
	     end
458
	       
459
	end
460
      else
461
	begin
462
	  (* Declaring predicate *)
463
	  fprintf fmt "(declare-rel %a (%a))@."
464
	    pp_machine_reset_name m.mname.node_id
465
	    (Utils.fprintf_list ~sep:" " pp_type)
466
	    (List.map (fun v -> v.var_type) (reset_vars machines m));
467

    
468
	  fprintf fmt "(declare-rel %a (%a))@."
469
	    pp_machine_step_name m.mname.node_id
470
	    (Utils.fprintf_list ~sep:" " pp_type)
471
	    (List.map (fun v -> v.var_type) (step_vars machines m));
472

    
473
	  pp_print_newline fmt ();
474

    
475
	  (* Rule for reset *)
476
	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
477
	    (pp_machine_reset machines) m 
478
	    pp_machine_reset_name m.mname.node_id
479
	    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);
480

    
481
          match m.mstep.step_asserts with
482
	  | [] ->
483
	     begin
484
	       fprintf fmt "; Step rule @.";
485
	       (* Rule for step*)
486
	       fprintf fmt "@[<v 2>(rule (=> @ ";
487
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
488
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
489
		 pp_machine_step_name m.mname.node_id
490
		 (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
491
	     end
492
	  | assertsl -> 
493
	     begin
494
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
495
	       (* print_string pp_val; *)
496
	       fprintf fmt "; Step rule with Assertions @.";
497
	       
498
	       (*Rule for step*)
499
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
500
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
501
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
502
		 pp_machine_step_name m.mname.node_id
503
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
504
	     end
505
	       
506
	       
507
	end
508
    end
509

    
510

    
511
let mk_flags arity =
512
  let b_range =
513
   let rec range i j =
514
     if i > arity then [] else i :: (range (i+1) j) in
515
   range 2 arity;
516
 in
517
 List.fold_left (fun acc x -> acc ^ " false") "true" b_range
518

    
519

    
520
  (*Get sfunction infos from command line*)
521
let get_sf_info() =
522
  let splitted = Str.split (Str.regexp "@") !Options.sfunction in
523
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. sfunction name: %s@," !Options.sfunction);
524
  let sf_name, flags, arity = match splitted with
525
      [h;flg;par] -> h, flg, par
526
    | _ -> failwith "Wrong Sfunction info"
527

    
528
  in
529
  Log.report ~level:1 (fun fmt -> fprintf fmt "... sf_name: %s@, .. flags: %s@ .. arity: %s@," sf_name flags arity);
530
  sf_name, flags, arity
531

    
532

    
533
    (*a function to print the rules in case we have an s-function*)
534
  let print_sfunction machines fmt m =
535
      if m.mname.node_id = arrow_id then
536
        (* We don't print arrow function *)
537
        ()
538
      else
539
        begin
540
          Format.fprintf fmt "; SFUNCTION@.";
541
          Format.fprintf fmt "; %s@." m.mname.node_id;
542
          Format.fprintf fmt "; EndPoint Predicate %s." !Options.sfunction;
543

    
544
          (* Check if there is annotation for s-function *)
545
          if m.mannot != [] then(
546
              Format.fprintf fmt "; @[%a@]@]@\n" (Utils.fprintf_list ~sep:"@ " Printers.pp_s_function) m.mannot;
547
            );
548

    
549
       (* Printing variables *)
550
          Utils.fprintf_list ~sep:"@." pp_decl_var fmt
551
                             ((step_vars machines m)@
552
    	                        (rename_machine_list m.mname.node_id m.mstep.step_locals));
553
          Format.pp_print_newline fmt ();
554
          let sf_name, flags, arity = get_sf_info() in
555

    
556
       if is_stateless m then
557
         begin
558
           (* Declaring single predicate *)
559
           Format.fprintf fmt "(declare-rel %a (%a))@."
560
    	                  pp_machine_stateless_name m.mname.node_id
561
    	                  (Utils.fprintf_list ~sep:" " pp_type)
562
    	                  (List.map (fun v -> v.var_type) (reset_vars machines m));
563
           Format.pp_print_newline fmt ();
564
           (* Rule for single predicate *)
565
           let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in
566
           Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@."
567
                          str_flags
568
                          (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m)
569
	                  pp_machine_stateless_name m.mname.node_id
570
	                  (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m);
571
         end
572
      else
573
         begin
574
           (* Declaring predicate *)
575
           Format.fprintf fmt "(declare-rel %a (%a))@."
576
    	                  pp_machine_reset_name m.mname.node_id
577
    	                  (Utils.fprintf_list ~sep:" " pp_type)
578
    	                  (List.map (fun v -> v.var_type) (inout_vars machines m));
579

    
580
           Format.fprintf fmt "(declare-rel %a (%a))@."
581
    	                  pp_machine_step_name m.mname.node_id
582
    	                  (Utils.fprintf_list ~sep:" " pp_type)
583
    	                  (List.map (fun v -> v.var_type) (step_vars machines m));
584

    
585
           Format.pp_print_newline fmt ();
586
          (* Adding assertions *)
587
           match m.mstep.step_asserts with
588
	  | [] ->
589
	    begin
590

    
591
	      (* Rule for step*)
592
	      fprintf fmt "@[<v 2>(rule (=> @ ";
593
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
594
	      fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
595
		pp_machine_step_name m.mname.node_id
596
		(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
597
	    end
598
	  | assertsl ->
599
	    begin
600
	      let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
601
	      (* print_string pp_val; *)
602
	      fprintf fmt "; with Assertions @.";
603

    
604
	      (*Rule for step*)
605
	      fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
606
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
607
	      fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
608
		pp_machine_step_name m.mname.node_id
609
		(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
610
	    end
611

    
612
         end
613

    
614
        end
615

    
616

    
617
(**************** XML printing functions *************)
618

    
619
	  let rec pp_xml_expr fmt expr =
620
  (match expr.expr_annot with 
621
  | None -> fprintf fmt "%t" 
622
  | Some ann -> fprintf fmt "@[(%a %t)@]" pp_xml_expr_annot ann)
623
    (fun fmt -> 
624
      match expr.expr_desc with
625
    | Expr_const c -> Printers.pp_const fmt c
626
    | Expr_ident id -> fprintf fmt "%s" id
627
    | Expr_array a -> fprintf fmt "[%a]" pp_xml_tuple a
628
    | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_xml_expr a Dimension.pp_dimension d
629
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_xml_expr a Dimension.pp_dimension d
630
    | Expr_tuple el -> fprintf fmt "(%a)" pp_xml_tuple el
631
    | Expr_ite (c, t, e) -> fprintf fmt "@[<hov 1>(if %a then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@])" pp_xml_expr c pp_xml_expr t pp_xml_expr e
632
    | Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_xml_expr e1 pp_xml_expr e2
633
    | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_xml_expr e1 pp_xml_expr e2
634
    | Expr_pre e -> fprintf fmt "pre %a" pp_xml_expr e
635
    | Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_xml_expr e l id
636
    | Expr_merge (id, hl) -> 
637
      fprintf fmt "merge %s %a" id pp_xml_handlers hl
638
    | Expr_appl (id, e, r) -> pp_xml_app fmt id e r
639
    )
640
and pp_xml_tuple fmt el =
641
 Utils.fprintf_list ~sep:"," pp_xml_expr fmt el
642

    
643
and pp_xml_handler fmt (t, h) =
644
 fprintf fmt "(%s -> %a)" t pp_xml_expr h
645

    
646
and pp_xml_handlers fmt hl =
647
 Utils.fprintf_list ~sep:" " pp_xml_handler fmt hl
648

    
649
and pp_xml_app fmt id e r =
650
  match r with
651
  | None -> pp_xml_call fmt id e
652
  | Some c -> fprintf fmt "%t every (%a)" (fun fmt -> pp_xml_call fmt id e) pp_xml_expr c 
653

    
654
and pp_xml_call fmt id e =
655
  match id, e.expr_desc with
656
  | "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_xml_expr e1 pp_xml_expr e2
657
  | "uminus", _ -> fprintf fmt "(- %a)" pp_xml_expr e
658
  | "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_xml_expr e1 pp_xml_expr e2
659
  | "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_xml_expr e1 pp_xml_expr e2
660
  | "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_xml_expr e1 pp_xml_expr e2
661
  | "mod", Expr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_xml_expr e1 pp_xml_expr e2
662
  | "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a and %a)" pp_xml_expr e1 pp_xml_expr e2
663
  | "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a or %a)" pp_xml_expr e1 pp_xml_expr e2
664
  | "xor", Expr_tuple([e1;e2]) -> fprintf fmt "(%a xor %a)" pp_xml_expr e1 pp_xml_expr e2
665
  | "impl", Expr_tuple([e1;e2]) -> fprintf fmt "(%a => %a)" pp_xml_expr e1 pp_xml_expr e2
666
  | "<", Expr_tuple([e1;e2]) -> fprintf fmt "(%a &lt; %a)" pp_xml_expr e1 pp_xml_expr e2
667
  | "<=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a &lt;= %a)" pp_xml_expr e1 pp_xml_expr e2
668
  | ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a &gt; %a)" pp_xml_expr e1 pp_xml_expr e2
669
  | ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a &gt;= %a)" pp_xml_expr e1 pp_xml_expr e2
670
  | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_xml_expr e1 pp_xml_expr e2
671
  | "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_xml_expr e1 pp_xml_expr e2
672
  | "not", _ -> fprintf fmt "(not %a)" pp_xml_expr e
673
  | _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_xml_expr e
674
  | _ -> fprintf fmt "%s (%a)" id pp_xml_expr e
675

    
676
and pp_xml_eexpr fmt e =
677
  fprintf fmt "%a%t %a"
678
    (Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers) e.eexpr_quantifiers
679
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
680
    pp_xml_expr e.eexpr_qfexpr
681

    
682
and  pp_xml_sf_value fmt e =
683
   fprintf fmt "%a"
684
     (* (Utils.fprintf_list ~sep:"; " pp_xml_quantifiers) e.eexpr_quantifiers *)
685
     (* (fun fmt -> match e.eexpr_quantifiers *)
686
     (*             with [] -> () *)
687
     (*                | _ -> fprintf fmt ";") *)
688
     pp_xml_expr e.eexpr_qfexpr
689

    
690
and pp_xml_s_function fmt expr_ann =
691
  let pp_xml_annot fmt (kwds, ee) =
692
    Format.fprintf fmt " %t : %a"
693
                   (fun fmt -> match kwds with
694
                               | [] -> assert false
695
                               | [x] -> Format.pp_print_string fmt x
696
                               | _ -> Format.fprintf fmt "%a" (Utils.fprintf_list ~sep:"/" Format.pp_print_string) kwds)
697
                   pp_xml_sf_value ee
698
  in
699
  Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
700

    
701
and pp_xml_expr_annot fmt expr_ann =
702
  let pp_xml_annot fmt (kwds, ee) =
703
    Format.fprintf fmt "(*! %t: %a; *)"
704
      (fun fmt -> match kwds with | [] -> assert false | [x] -> Format.pp_print_string fmt x | _ -> Format.fprintf fmt "/%a/" (Utils.fprintf_list ~sep:"/" Format.pp_print_string) kwds)
705
      pp_xml_eexpr ee
706
  in
707
  Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
708

    
709

    
710
(* Local Variables: *)
711
(* compile-command:"make -C ../../.." *)
712
(* End: *)