Project

General

Profile

Download (26.6 KB) Statistics
| Branch: | Tag: | Revision:
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

    
12
(* The compilation presented here was first defined in Garoche, Gurfinkel,
13
   Kahsai, HCSV'14.
14

    
15
   This is a modified version that handle reset *)
16

    
17
open Format
18
open Lustre_types
19
open Machine_code_types
20
open Corelang
21
open Machine_code_common
22
open Horn_backend_common
23

    
24
(********************************************************************************************)
25
(* Instruction Printing functions *)
26
(********************************************************************************************)
27

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

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

    
38
(* Prints a constant value *)
39
let pp_horn_const fmt c =
40
  match c with
41
  | Const_int i ->
42
    pp_print_int fmt i
43
  | Const_real r ->
44
    Real.pp fmt r
45
  | Const_tag t ->
46
    pp_horn_tag fmt t
47
  | _ ->
48
    assert false
49

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

    
72
let pp_mod pp_val v1 v2 fmt =
73
  if Types.is_int_type v1.value_type && not !Options.integer_div_euclidean then
74
    (* C semantics: converting it from Euclidean operators (a mod_M b) - ((a
75
       mod_M b > 0 && a < 0) ? abs(b) : 0) *)
76
    Format.fprintf fmt
77
      "(- (mod %a %a) (ite (and (> (mod %a %a) 0) (< %a 0)) (abs %a) 0))" pp_val
78
      v1 pp_val v2 pp_val v1 pp_val v2 pp_val v1 pp_val v2
79
  else 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 (a - (a mod_C b))
84
       div_M b *)
85
    Format.fprintf fmt "(div (- %a %t) %a)" pp_val v1 (pp_mod pp_val v1 v2)
86
      pp_val v2
87
  else Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
88

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

    
123
(* Prints a value expression [v], with internal function calls only. [pp_var] is
124
   a printer for variables (typically [pp_c_var_read]), but an offset suffix may
125
   be added for array variables *)
126
let rec pp_horn_val ?(is_lhs = false) m self pp_var fmt v =
127
  match v.value_desc with
128
  | Cst c ->
129
    pp_horn_const fmt c
130
  (* Code specific for arrays *)
131
  | Array il ->
132
    (* An array definition: (store ( ... (store ( store ( default_val ) idx_n
133
       val_n ) idx_n-1 val_n-1) ... idx_1 val_1 ) *)
134
    let rec print fmt (tab, x) =
135
      match tab with
136
      | [] ->
137
        pp_default_val fmt v.value_type (* (get_type v) *)
138
      | h :: t ->
139
        fprintf fmt "(store %a %i %a)" print
140
          (t, x + 1)
141
          x
142
          (pp_horn_val ~is_lhs m self pp_var)
143
          h
144
    in
145
    print fmt (il, 0)
146
  | Access (tab, index) ->
147
    fprintf fmt "(select %a %a)"
148
      (pp_horn_val ~is_lhs m self pp_var)
149
      tab
150
      (pp_horn_val ~is_lhs m self pp_var)
151
      index
152
  (* Code specific for arrays *)
153
  | Power _ ->
154
    assert false
155
  | Var v ->
156
    if is_memory m v then
157
      if Types.is_array_type v.var_type then assert false
158
      else
159
        pp_var fmt
160
          (rename_machine self
161
             ((if is_lhs then rename_next else rename_current (* self *)) v))
162
    else pp_var fmt (rename_machine self v)
163
  | Fun (n, vl) ->
164
    fprintf fmt "%a" (pp_basic_lib_fun n (pp_horn_val m self pp_var)) vl
165
  | ResetFlag ->
166
    (* TODO: handle reset flag *)
167
    assert false
168

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

    
177
(* type_directed assignment: array vs. statically sized type - [var_type]: type
178
   of variable to be assigned - [var_name]: name of variable to be assigned -
179
   [value]: assigned value - [pp_var]: printer for variables *)
180
let pp_assign m pp_var fmt var_name value =
181
  let self = m.mname.node_id in
182
  fprintf fmt "(= %a %a)"
183
    (pp_horn_val ~is_lhs:true m self pp_var)
184
    var_name
185
    (pp_value_suffix m self pp_var)
186
    value
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 =
192
    List.find (fun m -> m.mname.node_id = node_name n) machines
193
  in
194

    
195
  let m_list =
196
    rename_machine_list (concat m.mname.node_id i)
197
      (rename_mid_list (full_memory_vars machines target_machine))
198
  in
199
  let c_list =
200
    rename_machine_list (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)" (pp_horn_var m) mhd (pp_horn_var m) chd
206
  | _ ->
207
    fprintf fmt "@[<v 0>(and @[<v 0>";
208
    List.iter2
209
      (fun mhd chd ->
210
        fprintf fmt "(= %a %a)@ " (pp_horn_var m) mhd (pp_horn_var m) chd)
211
      m_list c_list;
212
    fprintf fmt ")@]@ @]"
213

    
214
let pp_instance_reset machines m fmt i =
215
  let n, _ = List.assoc i m.minstances in
216
  let target_machine =
217
    List.find (fun m -> m.mname.node_id = node_name n) machines
218
  in
219

    
220
  fprintf fmt "(%a @[<v 0>%a)@]" pp_machine_reset_name (node_name n)
221
    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
222
    (rename_machine_list (concat m.mname.node_id i)
223
       (rename_current_list (full_memory_vars machines target_machine))
224
    @ rename_machine_list (concat m.mname.node_id i)
225
        (rename_mid_list (full_memory_vars machines target_machine)))
226

    
227
let pp_instance_call machines reset_instances m fmt i inputs outputs =
228
  let self = m.mname.node_id in
229
  try
230
    (* stateful node instance *)
231
    let n, _ = List.assoc i m.minstances in
232
    let target_machine =
233
      List.find (fun m -> m.mname.node_id = node_name n) machines
234
    in
235
    (* Checking whether this specific instances has been reset yet *)
236
    if not (List.mem i reset_instances) then
237
      (* If not, declare mem_m = mem_c *)
238
      pp_no_reset machines m fmt i;
239

    
240
    let mems = full_memory_vars machines target_machine in
241
    let rename_mems f =
242
      rename_machine_list (concat m.mname.node_id i) (f mems)
243
    in
244
    let mid_mems = rename_mems rename_mid_list in
245
    let next_mems = rename_mems rename_next_list in
246

    
247
    match node_name n, inputs, outputs, mid_mems, next_mems with
248
    | "_arrow", [ i1; i2 ], [ o ], [ mem_m ], [ mem_x ] ->
249
      fprintf fmt "@[<v 5>(and ";
250
      fprintf fmt "(= %a (ite %a %a %a))"
251
        (pp_horn_val ~is_lhs:true m self (pp_horn_var m))
252
        (mk_val (Var o) o.var_type)
253
        (* output var *)
254
        (pp_horn_var m)
255
        mem_m
256
        (pp_horn_val m self (pp_horn_var m))
257
        i1
258
        (pp_horn_val m self (pp_horn_var m))
259
        i2;
260
      fprintf fmt "@ ";
261
      fprintf fmt "(= %a false)" (pp_horn_var m) mem_x;
262
      fprintf fmt ")@]"
263
    | _ ->
264
      fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]" pp_machine_step_name (node_name n)
265
        (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
266
        inputs
267
        (Utils.pp_final_char_if_non_empty "@ " inputs)
268
        (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
269
        (List.map (fun v -> mk_val (Var v) v.var_type) outputs)
270
        (Utils.pp_final_char_if_non_empty "@ " outputs)
271
        (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
272
        (mid_mems @ next_mems)
273
  with Not_found ->
274
    (* stateless node instance *)
275
    let n, _ = List.assoc i m.mcalls in
276
    fprintf fmt "(%a @[<v 0>%a%t%a)@]" pp_machine_stateless_name (node_name n)
277
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
278
      inputs
279
      (Utils.pp_final_char_if_non_empty "@ " inputs)
280
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
281
      (List.map (fun v -> mk_val (Var v) v.var_type) outputs)
282

    
283
(* Print the instruction and update the set of reset instances *)
284
let rec pp_machine_instr machines reset_instances (m : machine_t) fmt instr :
285
    ident list =
286
  match get_instr_desc instr with
287
  | MSpec _ | MComment _ ->
288
    reset_instances
289
  (* TODO: handle reset flag *)
290
  | MResetAssign _ ->
291
    reset_instances
292
  (* TODO: handle clear_reset *)
293
  | MClearReset ->
294
    reset_instances
295
  | MNoReset i ->
296
    (* we assign middle_mem with mem_m. And declare i as reset *)
297
    pp_no_reset machines m fmt i;
298
    i :: reset_instances
299
  | MSetReset i ->
300
    (* we assign middle_mem with reset: reset(mem_m) *)
301
    pp_instance_reset machines m fmt i;
302
    i :: reset_instances
303
  | MLocalAssign (i, v) ->
304
    pp_assign m (pp_horn_var m) fmt (mk_val (Var i) i.var_type) v;
305
    reset_instances
306
  | MStateAssign (i, v) ->
307
    pp_assign m (pp_horn_var m) fmt (mk_val (Var i) i.var_type) v;
308
    reset_instances
309
  | MStep ([ _ ], i, vl)
310
    when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl)
311
    ->
312
    assert false (* This should not happen anymore *)
313
  | MStep (il, i, vl) ->
314
    (* if reset instance, just print the call over mem_m , otherwise declare
315
       mem_m = mem_c and print the call to mem_m *)
316
    pp_instance_call machines reset_instances m fmt i vl il;
317
    reset_instances
318
  (* Since this instance call will only happen once, we don't have to update
319
     reset_instances *)
320
  | MBranch (g, hl) ->
321
    (* (g = tag1 => expr1) and (g = tag2 => expr2) ... should not be produced
322
       yet. Later, we will have to compare the reset_instances of each branch
323
       and introduced the mem_m = mem_c for branches to do not address it while
324
       other did. Am I clear ? *)
325
    (* For each branch we obtain the logical encoding, and the information
326
       whether a sub node has been reset or not. If a node has been reset in one
327
       of the branch, then all others have to have the mem_m = mem_c statement. *)
328
    let self = m.mname.node_id in
329
    let pp_branch fmt (tag, instrs) =
330
      fprintf fmt "@[<v 3>(or (not (= %a %a))@ "
331
        (*"@[<v 3>(=> (= %a %s)@ "*)
332
        (* Issues with some versions of Z3. It seems that => within Horn
333
           predicate may cause trouble. I have hard time producing a MWE, so
334
           I'll just keep the fix here as (not a) or b *)
335
        (pp_horn_val m self (pp_horn_var m))
336
        g pp_horn_tag tag;
337
      let _ (* rs *) =
338
        pp_machine_instrs machines reset_instances m fmt instrs
339
      in
340
      fprintf fmt "@])";
341
      ()
342
      (* rs *)
343
    in
344
    pp_conj pp_branch fmt hl;
345
    reset_instances
346

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

    
368
let pp_machine_reset machines fmt m =
369
  let locals = local_memory_vars 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)" (pp_horn_var m) (rename_mid v) (pp_horn_var m)
375
         (rename_current v)))
376
    fmt locals;
377
  fprintf fmt "@ ";
378

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

    
394
  fprintf fmt "@]@ )"
395

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

    
398
(* Print the machine m: two functions: m_init and m_step - m_init is a predicate
399
   over m memories - m_step is a predicate over old_memories, inputs,
400
   new_memories, outputs We first declare all variables then the two /rules/. *)
401
let print_machine machines fmt m =
402
  if m.mname.node_id = Arrow.arrow_id then (* We don't print arrow function *)
403
    ()
404
  else (
405
    fprintf fmt "; %s@." m.mname.node_id;
406

    
407
    (* Printing variables *)
408
    Utils.fprintf_list ~sep:"@." pp_decl_var fmt
409
      (inout_vars m
410
      @ rename_current_list (full_memory_vars machines m)
411
      @ rename_mid_list (full_memory_vars machines m)
412
      @ rename_next_list (full_memory_vars machines m)
413
      @ rename_machine_list m.mname.node_id m.mstep.step_locals);
414
    pp_print_newline fmt ();
415

    
416
    if is_stateless m then (
417
      (* Declaring single predicate *)
418
      fprintf fmt "(declare-rel %a (%a))@." pp_machine_stateless_name
419
        m.mname.node_id
420
        (Utils.fprintf_list ~sep:" " pp_type)
421
        (List.map (fun v -> v.var_type) (inout_vars m));
422

    
423
      match m.mstep.step_asserts with
424
      | [] ->
425
        (* Rule for single predicate *)
426
        fprintf fmt "; Stateless step rule @.";
427
        fprintf fmt "@[<v 2>(rule (=> @ ";
428
        ignore
429
          (pp_machine_instrs machines []
430
             (* No reset info for stateless nodes *) m fmt m.mstep.step_instrs);
431
        fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_stateless_name
432
          m.mname.node_id
433
          (Utils.fprintf_list ~sep:" " (pp_horn_var m))
434
          (inout_vars m)
435
      | assertsl ->
436
        let pp_val =
437
          pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m)
438
        in
439

    
440
        fprintf fmt "; Stateless step rule with Assertions @.";
441
        (*Rule for step*)
442
        fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
443
        ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
444
        fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val)
445
          assertsl pp_machine_stateless_name m.mname.node_id
446
          (Utils.fprintf_list ~sep:" " (pp_horn_var m))
447
          (step_vars machines m))
448
    else (
449
      (* Declaring predicate *)
450
      fprintf fmt "(declare-rel %a (%a))@." pp_machine_reset_name
451
        m.mname.node_id
452
        (Utils.fprintf_list ~sep:" " pp_type)
453
        (List.map (fun v -> v.var_type) (reset_vars machines m));
454

    
455
      fprintf fmt "(declare-rel %a (%a))@." pp_machine_step_name m.mname.node_id
456
        (Utils.fprintf_list ~sep:" " pp_type)
457
        (List.map (fun v -> v.var_type) (step_vars machines m));
458

    
459
      pp_print_newline fmt ();
460

    
461
      (* Rule for reset *)
462
      fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
463
        (pp_machine_reset machines)
464
        m pp_machine_reset_name m.mname.node_id
465
        (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
466
        (reset_vars machines m);
467

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

    
485
        (*Rule for step*)
486
        fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
487
        ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
488
        fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val)
489
          assertsl pp_machine_step_name m.mname.node_id
490
          (Utils.fprintf_list ~sep:" " (pp_horn_var m))
491
          (step_vars machines m)))
492

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

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

    
513
  Log.report ~level:1 (fun fmt ->
514
      fprintf fmt "... sf_name: %s@, .. flags: %s@ .. arity: %s@," sf_name flags
515
        arity);
516
  sf_name, flags, arity
517

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

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

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

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

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

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

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

    
593
(**************** XML printing functions *************)
594

    
595
let rec pp_xml_expr fmt expr =
596
  (match expr.expr_annot with
597
  | None ->
598
    fprintf fmt "%t"
599
  | Some ann ->
600
    fprintf fmt "@[(%a %t)@]" pp_xml_expr_annot ann) (fun fmt ->
601
      match expr.expr_desc with
602
      | Expr_const c ->
603
        Printers.pp_const fmt c
604
      | Expr_ident id ->
605
        fprintf fmt "%s" id
606
      | Expr_array a ->
607
        fprintf fmt "[%a]" pp_xml_tuple a
608
      | Expr_access (a, d) ->
609
        fprintf fmt "%a[%a]" pp_xml_expr a Dimension.pp_dimension d
610
      | Expr_power (a, d) ->
611
        fprintf fmt "(%a^%a)" pp_xml_expr a Dimension.pp_dimension d
612
      | Expr_tuple el ->
613
        fprintf fmt "(%a)" pp_xml_tuple el
614
      | Expr_ite (c, t, e) ->
615
        fprintf fmt
616
          "@[<hov 1>(if %a then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@])"
617
          pp_xml_expr c pp_xml_expr t pp_xml_expr e
618
      | Expr_arrow (e1, e2) ->
619
        fprintf fmt "(%a -> %a)" pp_xml_expr e1 pp_xml_expr e2
620
      | Expr_fby (e1, e2) ->
621
        fprintf fmt "%a fby %a" pp_xml_expr e1 pp_xml_expr e2
622
      | Expr_pre e ->
623
        fprintf fmt "pre %a" pp_xml_expr e
624
      | Expr_when (e, id, l) ->
625
        fprintf fmt "%a when %s(%s)" pp_xml_expr e l id
626
      | Expr_merge (id, hl) ->
627
        fprintf fmt "merge %s %a" id pp_xml_handlers hl
628
      | Expr_appl (id, e, r) ->
629
        pp_xml_app fmt id e r)
630

    
631
and pp_xml_tuple fmt el = Utils.fprintf_list ~sep:"," pp_xml_expr fmt el
632

    
633
and pp_xml_handler fmt (t, h) = fprintf fmt "(%s -> %a)" t pp_xml_expr h
634

    
635
and pp_xml_handlers fmt hl = Utils.fprintf_list ~sep:" " pp_xml_handler fmt hl
636

    
637
and pp_xml_app fmt id e r =
638
  match r with
639
  | None ->
640
    pp_xml_call fmt id e
641
  | Some c ->
642
    fprintf fmt "%t every (%a)" (fun fmt -> pp_xml_call fmt id e) pp_xml_expr c
643

    
644
and pp_xml_call fmt id e =
645
  match id, e.expr_desc with
646
  | "+", Expr_tuple [ e1; e2 ] ->
647
    fprintf fmt "(%a + %a)" pp_xml_expr e1 pp_xml_expr e2
648
  | "uminus", _ ->
649
    fprintf fmt "(- %a)" pp_xml_expr e
650
  | "-", Expr_tuple [ e1; e2 ] ->
651
    fprintf fmt "(%a - %a)" pp_xml_expr e1 pp_xml_expr e2
652
  | "*", Expr_tuple [ e1; e2 ] ->
653
    fprintf fmt "(%a * %a)" pp_xml_expr e1 pp_xml_expr e2
654
  | "/", Expr_tuple [ e1; e2 ] ->
655
    fprintf fmt "(%a / %a)" pp_xml_expr e1 pp_xml_expr e2
656
  | "mod", Expr_tuple [ e1; e2 ] ->
657
    fprintf fmt "(%a mod %a)" pp_xml_expr e1 pp_xml_expr e2
658
  | "&&", Expr_tuple [ e1; e2 ] ->
659
    fprintf fmt "(%a and %a)" pp_xml_expr e1 pp_xml_expr e2
660
  | "||", Expr_tuple [ e1; e2 ] ->
661
    fprintf fmt "(%a or %a)" pp_xml_expr e1 pp_xml_expr e2
662
  | "xor", Expr_tuple [ e1; e2 ] ->
663
    fprintf fmt "(%a xor %a)" pp_xml_expr e1 pp_xml_expr e2
664
  | "impl", Expr_tuple [ e1; e2 ] ->
665
    fprintf fmt "(%a => %a)" pp_xml_expr e1 pp_xml_expr e2
666
  | "<", Expr_tuple [ e1; e2 ] ->
667
    fprintf fmt "(%a &lt; %a)" pp_xml_expr e1 pp_xml_expr e2
668
  | "<=", Expr_tuple [ e1; e2 ] ->
669
    fprintf fmt "(%a &lt;= %a)" pp_xml_expr e1 pp_xml_expr e2
670
  | ">", Expr_tuple [ e1; e2 ] ->
671
    fprintf fmt "(%a &gt; %a)" pp_xml_expr e1 pp_xml_expr e2
672
  | ">=", Expr_tuple [ e1; e2 ] ->
673
    fprintf fmt "(%a &gt;= %a)" pp_xml_expr e1 pp_xml_expr e2
674
  | "!=", Expr_tuple [ e1; e2 ] ->
675
    fprintf fmt "(%a != %a)" pp_xml_expr e1 pp_xml_expr e2
676
  | "=", Expr_tuple [ e1; e2 ] ->
677
    fprintf fmt "(%a = %a)" pp_xml_expr e1 pp_xml_expr e2
678
  | "not", _ ->
679
    fprintf fmt "(not %a)" pp_xml_expr e
680
  | _, Expr_tuple _ ->
681
    fprintf fmt "%s %a" id pp_xml_expr e
682
  | _ ->
683
    fprintf fmt "%s (%a)" id pp_xml_expr e
684

    
685
and pp_xml_eexpr fmt e =
686
  fprintf fmt "%a%t %a"
687
    (Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers)
688
    e.eexpr_quantifiers
689
    (fun fmt ->
690
      match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
691
    pp_xml_expr e.eexpr_qfexpr
692

    
693
and pp_xml_sf_value fmt e =
694
  fprintf fmt "%a"
695
    (* (Utils.fprintf_list ~sep:"; " pp_xml_quantifiers) e.eexpr_quantifiers *)
696
    (* (fun fmt -> match e.eexpr_quantifiers *)
697
    (*             with [] -> () *)
698
    (*                | _ -> fprintf fmt ";") *)
699
    pp_xml_expr e.eexpr_qfexpr
700

    
701
and pp_xml_s_function fmt expr_ann =
702
  let pp_xml_annot fmt (kwds, ee) =
703
    Format.fprintf fmt " %t : %a"
704
      (fun fmt ->
705
        match kwds with
706
        | [] ->
707
          assert false
708
        | [ x ] ->
709
          Format.pp_print_string fmt x
710
        | _ ->
711
          Format.fprintf fmt "%a"
712
            (Utils.fprintf_list ~sep:"/" Format.pp_print_string)
713
            kwds)
714
      pp_xml_sf_value ee
715
  in
716
  Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
717

    
718
and pp_xml_expr_annot fmt expr_ann =
719
  let pp_xml_annot fmt (kwds, ee) =
720
    Format.fprintf fmt "(*! %t: %a; *)"
721
      (fun fmt ->
722
        match kwds with
723
        | [] ->
724
          assert false
725
        | [ x ] ->
726
          Format.pp_print_string fmt x
727
        | _ ->
728
          Format.fprintf fmt "/%a/"
729
            (Utils.fprintf_list ~sep:"/" Format.pp_print_string)
730
            kwds)
731
      pp_xml_eexpr ee
732
  in
733
  Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
734

    
735
(* Local Variables: *)
736
(* compile-command:"make -C ../../.." *)
737
(* End: *)
(4-4/5)