Project

General

Profile

Download (43.2 KB) Statistics
| Branch: | Tag: | Revision:
1
open Lustre_types
2
open Utils
3
open Seal_utils
4
open Zustre_data
5
(* Access to Z3 context *)
6

    
7
(* Switched system extraction: expression are memoized *)
8
(*let expr_mem = Hashtbl.create 13*)
9

    
10
let add_init defs vid = Hashtbl.add defs vid [ [], IsInit ]
11

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

    
17
let is_init_name = "__is_init"
18

    
19
let const_defs = Hashtbl.create 13
20

    
21
let is_const id = Hashtbl.mem const_defs id
22

    
23
let is_enum_const id = Hashtbl.mem Zustre_data.const_tags id
24

    
25
let get_const id = Hashtbl.find const_defs id
26

    
27
(* expressions are only basic constructs here, no more ite, tuples, arrows, fby,
28
   ... *)
29

    
30
(* Set of hash to support memoization *)
31
let expr_hash : (expr * Utils.tag) list ref = ref []
32

    
33
let ze_hash : (Z3.Expr.expr, Utils.tag) Hashtbl.t = Hashtbl.create 13
34

    
35
let e_hash : (Utils.tag, Z3.Expr.expr) Hashtbl.t = Hashtbl.create 13
36

    
37
let pp_hash pp_key pp_v fmt h =
38
  Hashtbl.iter
39
    (fun key v -> Format.fprintf fmt "%a -> %a@ " pp_key key pp_v v)
40
    h
41

    
42
let pp_e_map fmt =
43
  List.iter
44
    (fun (e, t) -> Format.fprintf fmt "%i -> %a@ " t Printers.pp_expr e)
45
    !expr_hash
46

    
47
let pp_ze_hash fmt =
48
  pp_hash
49
    (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))
50
    Format.pp_print_int fmt ze_hash
51

    
52
let pp_e_hash fmt =
53
  pp_hash Format.pp_print_int
54
    (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))
55
    fmt e_hash
56

    
57
let mem_expr e =
58
  (* Format.eprintf "Searching for %a in map: @[<v 0>%t@]"
59
   *   Printers.pp_expr e
60
   *   pp_e_map; *)
61
  let res = List.exists (fun (e', _) -> Corelang.is_eq_expr e e') !expr_hash in
62
  (* Format.eprintf "found?%b@." res; *)
63
  res
64

    
65
let mem_zexpr ze = Hashtbl.mem ze_hash ze
66

    
67
let get_zexpr e =
68
  let _, uid = List.find (fun (e', _) -> Corelang.is_eq_expr e e') !expr_hash in
69
  (* Format.eprintf "found expr=%a id=%i@." Printers.pp_expr eref eref.expr_tag; *)
70
  Hashtbl.find e_hash uid
71

    
72
let get_expr ze =
73
  let uid = Hashtbl.find ze_hash ze in
74
  let e, _ = List.find (fun (_, t) -> t = uid) !expr_hash in
75
  e
76

    
77
let neg_ze z3e = Z3.Boolean.mk_not !ctx z3e
78

    
79
let is_init_z3e = Z3.Expr.mk_const_s !ctx is_init_name Zustre_common.bool_sort
80

    
81
let get_zid (ze : Z3.Expr.expr) : Utils.tag =
82
  try
83
    if Z3.Expr.equal ze is_init_z3e then -1
84
    else if Z3.Expr.equal ze (neg_ze is_init_z3e) then -2
85
    else Hashtbl.find ze_hash ze
86
  with _ ->
87
    Format.eprintf "Looking for ze %s in Hash %a" (Z3.Expr.to_string ze)
88
      (fun fmt hash ->
89
        Hashtbl.iter
90
          (fun ze uid ->
91
            Format.fprintf fmt "%s -> %i@ " (Z3.Expr.to_string ze) uid)
92
          hash)
93
      ze_hash;
94
    assert false
95

    
96
let add_expr =
97
  let cpt = ref 0 in
98
  fun e ze ->
99
    incr cpt;
100
    let uid = !cpt in
101
    expr_hash := (e, uid) :: !expr_hash;
102
    Hashtbl.add e_hash uid ze;
103
    Hashtbl.add ze_hash ze uid
104

    
105
let expr_to_z3_expr, zexpr_to_expr =
106
  (* List to store converted expression. *)
107
  (* let hash = ref [] in
108
   * let comp_expr e (e', _) = Corelang.is_eq_expr e e' in
109
   * let comp_zexpr ze (_, ze') = Z3.Expr.equal ze ze' in *)
110
  let rec e2ze e =
111
    (* Format.eprintf "e2ze %a: %a@." Printers.pp_expr e Types.print_ty
112
       e.expr_type; *)
113
    if mem_expr e then get_zexpr e
114
    else
115
      let res =
116
        match e.expr_desc with
117
        | Expr_const c ->
118
          let z3e = Zustre_common.horn_const_to_expr c in
119
          add_expr e z3e;
120
          z3e
121
        | Expr_ident id ->
122
          if is_const id then (
123
            let c = get_const id in
124
            let z3e = Zustre_common.horn_const_to_expr c in
125
            add_expr e z3e;
126
            z3e)
127
          else if is_enum_const id then (
128
            let z3e = Zustre_common.horn_tag_to_expr id in
129
            add_expr e z3e;
130
            z3e)
131
          else
132
            let fdecl_id = Zustre_common.get_fdecl id in
133
            let z3e = Z3.Expr.mk_const_f !ctx fdecl_id in
134
            add_expr e z3e;
135
            z3e
136
        | Expr_appl (id, args, None) (* no reset *) ->
137
          let el = Corelang.expr_list_of_expr args in
138

    
139
          let eltyp = List.map (fun e -> e.expr_type) el in
140
          let elv = List.map e2ze el in
141
          let z3e = Zustre_common.horn_basic_app id elv (eltyp, e.expr_type) in
142
          add_expr e z3e;
143
          z3e
144
        | Expr_tuple [ e ] ->
145
          let z3e = e2ze e in
146
          add_expr e z3e;
147
          z3e
148
        | _ ->
149
          (match e.expr_desc with
150
          | Expr_tuple _ ->
151
            Format.eprintf "tuple e2ze(%a)@.@?" Printers.pp_expr e
152
          | _ ->
153
            Format.eprintf "e2ze(%a)@.@?" Printers.pp_expr e);
154
          assert false
155
      in
156
      res
157
  in
158
  let rec ze2e ze =
159
    let ze_name ze =
160
      let fd = Z3.Expr.get_func_decl ze in
161
      Z3.Symbol.to_string (Z3.FuncDecl.get_name fd)
162
    in
163
    if mem_zexpr ze then None, Some (get_expr ze)
164
    else
165
      let open Corelang in
166
      let fd = Z3.Expr.get_func_decl ze in
167
      let zel = Z3.Expr.get_args ze in
168
      match Z3.Symbol.to_string (Z3.FuncDecl.get_name fd), zel with
169
      (* | var, [] -> (* should be in env *) get_e *)
170

    
171
      (* Extracting IsInit status *)
172
      | "not", [ ze ] when ze_name ze = is_init_name ->
173
        Some false, None
174
      | name, [] when name = is_init_name ->
175
        Some true, None
176
      (* Other constructs are converted to a lustre expression *)
177
      | op, _ -> (
178
        if Z3.Expr.is_numeral ze then
179
          let e =
180
            if Z3.Arithmetic.is_real ze then
181
              let s = Z3.Arithmetic.Real.numeral_to_string ze in
182
              (* Use to return a Num.ratio. Now Q.t *)
183
              let ratio = Z3.Arithmetic.Real.get_ratio ze in
184
              (* let num = Num.num_of_ratio ratio in let real = Real.create_num
185
                 num s in*)
186
              let real = Real.create_q ratio s in
187
              mkexpr Location.dummy_loc (Expr_const (Const_real real))
188
            else if Z3.Arithmetic.is_int ze then
189
              mkexpr Location.dummy_loc
190
                (Expr_const
191
                   (Const_int (Z.to_int (Z3.Arithmetic.Integer.get_big_int ze))))
192
            else if Z3.Expr.is_const ze then
193
              match Z3.Expr.to_string ze with
194
              | "true" ->
195
                mkexpr Location.dummy_loc (Expr_const (Const_tag tag_true))
196
              | "false" ->
197
                mkexpr Location.dummy_loc (Expr_const (Const_tag tag_false))
198
              | _ ->
199
                assert false
200
            else (
201
              Format.eprintf "Const err: %s %b@." (Z3.Expr.to_string ze)
202
                (Z3.Expr.is_const ze);
203
              assert false (* a numeral but no int nor real *))
204
          in
205
          None, Some e
206
        else
207
          match op with
208
          | "not" | "=" | "-" | "*" | "/" | ">=" | "<=" | ">" | "<" ->
209
            let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in
210
            None, Some (mkpredef_call Location.dummy_loc op args)
211
          | "+" ->
212
            (* Special treatment of + for 2+ args *)
213
            let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in
214
            let e =
215
              match args with
216
              | [] ->
217
                assert false
218
              | [ hd ] ->
219
                hd
220
              | e1 :: e2 :: tl ->
221
                let first_binary_and =
222
                  mkpredef_call Location.dummy_loc op [ e1; e2 ]
223
                in
224
                if tl = [] then first_binary_and
225
                else
226
                  List.fold_left
227
                    (fun e e_new ->
228
                      mkpredef_call Location.dummy_loc op [ e; e_new ])
229
                    first_binary_and tl
230
            in
231

    
232
            None, Some e
233
          | "and" | "or" -> (
234
            (* Special case since it can contain is_init pred *)
235
            let args = List.map (fun ze -> ze2e ze) zel in
236
            let op =
237
              if op = "and" then "&&"
238
              else if op = "or" then "||"
239
              else assert false
240
            in
241
            match args with
242
            | [] ->
243
              assert false
244
            | [ hd ] ->
245
              hd
246
            | hd :: tl ->
247
              List.fold_left
248
                (fun (is_init_opt1, expr_opt1) (is_init_opt2, expr_opt2) ->
249
                  ( (match is_init_opt1, is_init_opt2 with
250
                    | None, x | x, None ->
251
                      x
252
                    | Some _, Some _ ->
253
                      assert false),
254
                    match expr_opt1, expr_opt2 with
255
                    | None, x | x, None ->
256
                      x
257
                    | Some e1, Some e2 ->
258
                      Some (mkpredef_call Location.dummy_loc op [ e1; e2 ]) ))
259
                hd tl)
260
          | op ->
261
            let args = List.map (fun ze -> snd (ze2e ze)) zel in
262
            Format.eprintf "deal with op %s (nb args: %i). Expr is %s@." op
263
              (List.length args) (Z3.Expr.to_string ze);
264
            assert false)
265
  in
266
  (fun e -> e2ze e), fun ze -> ze2e ze
267

    
268
let zexpr_to_guard_list ze =
269
  let init_opt, expr_opt = zexpr_to_expr ze in
270
  (match init_opt with None -> [] | Some b -> [ IsInit, b ])
271
  @ match expr_opt with None -> [] | Some e -> [ Expr e, true ]
272

    
273
let simplify_neg_guard l =
274
  List.map
275
    (fun (g, posneg) ->
276
      match g with
277
      | IsInit ->
278
        g, posneg
279
      | Expr g ->
280
        if posneg then Expr (Corelang.push_negations g), true
281
        else
282
          (* Pushing the negation in the expression *)
283
          Expr (Corelang.push_negations ~neg:true g), true)
284
    l
285

    
286
(* TODO: individuellement demander si g1 => g2. Si c'est le cas, on peut ne
287
   garder que g1 dans la liste *)
288
(*****************************************************************)
289
(* Checking sat(isfiability) of an expression and simplifying it *)
290
(* All (free) variables have to be declared in the Z3 context    *)
291
(*****************************************************************)
292
(* let goal_simplify zl = let goal = Z3.Goal.mk_goal !ctx false false false in
293
   Z3.Goal.add goal zl; let goal' = Z3.Goal.simplify goal None in (*
294
   Format.eprintf "Goal before: %s@.Goal after : %s@.Sat? %s@." *
295
   (Z3.Goal.to_string goal) * (Z3.Goal.to_string goal') *
296
   (Z3.Solver.string_of_status status_res) * ; *) let ze = Z3.Goal.as_expr goal'
297
   in (* Format.eprintf "as an expr: %s@." (Z3.Expr.to_string ze); *)
298
   zexpr_to_guard_list ze *)
299

    
300
let implies =
301
  let ze_implies_hash : (Utils.tag * Utils.tag, bool) Hashtbl.t =
302
    Hashtbl.create 13
303
  in
304
  fun ze1 ze2 ->
305
    let ze1_uid = get_zid ze1 in
306
    let ze2_uid = get_zid ze2 in
307
    if Hashtbl.mem ze_implies_hash (ze1_uid, ze2_uid) then
308
      Hashtbl.find ze_implies_hash (ze1_uid, ze2_uid)
309
    else (
310
      if !seal_debug then
311
        report ~level:6 (fun fmt ->
312
            Format.fprintf fmt "Checking implication: %s => %s?@ "
313
              (Z3.Expr.to_string ze1) (Z3.Expr.to_string ze2));
314
      let solver = Z3.Solver.mk_simple_solver !ctx in
315
      let tgt = Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_implies !ctx ze1 ze2) in
316
      let res =
317
        try
318
          let status_res = Z3.Solver.check solver [ tgt ] in
319
          match status_res with
320
          | Z3.Solver.UNSATISFIABLE ->
321
            if !seal_debug then
322
              report ~level:6 (fun fmt -> Format.fprintf fmt "Valid!@ ");
323
            true
324
          | _ ->
325
            if !seal_debug then
326
              report ~level:6 (fun fmt ->
327
                  Format.fprintf fmt "not proved valid@ ");
328
            false
329
        with Zustre_common.UnknownFunction (_, msg) ->
330
          report ~level:1 msg;
331
          false
332
      in
333
      Hashtbl.add ze_implies_hash (ze1_uid, ze2_uid) res;
334
      res)
335

    
336
let rec simplify zl =
337
  match zl with
338
  | [] | [ _ ] ->
339
    zl
340
  | hd :: tl ->
341
    (* Forall e in tl, checking whether hd => e or e => hd, to keep hd in the
342
       first case and e in the second one *)
343
    let tl = simplify tl in
344
    let keep_hd, tl =
345
      List.fold_left
346
        (fun (keep_hd, accu) e ->
347
          if implies hd e then true, accu (* throwing away e *)
348
          else if implies e hd then false, e :: accu (* throwing away hd *)
349
          else keep_hd, e :: accu (* keeping both *))
350
        (true, []) tl
351
    in
352
    (* Format.eprintf "keep_hd?%b hd=%s, tl=[%a]@."
353
     *   keep_hd
354
     *   (Z3.Expr.to_string hd)
355
     * (Utils.fprintf_list ~sep:"; " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) tl
356
     *   ; *)
357
    if keep_hd then hd :: tl else tl
358

    
359
let check_sat ?(just_check = false) (l : elem_boolexpr guard) :
360
    bool * elem_boolexpr guard =
361
  (* Syntactic simplification *)
362
  if false then Format.eprintf "Before simplify: %a@." (pp_guard_list pp_elem) l;
363
  let l = simplify_neg_guard l in
364
  if false then (
365
    Format.eprintf "After simplify: %a@." (pp_guard_list pp_elem) l;
366
    Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " (pp_guard_list pp_elem) l);
367

    
368
  let solver = Z3.Solver.mk_simple_solver !ctx in
369
  try
370
    let zl =
371
      List.map
372
        (fun (e, posneg) ->
373
          let ze =
374
            match e with IsInit -> is_init_z3e | Expr e -> expr_to_z3_expr e
375
          in
376
          if posneg then ze else neg_ze ze)
377
        l
378
    in
379
    if false then
380
      Format.eprintf "Z3 exprs1: [%a]@ "
381
        (fprintf_list ~sep:",@ " (fun fmt e ->
382
             Format.fprintf fmt "%s" (Z3.Expr.to_string e)))
383
        zl;
384
    let zl = simplify zl in
385
    if false then
386
      Format.eprintf "Z3 exprs2: [%a]@ "
387
        (fprintf_list ~sep:",@ " (fun fmt e ->
388
             Format.fprintf fmt "%s" (Z3.Expr.to_string e)))
389
        zl;
390
    (* Format.eprintf "Calling Z3@."; *)
391
    let status_res = Z3.Solver.check solver zl in
392
    (* Format.eprintf "Z3 done@."; *)
393
    if false then
394
      Format.eprintf "Z3 status: %s@ @]@. "
395
        (Z3.Solver.string_of_status status_res);
396
    match status_res with
397
    | Z3.Solver.UNSATISFIABLE ->
398
      false, []
399
    | _ ->
400
      if false && just_check then true, l
401
      else
402
        (* TODO: may be reactivate but it may create new expressions *)
403
        (* let l = goal_simplify zl in *)
404
        let l =
405
          List.fold_left (fun accu ze -> accu @ zexpr_to_guard_list ze) [] zl
406
        in
407

    
408
        (* Format.eprintf "@.@[<v 2>Check_Sat:@ before: %a@ after: %a@. Goal
409
           precise? %b/%b@]@.@. " * pp_guard_list l pp_guard_list l' *
410
           (Z3.Goal.is_precise goal) * (Z3.Goal.is_precise goal'); *)
411
        true, l
412
  with Zustre_common.UnknownFunction (_, msg) ->
413
    report ~level:1 msg;
414
    true, l
415
(* keeping everything. *)
416

    
417
(**************************************************************)
418

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

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

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

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

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

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

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

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

    
539
            (* Format.eprintf "@]@ Result is [%a]@ " * pp_guard_list gl; *)
540
            if ok then (gl, e2) :: accu, false else accu, all_invalid)
541
          (accu, all_invalid) gel1)
542
      ([], true) gel2
543
  in
544
  not all_invalid, l
545

    
546
(* Transform the guard expressions ge = [gl1, e1; gl2, e2;...] as [gl1, e1=id;
547
   gl2, e2=id; ...] *)
548
let mk_ge_eq_id ge id =
549
  List.map
550
    (fun (gl, g_e) ->
551
      ( gl,
552
        if id = "true" then g_e
553
        else
554
          match g_e with
555
          | Expr g_e ->
556
            if id = "false" then Expr (Corelang.push_negations ~neg:true g_e)
557
            else
558
              let loc = g_e.expr_loc in
559
              Expr (Corelang.mk_eq loc g_e (Corelang.expr_of_ident id loc))
560
          | _ ->
561
            assert false ))
562
    ge
563

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

    
667
and add_def defs vid expr =
668
  (* Format.eprintf "Add_def: %s = %a@."
669
   *   vid
670
   *   Printers.pp_expr expr; *)
671
  let vid_defs = rewrite defs expr in
672
  (* Format.eprintf "-> @[<v 0>%a@]@."
673
   *   (Utils.fprintf_list ~sep:"@ "
674
   *      (pp_guard_expr pp_elem)) vid_defs; *)
675
  report ~level:6 (fun fmt ->
676
      Format.fprintf fmt "Add_def: %s = %a@. -> @[<v 0>%a@]@." vid
677
        Printers.pp_expr expr
678
        (Utils.fprintf_list ~sep:"@ " (pp_guard_expr pp_elem))
679
        vid_defs);
680
  Hashtbl.add defs vid vid_defs;
681
  vid_defs
682

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

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

    
711
let split_mem_defs (elem : element)
712
    (mem_defs : (ident * elem_guarded_expr list) list) :
713
    (ident * elem_guarded_expr mdef_t) list
714
    * (ident * elem_guarded_expr mdef_t) list =
715
  List.fold_right
716
    (fun (m, mdefs) (accu_pos, accu_neg) ->
717
      let pos, neg = split_mdefs elem mdefs in
718
      (m, pos) :: accu_pos, (m, neg) :: accu_neg)
719
    mem_defs ([], [])
720

    
721
(* Split a list of mem_defs into init and step lists of guarded expressions per
722
   memory. *)
723
let split_init mem_defs = split_mem_defs IsInit mem_defs
724

    
725
(* Previous version of the function: way too costly let pick_guard mem_defs :
726
   expr option = let gel = List.flatten (List.map snd mem_defs) in let gl =
727
   List.flatten (List.map fst gel) in let all_guards = List.map ( (* selecting
728
   guards and getting rid of boolean *) fun (e,b) -> match e with | Expr e -> e
729
   | _ -> assert false (* should have been filtered out yet *) ) gl in (* TODO ,
730
   one could sort by occurence and provided the most common one *) try Some
731
   (List.hd all_guards) with _ -> None *)
732

    
733
(* Returning the first non empty guard expression *)
734
let rec pick_guard mem_defs : expr option =
735
  match mem_defs with
736
  | [] ->
737
    None
738
  | (_, gel) :: tl ->
739
    let found =
740
      List.fold_left
741
        (fun found (g, _) ->
742
          if found = None then
743
            match g with
744
            | [] ->
745
              None
746
            | (Expr e, _) :: _ ->
747
              Some e
748
            | (IsInit, _) :: _ ->
749
              assert false (* should be removed already *)
750
          else found)
751
        None gel
752
    in
753
    if found = None then pick_guard tl else found
754

    
755
(* Transform a list of variable * guarded exprs into a list of guarded pairs
756
   (variable, expressions) *)
757
let rec build_switch_sys
758
    (mem_defs : (Utils.ident * elem_guarded_expr list) list) prefix :
759
    ((expr * bool) list * (ident * expr) list) list =
760
  if !seal_debug then
761
    report ~level:4 (fun fmt ->
762
        Format.fprintf fmt "@[<v 2>Build_switch with@ %a@]@." pp_all_defs
763
          mem_defs);
764
  (* if all mem_defs have empty guards, we are done, return prefix, mem_defs
765
     expr.
766

    
767
     otherwise pick a guard in one of the mem, eg (g, b) then for each other
768
     mem, one need to select the same guard g with the same status b, *)
769
  let res =
770
    if
771
      List.for_all
772
        (fun (_, mdefs) ->
773
          (* All defs are unguarded *)
774
          match mdefs with
775
          | [ ([], _) ] ->
776
            true (* Regular unguarded expression *)
777
          | [] ->
778
            true
779
          (* A unbalanced definition of the memory. Here we have m_{k+1} -> m_k *)
780
          | _ ->
781
            false)
782
        mem_defs
783
    then
784
      [
785
        ( prefix,
786
          List.map
787
            (fun (m, gel) ->
788
              match gel with
789
              | [ (_, e) ] ->
790
                let e =
791
                  match e with Expr e -> e | _ -> assert false
792
                  (* No IsInit expression *)
793
                in
794
                m, e
795
              | [] ->
796
                m, Corelang.expr_of_ident m Location.dummy_loc
797
              | _ ->
798
                assert false)
799
            mem_defs );
800
      ]
801
    else
802
      (* Picking a guard *)
803
      let elem_opt : expr option = pick_guard mem_defs in
804
      match elem_opt with
805
      | None ->
806
        Format.eprintf "Issues picking guard in mem_defs: %a@." pp_all_defs
807
          mem_defs;
808
        assert false (* Otherwise the first case should have matched *)
809
      | Some elem -> (
810
        report ~level:4 (fun fmt ->
811
            Format.fprintf fmt "selecting guard %a@." Printers.pp_expr elem);
812
        let pos, neg = split_mem_defs (Expr elem) mem_defs in
813
        report ~level:4 (fun fmt -> Format.fprintf fmt "split by guard done@.");
814

    
815
        (* Format.eprintf "Selected item %a in@.%a@.POS=%a@.NEG=%a@."
816
           Printers.pp_expr elem pp_all_defs mem_defs pp_all_defs pos
817
           pp_all_defs neg ; *)
818
        (* Special cases to avoid useless computations: true, false conditions *)
819
        match elem.expr_desc with
820
        (*| Expr_ident "true" -> build_switch_sys pos prefix *)
821
        | Expr_const (Const_tag tag) when tag = tag_true ->
822
          build_switch_sys pos prefix
823
        (*| Expr_ident "false" -> build_switch_sys neg prefix *)
824
        | Expr_const (Const_tag tag) when tag = tag_false ->
825
          build_switch_sys neg prefix
826
        | _ ->
827
          (* Regular case *)
828
          report ~level:4 (fun fmt ->
829
              Format.fprintf fmt "Building both children branches@.");
830
          (* let _ = ( * Format.eprintf "Expr is %a@." Printers.pp_expr elem; *
831
             match elem.expr_desc with * | Expr_const _ -> Format.eprintf "a
832
             const@." * * | Expr_ident _ -> Format.eprintf "an ident@." * | _ ->
833
             Format.eprintf "something else@." * ) * in *)
834
          let clean l =
835
            let l = List.map (fun (e, b) -> Expr e, b) l in
836
            report ~level:4 (fun fmt ->
837
                Format.fprintf fmt "Checking satisfiability of %a@."
838
                  (pp_guard_list pp_elem) l);
839
            let ok, l = check_sat l in
840
            let l = List.map (fun (e, b) -> deelem e, b) l in
841
            ok, l
842
          in
843
          let pos_prefix = (elem, true) :: prefix in
844
          let neg_prefix = (elem, false) :: prefix in
845
          report ~level:4 (fun fmt ->
846
              Format.fprintf fmt "Cleaning branches ...@.");
847
          let ok_pos, pos_prefix = clean pos_prefix in
848
          report ~level:4 (fun fmt ->
849
              Format.fprintf fmt "Cleaning branche pos done@.");
850
          let ok_neg, neg_prefix = clean neg_prefix in
851
          report ~level:4 (fun fmt ->
852
              Format.fprintf fmt "Cleaning branche neg done@.");
853
          report ~level:4 (fun fmt ->
854
              Format.fprintf fmt "Cleaning branches done@.");
855
          report ~level:4 (fun fmt ->
856
              Format.fprintf fmt "Enforcing %a@." Printers.pp_expr elem);
857
          let ok_l = if ok_pos then build_switch_sys pos pos_prefix else [] in
858
          report ~level:4 (fun fmt ->
859
              Format.fprintf fmt "Enforcing not(%a)@." Printers.pp_expr elem);
860
          let nok_l = if ok_neg then build_switch_sys neg neg_prefix else [] in
861
          ok_l @ nok_l)
862
  in
863
  if !seal_debug then
864
    report ~level:4 (fun fmt ->
865
        Format.fprintf fmt "@[<v 2>===> @[%t@ @]@]@ @]@ " (fun fmt ->
866
            List.iter
867
              (fun (gl, up) ->
868
                Format.fprintf fmt "[@[%a@]] -> (%a)@ "
869
                  (pp_guard_list Printers.pp_expr)
870
                  gl (pp_up Printers.pp_expr) up)
871
              res));
872
  res
873

    
874
let build_environement consts (mems : var_decl list) nd =
875
  Z3.Params.update_param_value !ctx "timeout" "10000";
876

    
877
  (* rescheduling node: has been scheduled already, no need to protect the call
878
     to schedule_node *)
879
  let nd_report = Scheduling.schedule_node nd in
880
  let schedule = nd_report.Scheduling_type.schedule in
881
  let eqs, auts = Corelang.get_node_eqs nd in
882
  assert (auts = []);
883
  (* Automata should be expanded by now *)
884
  let sorted_eqs, unused =
885
    Scheduling.sort_equations_from_schedule eqs schedule
886
  in
887
  let defs : (ident, elem_guarded_expr list) Hashtbl.t = Hashtbl.create 13 in
888
  let add_def = add_def defs in
889

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

    
910
  report ~level:4 (fun fmt ->
911
      Format.fprintf fmt "Computing definitions for equations@.%a@."
912
        Printers.pp_node_eqs sorted_eqs);
913

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

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

    
958
  report ~level:2 (fun fmt ->
959
      Format.fprintf fmt
960
        "Printing out (guarded) memories definitions (may takes time)@.");
961
  (* Printing memories definitions *)
962
  report ~level:3 (fun fmt ->
963
      Format.fprintf fmt "@[<v 0>%a@]@."
964
        (Utils.fprintf_list ~sep:"@ " (fun fmt (m, mdefs) ->
965
             Format.fprintf fmt "%s -> [@[<v 0>%a@] ]@ " m
966
               (Utils.fprintf_list ~sep:"@ " (pp_guard_expr pp_elem))
967
               mdefs))
968
        mem_defs);
969
  mem_defs, output_defs
970

    
971
(* Iter through the elements and gather them by updates *)
972
let merge_updates sys =
973
  (* The map will associate to each update up the pair (set, set list) where set
974
     is the share guards and set list a list of disjunctive guards. Each set
975
     represents a conjunction of expressions. *)
976

    
977
  (* We perform multiple pass to avoid errors *)
978
  let map =
979
    List.fold_left
980
      (fun map (gl, up) ->
981
        (* creating a new set to describe gl *)
982
        let new_set =
983
          List.fold_left (fun set g -> Guards.add g set) Guards.empty gl
984
        in
985
        (* updating the map with up -> new_set *)
986
        if UpMap.mem up map then
987
          let guard_set = UpMap.find up map in
988
          UpMap.add up (new_set :: guard_set) map
989
        else UpMap.add up [ new_set ] map)
990
      UpMap.empty sys
991
  in
992

    
993
  (* Processing the set of guards leading to the same update: return conj, disj
994
     with conf is a set of guards, and disj a DNF, ie a list of set of guards *)
995
  let map =
996
    UpMap.map
997
      (fun guards ->
998
        match guards with
999
        | [] ->
1000
          Guards.empty, [] (* Nothing *)
1001
        | [ s ] ->
1002
          s, [] (* basic case *)
1003
        | hd :: tl ->
1004
          let shared =
1005
            List.fold_left (fun shared s -> Guards.inter shared s) hd tl
1006
          in
1007
          let remaining = List.map (fun s -> Guards.diff s shared) guards in
1008
          (* If one of them is empty, we can remove the others, otherwise keep
1009
             them *)
1010
          if List.exists Guards.is_empty remaining then shared, []
1011
          else shared, remaining)
1012
      map
1013
  in
1014
  let rec mk_binop op l =
1015
    match l with
1016
    | [] ->
1017
      assert false
1018
    | [ e ] ->
1019
      e
1020
    | hd :: tl ->
1021
      Corelang.mkpredef_call hd.expr_loc op [ hd; mk_binop op tl ]
1022
  in
1023
  let gl_as_expr gl =
1024
    let gl = Guards.elements gl in
1025
    let export (e, b) = if b then e else Corelang.push_negations ~neg:true e in
1026
    match gl with
1027
    | [] ->
1028
      []
1029
    | [ e ] ->
1030
      [ export e ]
1031
    | _ ->
1032
      [ mk_binop "&&" (List.map export gl) ]
1033
  in
1034
  let clean_disj disj =
1035
    match disj with
1036
    | [] ->
1037
      []
1038
    | [ _ ] ->
1039
      assert false (* A disjunction with a single case can be ignored *)
1040
    | _ :: _ :: _ ->
1041
      (* First basic version: producing a DNF One can later, (1) simplify it
1042
         with z3, or (2) build the compact tree with maximum shared
1043
         subexpression (and simplify it with z3) *)
1044
      let elems =
1045
        List.fold_left (fun accu gl -> gl_as_expr gl @ accu) [] disj
1046
      in
1047
      let or_expr = mk_binop "||" elems in
1048
      [ or_expr ]
1049
    (* TODO disj*)
1050
    (* get the item that occurs in most case *)
1051
    (* List.fold_left (fun accu s ->
1052
     *     List.fold_left (fun accu (e,b) ->
1053
     *         if List.mem_assoc (e.expr_tag, b)
1054
     *       ) accu (Guards.elements s)
1055
     *   ) [] disj *)
1056
  in
1057
  if !seal_debug then Format.eprintf "Map: %i elements@ " (UpMap.cardinal map);
1058
  UpMap.fold
1059
    (fun up (common, disj) accu ->
1060
      if !seal_debug then
1061
        report ~level:6 (fun fmt ->
1062
            Format.fprintf fmt
1063
              "Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@."
1064
              Guards.pp_short common
1065
              (fprintf_list ~sep:";@ " Guards.pp_long)
1066
              disj UpMap.pp up);
1067
      let disj = clean_disj disj in
1068
      let guard_expr = gl_as_expr common @ disj in
1069

    
1070
      ( (match guard_expr with
1071
        | [] ->
1072
          None
1073
        | _ ->
1074
          Some (mk_binop "&&" guard_expr)),
1075
        up )
1076
      :: accu)
1077
    map []
1078

    
1079
(* Take a normalized node and extract a list of switches: (cond, update) meaning
1080
   "if cond then update" where update shall define all node memories. Everything
1081
   as to be expressed over inputs or memories, intermediate variables are
1082
   removed through inlining *)
1083
let node_as_switched_sys consts (mems : var_decl list) nd =
1084
  let mem_defs, output_defs = build_environement consts mems nd in
1085

    
1086
  let init_defs, update_defs = split_init mem_defs in
1087
  let init_out, update_out = split_init output_defs in
1088

    
1089
  report ~level:3 (fun fmt ->
1090
      Format.fprintf fmt "@[<v 0>Init:@ %a@ Step:@ %a@]@."
1091
        (pp_assign_map pp_elem) init_defs (pp_assign_map pp_elem) update_defs);
1092

    
1093
  report ~level:1 (fun fmt ->
1094
      Format.fprintf fmt "init/step as a switched system ...@.");
1095
  let sw_init = build_switch_sys init_defs [] in
1096
  let sw_sys = build_switch_sys update_defs [] in
1097
  report ~level:1 (fun fmt ->
1098
      Format.fprintf fmt "init/step as a switched system ... done@.");
1099

    
1100
  report ~level:1 (fun fmt ->
1101
      Format.fprintf fmt "output function as a switched system ...@.");
1102
  let init_out = build_switch_sys init_out [] in
1103
  let update_out = build_switch_sys update_out [] in
1104

    
1105
  report ~level:1 (fun fmt ->
1106
      Format.fprintf fmt "output function as a switched system ... done@.");
1107

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

    
1111
  let sw_init = clean_sys sw_init in
1112
  let sw_sys = clean_sys sw_sys in
1113
  let init_out = clean_sys init_out in
1114
  let update_out = clean_sys update_out in
1115

    
1116
  report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_init:@.");
1117
  let sw_init = merge_updates sw_init in
1118
  report ~level:3 (fun fmt -> Format.fprintf fmt "Process sw_sys:@.");
1119
  let sw_sys = merge_updates sw_sys in
1120
  report ~level:3 (fun fmt -> Format.fprintf fmt "Process init_out:@.");
1121
  let init_out = merge_updates init_out in
1122
  report ~level:3 (fun fmt -> Format.fprintf fmt "Process update_out:@.");
1123
  let update_out = merge_updates update_out in
1124
  report ~level:1 (fun fmt ->
1125
      Format.fprintf fmt
1126
        "removing dead branches and merging remaining ... done@.");
1127

    
1128
  sw_init, sw_sys, init_out, update_out
1129

    
1130
let fun_as_switched_sys consts nd =
1131
  let _, update_out = build_environement consts [] nd in
1132

    
1133
  report ~level:1 (fun fmt ->
1134
      Format.fprintf fmt "output function as a switched system ...@.");
1135
  let update_out = build_switch_sys update_out [] in
1136
  report ~level:1 (fun fmt ->
1137
      Format.fprintf fmt "output function as a switched system ... done@.");
1138

    
1139
  report ~level:1 (fun fmt ->
1140
      Format.fprintf fmt "removing dead branches and merging remaining ...@.");
1141
  let update_out = clean_sys update_out in
1142
  let update_out = merge_updates update_out in
1143
  report ~level:1 (fun fmt ->
1144
      Format.fprintf fmt
1145
        "removing dead branches and merging remaining ... done@.");
1146

    
1147
  update_out
1148

    
1149
(* Some code that was used to check for duplicate entries in guards.
1150

    
1151
   (* Some additional checks *)
1152

    
1153
   if false then begin Format.eprintf "@.@.CHECKING!!!!!!!!!!!@.";
1154
   Format.eprintf "Any duplicate expression in guards?@.";
1155

    
1156
   let sw_sys = List.map (fun (gl, up) -> let gl = List.sort (fun (e,b) (e',b')
1157
   -> let res = compare e.expr_tag e'.expr_tag in if res = 0 then
1158
   (Format.eprintf "Same exprs?@.%a@.%a@.@." Printers.pp_expr e Printers.pp_expr
1159
   e' ); res ) gl in gl, up ) sw_sys in Format.eprintf "Another check for
1160
   duplicates in guard list@."; List.iter (fun (gl, _) -> let rec aux hd l =
1161
   match l with [] -> () | (e,b)::tl -> let others = hd@tl in List.iter (fun
1162
   (e',_) -> if Corelang.is_eq_expr e e' then (Format.eprintf "Same
1163
   exprs?@.%a@.%a@.@." Printers.pp_expr e Printers.pp_expr e' )) others; aux
1164
   ((e,b)::hd) tl in aux [] gl ) sw_sys; Format.eprintf "Checking duplicates in
1165
   updates@."; let rec check_dup_up accu l = match l with | [] -> () | ((gl, up)
1166
   as hd)::tl -> let others = accu@tl in List.iter (fun (gl',up') -> if up = up'
1167
   then Format.eprintf "Same updates?@.%a@.%a@.%a@.%a@.@."
1168

    
1169
   pp_gl_short gl pp_up up pp_gl_short gl' pp_up up'
1170

    
1171
   ) others;
1172

    
1173
   check_dup_up (hd::accu) tl
1174

    
1175
   in check_dup_up [] sw_sys; let _ (* sw_sys *) = List.sort (fun (gl1, _) (gl2,
1176
   _) -> let glid gl = List.map (fun (e,_) -> e.expr_tag) gl in
1177

    
1178
   let res = compare (glid gl1) (glid gl2) in if res = 0 then Format.eprintf
1179
   "Same guards?@.%a@.%a@.@." pp_gl_short gl1 pp_gl_short gl2 ; res
1180

    
1181
   ) sw_sys
1182

    
1183
   in () end; *)
(3-3/6)