Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (45.8 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 s = Z3.Arithmetic.Real.numeral_to_string ze in
169
              (* Use to return a Num.ratio. Now Q.t *)
170
              let ratio = Z3.Arithmetic.Real.get_ratio ze in
171
              (*let num =  Num.num_of_ratio ratio in
172
              let real = Real.create_num num s in*)
173
              let real = Real.create_q ratio s in
174
              mkexpr
175
                Location.dummy_loc
176
                (Expr_const
177
                   (Const_real real))
178
            else if Z3.Arithmetic.is_int ze then
179
              mkexpr
180
                Location.dummy_loc
181
                (Expr_const
182
                   (Const_int 
183
                      (Z.to_int (Z3.Arithmetic.Integer.get_big_int ze))))
184
            else if Z3.Expr.is_const ze then
185
              match Z3.Expr.to_string ze with
186
              | "true" -> mkexpr Location.dummy_loc
187
                            (Expr_const (Const_tag (tag_true)))
188
              | "false" ->
189
                 mkexpr Location.dummy_loc
190
                   (Expr_const (Const_tag (tag_false)))
191
              | _ -> assert false
192
            else
193
              (
194
                Format.eprintf "Const err: %s %b@." (Z3.Expr.to_string ze) (Z3.Expr.is_const ze);
195
                assert false (* a numeral but no int nor real *)
196
              )
197
          in
198
          None, Some e
199
        else
200
          match op with
201
          | "not" | "=" | "-" | "*" | "/"
202
            | ">=" | "<=" | ">" | "<" 
203
            ->
204
             let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in
205
             None, Some (mkpredef_call Location.dummy_loc op args)
206
          | "+" -> ( (* Special treatment of + for 2+ args *)
207
            let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in
208
            let e = match args with
209
                [] -> assert false
210
              | [hd] -> hd
211
              | e1::e2::tl ->
212
                 let first_binary_and = mkpredef_call Location.dummy_loc op [e1;e2] in
213
                 if tl = [] then first_binary_and else
214
                   List.fold_left (fun e e_new ->
215
                       mkpredef_call Location.dummy_loc op [e;e_new]
216
                     ) first_binary_and tl
217
                 
218
            in
219
            None, Some e 
220
          )
221
          | "and" | "or" -> (
222
            (* Special case since it can contain is_init pred *)
223
            let args = List.map (fun ze -> ze2e ze) zel in
224
            let op = if op = "and" then "&&" else if op = "or" then "||" else assert false in 
225
            match args with
226
            | [] -> assert false
227
            | [hd] -> hd
228
            | hd::tl ->
229
               List.fold_left
230
                 (fun (is_init_opt1, expr_opt1) (is_init_opt2, expr_opt2) ->
231
                   (match is_init_opt1, is_init_opt2 with
232
                      None, x | x, None -> x
233
                      | Some _, Some _ -> assert false),
234
                   (match expr_opt1, expr_opt2 with
235
                    | None, x | x, None -> x
236
                    | Some e1, Some e2 ->
237
                       Some (mkpredef_call Location.dummy_loc op [e1; e2])
238
                 ))
239
                 hd tl 
240
          )
241
          | op -> 
242
             let args = List.map (fun ze ->  (snd (ze2e ze))) zel in
243
             Format.eprintf "deal with op %s (nb args: %i). Expr is %s@."  op (List.length args) (Z3.Expr.to_string ze); assert false
244
      )
245
  in
246
  (fun e -> e2ze e), (fun ze -> ze2e ze)
247

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

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

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

    
421

    
422
(**************************************************************)
423

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

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

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

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

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

    
461
 *)
462

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

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

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

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

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

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

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

    
710
(* Takes a list of guarded exprs (ge) and a guard
711
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.
712

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

    
756

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

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

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

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

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

    
923
let build_environement  consts (mems:var_decl list) nd =
924
    
925
  Z3.Params.update_param_value !ctx "timeout" "10000";
926

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

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

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

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

    
1011
  
1012
  report ~level:2 (fun fmt -> Format.fprintf fmt "Printing out (guarded) memories definitions (may takes time)@.");
1013
  (* Printing memories definitions *)
1014
  report ~level:3
1015
    (fun fmt ->
1016
      Format.fprintf fmt
1017
        "@[<v 0>%a@]@."
1018
        (Utils.fprintf_list ~sep:"@ "
1019
           (fun fmt (m,mdefs) ->
1020
             Format.fprintf fmt
1021
               "%s -> [@[<v 0>%a@] ]@ "
1022
               m
1023
               (Utils.fprintf_list ~sep:"@ "
1024
                  (pp_guard_expr pp_elem)) mdefs
1025
        ))
1026
        mem_defs);
1027
  mem_defs, output_defs 
1028

    
1029

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

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

    
1102

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

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

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

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

    
1154

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

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

    
1166
  let sw_init = clean_sys sw_init in
1167
  let sw_sys = clean_sys sw_sys in
1168
  let init_out = clean_sys init_out in
1169
  let update_out = clean_sys update_out in
1170

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

    
1182
  sw_init , sw_sys, init_out, update_out
1183

    
1184

    
1185
let fun_as_switched_sys consts  nd =
1186
  let _, update_out = build_environement consts [] nd in
1187

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

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

    
1201
  update_out
1202

    
1203

    
1204

    
1205

    
1206
                                
1207
                                (* Some code that was used to check for duplicate entries in guards.
1208

    
1209

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

    
1254
                                           pp_gl_short gl
1255
                                           pp_up up
1256
                                           pp_gl_short gl'
1257
                                           pp_up up'
1258
                                       
1259
             ) others;
1260
           
1261
           
1262

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

    
1277
          ) sw_sys
1278

    
1279
      in
1280
      ()
1281
    end;
1282
  
1283

    
1284
                                 *)