Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (27.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 Lustre_types
20
open Machine_code_types
21
open Corelang
22
open Machine_code_common
23

    
24
open Horn_backend_common
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
  let t = Types.dynamic_type t in
101
  if Types.is_bool_type t  then fprintf fmt "true" else
102
  if Types.is_int_type t then fprintf fmt "0" else 
103
  if Types.is_real_type t then fprintf fmt "0" else 
104
  match (Types.dynamic_type t).Types.tdesc with
105
  | Types.Tarray(dim, l) -> (* TODO PL: this strange code has to be (heavily) checked *)
106
     let valt = Types.array_element_type t in
107
     fprintf fmt "((as const (Array Int %a)) %a)"
108
       pp_type valt 
109
       pp_default_val valt
110
  | Types.Tstruct(l) -> assert false
111
  | Types.Ttuple(l) -> assert false
112
  |_ -> assert false
113

    
114

    
115
let pp_basic_lib_fun i pp_val fmt vl =
116
  match i, vl with
117
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3
118

    
119
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
120
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
121
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
122
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
123
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
124
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
125
  | "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
126
  | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
127
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
128
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
129
  | "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
130
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
131
  | _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)
132
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
133

    
134
*)
135

    
136

    
137
(* Prints a value expression [v], with internal function calls only.
138
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
139
   but an offset suffix may be added for array variables
140
*)
141
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
142
  match v.value_desc with
143
  | Cst c       -> pp_horn_const fmt c
144

    
145
  (* Code specific for arrays *)
146
  | Array il    ->
147
     (* An array definition: 
148
	(store (
149
	  ...
150
 	    (store (
151
	       store (
152
	          default_val
153
	       ) 
154
	       idx_n val_n
155
	    ) 
156
	    idx_n-1 val_n-1)
157
	  ... 
158
	  idx_1 val_1
159
	) *)
160
     let rec print fmt (tab, x) =
161
       match tab with
162
       | [] -> pp_default_val fmt v.value_type(* (get_type v) *)
163
       | h::t ->
164
	  fprintf fmt "(store %a %i %a)"
165
	    print (t, (x+1))
166
	    x
167
	    (pp_horn_val ~is_lhs:is_lhs self pp_var) h
168
     in
169
     print fmt (il, 0)
170
       
171
  | Access(tab,index) ->
172
     fprintf fmt "(select %a %a)"
173
       (pp_horn_val ~is_lhs:is_lhs self pp_var) tab
174
       (pp_horn_val ~is_lhs:is_lhs self pp_var) index
175

    
176
  (* Code specific for arrays *)
177
    
178
  | Power (v, n)  -> assert false
179
  | LocalVar v    -> pp_var fmt (rename_machine self v)
180
  | StateVar v    ->
181
     if Types.is_array_type v.var_type
182
     then assert false
183
     else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
184
  | Fun (n, vl)   -> fprintf fmt "%a" (pp_basic_lib_fun n (pp_horn_val self pp_var)) vl
185

    
186
(* Prints a [value] indexed by the suffix list [loop_vars] *)
187
let rec pp_value_suffix self pp_value fmt value =
188
 match value.value_desc with
189
 | Fun (n, vl)  ->
190
   pp_basic_lib_fun n (pp_value_suffix self pp_value) fmt vl
191
 |  _            ->
192
   pp_horn_val self pp_value fmt value
193

    
194
(* type_directed assignment: array vs. statically sized type
195
   - [var_type]: type of variable to be assigned
196
   - [var_name]: name of variable to be assigned
197
   - [value]: assigned value
198
   - [pp_var]: printer for variables
199
*)
200
let pp_assign m pp_var fmt var_name value =
201
  let self = m.mname.node_id in
202
  fprintf fmt "(= %a %a)" 
203
    (pp_horn_val ~is_lhs:true self pp_var) var_name
204
    (pp_value_suffix self pp_var) value
205
    
206

    
207
(* In case of no reset call, we define mid_mem = current_mem *)
208
let pp_no_reset machines m fmt i =
209
  let (n,_) = List.assoc i m.minstances in
210
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
211

    
212
  let m_list = 
213
    rename_machine_list
214
      (concat m.mname.node_id i)
215
      (rename_mid_list (full_memory_vars machines target_machine))
216
  in
217
  let c_list =
218
    rename_machine_list
219
      (concat m.mname.node_id i)
220
      (rename_current_list (full_memory_vars machines target_machine))
221
  in
222
  match c_list, m_list with
223
  | [chd], [mhd] ->
224
    fprintf fmt "(= %a %a)"
225
      (pp_horn_var m) mhd
226
      (pp_horn_var m) chd
227
  
228
  | _ -> (
229
    fprintf fmt "@[<v 0>(and @[<v 0>";
230
    List.iter2 (fun mhd chd -> 
231
      fprintf fmt "(= %a %a)@ "
232
      (pp_horn_var m) mhd
233
      (pp_horn_var m) chd
234
    )
235
      m_list
236
      c_list      ;
237
    fprintf fmt ")@]@ @]"
238
  )
239

    
240
let pp_instance_reset machines m fmt i =
241
  let (n,_) = List.assoc i m.minstances in
242
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
243
  
244
  fprintf fmt "(%a @[<v 0>%a)@]"
245
    pp_machine_reset_name (node_name n)
246
    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) 
247
    (
248
      (rename_machine_list
249
	 (concat m.mname.node_id i)
250
	 (rename_current_list (full_memory_vars machines target_machine))
251
      ) 
252
      @
253
	(rename_machine_list
254
	   (concat m.mname.node_id i)
255
	   (rename_mid_list (full_memory_vars machines target_machine))
256
	)
257
    )
258

    
259
let pp_instance_call machines reset_instances m fmt i inputs outputs =
260
  let self = m.mname.node_id in
261
  try (* stateful node instance *)
262
    begin
263
      let (n,_) = List.assoc i m.minstances in
264
      let target_machine = List.find (fun m  -> m.mname.node_id = node_name n) machines in
265
      (* Checking whether this specific instances has been reset yet *)
266
      if not (List.mem i reset_instances) then
267
	(* If not, declare mem_m = mem_c *)
268
	pp_no_reset machines m fmt i;
269
      
270
      let mems = full_memory_vars machines target_machine in
271
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
272
      let mid_mems = rename_mems rename_mid_list in
273
      let next_mems = rename_mems rename_next_list in
274

    
275
      match node_name n, inputs, outputs, mid_mems, next_mems with
276
      | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
277
	fprintf fmt "@[<v 5>(and ";
278
	fprintf fmt "(= %a (ite %a %a %a))"
279
	  (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *)
280
	  (pp_horn_var m) mem_m 
281
	  (pp_horn_val self (pp_horn_var m)) i1
282
	  (pp_horn_val self (pp_horn_var m)) i2
283
	;
284
	fprintf fmt "@ ";
285
	fprintf fmt "(= %a false)" (pp_horn_var m) mem_x;
286
	fprintf fmt ")@]"
287
      end
288

    
289
      | node_name_n -> begin
290
	fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]"
291
	  pp_machine_step_name (node_name n)
292
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) inputs
293
	  (Utils.pp_final_char_if_non_empty "@ " inputs)
294
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
295
	  (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
296
	  (Utils.pp_final_char_if_non_empty "@ " outputs)
297
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)
298
	
299
      end
300
    end
301
  with Not_found -> ( (* stateless node instance *)
302
    let (n,_) = List.assoc i m.mcalls in
303
    fprintf fmt "(%a @[<v 0>%a%t%a)@]"
304
      pp_machine_stateless_name (node_name n)
305
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
306
      inputs
307
      (Utils.pp_final_char_if_non_empty "@ " inputs)
308
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
309
      (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
310
  )
311
    
312
    
313
(* Print the instruction and update the set of reset instances *)
314
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =
315
  match get_instr_desc instr with
316
  | MComment _ -> reset_instances
317
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
318
    pp_no_reset machines m fmt i;
319
    i::reset_instances
320
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
321
    pp_instance_reset machines m fmt i;
322
    i::reset_instances
323
  | MLocalAssign (i,v) ->
324
    pp_assign
325
      m (pp_horn_var m) fmt
326
      (mk_val (LocalVar i) i.var_type) v;
327
    reset_instances
328
  | MStateAssign (i,v) ->
329
    pp_assign
330
      m (pp_horn_var m) fmt
331
      (mk_val (StateVar i) i.var_type) v;
332
    reset_instances
333
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
334
    assert false (* This should not happen anymore *)
335
  | MStep (il, i, vl) ->
336
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
337
       mem_c and print the call to mem_m *)
338
    pp_instance_call machines reset_instances m fmt i vl il;
339
    reset_instances (* Since this instance call will only happen once, we
340
		       don't have to update reset_instances *)
341

    
342
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
343
			 should not be produced yet. Later, we will have to
344
			 compare the reset_instances of each branch and
345
			 introduced the mem_m = mem_c for branches to do not
346
			 address it while other did. Am I clear ? *)
347
    (* For each branch we obtain the logical encoding, and the information
348
       whether a sub node has been reset or not. If a node has been reset in one
349
       of the branch, then all others have to have the mem_m = mem_c
350
       statement. *)
351
    let self = m.mname.node_id in
352
    let pp_branch fmt (tag, instrs) =
353
      fprintf fmt 
354
	"@[<v 3>(or (not (= %a %a))@ " 
355
	(*"@[<v 3>(=> (= %a %s)@ "*)  (* Issues with some versions of Z3. It
356
					  seems that => within Horn predicate
357
					  may cause trouble. I have hard time
358
					  producing a MWE, so I'll just keep the
359
					  fix here as (not a) or b *)
360
	(pp_horn_val self (pp_horn_var m)) g
361
	pp_horn_tag tag;
362
      let _ (* rs *) = pp_machine_instrs machines reset_instances m fmt instrs in 
363
      fprintf fmt "@])";
364
      () (* rs *)
365
    in
366
    pp_conj pp_branch fmt hl;
367
    reset_instances 
368

    
369
and pp_machine_instrs machines reset_instances m fmt instrs = 
370
  let ppi rs fmt i = pp_machine_instr machines rs m fmt i in
371
  match instrs with
372
  | [x] -> ppi reset_instances fmt x 
373
  | _::_ ->
374
    fprintf fmt "(and @[<v 0>";
375
    let rs = List.fold_left (fun rs i -> 
376
      let rs = ppi rs fmt i in
377
      fprintf fmt "@ ";
378
      rs
379
    )
380
      reset_instances instrs 
381
    in
382
    fprintf fmt "@])";
383
    rs
384

    
385
  | [] -> fprintf fmt "true"; reset_instances
386

    
387
let pp_machine_reset machines fmt m =
388
  let locals = local_memory_vars machines m in
389
  fprintf fmt "@[<v 5>(and @ ";
390

    
391
  (* print "x_m = x_c" for each local memory *)
392
  (Utils.fprintf_list ~sep:"@ " (fun fmt v -> 
393
    fprintf fmt "(= %a %a)"
394
      (pp_horn_var m) (rename_mid v)
395
      (pp_horn_var m) (rename_current v)
396
   )) fmt locals;
397
  fprintf fmt "@ ";
398

    
399
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
400
     Special treatment for _arrow: _first = true
401
  *)
402
  (Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) ->
403
    let name = node_name n in
404
    if name = "_arrow" then ( 
405
      fprintf fmt "(= %s._arrow._first_m true)"
406
	(concat m.mname.node_id id)  
407
    ) else (
408
      let machine_n = get_machine machines name in 
409
      fprintf fmt "(%s_reset @[<hov 0>%a@])" 
410
	name
411
	(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) 
412
	(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
413
    )
414
   )) fmt m.minstances;
415

    
416
  fprintf fmt "@]@ )"
417

    
418

    
419

    
420
(**************************************************************)
421

    
422

    
423
(* Print the machine m:
424
   two functions: m_init and m_step
425
   - m_init is a predicate over m memories
426
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
427
   We first declare all variables then the two /rules/.
428
*)
429
let print_machine machines fmt m =
430
  if m.mname.node_id = Arrow.arrow_id then
431
    (* We don't print arrow function *)
432
    ()
433
  else
434
    begin
435
      fprintf fmt "; %s@." m.mname.node_id;
436
      
437
      (* Printing variables *)
438
      Utils.fprintf_list ~sep:"@." pp_decl_var fmt
439
	(
440
	  (inout_vars machines m)@
441
	    (rename_current_list (full_memory_vars machines m)) @
442
	    (rename_mid_list (full_memory_vars machines m)) @
443
	    (rename_next_list (full_memory_vars machines m)) @
444
	    (rename_machine_list m.mname.node_id m.mstep.step_locals)
445
	);
446
      pp_print_newline fmt ();
447

    
448
      if is_stateless m then
449
	begin
450
	  (* Declaring single predicate *)
451
	  fprintf fmt "(declare-rel %a (%a))@."
452
	    pp_machine_stateless_name m.mname.node_id
453
	    (Utils.fprintf_list ~sep:" " pp_type)
454
	    (List.map (fun v -> v.var_type) (inout_vars machines m));
455

    
456
          match m.mstep.step_asserts with
457
	  | [] ->
458
	     begin
459

    
460
	       (* Rule for single predicate *)
461
	       fprintf fmt "; Stateless step rule @.";
462
	       fprintf fmt "@[<v 2>(rule (=> @ ";
463
	       ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);
464
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
465
		 pp_machine_stateless_name m.mname.node_id
466
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m);
467
	     end
468
	  | assertsl ->
469
	     begin
470
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
471
	       
472
	       fprintf fmt "; Stateless step rule with Assertions @.";
473
	       (*Rule for step*)
474
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
475
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
476
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
477
		 pp_machine_stateless_name m.mname.node_id
478
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
479
	  
480
	     end
481
	       
482
	end
483
      else
484
	begin
485
	  (* Declaring predicate *)
486
	  fprintf fmt "(declare-rel %a (%a))@."
487
	    pp_machine_reset_name m.mname.node_id
488
	    (Utils.fprintf_list ~sep:" " pp_type)
489
	    (List.map (fun v -> v.var_type) (reset_vars machines m));
490

    
491
	  fprintf fmt "(declare-rel %a (%a))@."
492
	    pp_machine_step_name m.mname.node_id
493
	    (Utils.fprintf_list ~sep:" " pp_type)
494
	    (List.map (fun v -> v.var_type) (step_vars machines m));
495

    
496
	  pp_print_newline fmt ();
497

    
498
	  (* Rule for reset *)
499
	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
500
	    (pp_machine_reset machines) m 
501
	    pp_machine_reset_name m.mname.node_id
502
	    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);
503

    
504
          match m.mstep.step_asserts with
505
	  | [] ->
506
	     begin
507
	       fprintf fmt "; Step rule @.";
508
	       (* Rule for step*)
509
	       fprintf fmt "@[<v 2>(rule (=> @ ";
510
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
511
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
512
		 pp_machine_step_name m.mname.node_id
513
		 (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
514
	     end
515
	  | assertsl -> 
516
	     begin
517
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
518
	       (* print_string pp_val; *)
519
	       fprintf fmt "; Step rule with Assertions @.";
520
	       
521
	       (*Rule for step*)
522
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
523
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
524
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
525
		 pp_machine_step_name m.mname.node_id
526
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
527
	     end
528
	       
529
	       
530
	end
531
    end
532

    
533

    
534
let mk_flags arity =
535
  let b_range =
536
   let rec range i j =
537
     if i > arity then [] else i :: (range (i+1) j) in
538
   range 2 arity;
539
 in
540
 List.fold_left (fun acc x -> acc ^ " false") "true" b_range
541

    
542

    
543
  (*Get sfunction infos from command line*)
544
let get_sf_info() =
545
  let splitted = Str.split (Str.regexp "@") !Options.sfunction in
546
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. sfunction name: %s@," !Options.sfunction);
547
  let sf_name, flags, arity = match splitted with
548
      [h;flg;par] -> h, flg, par
549
    | _ -> failwith "Wrong Sfunction info"
550

    
551
  in
552
  Log.report ~level:1 (fun fmt -> fprintf fmt "... sf_name: %s@, .. flags: %s@ .. arity: %s@," sf_name flags arity);
553
  sf_name, flags, arity
554

    
555

    
556
    (*a function to print the rules in case we have an s-function*)
557
  let print_sfunction machines fmt m =
558
      if m.mname.node_id = Arrow.arrow_id then
559
        (* We don't print arrow function *)
560
        ()
561
      else
562
        begin
563
          Format.fprintf fmt "; SFUNCTION@.";
564
          Format.fprintf fmt "; %s@." m.mname.node_id;
565
          Format.fprintf fmt "; EndPoint Predicate %s." !Options.sfunction;
566

    
567
          (* Check if there is annotation for s-function *)
568
          if m.mannot != [] then(
569
              Format.fprintf fmt "; @[%a@]@]@\n" (Utils.fprintf_list ~sep:"@ " Printers.pp_s_function) m.mannot;
570
            );
571

    
572
       (* Printing variables *)
573
          Utils.fprintf_list ~sep:"@." pp_decl_var fmt
574
                             ((step_vars machines m)@
575
    	                        (rename_machine_list m.mname.node_id m.mstep.step_locals));
576
          Format.pp_print_newline fmt ();
577
          let sf_name, flags, arity = get_sf_info() in
578

    
579
       if is_stateless m then
580
         begin
581
           (* Declaring single predicate *)
582
           Format.fprintf fmt "(declare-rel %a (%a))@."
583
    	                  pp_machine_stateless_name m.mname.node_id
584
    	                  (Utils.fprintf_list ~sep:" " pp_type)
585
    	                  (List.map (fun v -> v.var_type) (reset_vars machines m));
586
           Format.pp_print_newline fmt ();
587
           (* Rule for single predicate *)
588
           let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in
589
           Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@."
590
                          str_flags
591
                          (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m)
592
	                  pp_machine_stateless_name m.mname.node_id
593
	                  (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m);
594
         end
595
      else
596
         begin
597
           (* Declaring predicate *)
598
           Format.fprintf fmt "(declare-rel %a (%a))@."
599
    	                  pp_machine_reset_name m.mname.node_id
600
    	                  (Utils.fprintf_list ~sep:" " pp_type)
601
    	                  (List.map (fun v -> v.var_type) (inout_vars machines m));
602

    
603
           Format.fprintf fmt "(declare-rel %a (%a))@."
604
    	                  pp_machine_step_name m.mname.node_id
605
    	                  (Utils.fprintf_list ~sep:" " pp_type)
606
    	                  (List.map (fun v -> v.var_type) (step_vars machines m));
607

    
608
           Format.pp_print_newline fmt ();
609
          (* Adding assertions *)
610
           match m.mstep.step_asserts with
611
	  | [] ->
612
	    begin
613

    
614
	      (* Rule for step*)
615
	      fprintf fmt "@[<v 2>(rule (=> @ ";
616
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
617
	      fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
618
		pp_machine_step_name m.mname.node_id
619
		(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
620
	    end
621
	  | assertsl ->
622
	    begin
623
	      let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
624
	      (* print_string pp_val; *)
625
	      fprintf fmt "; with Assertions @.";
626

    
627
	      (*Rule for step*)
628
	      fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
629
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
630
	      fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
631
		pp_machine_step_name m.mname.node_id
632
		(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
633
	    end
634

    
635
         end
636

    
637
        end
638

    
639

    
640
(**************** XML printing functions *************)
641

    
642
	  let rec pp_xml_expr fmt expr =
643
  (match expr.expr_annot with 
644
  | None -> fprintf fmt "%t" 
645
  | Some ann -> fprintf fmt "@[(%a %t)@]" pp_xml_expr_annot ann)
646
    (fun fmt -> 
647
      match expr.expr_desc with
648
    | Expr_const c -> Printers.pp_const fmt c
649
    | Expr_ident id -> fprintf fmt "%s" id
650
    | Expr_array a -> fprintf fmt "[%a]" pp_xml_tuple a
651
    | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_xml_expr a Dimension.pp_dimension d
652
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_xml_expr a Dimension.pp_dimension d
653
    | Expr_tuple el -> fprintf fmt "(%a)" pp_xml_tuple el
654
    | 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
655
    | Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_xml_expr e1 pp_xml_expr e2
656
    | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_xml_expr e1 pp_xml_expr e2
657
    | Expr_pre e -> fprintf fmt "pre %a" pp_xml_expr e
658
    | Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_xml_expr e l id
659
    | Expr_merge (id, hl) -> 
660
      fprintf fmt "merge %s %a" id pp_xml_handlers hl
661
    | Expr_appl (id, e, r) -> pp_xml_app fmt id e r
662
    )
663
and pp_xml_tuple fmt el =
664
 Utils.fprintf_list ~sep:"," pp_xml_expr fmt el
665

    
666
and pp_xml_handler fmt (t, h) =
667
 fprintf fmt "(%s -> %a)" t pp_xml_expr h
668

    
669
and pp_xml_handlers fmt hl =
670
 Utils.fprintf_list ~sep:" " pp_xml_handler fmt hl
671

    
672
and pp_xml_app fmt id e r =
673
  match r with
674
  | None -> pp_xml_call fmt id e
675
  | Some c -> fprintf fmt "%t every (%a)" (fun fmt -> pp_xml_call fmt id e) pp_xml_expr c 
676

    
677
and pp_xml_call fmt id e =
678
  match id, e.expr_desc with
679
  | "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_xml_expr e1 pp_xml_expr e2
680
  | "uminus", _ -> fprintf fmt "(- %a)" pp_xml_expr e
681
  | "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_xml_expr e1 pp_xml_expr e2
682
  | "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_xml_expr e1 pp_xml_expr e2
683
  | "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_xml_expr e1 pp_xml_expr e2
684
  | "mod", Expr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_xml_expr e1 pp_xml_expr e2
685
  | "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a and %a)" pp_xml_expr e1 pp_xml_expr e2
686
  | "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a or %a)" pp_xml_expr e1 pp_xml_expr e2
687
  | "xor", Expr_tuple([e1;e2]) -> fprintf fmt "(%a xor %a)" pp_xml_expr e1 pp_xml_expr e2
688
  | "impl", Expr_tuple([e1;e2]) -> fprintf fmt "(%a => %a)" pp_xml_expr e1 pp_xml_expr e2
689
  | "<", Expr_tuple([e1;e2]) -> fprintf fmt "(%a &lt; %a)" pp_xml_expr e1 pp_xml_expr e2
690
  | "<=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a &lt;= %a)" pp_xml_expr e1 pp_xml_expr e2
691
  | ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a &gt; %a)" pp_xml_expr e1 pp_xml_expr e2
692
  | ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a &gt;= %a)" pp_xml_expr e1 pp_xml_expr e2
693
  | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_xml_expr e1 pp_xml_expr e2
694
  | "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_xml_expr e1 pp_xml_expr e2
695
  | "not", _ -> fprintf fmt "(not %a)" pp_xml_expr e
696
  | _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_xml_expr e
697
  | _ -> fprintf fmt "%s (%a)" id pp_xml_expr e
698

    
699
and pp_xml_eexpr fmt e =
700
  fprintf fmt "%a%t %a"
701
    (Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers) e.eexpr_quantifiers
702
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
703
    pp_xml_expr e.eexpr_qfexpr
704

    
705
and  pp_xml_sf_value fmt e =
706
   fprintf fmt "%a"
707
     (* (Utils.fprintf_list ~sep:"; " pp_xml_quantifiers) e.eexpr_quantifiers *)
708
     (* (fun fmt -> match e.eexpr_quantifiers *)
709
     (*             with [] -> () *)
710
     (*                | _ -> fprintf fmt ";") *)
711
     pp_xml_expr e.eexpr_qfexpr
712

    
713
and pp_xml_s_function fmt expr_ann =
714
  let pp_xml_annot fmt (kwds, ee) =
715
    Format.fprintf fmt " %t : %a"
716
                   (fun fmt -> match kwds with
717
                               | [] -> assert false
718
                               | [x] -> Format.pp_print_string fmt x
719
                               | _ -> Format.fprintf fmt "%a" (Utils.fprintf_list ~sep:"/" Format.pp_print_string) kwds)
720
                   pp_xml_sf_value ee
721
  in
722
  Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
723

    
724
and pp_xml_expr_annot fmt expr_ann =
725
  let pp_xml_annot fmt (kwds, ee) =
726
    Format.fprintf fmt "(*! %t: %a; *)"
727
      (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)
728
      pp_xml_eexpr ee
729
  in
730
  Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
731

    
732

    
733
(* Local Variables: *)
734
(* compile-command:"make -C ../../.." *)
735
(* End: *)