Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal / seal_extract.ml @ ae08b9fc

History | View | Annotate | Download (42.5 KB)

1
open Lustre_types
2
open Utils
3
open Seal_utils			
4
open Zustre_data (* Access to Z3 context *)
5
   
6

    
7
(* Switched system extraction: expression are memoized *)
8
(*let expr_mem = Hashtbl.create 13*)
9
    
10
let add_init defs vid =
11
  Hashtbl.add defs vid [[], IsInit]
12

    
13

    
14
(**************************************************************)
15
(* Convert from Lustre expressions to Z3 expressions and back *)
16
(* All (free) variables have to be declared in the Z3 context *)
17
(**************************************************************)
18

    
19
let is_init_name = "__is_init"
20

    
21
let const_defs = Hashtbl.create 13
22
let is_const id = Hashtbl.mem const_defs id
23
let get_const id = Hashtbl.find const_defs id
24
                 
25
(* expressions are only basic constructs here, no more ite, tuples,
26
   arrows, fby, ... *)
27

    
28
(* Set of hash to support memoization *)
29
let expr_hash: (expr * Utils.tag) list ref = ref []
30
let ze_hash: (Z3.Expr.expr, Utils.tag) Hashtbl.t = Hashtbl.create 13
31
let e_hash: (Utils.tag, Z3.Expr.expr) Hashtbl.t = Hashtbl.create 13
32
let pp_hash pp_key pp_v fmt h = Hashtbl.iter (fun key v -> Format.fprintf fmt "%a -> %a@ " pp_key key pp_v v) h
33
let pp_e_map fmt = List.iter (fun (e,t) -> Format.fprintf fmt "%i -> %a@ " t Printers.pp_expr e) !expr_hash
34
let pp_ze_hash fmt = pp_hash
35
                      (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))
36
                      Format.pp_print_int
37
                      fmt
38
                      ze_hash
39
let pp_e_hash fmt = pp_hash
40
                      Format.pp_print_int
41
                      (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))
42
                      fmt
43
                      e_hash                              
44
let mem_expr e =
45
  (* Format.eprintf "Searching for %a in map: @[<v 0>%t@]"
46
   *   Printers.pp_expr e
47
   *   pp_e_map; *)
48
  let res = List.exists (fun (e',_) -> Corelang.is_eq_expr e e') !expr_hash in
49
  (* Format.eprintf "found?%b@." res; *)
50
  res
51
  
52
let mem_zexpr ze =
53
  Hashtbl.mem ze_hash ze
54
let get_zexpr e =
55
  let eref, uid = List.find (fun (e',_) -> Corelang.is_eq_expr e e') !expr_hash in
56
  (* Format.eprintf "found expr=%a id=%i@." Printers.pp_expr eref eref.expr_tag; *)
57
  Hashtbl.find e_hash uid
58
let get_expr ze =
59
  let uid = Hashtbl.find ze_hash ze in
60
  let e,_ = List.find (fun (e,t) -> t = uid) !expr_hash in
61
  e
62
  
63
let neg_ze z3e = Z3.Boolean.mk_not !ctx z3e 
64
let is_init_z3e =
65
  Z3.Expr.mk_const_s !ctx is_init_name  Zustre_common.bool_sort 
66

    
67
let get_zid (ze:Z3.Expr.expr) : Utils.tag = 
68
  try
69
    if Z3.Expr.equal ze is_init_z3e then -1 else
70
      if Z3.Expr.equal ze (neg_ze is_init_z3e) then -2 else
71
    Hashtbl.find ze_hash ze
72
  with _ -> (Format.eprintf "Looking for ze %s in Hash %a"
73
               (Z3.Expr.to_string ze)
74
               (fun fmt hash -> Hashtbl.iter (fun ze uid -> Format.fprintf fmt "%s -> %i@ " (Z3.Expr.to_string ze) uid) hash ) ze_hash;
75
             assert false)
76
let add_expr =
77
  let cpt = ref 0 in
78
  fun e ze ->
79
  incr cpt;
80
  let uid = !cpt in
81
  expr_hash := (e, uid)::!expr_hash;
82
  Hashtbl.add e_hash uid ze;
83
  Hashtbl.add ze_hash ze uid
84

    
85
  
86
let expr_to_z3_expr, zexpr_to_expr =
87
  (* List to store converted expression. *)
88
  (* let hash = ref [] in
89
   * let comp_expr e (e', _) = Corelang.is_eq_expr e e' in
90
   * let comp_zexpr ze (_, ze') = Z3.Expr.equal ze ze' in *)
91
  
92
  let rec e2ze e =
93
    if mem_expr e then (
94
      get_zexpr e
95
    )
96
    else (
97
      let res =
98
        match e.expr_desc with
99
        | Expr_const c ->
100
           let z3e = Zustre_common.horn_const_to_expr c in
101
           add_expr e z3e;
102
           z3e
103
        | Expr_ident id -> (
104
          if is_const id then (
105
            let c = get_const id in
106
            let z3e = Zustre_common.horn_const_to_expr c in
107
            add_expr e z3e;
108
            z3e
109
        )
110
        else (
111
          let fdecl_id = Zustre_common.get_fdecl id in
112
          let z3e = Z3.Expr.mk_const_f !ctx fdecl_id in
113
          add_expr e z3e;
114
          z3e
115
          )
116
        )
117
      | Expr_appl (id,args, None) (* no reset *) ->
118
         let z3e = Zustre_common.horn_basic_app id e2ze (Corelang.expr_list_of_expr args) in
119
         add_expr e z3e;
120
         z3e
121
      | Expr_tuple [e] ->
122
         let z3e = e2ze e in
123
         add_expr e z3e;
124
         z3e
125
      | _ -> ( match e.expr_desc with Expr_tuple _ -> Format.eprintf "tuple e2ze(%a)@.@?" Printers.pp_expr e
126
                                    | _ -> Format.eprintf "e2ze(%a)@.@?" Printers.pp_expr e)
127
                 ; assert false
128
      in
129
      res
130
    )
131
  in
132
  let rec ze2e ze =
133
    let ze_name ze =
134
      let fd = Z3.Expr.get_func_decl ze in
135
      Z3.Symbol.to_string (Z3.FuncDecl.get_name fd)
136
    in
137
    if mem_zexpr ze then
138
      None, Some (get_expr ze)
139
    else
140
      let open Corelang in
141
      let fd = Z3.Expr.get_func_decl ze in
142
      let zel = Z3.Expr.get_args ze in
143
      match Z3.Symbol.to_string (Z3.FuncDecl.get_name fd), zel with
144
      (*      | var, [] -> (* should be in env *) get_e *)
145

    
146
      (* Extracting IsInit status *)
147
      | "not", [ze] when ze_name ze = is_init_name ->
148
         Some false, None
149
      | name, [] when name = is_init_name -> Some true, None
150
      (* Other constructs are converted to a lustre expression *)
151
      | op, _ -> (
152
        
153
        
154
        if Z3.Expr.is_numeral ze then
155
          let e =
156
            if Z3.Arithmetic.is_real ze then
157
              let num =  Num.num_of_ratio (Z3.Arithmetic.Real.get_ratio ze) in
158
              let s = Z3.Arithmetic.Real.numeral_to_string ze in
159
              mkexpr
160
                Location.dummy_loc
161
                (Expr_const
162
                   (Const_real
163
                      (num, 0, s)))
164
            else if Z3.Arithmetic.is_int ze then
165
              mkexpr
166
                Location.dummy_loc
167
                (Expr_const
168
                   (Const_int
169
                      (Big_int.int_of_big_int (Z3.Arithmetic.Integer.get_big_int ze))))
170
            else if Z3.Expr.is_const ze then
171
              match Z3.Expr.to_string ze with
172
              | "true" -> mkexpr Location.dummy_loc
173
                            (Expr_const (Const_tag (tag_true)))
174
              | "false" ->
175
                 mkexpr Location.dummy_loc
176
                   (Expr_const (Const_tag (tag_false)))
177
              | _ -> assert false
178
            else
179
              (
180
                Format.eprintf "Const err: %s %b@." (Z3.Expr.to_string ze) (Z3.Expr.is_const ze);
181
                assert false (* a numeral but no int nor real *)
182
              )
183
          in
184
          None, Some e
185
        else
186
          match op with
187
          | "not" | "=" | "-" | "*" | "/"
188
            | ">=" | "<=" | ">" | "<" 
189
            ->
190
             let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in
191
             None, Some (mkpredef_call Location.dummy_loc op args)
192
          | "+" -> ( (* Special treatment of + for 2+ args *)
193
            let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in
194
            let e = match args with
195
                [] -> assert false
196
              | [hd] -> hd
197
              | e1::e2::tl ->
198
                 let first_binary_and = mkpredef_call Location.dummy_loc op [e1;e2] in
199
                 if tl = [] then first_binary_and else
200
                   List.fold_left (fun e e_new ->
201
                       mkpredef_call Location.dummy_loc op [e;e_new]
202
                     ) first_binary_and tl
203
                 
204
            in
205
            None, Some e 
206
          )
207
          | "and" | "or" -> (
208
            (* Special case since it can contain is_init pred *)
209
            let args = List.map (fun ze -> ze2e ze) zel in
210
            let op = if op = "and" then "&&" else if op = "or" then "||" else assert false in 
211
            match args with
212
            | [] -> assert false
213
            | [hd] -> hd
214
            | hd::tl ->
215
               List.fold_left
216
                 (fun (is_init_opt1, expr_opt1) (is_init_opt2, expr_opt2) ->
217
                   (match is_init_opt1, is_init_opt2 with
218
                      None, x | x, None -> x
219
                      | Some _, Some _ -> assert false),
220
                   (match expr_opt1, expr_opt2 with
221
                    | None, x | x, None -> x
222
                    | Some e1, Some e2 ->
223
                       Some (mkpredef_call Location.dummy_loc op [e1; e2])
224
                 ))
225
                 hd tl 
226
          )
227
          | op -> 
228
             let args = List.map (fun ze ->  (snd (ze2e ze))) zel in
229
             Format.eprintf "deal with op %s (nb args: %i). Expr is %s@."  op (List.length args) (Z3.Expr.to_string ze); assert false
230
      )
231
  in
232
  (fun e -> e2ze e), (fun ze -> ze2e ze)
233

    
234
               
235
let zexpr_to_guard_list ze =
236
  let init_opt, expr_opt = zexpr_to_expr ze in
237
  (match init_opt with
238
   | None -> []
239
   |Some b -> [IsInit, b]
240
  ) @ (match expr_opt with
241
       | None -> []
242
       | Some e -> [Expr e, true]
243
      )
244
                
245
               
246
let simplify_neg_guard l =
247
  List.map (fun (g,posneg) ->
248
      match g with
249
      | IsInit -> g, posneg
250
      | Expr g ->
251
          if posneg then
252
            Expr (Corelang.push_negations g),
253
            true
254
          else
255
            (* Pushing the negation in the expression *)
256
            Expr(Corelang.push_negations ~neg:true g),
257
            true
258
    ) l 
259

    
260
(* TODO:
261
individuellement demander si g1 => g2. Si c'est le cas, on peut ne garder que g1 dans la liste
262
*)    
263
(*****************************************************************)
264
(* Checking sat(isfiability) of an expression and simplifying it *)
265
(* All (free) variables have to be declared in the Z3 context    *)
266
(*****************************************************************)
267
(*
268
let goal_simplify zl =
269
  let goal = Z3.Goal.mk_goal !ctx false false false in
270
  Z3.Goal.add goal zl;
271
  let goal' = Z3.Goal.simplify goal None in
272
  (* Format.eprintf "Goal before: %s@.Goal after : %s@.Sat? %s@."
273
   *   (Z3.Goal.to_string goal)
274
   *   (Z3.Goal.to_string goal')
275
   *   (Z3.Solver.string_of_status status_res) 
276
   * ; *)
277
  let ze = Z3.Goal.as_expr goal' in
278
  (* Format.eprintf "as an expr: %s@." (Z3.Expr.to_string ze); *)
279
  zexpr_to_guard_list ze
280
  *)
281
  
282
let implies =
283
  let ze_implies_hash : ((Utils.tag * Utils.tag), bool) Hashtbl.t  = Hashtbl.create 13 in
284
  fun ze1 ze2 ->
285
  let ze1_uid = get_zid ze1 in
286
  let ze2_uid = get_zid ze2 in
287
  if Hashtbl.mem ze_implies_hash (ze1_uid, ze2_uid) then
288
    Hashtbl.find ze_implies_hash (ze1_uid, ze2_uid)
289
  else
290
    begin
291
      if !seal_debug then (
292
        report ~level:6 (fun fmt -> Format.fprintf fmt "Checking implication: %s => %s?@ "
293
          (Z3.Expr.to_string ze1) (Z3.Expr.to_string ze2)
294
      )); 
295
      let solver = Z3.Solver.mk_simple_solver !ctx in
296
      let tgt = Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_implies !ctx ze1 ze2) in
297
      let res =
298
        try
299
          let status_res = Z3.Solver.check solver [tgt] in
300
          match status_res with
301
          | Z3.Solver.UNSATISFIABLE -> if !seal_debug then
302
                                         report ~level:6 (fun fmt -> Format.fprintf fmt "Valid!@ "); 
303
             true
304
          | _ -> if !seal_debug then report ~level:6 (fun fmt -> Format.fprintf fmt "not proved valid@ "); 
305
             false
306
        with Zustre_common.UnknownFunction(id, msg) -> (
307
          report ~level:1 msg;
308
          false
309
        )
310
      in
311
      Hashtbl.add ze_implies_hash (ze1_uid,ze2_uid) res ;
312
      res
313
    end
314
                                               
315
let rec simplify zl =
316
  match zl with
317
  | [] | [_] -> zl
318
  | hd::tl -> (
319
    (* Forall e in tl, checking whether hd => e or e => hd, to keep hd
320
     in the first case and e in the second one *)
321
    let tl = simplify tl in
322
    let keep_hd, tl =
323
      List.fold_left (fun (keep_hd, accu) e ->
324
          if implies hd e then
325
            true, accu (* throwing away e *)
326
          else if implies e hd then
327
            false, e::accu (* throwing away hd *)
328
          else
329
            keep_hd, e::accu (* keeping both *)
330
        ) (true,[]) tl
331
    in
332
    (* Format.eprintf "keep_hd?%b hd=%s, tl=[%a]@."
333
     *   keep_hd
334
     *   (Z3.Expr.to_string hd)
335
     * (Utils.fprintf_list ~sep:"; " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) tl
336
     *   ; *)
337
    if keep_hd then
338
      hd::tl
339
    else
340
      tl
341
  )
342
  
343
let check_sat ?(just_check=false) (l: elem_boolexpr guard) : bool * (elem_boolexpr guard) =
344
  (* Syntactic simplification *)
345
  if false then
346
    Format.eprintf "Before simplify: %a@." (pp_guard_list pp_elem) l; 
347
  let l = simplify_neg_guard l in
348
  if false then (
349
    Format.eprintf "After simplify: %a@." (pp_guard_list pp_elem) l; 
350
    Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " (pp_guard_list pp_elem)l;
351
  );
352
  let solver = Z3.Solver.mk_simple_solver !ctx in
353
  try (
354
    let zl =
355
      List.map (fun (e, posneg) ->
356
          let ze =
357
            match e with
358
            | IsInit -> is_init_z3e
359
            | Expr e -> expr_to_z3_expr e 
360
          in
361
          if posneg then
362
            ze
363
          else
364
            neg_ze ze
365
        ) l
366
    in
367
    if false then Format.eprintf "Z3 exprs1: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; 
368
    let zl = simplify zl in
369
        if false then Format.eprintf "Z3 exprs2: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; 
370
    let status_res = Z3.Solver.check solver zl in
371
     if false then Format.eprintf "Z3 status: %s@ @]@. " (Z3.Solver.string_of_status status_res); 
372
    match status_res with
373
    | Z3.Solver.UNSATISFIABLE -> false, []
374
    | _ -> (
375
      if false && just_check then
376
        true, l
377
      else
378
        (* TODO: may be reactivate but it may create new expressions *)
379
        (* let l = goal_simplify zl in *)
380
        let l = List.fold_left
381
                  (fun accu ze -> accu @ (zexpr_to_guard_list ze))
382
                  []
383
                  zl
384
        in
385
  (* Format.eprintf "@.@[<v 2>Check_Sat:@ before: %a@ after:
386
       %a@. Goal precise? %b/%b@]@.@. " * pp_guard_list l
387
       pp_guard_list l' * (Z3.Goal.is_precise goal) *
388
       (Z3.Goal.is_precise goal'); *)
389
  
390

    
391
        true, l
392
        
393
         
394
    )
395
         
396
  )
397
  with Zustre_common.UnknownFunction(id, msg) -> (
398
    report ~level:1 msg;
399
    true, l (* keeping everything. *)
400
  )
401
      
402
  
403

    
404

    
405
(**************************************************************)
406

    
407
  
408
let clean_sys sys =
409
  List.fold_left (fun accu (guards, updates) ->
410
      let sat, guards' =  check_sat (List.map (fun (g, pn) -> Expr g, pn) guards) in
411
      (*Format.eprintf "Guard: %a@.Guard cleaned: %a@.Sat? %b@."
412
        (fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr))  guards
413
        (fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr))  guards'
414
        sat
415

    
416
      ;*)
417
        if sat then
418
        (List.map (fun (e, b) -> (deelem e, b)) guards', updates)::accu
419
      else
420
        accu
421
    )
422
    [] sys
423

    
424
(* Most costly function: has the be efficiently implemented.  All
425
   registered guards are initially produced by the call to
426
   combine_guards. We csan normalize the guards to ease the
427
   comparisons.
428

    
429
   We assume that gl1 and gl2 are already both satisfiable and in a
430
   kind of reduced form. Let lshort and llong be the short and long
431
   list of gl1, gl2. We check whether each element elong of llong is
432
   satisfiable with lshort. If no, stop. If yes, we search to reduce
433
   the list. If elong => eshort_i, we can remove eshort_i from
434
   lshort. we can continue with this lshort shortened, lshort'; it is
435
   not necessary to add yet elong in lshort' since we already know
436
   rthat elong is somehow reduced with respect to other elements of
437
   llong. If eshort_i => elong, then we keep ehosrt_i in lshort and do
438
   not store elong.
439

    
440
   After iterating through llong, we have a shortened version of
441
   lshort + some elements of llong that have to be remembered. We add
442
   them to this new consolidated list. 
443

    
444
 *)
445

    
446
(* combine_guards ~fresh:Some(e,b) gl1 gl2 returns ok, gl with ok=true
447
   when (e=b) ang gl1 and gl2 is satisfiable and gl is a consilidated
448
   version of it.  *)
449
let combine_guards ?(fresh=None) gl1 gl2 =
450
  (* Filtering out trivial cases. More semantics ones would have to be
451
     addressed later *)
452
  let check_sat e = (* temp function before we clean the original one *)
453
    let ok, _ = check_sat e in
454
    ok
455
  in
456
  let implies (e1,pn1) (e2,pn2) =
457
    let e2z e pn =
458
      match e with
459
        | IsInit -> if pn then is_init_z3e else neg_ze is_init_z3e
460
        | Expr e -> expr_to_z3_expr (if pn then e else (Corelang.push_negations ~neg:true e))
461
      in
462
    implies (e2z e1 pn1) (e2z e2 pn2)
463
  in
464
  let lshort, llong =
465
    if List.length gl1 > List.length gl2 then gl2, gl1 else gl1, gl2
466
  in
467
  let merge long short =
468
    let short, long_sel, ok = 
469
    List.fold_left (fun (short,long_sel, ok) long_e ->
470
        if not ok then
471
          [],[], false (* Propagating unsat case *)
472
        else if check_sat (long_e::short) then
473
          let short, keep_long_e =
474
            List.fold_left (fun (accu_short, keep_long_e) eshort_i ->
475
                if not keep_long_e then (* shorten the algo *)
476
                  eshort_i :: accu_short, false
477
                else (* keep_long_e = true in the following *)
478
                  if implies eshort_i long_e then
479
                    (* First case is trying to remove long_e!
480

    
481
                     Since short is already normalized, we can remove
482
                     long_e. If later long_e is stronger than another
483
                     element of short, then necessarily eshort_i =>
484
                     long_e ->
485
                     that_other_element_of_short. Contradiction. *)
486
                    eshort_i::accu_short, false
487
                  else if implies long_e eshort_i then 
488
                    (* removing eshort_i, keeping long_e. *)
489
                    accu_short, true
490
                  else (* Not comparable, keeping both *)
491
                    eshort_i::accu_short, true
492
              )
493
              ([],true) (* Initially we assume that we will keep long_e *)
494
              short
495
          in
496
          if keep_long_e then
497
            short, long_e::long_sel, true
498
          else
499
            short, long_sel, true
500
        else
501
          [],[],false
502
      ) (short, [], true) long
503
    in
504
    ok, long_sel@short
505
  in
506
  let ok, l = match fresh with
507
    | None -> true, []
508
    | Some g -> merge [g] []
509
  in
510
  if not ok then
511
    false, []
512
  else
513
    let ok, lshort = merge lshort l in
514
    if not ok then
515
      false, []
516
    else
517
      merge llong lshort
518
    
519

    
520
(* Encode "If gel1=posneg then gel2":
521
   - Compute the combination of guarded exprs in gel1 and gel2:
522
     - Each guarded_expr in gel1 is transformed as a guard: the
523
       expression is associated to posneg.
524
     - Existing guards in gel2 are concatenated to that list of guards
525
     - We keep expr in the ge of gel2 as the legitimate expression 
526
 *)
527
let concatenate_ge gel1 posneg gel2 =
528
  let l, all_invalid =
529
    List.fold_left (
530
        fun (accu, all_invalid) (g2,e2) ->
531
        List.fold_left (
532
            fun (accu, all_invalid) (g1,e1) ->
533
            (* Format.eprintf "@[<v 2>Combining guards: (%a=%b) AND [%a] AND [%a]@ "
534
             *  pp_elem e1
535
             *  posneg
536
             *  pp_guard_list g1
537
             *  pp_guard_list g2; *)
538

    
539
            let ok, gl = combine_guards ~fresh:(Some(e1,posneg)) g1 g2 in
540
            (* Format.eprintf "@]@ Result is [%a]@ "
541
             *   pp_guard_list gl; *)
542

    
543
            if ok then
544
              (gl, e2)::accu, false
545
            else (
546
              accu, all_invalid
547
            )
548
          ) (accu, all_invalid) gel1
549
      ) ([], true) gel2
550
  in
551
  not all_invalid, l
552

    
553
(* Transform the guard expressions ge = [gl1, e1; gl2, e2;...] as
554
   [gl1, e1=id; gl2, e2=id; ...]  *)
555
let mk_ge_eq_id ge id =
556
  List.map
557
    (fun (gl, g_e) ->
558
      gl,
559
      if id = "true" then
560
        g_e
561
      else
562
        match g_e with
563
        | Expr g_e ->
564
           if id = "false" then
565
             Expr (Corelang.push_negations ~neg:true g_e)
566
           else  
567
             let loc = g_e.expr_loc in
568
             Expr(Corelang.mk_eq loc
569
                    g_e
570
                    (Corelang.expr_of_ident id loc))
571
        | _ -> assert false
572
    )  ge 
573

    
574
    (* Rewrite the expression expr, replacing any occurence of a variable
575
   by its definition.
576
     *)
577
let rec rewrite defs expr : elem_guarded_expr list =
578
  let rewrite = rewrite defs in
579
  let res =
580
    match expr.expr_desc with
581
    | Expr_appl (id, args, None) ->
582
       let args = rewrite args in
583
       List.map (fun (guards, e) ->
584
           guards,
585
           Expr (Corelang.mkexpr expr.expr_loc (Expr_appl(id, deelem e, None)))
586
         ) args 
587
    | Expr_const _  -> [[], Expr expr]
588
    | Expr_ident id ->
589
       if Hashtbl.mem defs id then
590
         Hashtbl.find defs id
591
       else
592
         (* id should be an input *)
593
         [[], Expr expr]
594
    | Expr_ite (g, e1, e2) ->
595
       let g = rewrite g and
596
           e1 = rewrite e1 and
597
           e2 = rewrite e2 in
598
       let ok_then, g_then = concatenate_ge g true e1 in
599
       let ok_else, g_else = concatenate_ge g false e2 in
600
       (if ok_then then g_then else [])@
601
         (if ok_else then g_else else [])
602
    | Expr_merge (g_id, branches) ->
603
       if Hashtbl.mem defs g_id then
604
         let g = Hashtbl.find defs g_id in
605
         (* Format.eprintf "Expr_merge %s = %a@." g_id (pp_mdefs pp_elem) g ; *)
606
         List.fold_left (fun accu (id, e) ->
607
             let g = mk_ge_eq_id g id in
608
             let e = rewrite e in
609
             let ok, g_eq_id = concatenate_ge g true e in
610
             if ok then g_eq_id@accu else accu
611
           ) [] branches
612
       else
613
         assert false (* g should be defined already *)
614
    | Expr_when (e, id, l) ->
615
       let e = rewrite e in
616
       let id_def = Hashtbl.find defs id in
617
       let clock = mk_ge_eq_id id_def l in
618
       let ok, new_ge = concatenate_ge clock true e in
619
       if ok then new_ge else []
620
    | Expr_arrow _ -> [[], IsInit] (* At this point the only arrow should be true -> false *)
621
    | Expr_tuple el ->
622
       (* Each expr is associated to its flatten guarded expr list *)
623
       let gell = List.map rewrite el in
624
       (* Computing all combinations: we obtain a list of guarded tuple *)
625
       let rec aux gell : (elem_boolexpr guard * expr list) list =
626
         match gell with
627
         | [] -> assert false (* Not happening *)
628
         | [gel] -> List.map (fun (g,e) -> g, [deelem e]) gel
629
         | gel::getl ->
630
            let getl = aux getl in
631
            List.fold_left (
632
                fun accu (g,e) ->
633
                List.fold_left (
634
                    fun accu (gl, minituple) ->
635
                    let is_compat, guard_comb = combine_guards g gl in
636
                    if is_compat then
637
                      let new_gt : elem_boolexpr guard * expr list = (guard_comb, (deelem e)::minituple) in
638
                      new_gt::accu
639
                    else
640
                      accu
641
                    
642
                  ) accu getl
643
              ) [] gel
644
       in
645
       let gtuples = aux gell in
646
       (* Rebuilding the valid type: guarded expr list (with tuple exprs) *)
647
       List.map
648
         (fun (g,tuple) -> g, Expr (Corelang.mkexpr expr.expr_loc (Expr_tuple tuple)))
649
         gtuples
650
    | Expr_fby _
651
      | Expr_appl _
652
                  (* Should be removed by mormalization and inlining *)
653
      -> Format.eprintf "Pb expr: %a@.@?" Printers.pp_expr expr; assert false
654
    | Expr_array _ | Expr_access _ | Expr_power _
655
                                                (* Arrays not handled here yet *)
656
      -> assert false
657
    | Expr_pre _ -> (* Not rewriting mem assign *)
658
       assert false
659
  in
660
  (* Format.eprintf "Rewriting %a as [@[<v 0>%a@]]@ "
661
   *   Printers.pp_expr expr
662
   *   (Utils.fprintf_list ~sep:"@ "
663
   *        pp_guard_expr) res; *)
664
  res
665
and add_def defs vid expr =
666
  (* Format.eprintf "Add_def: %s = %a@."
667
   *   vid
668
   *   Printers.pp_expr expr; *)
669
  let vid_defs = rewrite defs expr in
670
  (* Format.eprintf "-> @[<v 0>%a@]@."
671
   *   (Utils.fprintf_list ~sep:"@ "
672
   *      (pp_guard_expr pp_elem)) vid_defs;   *)
673
  (* Format.eprintf "Add_def: %s = %a@. -> @[<v 0>%a@]@."
674
   *     vid
675
   *     Printers.pp_expr expr
676
   *     (
677
   *       (Utils.fprintf_list ~sep:"@ "
678
   *          pp_guard_expr)) vid_defs;  *)
679
  Hashtbl.add defs vid vid_defs
680

    
681
(* Takes a list of guarded exprs (ge) and a guard
682
returns the same list of ge splited into the ones where the guard is true and the ones where it is false. In both lists the associated ge do not mention that guard anymore.
683

    
684
When a given ge doesn't mention positively or negatively such guards, it is duplicated in both lists *)
685
let split_mdefs elem (mdefs: elem_guarded_expr list) =
686
  List.fold_left (
687
      fun (selected, left_out)
688
          ((guards, expr) as ge) ->
689
      (* select the element of guards that match the argument elem *)
690
      let sel, others_guards = List.partition (select_elem elem) guards in
691
      match sel with
692
      (* we extract the element from the list and add it to the
693
         appropriate list *)
694
      | [_, sel_status] ->
695
         if sel_status then
696
           (others_guards,expr)::selected, left_out
697
         else selected, (others_guards,expr)::left_out
698
      | [] -> (* no such guard exists, we have to duplicate the
699
              guard_expr in both lists *)
700
         ge::selected, ge::left_out
701
      | _ -> (
702
        Format.eprintf "@.Spliting list on elem %a.@.List:%a@."
703
          pp_elem elem
704
          (pp_mdefs pp_elem) mdefs;
705
        assert false (* more then one element selected. Should
706
                          not happen , or trival dead code like if
707
                              x then if not x then dead code *)
708
      )
709
    ) ([],[]) mdefs
710
    
711
let split_mem_defs
712
      (elem: element)
713
      (mem_defs: (ident * elem_guarded_expr list) list)
714
      :
715
      ((ident * elem_guarded_expr mdef_t) list) * ((ident * elem_guarded_expr mdef_t) list)
716
  
717
  =
718
  List.fold_right (fun (m,mdefs)
719
                       (accu_pos, accu_neg) ->
720
      let pos, neg =
721
        split_mdefs elem mdefs 
722
      in
723
      (m, pos)::accu_pos,
724
      (m, neg)::accu_neg
725
    ) mem_defs ([],[])
726

    
727

    
728
(* Split a list of mem_defs into init and step lists of guarded
729
   expressions per memory. *)
730
let split_init mem_defs =
731
  split_mem_defs IsInit mem_defs 
732

    
733
(* Previous version of the function: way too costly 
734
let pick_guard mem_defs : expr option =  
735
  let gel = List.flatten (List.map snd mem_defs) in
736
  let gl = List.flatten (List.map fst gel) in
737
  let all_guards =
738
    List.map (
739
        (* selecting guards and getting rid of boolean *)
740
        fun (e,b) ->
741
        match e with
742
        | Expr e -> e
743
        | _ -> assert false
744
      (* should have been filtered out
745
                                      yet *)
746
      ) gl
747
  in
748
  (* TODO , one could sort by occurence and provided the most common
749
     one *)
750
  try
751
  Some (List.hd all_guards)  
752
  with _ -> None
753
   *)
754

    
755
(* Returning the first non empty guard expression *)
756
let rec pick_guard mem_defs : expr option =
757
  match mem_defs with
758
  | [] -> None
759
  | (_, gel)::tl -> (
760
    let found =
761
      List.fold_left (fun found (g,_) ->
762
          if found = None then
763
            match g with
764
            | [] -> None
765
            | (Expr e, _)::_ -> Some e
766
            | (IsInit, _)::_ -> assert false (* should be removed already *)
767
          else
768
            found
769
        ) None gel
770
    in
771
    if found = None then pick_guard tl else found
772
  )
773
          
774

    
775
(* Transform a list of variable * guarded exprs into a list of guarded pairs (variable, expressions)
776
*)
777
let rec build_switch_sys
778
          (mem_defs : (Utils.ident * elem_guarded_expr list) list )
779
          prefix
780
        :
781
          ((expr * bool) list * (ident * expr) list ) list =
782
  if !seal_debug then
783
    report ~level:4 (fun fmt -> Format.fprintf fmt "@[<v 2>Build_switch with@ %a@]@."
784
                                  pp_all_defs
785
                                  mem_defs);
786
  (* if all mem_defs have empty guards, we are done, return prefix,
787
     mem_defs expr.
788

    
789
     otherwise pick a guard in one of the mem, eg (g, b) then for each
790
     other mem, one need to select the same guard g with the same
791
     status b, *)
792
  let res =
793
  if List.for_all (fun (m,mdefs) ->
794
         (* All defs are unguarded *)
795
         match mdefs with
796
         | [[], _] -> true (* Regular unguarded expression *)
797
         | [] -> true (* A unbalanced definition of the memory. Here
798
                         we have m_{k+1} -> m_k *)
799
         | _ -> false
800
       ) mem_defs
801
  then
802
    [prefix ,
803
     List.map (fun (m,gel) ->
804
         match gel with
805
         | [_,e] ->
806
            let e =
807
              match e with
808
              | Expr e -> e
809
              | _ -> assert false (* No IsInit expression *)
810
            in
811
            m,e
812
         | [] -> m, Corelang.expr_of_ident m Location.dummy_loc
813
         | _ -> assert false
814
       ) mem_defs]
815
  else
816
    (* Picking a guard *)
817
    let elem_opt : expr option = pick_guard mem_defs in
818
    match elem_opt with
819
      None -> (
820
       Format.eprintf "Issues picking guard in mem_defs: %a@." pp_all_defs mem_defs;
821
       assert false (* Otherwise the first case should have matched *)
822
    )
823
    | Some elem -> (
824
      report ~level:4 (fun fmt -> Format.fprintf fmt "selecting guard %a@." Printers.pp_expr elem);
825
      let pos, neg =
826
        split_mem_defs
827
          (Expr elem)
828
          mem_defs
829
      in
830
      (* Special cases to avoid useless computations: true, false conditions *)
831
      match elem.expr_desc with
832
      (*| Expr_ident "true"  ->   build_switch_sys pos prefix *)
833
      | Expr_const (Const_tag tag) when tag = Corelang.tag_true
834
        ->   build_switch_sys pos prefix
835
      (*| Expr_ident "false" ->   build_switch_sys neg prefix *)
836
      | Expr_const (Const_tag tag) when tag = Corelang.tag_false 
837
        ->   build_switch_sys neg prefix
838
      | _ -> (* Regular case *)
839
         (* let _ = (
840
          *     Format.eprintf "Expr is %a@." Printers.pp_expr elem;
841
          *     match elem.expr_desc with
842
          *     | Expr_const _ -> Format.eprintf "a const@."
843
          *                     
844
          *     | Expr_ident _ -> Format.eprintf "an ident@."
845
          *     | _ -> Format.eprintf "something else@."
846
          *   )
847
          * in *)
848
         let clean l =
849
           let l = List.map (fun (e,b) -> (Expr e), b) l in
850
           let ok, l = check_sat l in
851
           let l = List.map (fun (e,b) -> deelem e, b) l in
852
           ok, l
853
         in
854
         let pos_prefix = (elem, true)::prefix in
855
         let neg_prefix = (elem, false)::prefix in
856
         let ok_pos, pos_prefix = clean pos_prefix in         
857
         let ok_neg, neg_prefix = clean neg_prefix in
858
         report ~level:4 (fun fmt -> Format.fprintf fmt "Enforcing %a@." Printers.pp_expr elem);
859
         let ok_l = if ok_pos then build_switch_sys pos pos_prefix else [] in
860
         report ~level:4 (fun fmt -> Format.fprintf fmt "Enforcing not(%a)@." Printers.pp_expr elem);
861
         let nok_l = if ok_neg then build_switch_sys neg neg_prefix else [] in
862
         ok_l @ nok_l
863
    )
864
  in
865
    if !seal_debug then (
866
      report ~level:4 (fun fmt ->
867
          Format.fprintf fmt
868
            "@[<v 2>===> @[%t@ @]@]@ @]@ "
869
            (fun fmt -> List.iter (fun (gl,up) ->
870
                            Format.fprintf fmt "[@[%a@]] -> (%a)@ "
871
                              (pp_guard_list Printers.pp_expr) gl pp_up up) res);
872
          
873
    ));
874
    res
875
  
876

    
877
      
878
(* Take a normalized node and extract a list of switches: (cond,
879
   update) meaning "if cond then update" where update shall define all
880
   node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *)
881
let node_as_switched_sys consts (mems:var_decl list) nd =
882
  (* rescheduling node: has been scheduled already, no need to protect
883
     the call to schedule_node *)
884
  let nd_report = Scheduling.schedule_node nd in
885
  let schedule = nd_report.Scheduling_type.schedule in
886
  let eqs, auts = Corelang.get_node_eqs nd in
887
  assert (auts = []); (* Automata should be expanded by now *)
888
  let sorted_eqs, unused = Scheduling.sort_equations_from_schedule eqs schedule in
889
  let defs : (ident,  elem_guarded_expr list) Hashtbl.t = Hashtbl.create 13 in
890
  let add_def = add_def defs in
891

    
892
  let vars = Corelang.get_node_vars nd in
893
  (* Filtering out unused vars *)
894
  let vars = List.filter (fun v -> not (List.mem v.var_id unused)) vars in
895
  (* Registering all locals variables as Z3 predicates. Will be use to
896
     simplify the expansion *) 
897
  let _ =
898
    List.iter (fun v ->
899
        let fdecl = Z3.FuncDecl.mk_func_decl_s
900
                      !ctx
901
                      v.var_id
902
                      []
903
                      (Zustre_common.type_to_sort v.var_type)
904
        in
905
        ignore (Zustre_common.register_fdecl v.var_id fdecl)
906
      ) vars
907
  in
908
  let _ =
909
    List.iter (fun c -> Hashtbl.add const_defs c.const_id c.const_value) consts
910
  in
911

    
912
  
913
  (* Registering node equations: identifying mem definitions and
914
     storing others in the "defs" hashtbl.
915

    
916
     Each assign is stored in a hash tbl as list of guarded
917
     expressions. The memory definition is also "rewritten" as such a
918
     list of guarded assigns.  *)
919
  let mem_defs, output_defs =
920
    List.fold_left (fun (accu_mems, accu_outputs) eq ->
921
        match eq.eq_lhs with
922
        | [vid] ->
923
           (* Only focus on memory definitions *)
924
           if List.exists (fun v -> v.var_id = vid) mems then 
925
             (
926
               match eq.eq_rhs.expr_desc with
927
               | Expr_pre def_m ->
928
                  report ~level:3 (fun fmt ->
929
                      Format.fprintf fmt "Preparing mem %s@." vid);
930
                  (vid, rewrite defs def_m)::accu_mems, accu_outputs
931
               | _ -> assert false
932
             ) 
933
           else if List.exists (fun v -> v.var_id = vid) nd.node_outputs then (
934
             report ~level:3 (fun fmt ->
935
                 Format.fprintf fmt "Output variable %s@." vid);
936
             add_def vid eq.eq_rhs;
937
             accu_mems, (vid, rewrite defs eq.eq_rhs)::accu_outputs
938
             
939
           )
940
           else
941
             (
942
               report ~level:3 (fun fmt ->
943
                   Format.fprintf fmt "Registering variable %s@." vid);
944
               add_def vid eq.eq_rhs;
945
               accu_mems, accu_outputs
946
             )
947
        | _ -> assert false (* should have been removed by normalization *)
948
      ) ([], []) sorted_eqs
949
  in
950

    
951
  
952
  report ~level:2 (fun fmt -> Format.fprintf fmt "Printing out (guarded) memories definitions (may takes time)@.");
953
  (* Printing memories definitions *)
954
  report ~level:3
955
    (fun fmt ->
956
      Format.fprintf fmt
957
        "@[<v 0>%a@]@."
958
        (Utils.fprintf_list ~sep:"@ "
959
           (fun fmt (m,mdefs) ->
960
             Format.fprintf fmt
961
               "%s -> [@[<v 0>%a@] ]@ "
962
               m
963
               (Utils.fprintf_list ~sep:"@ "
964
                  (pp_guard_expr pp_elem)) mdefs
965
        ))
966
        mem_defs);
967
  (* Format.eprintf "Split init@."; *)
968
  let init_defs, update_defs =
969
    split_init mem_defs 
970
  in
971
  let init_out, update_out =
972
    split_init output_defs
973
  in
974
  report ~level:3
975
    (fun fmt ->
976
      Format.fprintf fmt
977
        "@[<v 0>Init:@ %a@]@."
978
        (Utils.fprintf_list ~sep:"@ "
979
           (fun fmt (m,mdefs) ->
980
             Format.fprintf fmt
981
               "%s -> @[<v 0>[%a@] ]@ "
982
               m
983
               (Utils.fprintf_list ~sep:"@ "
984
                  (pp_guard_expr pp_elem)) mdefs
985
        ))
986
        init_defs);
987
  report ~level:3
988
    (fun fmt ->
989
      Format.fprintf fmt
990
        "@[<v 0>Step:@ %a@]@."
991
        (Utils.fprintf_list ~sep:"@ "
992
           (fun fmt (m,mdefs) ->
993
             Format.fprintf fmt
994
               "%s -> @[<v 0>[%a@] ]@ "
995
               m
996
               (Utils.fprintf_list ~sep:"@ "
997
                  (pp_guard_expr pp_elem)) mdefs
998
        ))
999
        update_defs);
1000
  (* Format.eprintf "Build init@."; *)
1001
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build init@.");
1002
  let sw_init= 
1003
    build_switch_sys init_defs []
1004
  in
1005
  (* Format.eprintf "Build step@."; *)
1006
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build step@.");
1007
  let sw_sys =
1008
    build_switch_sys update_defs []
1009
  in
1010

    
1011
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build init out@.");
1012
  let init_out =
1013
    build_switch_sys init_out []
1014
  in
1015
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build step out@.");
1016

    
1017
  let update_out =
1018
    build_switch_sys update_out []
1019
  in
1020

    
1021
  let sw_init = clean_sys sw_init in
1022
  let sw_sys = clean_sys sw_sys in
1023
  let init_out = clean_sys init_out in
1024
  let update_out = clean_sys update_out in
1025

    
1026
  (* Some additional checks *)
1027
  
1028
  if false then
1029
    begin
1030
      Format.eprintf "@.@.CHECKING!!!!!!!!!!!@.";
1031
      Format.eprintf "Any duplicate expression in guards?@.";
1032
      
1033
      let sw_sys =
1034
        List.map (fun (gl, up) ->
1035
            let gl = List.sort (fun (e,b) (e',b') ->
1036
                         let res = compare e.expr_tag e'.expr_tag in
1037
                         if res = 0 then (Format.eprintf "Same exprs?@.%a@.%a@.@."
1038
                                            Printers.pp_expr e
1039
                                            Printers.pp_expr e'
1040
                                         );
1041
                         res
1042
                       ) gl in
1043
            gl, up
1044
          ) sw_sys 
1045
      in
1046
      Format.eprintf "Another check for duplicates in guard list@.";
1047
      List.iter (fun (gl, _) ->
1048
          let rec aux hd l =
1049
            match l with
1050
              [] -> ()
1051
            | (e,b)::tl -> let others = hd@tl in
1052
                           List.iter (fun (e',_) -> if Corelang.is_eq_expr e e' then
1053
                                                      (Format.eprintf "Same exprs?@.%a@.%a@.@."
1054
                                                         Printers.pp_expr e
1055
                                                         Printers.pp_expr e'
1056
                             )) others;
1057
                           aux ((e,b)::hd) tl
1058
          in
1059
          aux [] gl
1060
        ) sw_sys;
1061
      Format.eprintf "Checking duplicates in updates@.";
1062
      let rec check_dup_up accu l =
1063
        match l with
1064
        | [] -> ()
1065
        | ((gl, up) as hd)::tl ->
1066
           let others = accu@tl in
1067
           List.iter (fun (gl',up') -> if up = up' then
1068
                                         Format.eprintf "Same updates?@.%a@.%a@.%a@.%a@.@."
1069

    
1070
                                           pp_gl_short gl
1071
                                           pp_up up
1072
                                           pp_gl_short gl'
1073
                                           pp_up up'
1074
                                       
1075
             ) others;
1076
           
1077
           
1078

    
1079
           check_dup_up (hd::accu) tl
1080
           
1081
      in
1082
      check_dup_up [] sw_sys;
1083
      let sw_sys =
1084
        List.sort (fun (gl1, _) (gl2, _) ->
1085
            let glid gl = List.map (fun (e,_) -> e.expr_tag) gl in
1086
            
1087
            let res = compare (glid gl1) (glid gl2) in
1088
            if res = 0 then Format.eprintf "Same guards?@.%a@.%a@.@."
1089
                              pp_gl_short gl1 pp_gl_short gl2
1090
            ;
1091
              res
1092

    
1093
          ) sw_sys
1094

    
1095
      in
1096
      ()
1097
    end;
1098
  
1099

    
1100
  (* Iter through the elements and gather them by updates *)
1101
  let process sys =
1102
    (* The map will associate to each update up the pair (set, set
1103
       list) where set is the share guards and set list a list of
1104
       disjunctive guards. Each set represents a conjunction of
1105
       expressions. *)
1106
    report ~level:3 (fun fmt -> Format.fprintf fmt "%t@."
1107
                                  (fun fmt -> List.iter (fun (gl,up) ->
1108
                                                  Format.fprintf fmt "[@[%a@]] -> (%a)@ "
1109
                                                    (pp_guard_list Printers.pp_expr) gl pp_up up) sw_init));
1110
    
1111
    (* We perform multiple pass to avoid errors *)
1112
    let map =
1113
      List.fold_left (fun map (gl,up) ->
1114
          (* creating a new set to describe gl *)
1115
          let new_set =
1116
            List.fold_left
1117
              (fun set g -> Guards.add g set)
1118
              Guards.empty
1119
              gl
1120
          in
1121
          (* updating the map with up -> new_set *)
1122
          if UpMap.mem up map then
1123
            let guard_set = UpMap.find up map in
1124
            UpMap.add up (new_set::guard_set) map
1125
          else
1126
            UpMap.add up [new_set] map
1127
        ) UpMap.empty sys
1128
    in
1129
    (* Processing the set of guards leading to the same update: return
1130
       conj, disj with conf is a set of guards, and disj a DNF, ie a
1131
       list of set of guards *)
1132
    let map =
1133
      UpMap.map (
1134
          fun guards ->
1135
          match guards with
1136
          | [] -> Guards.empty, [] (* Nothing *)
1137
          | [s]-> s, [] (* basic case *)
1138
          | hd::tl ->
1139
             let shared = List.fold_left (fun shared s -> Guards.inter shared s) hd tl in
1140
             let remaining = List.map (fun s -> Guards.diff s shared) guards in
1141
             (* If one of them is empty, we can remove the others, otherwise keep them *)
1142
             if List.exists Guards.is_empty remaining then
1143
               shared, []
1144
             else
1145
               shared, remaining
1146
        ) map
1147
    in
1148
  let rec mk_binop op l = match l with
1149
      [] -> assert false
1150
    | [e] -> e
1151
    | hd::tl -> Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl]
1152
  in
1153
  let gl_as_expr gl =
1154
    let gl = Guards.elements gl in
1155
    let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in 
1156
    match gl with
1157
      [] -> []
1158
    | [e] -> [export e]
1159
    | _ ->
1160
       [mk_binop "&&"
1161
          (List.map export gl)]
1162
  in
1163
  let rec clean_disj disj =
1164
    match disj with
1165
    | [] -> []
1166
    | [_] -> assert false (* A disjunction was a single case can be ignored *) 
1167
    | _::_::_ -> (
1168
      (* First basic version: producing a DNF One can later, (1)
1169
           simplify it with z3, or (2) build the compact tree with
1170
           maximum shared subexpression (and simplify it with z3) *)
1171
      let elems = List.fold_left (fun accu gl -> (gl_as_expr gl) @ accu) [] disj in
1172
      let or_expr = mk_binop "||" elems in
1173
      [or_expr]
1174

    
1175

    
1176
    (* TODO disj*)
1177
    (* get the item that occurs in most case *)
1178
    (* List.fold_left (fun accu s ->
1179
     *     List.fold_left (fun accu (e,b) ->
1180
     *         if List.mem_assoc (e.expr_tag, b)
1181
     *       ) accu (Guards.elements s)
1182
     *   ) [] disj *)
1183

    
1184
    )
1185
  in
1186
  if !seal_debug then Format.eprintf "Map: %i elements@ " (UpMap.cardinal map);
1187
  UpMap.fold (fun up (common, disj) accu ->
1188
      if !seal_debug then
1189
        Format.eprintf
1190
          "Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@."
1191
          Guards.pp_short common
1192
          (fprintf_list ~sep:";@ " Guards.pp_long) disj
1193
          UpMap.pp up;
1194
      let disj = clean_disj disj in
1195
      let guard_expr = (gl_as_expr common)@disj in
1196
      
1197
      ((match guard_expr with
1198
        | [] -> None 
1199
        | _ -> Some (mk_binop "&&" guard_expr)), up)::accu
1200
    ) map []
1201
  
1202
    in
1203
    
1204
    
1205
    
1206
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_init:@.");
1207
    let sw_init = process sw_init in
1208
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_sys:@.");
1209
    let sw_sys = process sw_sys in
1210
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process init_out:@.");
1211
    let init_out = process init_out in
1212
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process update_out:@.");
1213
    let update_out = process update_out in
1214
    sw_init , sw_sys, init_out, update_out