Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (26.6 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
(* Default value for each type, used when building arrays. Eg integer array
50
   [2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
51
   for the type integer (arrays).
52
*)
53
let rec pp_default_val fmt t =
54
  let t = Types.dynamic_type t in
55
  if Types.is_bool_type t  then fprintf fmt "true" else
56
  if Types.is_int_type t then fprintf fmt "0" else 
57
  if Types.is_real_type t then fprintf fmt "0" else 
58
  match (Types.dynamic_type t).Types.tdesc with
59
  | Types.Tarray(dim, l) -> (* TODO PL: this strange code has to be (heavily) checked *)
60
     let valt = Types.array_element_type t in
61
     fprintf fmt "((as const (Array Int %a)) %a)"
62
       pp_type valt 
63
       pp_default_val valt
64
  | Types.Tstruct(l) -> assert false
65
  | Types.Ttuple(l) -> assert false
66
  |_ -> assert false
67

    
68
let pp_mod pp_val v1 v2 fmt =
69
  if Types.is_int_type v1.value_type &&  not !Options.integer_div_euclidean then
70
    (* C semantics: converting it from Euclidean operators
71
       (a mod_M b) - ((a mod_M b > 0 && a < 0) ? abs(b) : 0)            
72
    *)
73
    Format.fprintf fmt "(- (mod %a %a) (ite (and (> (mod %a %a) 0) (< %a 0)) (abs %a) 0))"
74
      pp_val v1 pp_val v2
75
      pp_val v1 pp_val v2
76
      pp_val v1
77
      pp_val v2
78
  else
79
    Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
80

    
81
let pp_div pp_val v1 v2 fmt =
82
  if Types.is_int_type v1.value_type &&  not !Options.integer_div_euclidean then
83
    (* C semantics: converting it from Euclidean operators
84
       (a - (a mod_C b)) div_M b
85
    *)
86
    Format.fprintf fmt "(div (- %a %t) %a)"
87
      pp_val v1
88
      (pp_mod pp_val v1 v2)
89
      pp_val v2
90
  else
91
    Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
92

    
93

    
94
let pp_basic_lib_fun i pp_val fmt vl =
95
  match i, vl with
96
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3
97
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
98
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
99
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
100
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
101
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
102
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
103
  | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
104
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
105
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
106
  | "mod", [v1; v2] -> pp_mod pp_val v1 v2 fmt
107
  | "/", [v1; v2] -> pp_div pp_val v1 v2 fmt
108
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
109
  | _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)
110
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
111

    
112
*)
113

    
114

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

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

    
154
  (* Code specific for arrays *)
155
    
156
  | Power (v, n)  -> assert false
157
  | Var v    ->
158
     if is_memory m v then
159
       if Types.is_array_type v.var_type
160
       then assert false
161
       else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
162
     else
163
       pp_var fmt (rename_machine self v)
164
    
165
  | Fun (n, vl)   -> fprintf fmt "%a" (pp_basic_lib_fun n (pp_horn_val m self pp_var)) vl
166

    
167
(* Prints a [value] indexed by the suffix list [loop_vars] *)
168
let rec pp_value_suffix m self pp_value fmt value =
169
 match value.value_desc with
170
 | Fun (n, vl)  ->
171
    pp_basic_lib_fun n (pp_value_suffix m self pp_value) fmt vl
172
 |  _            ->
173
   pp_horn_val m self pp_value fmt value
174

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

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

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

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

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

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

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

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

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

    
366
  | [] -> fprintf fmt "true"; reset_instances
367

    
368
let pp_machine_reset machines fmt m =
369
  let locals = local_memory_vars machines m in
370
  fprintf fmt "@[<v 5>(and @ ";
371

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

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

    
397
  fprintf fmt "@]@ )"
398

    
399

    
400

    
401
(**************************************************************)
402

    
403
let is_stateless m = m.minstances = [] && m.mmemory = []
404

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

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

    
438
          match m.mstep.step_asserts with
439
	  | [] ->
440
	     begin
441

    
442
	       (* Rule for single predicate *)
443
	       fprintf fmt "; Stateless step rule @.";
444
	       fprintf fmt "@[<v 2>(rule (=> @ ";
445
	       ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);
446
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
447
		 pp_machine_stateless_name m.mname.node_id
448
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m);
449
	     end
450
	  | assertsl ->
451
	     begin
452
	       let pp_val = pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m) in
453
	       
454
	       fprintf fmt "; Stateless step rule with Assertions @.";
455
	       (*Rule for step*)
456
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
457
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
458
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
459
		 pp_machine_stateless_name m.mname.node_id
460
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
461
	  
462
	     end
463
	       
464
	end
465
      else
466
	begin
467
	  (* Declaring predicate *)
468
	  fprintf fmt "(declare-rel %a (%a))@."
469
	    pp_machine_reset_name m.mname.node_id
470
	    (Utils.fprintf_list ~sep:" " pp_type)
471
	    (List.map (fun v -> v.var_type) (reset_vars machines m));
472

    
473
	  fprintf fmt "(declare-rel %a (%a))@."
474
	    pp_machine_step_name m.mname.node_id
475
	    (Utils.fprintf_list ~sep:" " pp_type)
476
	    (List.map (fun v -> v.var_type) (step_vars machines m));
477

    
478
	  pp_print_newline fmt ();
479

    
480
	  (* Rule for reset *)
481
	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
482
	    (pp_machine_reset machines) m 
483
	    pp_machine_reset_name m.mname.node_id
484
	    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);
485

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

    
515

    
516
let mk_flags arity =
517
  let b_range =
518
   let rec range i j =
519
     if i > arity then [] else i :: (range (i+1) j) in
520
   range 2 arity;
521
 in
522
 List.fold_left (fun acc x -> acc ^ " false") "true" b_range
523

    
524

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

    
533
  in
534
  Log.report ~level:1 (fun fmt -> fprintf fmt "... sf_name: %s@, .. flags: %s@ .. arity: %s@," sf_name flags arity);
535
  sf_name, flags, arity
536

    
537

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

    
549
          (* Check if there is annotation for s-function *)
550
          if m.mannot != [] then(
551
              Format.fprintf fmt "; @[%a@]@]@\n" (Utils.fprintf_list ~sep:"@ " Printers.pp_s_function) m.mannot;
552
            );
553

    
554
       (* Printing variables *)
555
          Utils.fprintf_list ~sep:"@." pp_decl_var fmt
556
                             ((step_vars machines m)@
557
    	                        (rename_machine_list m.mname.node_id m.mstep.step_locals));
558
          Format.pp_print_newline fmt ();
559
          let sf_name, flags, arity = get_sf_info() in
560

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

    
585
           Format.fprintf fmt "(declare-rel %a (%a))@."
586
    	                  pp_machine_step_name m.mname.node_id
587
    	                  (Utils.fprintf_list ~sep:" " pp_type)
588
    	                  (List.map (fun v -> v.var_type) (step_vars machines m));
589

    
590
           Format.pp_print_newline fmt ();
591
          (* Adding assertions *)
592
           match m.mstep.step_asserts with
593
	  | [] ->
594
	    begin
595

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

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

    
617
         end
618

    
619
        end
620

    
621

    
622
(**************** XML printing functions *************)
623

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

    
648
and pp_xml_handler fmt (t, h) =
649
 fprintf fmt "(%s -> %a)" t pp_xml_expr h
650

    
651
and pp_xml_handlers fmt hl =
652
 Utils.fprintf_list ~sep:" " pp_xml_handler fmt hl
653

    
654
and pp_xml_app fmt id e r =
655
  match r with
656
  | None -> pp_xml_call fmt id e
657
  | Some c -> fprintf fmt "%t every (%a)" (fun fmt -> pp_xml_call fmt id e) pp_xml_expr c 
658

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

    
681
and pp_xml_eexpr fmt e =
682
  fprintf fmt "%a%t %a"
683
    (Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers) e.eexpr_quantifiers
684
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
685
    pp_xml_expr e.eexpr_qfexpr
686

    
687
and  pp_xml_sf_value fmt e =
688
   fprintf fmt "%a"
689
     (* (Utils.fprintf_list ~sep:"; " pp_xml_quantifiers) e.eexpr_quantifiers *)
690
     (* (fun fmt -> match e.eexpr_quantifiers *)
691
     (*             with [] -> () *)
692
     (*                | _ -> fprintf fmt ";") *)
693
     pp_xml_expr e.eexpr_qfexpr
694

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

    
706
and pp_xml_expr_annot fmt expr_ann =
707
  let pp_xml_annot fmt (kwds, ee) =
708
    Format.fprintf fmt "(*! %t: %a; *)"
709
      (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)
710
      pp_xml_eexpr ee
711
  in
712
  Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
713

    
714

    
715
(* Local Variables: *)
716
(* compile-command:"make -C ../../.." *)
717
(* End: *)