Project

General

Profile

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

    
15

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

    
21
let is_init_name = "__is_init"
22

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

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

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

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

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

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

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

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

    
420

    
421
(**************************************************************)
422

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

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

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

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

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

    
460
 *)
461

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

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

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

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

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

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

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

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

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

    
755

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

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

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

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

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

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

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

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

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

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

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

    
1028

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

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

    
1101

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

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

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

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

    
1153

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

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

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

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

    
1181
  sw_init , sw_sys, init_out, update_out
1182

    
1183

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

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

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

    
1200
  update_out
1201

    
1202

    
1203

    
1204

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

    
1208

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

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

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

    
1276
          ) sw_sys
1277

    
1278
      in
1279
      ()
1280
    end;
1281
  
1282

    
1283
                                 *)
(3-3/6)