Project

General

Profile

Download (43.6 KB) Statistics
| Branch: | Tag: | Revision:
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 is_enum_const id = Hashtbl.mem Zustre_data.const_tags id  
24
let get_const id = Hashtbl.find const_defs id
25
                 
26
(* expressions are only basic constructs here, no more ite, tuples,
27
   arrows, fby, ... *)
28

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

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

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

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

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

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

    
398
        true, l
399
        
400
         
401
    )
402
         
403
  )
404
  with Zustre_common.UnknownFunction(id, msg) -> (
405
    report ~level:1 msg;
406
    true, l (* keeping everything. *)
407
  )
408
      
409
  
410

    
411

    
412
(**************************************************************)
413

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

    
423
      ;*)
424
        if sat then
425
        (List.map (fun (e, b) -> (deelem e, b)) guards', updates)::accu
426
      else
427
        accu
428
    )
429
    [] sys
430

    
431
(* Most costly function: has the be efficiently implemented.  All
432
   registered guards are initially produced by the call to
433
   combine_guards. We csan normalize the guards to ease the
434
   comparisons.
435

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

    
447
   After iterating through llong, we have a shortened version of
448
   lshort + some elements of llong that have to be remembered. We add
449
   them to this new consolidated list. 
450

    
451
 *)
452

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

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

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

    
548
            let ok, gl = combine_guards ~fresh:(Some(e1,posneg)) g1 g2 in
549
            (* Format.eprintf "@]@ Result is [%a]@ "
550
             *   pp_guard_list gl; *)
551

    
552
            if ok then
553
              (gl, e2)::accu, false
554
            else (
555
              accu, all_invalid
556
            )
557
          ) (accu, all_invalid) gel1
558
      ) ([], true) gel2
559
  in
560
  not all_invalid, l
561

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

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

    
699
(* Takes a list of guarded exprs (ge) and a guard
700
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.
701

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

    
745

    
746
(* Split a list of mem_defs into init and step lists of guarded
747
   expressions per memory. *)
748
let split_init mem_defs =
749
  split_mem_defs IsInit mem_defs 
750

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

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

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

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

    
902
      
903
(* Take a normalized node and extract a list of switches: (cond,
904
   update) meaning "if cond then update" where update shall define all
905
   node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *)
906
let node_as_switched_sys consts (mems:var_decl list) nd =
907
  (* rescheduling node: has been scheduled already, no need to protect
908
     the call to schedule_node *)
909
  let nd_report = Scheduling.schedule_node nd in
910
  let schedule = nd_report.Scheduling_type.schedule in
911
  let eqs, auts = Corelang.get_node_eqs nd in
912
  assert (auts = []); (* Automata should be expanded by now *)
913
  let sorted_eqs, unused = Scheduling.sort_equations_from_schedule eqs schedule in
914
  let defs : (ident,  elem_guarded_expr list) Hashtbl.t = Hashtbl.create 13 in
915
  let add_def = add_def defs in
916

    
917
  let vars = Corelang.get_node_vars nd in
918
  (* Filtering out unused vars *)
919
  let vars = List.filter (fun v -> not (List.mem v.var_id unused)) vars in
920
  (* Registering all locals variables as Z3 predicates. Will be use to
921
     simplify the expansion *)
922
  Zustre_common.decl_sorts (); 
923
  let _ =
924
    List.iter (fun v ->
925
        let fdecl = Z3.FuncDecl.mk_func_decl_s
926
                      !ctx
927
                      v.var_id
928
                      []
929
                      (Zustre_common.type_to_sort v.var_type)
930
        in
931
        ignore (Zustre_common.register_fdecl v.var_id fdecl)
932
      ) vars
933
  in
934
  let _ =
935
    List.iter (fun c -> Hashtbl.add const_defs c.const_id c.const_value) consts
936
  in
937

    
938
  report ~level:4 (fun fmt -> Format.fprintf fmt "Computing definitions for equations@.%a@."
939
                            Printers.pp_node_eqs sorted_eqs
940
    );
941
  
942
  
943
  (* Registering node equations: identifying mem definitions and
944
     storing others in the "defs" hashtbl.
945

    
946
     Each assign is stored in a hash tbl as list of guarded
947
     expressions. The memory definition is also "rewritten" as such a
948
     list of guarded assigns.  *)
949
  let mem_defs, output_defs =
950
    List.fold_left (fun (accu_mems, accu_outputs) eq ->
951
        match eq.eq_lhs with
952
        | [vid] ->
953
           (* Only focus on memory definitions *)
954
           if List.exists (fun v -> v.var_id = vid) mems then 
955
             (
956
               match eq.eq_rhs.expr_desc with
957
               | Expr_pre def_m ->
958
                  report ~level:3 (fun fmt ->
959
                      Format.fprintf fmt "Preparing mem %s@." vid);
960
                  let def_vid = rewrite defs def_m in
961
                  report ~level:4 (fun fmt ->
962
                      Format.fprintf fmt "%s = %a@." vid
963
 (
964
        (Utils.fprintf_list ~sep:"@ "
965
           (pp_guard_expr pp_elem))) 
966
                        def_vid);
967
                  (vid, def_vid)::accu_mems, accu_outputs
968
               | _ -> assert false
969
             ) 
970
           else if List.exists (fun v -> v.var_id = vid) nd.node_outputs then (
971
             report ~level:3 (fun fmt ->
972
                 Format.fprintf fmt "Output variable %s@." vid);
973
             let def_vid = add_def vid eq.eq_rhs in
974
             accu_mems, (vid, def_vid)::accu_outputs
975
             
976
           )
977
           else
978
             (
979
               report ~level:3 (fun fmt ->
980
                   Format.fprintf fmt "Registering variable %s@." vid);
981
               let _ = add_def vid eq.eq_rhs in
982
               accu_mems, accu_outputs
983
             )
984
        | _ -> assert false (* should have been removed by normalization *)
985
      ) ([], []) sorted_eqs
986
  in
987

    
988
  
989
  report ~level:2 (fun fmt -> Format.fprintf fmt "Printing out (guarded) memories definitions (may takes time)@.");
990
  (* Printing memories definitions *)
991
  report ~level:3
992
    (fun fmt ->
993
      Format.fprintf fmt
994
        "@[<v 0>%a@]@."
995
        (Utils.fprintf_list ~sep:"@ "
996
           (fun fmt (m,mdefs) ->
997
             Format.fprintf fmt
998
               "%s -> [@[<v 0>%a@] ]@ "
999
               m
1000
               (Utils.fprintf_list ~sep:"@ "
1001
                  (pp_guard_expr pp_elem)) mdefs
1002
        ))
1003
        mem_defs);
1004
  (* Format.eprintf "Split init@."; *)
1005
  let init_defs, update_defs =
1006
    split_init mem_defs 
1007
  in
1008
  let init_out, update_out =
1009
    split_init output_defs
1010
  in
1011
  report ~level:3
1012
    (fun fmt ->
1013
      Format.fprintf fmt
1014
        "@[<v 0>Init:@ %a@]@."
1015
        (Utils.fprintf_list ~sep:"@ "
1016
           (fun fmt (m,mdefs) ->
1017
             Format.fprintf fmt
1018
               "%s -> @[<v 0>[%a@] ]@ "
1019
               m
1020
               (Utils.fprintf_list ~sep:"@ "
1021
                  (pp_guard_expr pp_elem)) mdefs
1022
        ))
1023
        init_defs);
1024
  report ~level:3
1025
    (fun fmt ->
1026
      Format.fprintf fmt
1027
        "@[<v 0>Step:@ %a@]@."
1028
        (Utils.fprintf_list ~sep:"@ "
1029
           (fun fmt (m,mdefs) ->
1030
             Format.fprintf fmt
1031
               "%s -> @[<v 0>[%a@] ]@ "
1032
               m
1033
               (Utils.fprintf_list ~sep:"@ "
1034
                  (pp_guard_expr pp_elem)) mdefs
1035
        ))
1036
        update_defs);
1037
  (* Format.eprintf "Build init@."; *)
1038
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build init@.");
1039
  let sw_init= 
1040
    build_switch_sys init_defs []
1041
  in
1042
  (* Format.eprintf "Build step@."; *)
1043
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build step@.");
1044
  let sw_sys =
1045
    build_switch_sys update_defs []
1046
  in
1047

    
1048
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build init out@.");
1049
  let init_out =
1050
    build_switch_sys init_out []
1051
  in
1052
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build step out@.");
1053

    
1054
  let update_out =
1055
    build_switch_sys update_out []
1056
  in
1057

    
1058
  let sw_init = clean_sys sw_init in
1059
  let sw_sys = clean_sys sw_sys in
1060
  let init_out = clean_sys init_out in
1061
  let update_out = clean_sys update_out in
1062

    
1063
  (* Some additional checks *)
1064
  
1065
  if false then
1066
    begin
1067
      Format.eprintf "@.@.CHECKING!!!!!!!!!!!@.";
1068
      Format.eprintf "Any duplicate expression in guards?@.";
1069
      
1070
      let sw_sys =
1071
        List.map (fun (gl, up) ->
1072
            let gl = List.sort (fun (e,b) (e',b') ->
1073
                         let res = compare e.expr_tag e'.expr_tag in
1074
                         if res = 0 then (Format.eprintf "Same exprs?@.%a@.%a@.@."
1075
                                            Printers.pp_expr e
1076
                                            Printers.pp_expr e'
1077
                                         );
1078
                         res
1079
                       ) gl in
1080
            gl, up
1081
          ) sw_sys 
1082
      in
1083
      Format.eprintf "Another check for duplicates in guard list@.";
1084
      List.iter (fun (gl, _) ->
1085
          let rec aux hd l =
1086
            match l with
1087
              [] -> ()
1088
            | (e,b)::tl -> let others = hd@tl in
1089
                           List.iter (fun (e',_) -> if Corelang.is_eq_expr e e' then
1090
                                                      (Format.eprintf "Same exprs?@.%a@.%a@.@."
1091
                                                         Printers.pp_expr e
1092
                                                         Printers.pp_expr e'
1093
                             )) others;
1094
                           aux ((e,b)::hd) tl
1095
          in
1096
          aux [] gl
1097
        ) sw_sys;
1098
      Format.eprintf "Checking duplicates in updates@.";
1099
      let rec check_dup_up accu l =
1100
        match l with
1101
        | [] -> ()
1102
        | ((gl, up) as hd)::tl ->
1103
           let others = accu@tl in
1104
           List.iter (fun (gl',up') -> if up = up' then
1105
                                         Format.eprintf "Same updates?@.%a@.%a@.%a@.%a@.@."
1106

    
1107
                                           pp_gl_short gl
1108
                                           pp_up up
1109
                                           pp_gl_short gl'
1110
                                           pp_up up'
1111
                                       
1112
             ) others;
1113
           
1114
           
1115

    
1116
           check_dup_up (hd::accu) tl
1117
           
1118
      in
1119
      check_dup_up [] sw_sys;
1120
      let _ (* sw_sys *) =
1121
        List.sort (fun (gl1, _) (gl2, _) ->
1122
            let glid gl = List.map (fun (e,_) -> e.expr_tag) gl in
1123
            
1124
            let res = compare (glid gl1) (glid gl2) in
1125
            if res = 0 then Format.eprintf "Same guards?@.%a@.%a@.@."
1126
                              pp_gl_short gl1 pp_gl_short gl2
1127
            ;
1128
              res
1129

    
1130
          ) sw_sys
1131

    
1132
      in
1133
      ()
1134
    end;
1135
  
1136

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

    
1212

    
1213
    (* TODO disj*)
1214
    (* get the item that occurs in most case *)
1215
    (* List.fold_left (fun accu s ->
1216
     *     List.fold_left (fun accu (e,b) ->
1217
     *         if List.mem_assoc (e.expr_tag, b)
1218
     *       ) accu (Guards.elements s)
1219
     *   ) [] disj *)
1220

    
1221
    )
1222
  in
1223
  if !seal_debug then Format.eprintf "Map: %i elements@ " (UpMap.cardinal map);
1224
  UpMap.fold (fun up (common, disj) accu ->
1225
      if !seal_debug then
1226
        report ~level:6 (fun fmt -> Format.fprintf fmt 
1227
          "Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@."
1228
          Guards.pp_short common
1229
          (fprintf_list ~sep:";@ " Guards.pp_long) disj
1230
          UpMap.pp up);
1231
      let disj = clean_disj disj in
1232
      let guard_expr = (gl_as_expr common)@disj in
1233
      
1234
      ((match guard_expr with
1235
        | [] -> None 
1236
        | _ -> Some (mk_binop "&&" guard_expr)), up)::accu
1237
    ) map []
1238
  
1239
    in
1240
    
1241
    
1242
    
1243
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_init:@.");
1244
    let sw_init = process sw_init in
1245
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_sys:@.");
1246
    let sw_sys = process sw_sys in
1247
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process init_out:@.");
1248
    let init_out = process init_out in
1249
    report ~level:3 (fun fmt -> Format.fprintf fmt "Process update_out:@.");
1250
    let update_out = process update_out in
1251
    sw_init , sw_sys, init_out, update_out
(2-2/5)