Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (45.6 KB)

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

    
13

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

    
19
let is_init_name = "__is_init"
20

    
21
let const_defs = Hashtbl.create 13
22
let is_const id = Hashtbl.mem const_defs id
23
let 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
    (* Format.eprintf "e2ze %a: %a@." Printers.pp_expr e Types.print_ty e.expr_type; *)
95
    if mem_expr e then (
96
      get_zexpr e
97
    )
98
    else (
99
      let res =
100
        match e.expr_desc with
101
        | Expr_const c ->
102
           let z3e = Zustre_common.horn_const_to_expr c in
103
           add_expr e z3e;
104
           z3e
105
        | Expr_ident id -> (
106
          if is_const id then (
107
            let c = get_const id in
108
            let z3e = Zustre_common.horn_const_to_expr c in
109
            add_expr e z3e;
110
            z3e
111
          )
112
          else if is_enum_const id then (
113
            let z3e = Zustre_common.horn_tag_to_expr id in
114
            add_expr e z3e;
115
            z3e
116
          )
117
          else (
118
            let fdecl_id = Zustre_common.get_fdecl id in
119
            let z3e = Z3.Expr.mk_const_f !ctx fdecl_id in
120
            add_expr e z3e;
121
            z3e
122
          )
123
        )
124
        | Expr_appl (id,args, None) (* no reset *) ->
125
           let el = Corelang.expr_list_of_expr args in
126
           
127
           let eltyp = List.map (fun e -> e.expr_type) el in
128
           let elv = List.map e2ze el in
129
           let z3e = Zustre_common.horn_basic_app id elv (eltyp, e.expr_type) in
130
           add_expr e z3e;
131
           z3e
132
        | Expr_tuple [e] ->
133
           let z3e = e2ze e in
134
           add_expr e z3e;
135
           z3e
136
        | _ -> ( match e.expr_desc with Expr_tuple _ -> Format.eprintf "tuple e2ze(%a)@.@?" Printers.pp_expr e
137
                                      | _ -> Format.eprintf "e2ze(%a)@.@?" Printers.pp_expr e)
138
             ; assert false
139
      in
140
      res
141
    )
142
  in
143
  let rec ze2e ze =
144
    let ze_name ze =
145
      let fd = Z3.Expr.get_func_decl ze in
146
      Z3.Symbol.to_string (Z3.FuncDecl.get_name fd)
147
    in
148
    if mem_zexpr ze then
149
      None, Some (get_expr ze)
150
    else
151
      let open Corelang in
152
      let fd = Z3.Expr.get_func_decl ze in
153
      let zel = Z3.Expr.get_args ze in
154
      match Z3.Symbol.to_string (Z3.FuncDecl.get_name fd), zel with
155
      (*      | var, [] -> (* should be in env *) get_e *)
156

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

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

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

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

    
418

    
419
(**************************************************************)
420

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

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

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

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

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

    
458
 *)
459

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

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

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

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

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

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

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

    
707
(* Takes a list of guarded exprs (ge) and a guard
708
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.
709

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

    
753

    
754
(* Split a list of mem_defs into init and step lists of guarded
755
   expressions per memory. *)
756
let split_init mem_defs =
757
  split_mem_defs IsInit mem_defs 
758

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

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

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

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

    
920
let build_environement  consts (mems:var_decl list) nd =
921
    
922
  Z3.Params.update_param_value !ctx "timeout" "10000";
923

    
924
 
925
  (* rescheduling node: has been scheduled already, no need to protect
926
     the call to schedule_node *)
927
  let nd_report = Scheduling.schedule_node nd in
928
  let schedule = nd_report.Scheduling_type.schedule in
929
  let eqs, auts = Corelang.get_node_eqs nd in
930
  assert (auts = []); (* Automata should be expanded by now *)
931
  let sorted_eqs, unused = Scheduling.sort_equations_from_schedule eqs schedule in
932
  let defs : (ident,  elem_guarded_expr list) Hashtbl.t = Hashtbl.create 13 in
933
  let add_def = add_def defs in
934

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

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

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

    
1008
  
1009
  report ~level:2 (fun fmt -> Format.fprintf fmt "Printing out (guarded) memories definitions (may takes time)@.");
1010
  (* Printing memories definitions *)
1011
  report ~level:3
1012
    (fun fmt ->
1013
      Format.fprintf fmt
1014
        "@[<v 0>%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
        mem_defs);
1024
  mem_defs, output_defs 
1025

    
1026

    
1027
(* Iter through the elements and gather them by updates *)
1028
let merge_updates sys =
1029
  (* The map will associate to each update up the pair (set, set
1030
       list) where set is the share guards and set list a list of
1031
       disjunctive guards. Each set represents a conjunction of
1032
       expressions. *)
1033
  
1034
  (* We perform multiple pass to avoid errors *)
1035
  let map =
1036
    List.fold_left (fun map (gl,up) ->
1037
        (* creating a new set to describe gl *)
1038
        let new_set =
1039
          List.fold_left
1040
            (fun set g -> Guards.add g set)
1041
            Guards.empty
1042
            gl
1043
        in
1044
        (* updating the map with up -> new_set *)
1045
        if UpMap.mem up map then
1046
          let guard_set = UpMap.find up map in
1047
          UpMap.add up (new_set::guard_set) map
1048
        else
1049
          UpMap.add up [new_set] map
1050
      ) UpMap.empty sys
1051
  in
1052

    
1053
  (* Processing the set of guards leading to the same update: return
1054
       conj, disj with conf is a set of guards, and disj a DNF, ie a
1055
       list of set of guards *)
1056
  let map =
1057
    UpMap.map (
1058
        fun guards ->
1059
        match guards with
1060
        | [] -> Guards.empty, [] (* Nothing *)
1061
        | [s]-> s, [] (* basic case *)
1062
        | hd::tl ->
1063
           let shared = List.fold_left (fun shared s -> Guards.inter shared s) hd tl in
1064
           let remaining = List.map (fun s -> Guards.diff s shared) guards in
1065
           (* If one of them is empty, we can remove the others, otherwise keep them *)
1066
           if List.exists Guards.is_empty remaining then
1067
             shared, []
1068
           else
1069
             shared, remaining
1070
      ) map
1071
  in
1072
  let rec mk_binop op l = match l with
1073
      [] -> assert false
1074
    | [e] -> e
1075
    | hd::tl -> Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl]
1076
  in
1077
  let gl_as_expr gl =
1078
    let gl = Guards.elements gl in
1079
    let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in 
1080
    match gl with
1081
      [] -> []
1082
    | [e] -> [export e]
1083
    | _ ->
1084
       [mk_binop "&&"
1085
          (List.map export gl)]
1086
  in
1087
  let rec clean_disj disj =
1088
    match disj with
1089
    | [] -> []
1090
    | [_] -> assert false (* A disjunction with a single case can be ignored *) 
1091
    | _::_::_ -> (
1092
      (* First basic version: producing a DNF One can later, (1)
1093
           simplify it with z3, or (2) build the compact tree with
1094
           maximum shared subexpression (and simplify it with z3) *)
1095
      let elems = List.fold_left (fun accu gl -> (gl_as_expr gl) @ accu) [] disj in
1096
      let or_expr = mk_binop "||" elems in
1097
      [or_expr]
1098

    
1099

    
1100
    (* TODO disj*)
1101
    (* get the item that occurs in most case *)
1102
    (* List.fold_left (fun accu s ->
1103
     *     List.fold_left (fun accu (e,b) ->
1104
     *         if List.mem_assoc (e.expr_tag, b)
1105
     *       ) accu (Guards.elements s)
1106
     *   ) [] disj *)
1107

    
1108
    )
1109
  in
1110
  if !seal_debug then Format.eprintf "Map: %i elements@ " (UpMap.cardinal map);
1111
  UpMap.fold (fun up (common, disj) accu ->
1112
      if !seal_debug then
1113
        report ~level:6 (fun fmt -> Format.fprintf fmt 
1114
                                      "Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@."
1115
                                      Guards.pp_short common
1116
                                      (fprintf_list ~sep:";@ " Guards.pp_long) disj
1117
                                      UpMap.pp up);
1118
      let disj = clean_disj disj in
1119
      let guard_expr = (gl_as_expr common)@disj in
1120
      
1121
      ((match guard_expr with
1122
        | [] -> None 
1123
        | _ -> Some (mk_binop "&&" guard_expr)), up)::accu
1124
    ) map []
1125
  
1126
    
1127
    
1128

    
1129
(* Take a normalized node and extract a list of switches: (cond,
1130
   update) meaning "if cond then update" where update shall define all
1131
   node memories. Everything as to be expressed over inputs or
1132
   memories, intermediate variables are removed through inlining *)
1133
let node_as_switched_sys consts (mems:var_decl list) nd =
1134
  let mem_defs, output_defs = build_environement consts mems nd in
1135
  
1136
  let init_defs, update_defs = split_init mem_defs in
1137
  let init_out, update_out =   split_init output_defs in
1138
  
1139
  report ~level:3 (fun fmt -> Format.fprintf fmt "@[<v 0>Init:@ %a@ Step:@ %a@]@."
1140
                                (pp_assign_map pp_elem) init_defs
1141
                                (pp_assign_map pp_elem) update_defs);
1142
  
1143

    
1144
  report ~level:1 (fun fmt -> Format.fprintf fmt
1145
                                "init/step as a switched system ...@.");
1146
  let sw_init= build_switch_sys init_defs [] in
1147
  let sw_sys = build_switch_sys update_defs [] in
1148
  report ~level:1 (fun fmt -> Format.fprintf fmt
1149
                                "init/step as a switched system ... done@.");
1150

    
1151

    
1152
  report ~level:1 (fun fmt -> Format.fprintf fmt
1153
                                "output function as a switched system ...@.");
1154
  let init_out =   build_switch_sys init_out [] in
1155
  let update_out = build_switch_sys update_out [] in
1156
  
1157
  report ~level:1 (fun fmt -> Format.fprintf fmt
1158
                                "output function as a switched system ... done@.");
1159

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

    
1163
  let sw_init = clean_sys sw_init in
1164
  let sw_sys = clean_sys sw_sys in
1165
  let init_out = clean_sys init_out in
1166
  let update_out = clean_sys update_out in
1167

    
1168
  report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_init:@.");
1169
  let sw_init = merge_updates sw_init in
1170
  report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_sys:@.");
1171
  let sw_sys = merge_updates sw_sys in
1172
  report ~level:3 (fun fmt -> Format.fprintf fmt "Process init_out:@.");
1173
  let init_out = merge_updates init_out in
1174
  report ~level:3 (fun fmt -> Format.fprintf fmt "Process update_out:@.");
1175
  let update_out = merge_updates update_out in
1176
  report ~level:1 (fun fmt ->
1177
      Format.fprintf fmt "removing dead branches and merging remaining ... done@.");
1178

    
1179
  sw_init , sw_sys, init_out, update_out
1180

    
1181

    
1182
let fun_as_switched_sys consts  nd =
1183
  let _, update_out = build_environement consts [] nd in
1184

    
1185
  report ~level:1 (fun fmt -> Format.fprintf fmt
1186
                                "output function as a switched system ...@.");
1187
  let update_out = build_switch_sys update_out [] in
1188
  report ~level:1 (fun fmt -> Format.fprintf fmt
1189
                                "output function as a switched system ... done@.");
1190

    
1191
  report ~level:1 (fun fmt -> Format.fprintf fmt
1192
                                "removing dead branches and merging remaining ...@.");
1193
  let update_out = clean_sys update_out in
1194
  let update_out = merge_updates update_out in
1195
  report ~level:1 (fun fmt ->
1196
      Format.fprintf fmt "removing dead branches and merging remaining ... done@.");
1197

    
1198
  update_out
1199

    
1200

    
1201

    
1202

    
1203
                                
1204
                                (* Some code that was used to check for duplicate entries in guards.
1205

    
1206

    
1207
  (* Some additional checks *)
1208
  
1209
  if false then
1210
    begin
1211
      Format.eprintf "@.@.CHECKING!!!!!!!!!!!@.";
1212
      Format.eprintf "Any duplicate expression in guards?@.";
1213
      
1214
      let sw_sys =
1215
        List.map (fun (gl, up) ->
1216
            let gl = List.sort (fun (e,b) (e',b') ->
1217
                         let res = compare e.expr_tag e'.expr_tag in
1218
                         if res = 0 then (Format.eprintf "Same exprs?@.%a@.%a@.@."
1219
                                            Printers.pp_expr e
1220
                                            Printers.pp_expr e'
1221
                                         );
1222
                         res
1223
                       ) gl in
1224
            gl, up
1225
          ) sw_sys 
1226
      in
1227
      Format.eprintf "Another check for duplicates in guard list@.";
1228
      List.iter (fun (gl, _) ->
1229
          let rec aux hd l =
1230
            match l with
1231
              [] -> ()
1232
            | (e,b)::tl -> let others = hd@tl in
1233
                           List.iter (fun (e',_) -> if Corelang.is_eq_expr e e' then
1234
                                                      (Format.eprintf "Same exprs?@.%a@.%a@.@."
1235
                                                         Printers.pp_expr e
1236
                                                         Printers.pp_expr e'
1237
                             )) others;
1238
                           aux ((e,b)::hd) tl
1239
          in
1240
          aux [] gl
1241
        ) sw_sys;
1242
      Format.eprintf "Checking duplicates in updates@.";
1243
      let rec check_dup_up accu l =
1244
        match l with
1245
        | [] -> ()
1246
        | ((gl, up) as hd)::tl ->
1247
           let others = accu@tl in
1248
           List.iter (fun (gl',up') -> if up = up' then
1249
                                         Format.eprintf "Same updates?@.%a@.%a@.%a@.%a@.@."
1250

    
1251
                                           pp_gl_short gl
1252
                                           pp_up up
1253
                                           pp_gl_short gl'
1254
                                           pp_up up'
1255
                                       
1256
             ) others;
1257
           
1258
           
1259

    
1260
           check_dup_up (hd::accu) tl
1261
           
1262
      in
1263
      check_dup_up [] sw_sys;
1264
      let _ (* sw_sys *) =
1265
        List.sort (fun (gl1, _) (gl2, _) ->
1266
            let glid gl = List.map (fun (e,_) -> e.expr_tag) gl in
1267
            
1268
            let res = compare (glid gl1) (glid gl2) in
1269
            if res = 0 then Format.eprintf "Same guards?@.%a@.%a@.@."
1270
                              pp_gl_short gl1 pp_gl_short gl2
1271
            ;
1272
              res
1273

    
1274
          ) sw_sys
1275

    
1276
      in
1277
      ()
1278
    end;
1279
  
1280

    
1281
                                 *)