Project

General

Profile

Download (26.2 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 Utils
18
open Format
19
open Lustre_types
20
open Machine_code_types
21
open Corelang
22
open Machine_code_common
23
open Horn_backend_common
24

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

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

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

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

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

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

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

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

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

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

    
178
(* type_directed assignment: array vs. statically sized type - [var_type]: type
179
   of variable to be assigned - [var_name]: name of variable to be assigned -
180
   [value]: assigned value - [pp_var]: printer for variables *)
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)
185
    var_name
186
    (pp_value_suffix m self pp_var)
187
    value
188

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

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

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

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

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

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

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

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

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

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

    
370
  (* print "x_m = x_c" for each local memory *)
371
  (pp_print_list (fun fmt v ->
372
       fprintf fmt "(= %a %a)" (pp_horn_var m) (rename_mid v) (pp_horn_var m)
373
         (rename_current v)))
374
    fmt locals;
375
  fprintf fmt "@ ";
376

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

    
392
  fprintf fmt "@]@ )"
393

    
394
(**************************************************************)
395

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

    
405
    (* Printing variables *)
406
    pp_print_list ~pp_open_box:pp_open_vbox0 pp_decl_var fmt
407
      (inout_vars m
408
      @ rename_current_list (full_memory_vars machines m)
409
      @ rename_mid_list (full_memory_vars machines m)
410
      @ rename_next_list (full_memory_vars machines m)
411
      @ rename_machine_list m.mname.node_id m.mstep.step_locals);
412
    pp_print_newline fmt ();
413

    
414
    if is_stateless m then (
415
      (* Declaring single predicate *)
416
      fprintf fmt "(declare-rel %a (%a))@." pp_machine_stateless_name
417
        m.mname.node_id
418
        (pp_print_list pp_type)
419
        (List.map (fun v -> v.var_type) (inout_vars m));
420

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

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

    
453
      fprintf fmt "(declare-rel %a (%a))@." pp_machine_step_name m.mname.node_id
454
        (pp_print_list pp_type)
455
        (List.map (fun v -> v.var_type) (step_vars machines m));
456

    
457
      pp_print_newline fmt ();
458

    
459
      (* Rule for reset *)
460
      fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
461
        (pp_machine_reset machines)
462
        m pp_machine_reset_name m.mname.node_id
463
        (pp_print_list (pp_horn_var m))
464
        (reset_vars machines m);
465

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

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

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

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

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

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

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

    
531
    (* Printing variables *)
532
    pp_print_list ~pp_open_box:pp_open_vbox0 pp_decl_var fmt
533
      (step_vars machines m
534
      @ rename_machine_list m.mname.node_id m.mstep.step_locals);
535
    Format.pp_print_newline fmt ();
536
    let sf_name, flags, _ = get_sf_info () in
537

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

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

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

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

    
591
(**************** XML printing functions *************)
592

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

    
629
and pp_xml_tuple fmt el = pp_comma_list pp_xml_expr fmt el
630

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

    
633
and pp_xml_handlers fmt hl = pp_print_list pp_xml_handler fmt hl
634

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

    
642
and pp_xml_call fmt id e =
643
  match id, e.expr_desc with
644
  | "+", Expr_tuple [ e1; e2 ] ->
645
    fprintf fmt "(%a + %a)" pp_xml_expr e1 pp_xml_expr e2
646
  | "uminus", _ ->
647
    fprintf fmt "(- %a)" pp_xml_expr e
648
  | "-", Expr_tuple [ e1; e2 ] ->
649
    fprintf fmt "(%a - %a)" pp_xml_expr e1 pp_xml_expr e2
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
  | "mod", Expr_tuple [ e1; e2 ] ->
655
    fprintf fmt "(%a mod %a)" pp_xml_expr e1 pp_xml_expr e2
656
  | "&&", Expr_tuple [ e1; e2 ] ->
657
    fprintf fmt "(%a and %a)" pp_xml_expr e1 pp_xml_expr e2
658
  | "||", Expr_tuple [ e1; e2 ] ->
659
    fprintf fmt "(%a or %a)" pp_xml_expr e1 pp_xml_expr e2
660
  | "xor", Expr_tuple [ e1; e2 ] ->
661
    fprintf fmt "(%a xor %a)" pp_xml_expr e1 pp_xml_expr e2
662
  | "impl", Expr_tuple [ e1; e2 ] ->
663
    fprintf fmt "(%a => %a)" pp_xml_expr e1 pp_xml_expr e2
664
  | "<", Expr_tuple [ e1; e2 ] ->
665
    fprintf fmt "(%a &lt; %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 &gt; %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 != %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
  | "not", _ ->
677
    fprintf fmt "(not %a)" pp_xml_expr e
678
  | _, Expr_tuple _ ->
679
    fprintf fmt "%s %a" id pp_xml_expr e
680
  | _ ->
681
    fprintf fmt "%s (%a)" id pp_xml_expr e
682

    
683
and pp_xml_eexpr fmt e =
684
  fprintf fmt "%a%t %a"
685
    (pp_print_list ~pp_sep:pp_print_semicolon Printers.pp_quantifiers)
686
    e.eexpr_quantifiers
687
    (fun fmt ->
688
      match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
689
    pp_xml_expr e.eexpr_qfexpr
690

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

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

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

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