Project

General

Profile

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

    
14

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

    
20
let is_init_name = "__is_init"
21

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

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

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

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

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

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

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

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

    
419

    
420
(**************************************************************)
421

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

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

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

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

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

    
459
 *)
460

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

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

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

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

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

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

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

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

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

    
754

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

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

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

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

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

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

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

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

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

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

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

    
1027

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

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

    
1100

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

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

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

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

    
1152

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

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

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

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

    
1180
  sw_init , sw_sys, init_out, update_out
1181

    
1182

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

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

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

    
1199
  update_out
1200

    
1201

    
1202

    
1203

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

    
1207

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

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

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

    
1275
          ) sw_sys
1276

    
1277
      in
1278
      ()
1279
    end;
1280
  
1281

    
1282
                                 *)
(3-3/6)