Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal / seal_extract.ml @ 04a188ec

History | View | Annotate | Download (45.1 KB)

1
open Lustre_types
2
open Utils
3
open Seal_utils			
4
open Zustre_data (* Access to Z3 context *)
5
   
6
let _ =
7
  Z3.Params.update_param_value !ctx "timeout" "10000"
8
  
9
(* Switched system extraction: expression are memoized *)
10
(*let expr_mem = Hashtbl.create 13*)
11
    
12
let add_init defs vid =
13
  Hashtbl.add defs vid [[], IsInit]
14

    
15

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

    
21
let is_init_name = "__is_init"
22

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

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

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

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

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

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

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

    
402
        true, l
403
        
404
         
405
    )
406
         
407
  )
408
  with Zustre_common.UnknownFunction(id, msg) -> (
409
    report ~level:1 msg;
410
    true, l (* keeping everything. *)
411
  )
412
      
413
  
414

    
415

    
416
(**************************************************************)
417

    
418
  
419
let clean_sys sys =
420
  List.fold_left (fun accu (guards, updates) ->
421
      let sat, guards' =  check_sat (List.map (fun (g, pn) -> Expr g, pn) guards) in
422
      (*Format.eprintf "Guard: %a@.Guard cleaned: %a@.Sat? %b@."
423
        (fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr))  guards
424
        (fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr))  guards'
425
        sat
426

    
427
      ;*)
428
        if sat then
429
        (List.map (fun (e, b) -> (deelem e, b)) guards', updates)::accu
430
      else
431
        accu
432
    )
433
    [] sys
434

    
435
(* Most costly function: has the be efficiently implemented.  All
436
   registered guards are initially produced by the call to
437
   combine_guards. We csan normalize the guards to ease the
438
   comparisons.
439

    
440
   We assume that gl1 and gl2 are already both satisfiable and in a
441
   kind of reduced form. Let lshort and llong be the short and long
442
   list of gl1, gl2. We check whether each element elong of llong is
443
   satisfiable with lshort. If no, stop. If yes, we search to reduce
444
   the list. If elong => eshort_i, we can remove eshort_i from
445
   lshort. we can continue with this lshort shortened, lshort'; it is
446
   not necessary to add yet elong in lshort' since we already know
447
   rthat elong is somehow reduced with respect to other elements of
448
   llong. If eshort_i => elong, then we keep ehosrt_i in lshort and do
449
   not store elong.
450

    
451
   After iterating through llong, we have a shortened version of
452
   lshort + some elements of llong that have to be remembered. We add
453
   them to this new consolidated list. 
454

    
455
 *)
456

    
457
(* combine_guards ~fresh:Some(e,b) gl1 gl2 returns ok, gl with ok=true
458
   when (e=b) ang gl1 and gl2 is satisfiable and gl is a consilidated
459
   version of it.  *)
460
let combine_guards ?(fresh=None) gl1 gl2 =
461
  (* Filtering out trivial cases. More semantics ones would have to be
462
     addressed later *)
463
  let check_sat e = (* temp function before we clean the original one *)
464
    (* Format.eprintf "CheckSAT? %a@." (pp_guard_list pp_elem) e; *)
465
    let ok, _ = check_sat e in
466
    (* Format.eprintf "CheckSAT DONE@."; *)
467
    ok
468
  in
469
  let implies (e1,pn1) (e2,pn2) =
470
    let e2z e pn =
471
      match e with
472
        | IsInit -> if pn then is_init_z3e else neg_ze is_init_z3e
473
        | Expr e -> expr_to_z3_expr (if pn then e else (Corelang.push_negations ~neg:true e))
474
      in
475
    implies (e2z e1 pn1) (e2z e2 pn2)
476
  in
477
  let lshort, llong =
478
    if List.length gl1 > List.length gl2 then gl2, gl1 else gl1, gl2
479
  in
480
  let merge long short =
481
    let short, long_sel, ok = 
482
    List.fold_left (fun (short,long_sel, ok) long_e ->
483
        if not ok then
484
          [],[], false (* Propagating unsat case *)
485
        else if check_sat (long_e::short) then
486
          let short, keep_long_e =
487
            List.fold_left (fun (accu_short, keep_long_e) eshort_i ->
488
                if not keep_long_e then (* shorten the algo *)
489
                  eshort_i :: accu_short, false
490
                else (* keep_long_e = true in the following *)
491
                  if implies eshort_i long_e then
492
                    (* First case is trying to remove long_e!
493

    
494
                     Since short is already normalized, we can remove
495
                     long_e. If later long_e is stronger than another
496
                     element of short, then necessarily eshort_i =>
497
                     long_e ->
498
                     that_other_element_of_short. Contradiction. *)
499
                    eshort_i::accu_short, false
500
                  else if implies long_e eshort_i then 
501
                    (* removing eshort_i, keeping long_e. *)
502
                    accu_short, true
503
                  else (* Not comparable, keeping both *)
504
                    eshort_i::accu_short, true
505
              )
506
              ([],true) (* Initially we assume that we will keep long_e *)
507
              short
508
          in
509
          if keep_long_e then
510
            short, long_e::long_sel, true
511
          else
512
            short, long_sel, true
513
        else
514
          [],[],false
515
      ) (short, [], true) long
516
    in
517
    ok, long_sel@short
518
  in
519
  let ok, l = match fresh with
520
    | None -> true, []
521
    | Some g -> merge [g] []
522
  in
523
  if not ok then
524
    false, []
525
  else
526
    let ok, lshort = merge lshort l in
527
    if not ok then
528
      false, []
529
    else
530
      merge llong lshort
531
    
532

    
533
(* Encode "If gel1=posneg then gel2":
534
   - Compute the combination of guarded exprs in gel1 and gel2:
535
     - Each guarded_expr in gel1 is transformed as a guard: the
536
       expression is associated to posneg.
537
     - Existing guards in gel2 are concatenated to that list of guards
538
     - We keep expr in the ge of gel2 as the legitimate expression 
539
 *)
540
let concatenate_ge gel1 posneg gel2 =
541
  let l, all_invalid =
542
    List.fold_left (
543
        fun (accu, all_invalid) (g2,e2) ->
544
        List.fold_left (
545
            fun (accu, all_invalid) (g1,e1) ->
546
            (* Format.eprintf "@[<v 2>Combining guards: (%a=%b) AND [%a] AND [%a]@ "
547
             *  pp_elem e1
548
             *  posneg
549
             *  pp_guard_list g1
550
             *  pp_guard_list g2; *)
551

    
552
            let ok, gl = combine_guards ~fresh:(Some(e1,posneg)) g1 g2 in
553
            (* Format.eprintf "@]@ Result is [%a]@ "
554
             *   pp_guard_list gl; *)
555

    
556
            if ok then
557
              (gl, e2)::accu, false
558
            else (
559
              accu, all_invalid
560
            )
561
          ) (accu, all_invalid) gel1
562
      ) ([], true) gel2
563
  in
564
  not all_invalid, l
565

    
566
(* Transform the guard expressions ge = [gl1, e1; gl2, e2;...] as
567
   [gl1, e1=id; gl2, e2=id; ...]  *)
568
let mk_ge_eq_id ge id =
569
  List.map
570
    (fun (gl, g_e) ->
571
      gl,
572
      if id = "true" then
573
        g_e
574
      else
575
        match g_e with
576
        | Expr g_e ->
577
           if id = "false" then
578
             Expr (Corelang.push_negations ~neg:true g_e)
579
           else  
580
             let loc = g_e.expr_loc in
581
             Expr(Corelang.mk_eq loc
582
                    g_e
583
                    (Corelang.expr_of_ident id loc))
584
        | _ -> assert false
585
    )  ge 
586

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

    
703
(* Takes a list of guarded exprs (ge) and a guard
704
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.
705

    
706
When a given ge doesn't mention positively or negatively such guards, it is duplicated in both lists *)
707
let split_mdefs elem (mdefs: elem_guarded_expr list) =
708
  List.fold_left (
709
      fun (selected, left_out)
710
          ((guards, expr) as ge) ->
711
      (* select the element of guards that match the argument elem *)
712
      let sel, others_guards = List.partition (select_elem elem) guards in
713
      match sel with
714
      (* we extract the element from the list and add it to the
715
         appropriate list *)
716
      | [_, sel_status] ->
717
         if sel_status then
718
           (others_guards,expr)::selected, left_out
719
         else selected, (others_guards,expr)::left_out
720
      | [] -> (* no such guard exists, we have to duplicate the
721
              guard_expr in both lists *)
722
         ge::selected, ge::left_out
723
      | _ -> (
724
        Format.eprintf "@.Spliting list on elem %a.@.List:%a@."
725
          pp_elem elem
726
          (pp_mdefs pp_elem) mdefs;
727
        assert false (* more then one element selected. Should
728
                          not happen , or trival dead code like if
729
                              x then if not x then dead code *)
730
      )
731
    ) ([],[]) mdefs
732
    
733
let split_mem_defs
734
      (elem: element)
735
      (mem_defs: (ident * elem_guarded_expr list) list)
736
      :
737
      ((ident * elem_guarded_expr mdef_t) list) * ((ident * elem_guarded_expr mdef_t) list)
738
  
739
  =
740
  List.fold_right (fun (m,mdefs)
741
                       (accu_pos, accu_neg) ->
742
      let pos, neg =
743
        split_mdefs elem mdefs 
744
      in
745
      (m, pos)::accu_pos,
746
      (m, neg)::accu_neg
747
    ) mem_defs ([],[])
748

    
749

    
750
(* Split a list of mem_defs into init and step lists of guarded
751
   expressions per memory. *)
752
let split_init mem_defs =
753
  split_mem_defs IsInit mem_defs 
754

    
755
(* Previous version of the function: way too costly 
756
let pick_guard mem_defs : expr option =  
757
  let gel = List.flatten (List.map snd mem_defs) in
758
  let gl = List.flatten (List.map fst gel) in
759
  let all_guards =
760
    List.map (
761
        (* selecting guards and getting rid of boolean *)
762
        fun (e,b) ->
763
        match e with
764
        | Expr e -> e
765
        | _ -> assert false
766
      (* should have been filtered out
767
                                      yet *)
768
      ) gl
769
  in
770
  (* TODO , one could sort by occurence and provided the most common
771
     one *)
772
  try
773
  Some (List.hd all_guards)  
774
  with _ -> None
775
   *)
776

    
777
(* Returning the first non empty guard expression *)
778
let rec pick_guard mem_defs : expr option =
779
  match mem_defs with
780
  | [] -> None
781
  | (_, gel)::tl -> (
782
    let found =
783
      List.fold_left (fun found (g,_) ->
784
          if found = None then
785
            match g with
786
            | [] -> None
787
            | (Expr e, _)::_ -> Some e
788
            | (IsInit, _)::_ -> assert false (* should be removed already *)
789
          else
790
            found
791
        ) None gel
792
    in
793
    if found = None then pick_guard tl else found
794
  )
795
          
796

    
797
(* Transform a list of variable * guarded exprs into a list of guarded pairs (variable, expressions)
798
*)
799
let rec build_switch_sys
800
          (mem_defs : (Utils.ident * elem_guarded_expr list) list )
801
          prefix
802
        :
803
          ((expr * bool) list * (ident * expr) list ) list =
804
  if !seal_debug then
805
    report ~level:4 (fun fmt -> Format.fprintf fmt "@[<v 2>Build_switch with@ %a@]@."
806
                                  pp_all_defs
807
                                  mem_defs);
808
  (* if all mem_defs have empty guards, we are done, return prefix,
809
     mem_defs expr.
810

    
811
     otherwise pick a guard in one of the mem, eg (g, b) then for each
812
     other mem, one need to select the same guard g with the same
813
     status b, *)
814
  let res =
815
  if List.for_all (fun (m,mdefs) ->
816
         (* All defs are unguarded *)
817
         match mdefs with
818
         | [[], _] -> true (* Regular unguarded expression *)
819
         | [] -> true (* A unbalanced definition of the memory. Here
820
                         we have m_{k+1} -> m_k *)
821
         | _ -> false
822
       ) mem_defs
823
  then
824
    [prefix ,
825
     List.map (fun (m,gel) ->
826
         match gel with
827
         | [_,e] ->
828
            let e =
829
              match e with
830
              | Expr e -> e
831
              | _ -> assert false (* No IsInit expression *)
832
            in
833
            m,e
834
         | [] -> m, Corelang.expr_of_ident m Location.dummy_loc
835
         | _ -> assert false
836
       ) mem_defs]
837
  else
838
    (* Picking a guard *)
839
    let elem_opt : expr option = pick_guard mem_defs in
840
    match elem_opt with
841
      None -> (
842
       Format.eprintf "Issues picking guard in mem_defs: %a@." pp_all_defs mem_defs;
843
       assert false (* Otherwise the first case should have matched *)
844
    )
845
    | Some elem -> (
846
      report ~level:4 (fun fmt -> Format.fprintf fmt "selecting guard %a@." Printers.pp_expr elem);
847
      let pos, neg =
848
        split_mem_defs
849
          (Expr elem)
850
          mem_defs
851
      in
852
      report ~level:4 (fun fmt -> Format.fprintf fmt "split by guard done@.");
853
      
854
  (*    Format.eprintf "Selected item %a in@.%a@.POS=%a@.NEG=%a@."
855
        Printers.pp_expr elem
856
        pp_all_defs mem_defs
857
        pp_all_defs pos
858
        pp_all_defs neg
859
        ;
860
   *)
861
      (* Special cases to avoid useless computations: true, false conditions *)
862
      match elem.expr_desc with
863
      (*| Expr_ident "true"  ->   build_switch_sys pos prefix *)
864
      | Expr_const (Const_tag tag) when tag = tag_true
865
        ->   build_switch_sys pos prefix
866
      (*| Expr_ident "false" ->   build_switch_sys neg prefix *)
867
      | Expr_const (Const_tag tag) when tag = tag_false 
868
        ->   build_switch_sys neg prefix
869
      | _ -> (* Regular case *)
870
         report ~level:4 (fun fmt -> Format.fprintf fmt "Building both children branches@."); 
871
         (* let _ = (
872
          *     Format.eprintf "Expr is %a@." Printers.pp_expr elem;
873
          *     match elem.expr_desc with
874
          *     | Expr_const _ -> Format.eprintf "a const@."
875
          *                     
876
          *     | Expr_ident _ -> Format.eprintf "an ident@."
877
          *     | _ -> Format.eprintf "something else@."
878
          *   )
879
          * in *)
880
         let clean l =
881
           let l = List.map (fun (e,b) -> (Expr e), b) l in
882
           report ~level:4 (fun fmt -> Format.fprintf fmt "Checking satisfiability of %a@."
883
                                     (pp_guard_list pp_elem) l
884
             );
885
           let ok, l = check_sat l in
886
           let l = List.map (fun (e,b) -> deelem e, b) l in
887
           ok, l
888
         in
889
         let pos_prefix = (elem, true)::prefix in
890
         let neg_prefix = (elem, false)::prefix in
891
         report ~level:4 (fun fmt -> Format.fprintf fmt "Cleaning branches ...@."); 
892
         let ok_pos, pos_prefix = clean pos_prefix in         
893
         report ~level:4 (fun fmt -> Format.fprintf fmt "Cleaning branche pos done@."); 
894
         let ok_neg, neg_prefix = clean neg_prefix in
895
         report ~level:4 (fun fmt -> Format.fprintf fmt "Cleaning branche neg done@."); 
896
         report ~level:4 (fun fmt -> Format.fprintf fmt "Cleaning branches done@."); 
897
         report ~level:4 (fun fmt -> Format.fprintf fmt "Enforcing %a@." Printers.pp_expr elem);
898
         let ok_l = if ok_pos then build_switch_sys pos pos_prefix else [] in
899
         report ~level:4 (fun fmt -> Format.fprintf fmt "Enforcing not(%a)@." Printers.pp_expr elem);
900
         let nok_l = if ok_neg then build_switch_sys neg neg_prefix else [] in
901
         ok_l @ nok_l
902
    )
903
  in
904
    if !seal_debug then (
905
      report ~level:4 (fun fmt ->
906
          Format.fprintf fmt
907
            "@[<v 2>===> @[%t@ @]@]@ @]@ "
908
            (fun fmt -> List.iter (fun (gl,up) ->
909
                            Format.fprintf fmt "[@[%a@]] -> (%a)@ "
910
                              (pp_guard_list Printers.pp_expr) gl pp_up up) res);
911
          
912
    ));
913
    res
914
  
915

    
916
      
917
(* Take a normalized node and extract a list of switches: (cond,
918
   update) meaning "if cond then update" where update shall define all
919
   node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *)
920
let node_as_switched_sys consts (mems:var_decl list) nd =
921
  (* rescheduling node: has been scheduled already, no need to protect
922
     the call to schedule_node *)
923
  let nd_report = Scheduling.schedule_node nd in
924
  let schedule = nd_report.Scheduling_type.schedule in
925
  let eqs, auts = Corelang.get_node_eqs nd in
926
  assert (auts = []); (* Automata should be expanded by now *)
927
  let sorted_eqs, unused = Scheduling.sort_equations_from_schedule eqs schedule in
928
  let defs : (ident,  elem_guarded_expr list) Hashtbl.t = Hashtbl.create 13 in
929
  let add_def = add_def defs in
930

    
931
  let vars = Corelang.get_node_vars nd in
932
  (* Filtering out unused vars *)
933
  let vars = List.filter (fun v -> not (List.mem v.var_id unused)) vars in
934
  (* Registering all locals variables as Z3 predicates. Will be use to
935
     simplify the expansion *)
936
  Zustre_common.decl_sorts (); 
937
  let _ =
938
    List.iter (fun v ->
939
        let fdecl = Z3.FuncDecl.mk_func_decl_s
940
                      !ctx
941
                      v.var_id
942
                      []
943
                      (Zustre_common.type_to_sort v.var_type)
944
        in
945
        ignore (Zustre_common.register_fdecl v.var_id fdecl)
946
      ) vars
947
  in
948
  let _ =
949
    List.iter (fun c -> Hashtbl.add const_defs c.const_id c.const_value) consts
950
  in
951

    
952
  report ~level:4 (fun fmt -> Format.fprintf fmt "Computing definitions for equations@.%a@."
953
                            Printers.pp_node_eqs sorted_eqs
954
    );
955
  
956
  
957
  (* Registering node equations: identifying mem definitions and
958
     storing others in the "defs" hashtbl.
959

    
960
     Each assign is stored in a hash tbl as list of guarded
961
     expressions. The memory definition is also "rewritten" as such a
962
     list of guarded assigns.  *)
963
  report ~level:1 (fun fmt -> Format.fprintf fmt "registering all definitions in guarded form ...@.");
964
  let mem_defs, output_defs =
965
    List.fold_left (fun (accu_mems, accu_outputs) eq ->
966
        match eq.eq_lhs with
967
        | [vid] ->
968
           (* Only focus on memory definitions *)
969
           if List.exists (fun v -> v.var_id = vid) mems then 
970
             (
971
               match eq.eq_rhs.expr_desc with
972
               | Expr_pre def_m ->
973
                  report ~level:3 (fun fmt ->
974
                      Format.fprintf fmt "Preparing mem %s@." vid);
975
                  let def_vid = rewrite defs def_m in
976
                  report ~level:4 (fun fmt ->
977
                      Format.fprintf fmt "%s = %a@." vid
978
 (
979
        (Utils.fprintf_list ~sep:"@ "
980
           (pp_guard_expr pp_elem))) 
981
                        def_vid);
982
                  (vid, def_vid)::accu_mems, accu_outputs
983
               | _ -> assert false
984
             ) 
985
           else if List.exists (fun v -> v.var_id = vid) nd.node_outputs then (
986
             report ~level:3 (fun fmt ->
987
                 Format.fprintf fmt "Output variable %s@." vid);
988
             let def_vid = add_def vid eq.eq_rhs in
989
             accu_mems, (vid, def_vid)::accu_outputs
990
             
991
           )
992
           else
993
             (
994
               report ~level:3 (fun fmt ->
995
                   Format.fprintf fmt "Registering variable %s@." vid);
996
               let _ = add_def vid eq.eq_rhs in
997
               accu_mems, accu_outputs
998
             )
999
        | _ -> assert false (* should have been removed by normalization *)
1000
      ) ([], []) sorted_eqs
1001
  in
1002
  report ~level:1 (fun fmt -> Format.fprintf fmt "registering all definitions done@.");
1003

    
1004
  
1005
  report ~level:2 (fun fmt -> Format.fprintf fmt "Printing out (guarded) memories definitions (may takes time)@.");
1006
  (* Printing memories definitions *)
1007
  report ~level:3
1008
    (fun fmt ->
1009
      Format.fprintf fmt
1010
        "@[<v 0>%a@]@."
1011
        (Utils.fprintf_list ~sep:"@ "
1012
           (fun fmt (m,mdefs) ->
1013
             Format.fprintf fmt
1014
               "%s -> [@[<v 0>%a@] ]@ "
1015
               m
1016
               (Utils.fprintf_list ~sep:"@ "
1017
                  (pp_guard_expr pp_elem)) mdefs
1018
        ))
1019
        mem_defs);
1020
  (* Format.eprintf "Split init@."; *)
1021
  let init_defs, update_defs =
1022
    split_init mem_defs 
1023
  in
1024
  let init_out, update_out =
1025
    split_init output_defs
1026
  in
1027
  report ~level:3
1028
    (fun fmt ->
1029
      Format.fprintf fmt
1030
        "@[<v 0>Init:@ %a@]@."
1031
        (Utils.fprintf_list ~sep:"@ "
1032
           (fun fmt (m,mdefs) ->
1033
             Format.fprintf fmt
1034
               "%s -> @[<v 0>[%a@] ]@ "
1035
               m
1036
               (Utils.fprintf_list ~sep:"@ "
1037
                  (pp_guard_expr pp_elem)) mdefs
1038
        ))
1039
        init_defs);
1040
  report ~level:3
1041
    (fun fmt ->
1042
      Format.fprintf fmt
1043
        "@[<v 0>Step:@ %a@]@."
1044
        (Utils.fprintf_list ~sep:"@ "
1045
           (fun fmt (m,mdefs) ->
1046
             Format.fprintf fmt
1047
               "%s -> @[<v 0>[%a@] ]@ "
1048
               m
1049
               (Utils.fprintf_list ~sep:"@ "
1050
                  (pp_guard_expr pp_elem)) mdefs
1051
        ))
1052
        update_defs);
1053
  (* Format.eprintf "Build init@."; *)
1054
  
1055
  report ~level:1 (fun fmt -> Format.fprintf fmt "init/step as a switched system ...@.");
1056
  let sw_init= 
1057
    build_switch_sys init_defs []
1058
  in
1059
  (* Format.eprintf "Build step@."; *)
1060
  let sw_sys =
1061
    build_switch_sys update_defs []
1062
  in
1063
  report ~level:1 (fun fmt -> Format.fprintf fmt "init/step as a switched system ... done@.");
1064

    
1065
  report ~level:1 (fun fmt -> Format.fprintf fmt "output function as a switched system ...@.");
1066
  let init_out =
1067
    build_switch_sys init_out []
1068
  in
1069
  (* report ~level:1 (fun fmt -> Format.fprintf fmt "Build step out@."); *)
1070

    
1071
  let update_out =
1072
    build_switch_sys update_out []
1073
  in
1074
  report ~level:1 (fun fmt -> Format.fprintf fmt "output function as a switched system ... done@.");
1075

    
1076
  report ~level:1 (fun fmt -> Format.fprintf fmt "removing dead branches and merging remaining ...@.");
1077

    
1078
  let sw_init = clean_sys sw_init in
1079
  let sw_sys = clean_sys sw_sys in
1080
  let init_out = clean_sys init_out in
1081
  let update_out = clean_sys update_out in
1082
  report ~level:1 (fun fmt -> Format.fprintf fmt "removing dead branches and merging remaining ... done@.");
1083

    
1084
  (* Some additional checks *)
1085
  
1086
  if false then
1087
    begin
1088
      Format.eprintf "@.@.CHECKING!!!!!!!!!!!@.";
1089
      Format.eprintf "Any duplicate expression in guards?@.";
1090
      
1091
      let sw_sys =
1092
        List.map (fun (gl, up) ->
1093
            let gl = List.sort (fun (e,b) (e',b') ->
1094
                         let res = compare e.expr_tag e'.expr_tag in
1095
                         if res = 0 then (Format.eprintf "Same exprs?@.%a@.%a@.@."
1096
                                            Printers.pp_expr e
1097
                                            Printers.pp_expr e'
1098
                                         );
1099
                         res
1100
                       ) gl in
1101
            gl, up
1102
          ) sw_sys 
1103
      in
1104
      Format.eprintf "Another check for duplicates in guard list@.";
1105
      List.iter (fun (gl, _) ->
1106
          let rec aux hd l =
1107
            match l with
1108
              [] -> ()
1109
            | (e,b)::tl -> let others = hd@tl in
1110
                           List.iter (fun (e',_) -> if Corelang.is_eq_expr e e' then
1111
                                                      (Format.eprintf "Same exprs?@.%a@.%a@.@."
1112
                                                         Printers.pp_expr e
1113
                                                         Printers.pp_expr e'
1114
                             )) others;
1115
                           aux ((e,b)::hd) tl
1116
          in
1117
          aux [] gl
1118
        ) sw_sys;
1119
      Format.eprintf "Checking duplicates in updates@.";
1120
      let rec check_dup_up accu l =
1121
        match l with
1122
        | [] -> ()
1123
        | ((gl, up) as hd)::tl ->
1124
           let others = accu@tl in
1125
           List.iter (fun (gl',up') -> if up = up' then
1126
                                         Format.eprintf "Same updates?@.%a@.%a@.%a@.%a@.@."
1127

    
1128
                                           pp_gl_short gl
1129
                                           pp_up up
1130
                                           pp_gl_short gl'
1131
                                           pp_up up'
1132
                                       
1133
             ) others;
1134
           
1135
           
1136

    
1137
           check_dup_up (hd::accu) tl
1138
           
1139
      in
1140
      check_dup_up [] sw_sys;
1141
      let _ (* sw_sys *) =
1142
        List.sort (fun (gl1, _) (gl2, _) ->
1143
            let glid gl = List.map (fun (e,_) -> e.expr_tag) gl in
1144
            
1145
            let res = compare (glid gl1) (glid gl2) in
1146
            if res = 0 then Format.eprintf "Same guards?@.%a@.%a@.@."
1147
                              pp_gl_short gl1 pp_gl_short gl2
1148
            ;
1149
              res
1150

    
1151
          ) sw_sys
1152

    
1153
      in
1154
      ()
1155
    end;
1156
  
1157

    
1158
  (* Iter through the elements and gather them by updates *)
1159
  let process sys =
1160
    (* The map will associate to each update up the pair (set, set
1161
       list) where set is the share guards and set list a list of
1162
       disjunctive guards. Each set represents a conjunction of
1163
       expressions. *)
1164
    report ~level:3 (fun fmt -> Format.fprintf fmt "%t@."
1165
                                  (fun fmt -> List.iter (fun (gl,up) ->
1166
                                                  Format.fprintf fmt "[@[%a@]] -> (%a)@ "
1167
                                                    (pp_guard_list Printers.pp_expr) gl pp_up up) sw_init));
1168
    
1169
    (* We perform multiple pass to avoid errors *)
1170
    let map =
1171
      List.fold_left (fun map (gl,up) ->
1172
          (* creating a new set to describe gl *)
1173
          let new_set =
1174
            List.fold_left
1175
              (fun set g -> Guards.add g set)
1176
              Guards.empty
1177
              gl
1178
          in
1179
          (* updating the map with up -> new_set *)
1180
          if UpMap.mem up map then
1181
            let guard_set = UpMap.find up map in
1182
            UpMap.add up (new_set::guard_set) map
1183
          else
1184
            UpMap.add up [new_set] map
1185
        ) UpMap.empty sys
1186
    in
1187
    (* Processing the set of guards leading to the same update: return
1188
       conj, disj with conf is a set of guards, and disj a DNF, ie a
1189
       list of set of guards *)
1190
    let map =
1191
      UpMap.map (
1192
          fun guards ->
1193
          match guards with
1194
          | [] -> Guards.empty, [] (* Nothing *)
1195
          | [s]-> s, [] (* basic case *)
1196
          | hd::tl ->
1197
             let shared = List.fold_left (fun shared s -> Guards.inter shared s) hd tl in
1198
             let remaining = List.map (fun s -> Guards.diff s shared) guards in
1199
             (* If one of them is empty, we can remove the others, otherwise keep them *)
1200
             if List.exists Guards.is_empty remaining then
1201
               shared, []
1202
             else
1203
               shared, remaining
1204
        ) map
1205
    in
1206
  let rec mk_binop op l = match l with
1207
      [] -> assert false
1208
    | [e] -> e
1209
    | hd::tl -> Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl]
1210
  in
1211
  let gl_as_expr gl =
1212
    let gl = Guards.elements gl in
1213
    let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in 
1214
    match gl with
1215
      [] -> []
1216
    | [e] -> [export e]
1217
    | _ ->
1218
       [mk_binop "&&"
1219
          (List.map export gl)]
1220
  in
1221
  let rec clean_disj disj =
1222
    match disj with
1223
    | [] -> []
1224
    | [_] -> assert false (* A disjunction was a single case can be ignored *) 
1225
    | _::_::_ -> (
1226
      (* First basic version: producing a DNF One can later, (1)
1227
           simplify it with z3, or (2) build the compact tree with
1228
           maximum shared subexpression (and simplify it with z3) *)
1229
      let elems = List.fold_left (fun accu gl -> (gl_as_expr gl) @ accu) [] disj in
1230
      let or_expr = mk_binop "||" elems in
1231
      [or_expr]
1232

    
1233

    
1234
    (* TODO disj*)
1235
    (* get the item that occurs in most case *)
1236
    (* List.fold_left (fun accu s ->
1237
     *     List.fold_left (fun accu (e,b) ->
1238
     *         if List.mem_assoc (e.expr_tag, b)
1239
     *       ) accu (Guards.elements s)
1240
     *   ) [] disj *)
1241

    
1242
    )
1243
  in
1244
  if !seal_debug then Format.eprintf "Map: %i elements@ " (UpMap.cardinal map);
1245
  UpMap.fold (fun up (common, disj) accu ->
1246
      if !seal_debug then
1247
        report ~level:6 (fun fmt -> Format.fprintf fmt 
1248
          "Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@."
1249
          Guards.pp_short common
1250
          (fprintf_list ~sep:";@ " Guards.pp_long) disj
1251
          UpMap.pp up);
1252
      let disj = clean_disj disj in
1253
      let guard_expr = (gl_as_expr common)@disj in
1254
      
1255
      ((match guard_expr with
1256
        | [] -> None 
1257
        | _ -> Some (mk_binop "&&" guard_expr)), up)::accu
1258
    ) map []
1259
  
1260
    in
1261
    
1262
    
1263
    
1264
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_init:@.");
1265
    let sw_init = process sw_init in
1266
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_sys:@.");
1267
    let sw_sys = process sw_sys in
1268
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process init_out:@.");
1269
    let init_out = process init_out in
1270
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process update_out:@.");
1271
    let update_out = process update_out in
1272
    sw_init , sw_sys, init_out, update_out