Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal / seal_extract.ml @ 81229f63

History | View | Annotate | Download (39.2 KB)

1
open Lustre_types
2
open Utils
3
open Seal_utils			
4
open Zustre_data (* Access to Z3 context *)
5
   
6

    
7
(* Switched system extraction: expression are memoized *)
8
(*let expr_mem = Hashtbl.create 13*)
9
             
10
type element = IsInit | Expr of expr
11
                              
12
type guard = (element * bool) list
13
type guarded_expr = guard * element
14
type mdef_t = guarded_expr list
15

    
16
let pp_elem fmt e =
17
  match e with
18
  | IsInit -> Format.fprintf fmt "init"
19
  | Expr e -> Format.fprintf fmt "%a" Printers.pp_expr e 
20

    
21
let pp_guard_list fmt gl =
22
  (fprintf_list ~sep:"; "
23
     (fun fmt (e,b) -> if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) fmt gl
24
  
25
let pp_guard_expr fmt (gl,e) =
26
  Format.fprintf fmt "%a -> %a"
27
    pp_guard_list  gl
28
    pp_elem e
29

    
30
let pp_mdefs fmt gel = fprintf_list ~sep:"@ " pp_guard_expr fmt gel
31

    
32
  
33
let add_init defs vid =
34
  Hashtbl.add defs vid [[], IsInit]
35

    
36
let deelem e =  match e with
37
    Expr e -> e
38
  | IsInit -> assert false (* Wasn't expecting isinit here: we are building values! *)
39

    
40
let is_eq_elem elem elem' =
41
  match elem, elem' with
42
  | IsInit, IsInit -> true
43
  | Expr e, Expr e' -> e = e' (*
44
     Corelang.is_eq_expr e e' *)
45
  | _ -> false
46

    
47
let select_elem elem (gelem, _) =
48
  is_eq_elem elem gelem
49

    
50

    
51
(**************************************************************)
52
(* Convert from Lustre expressions to Z3 expressions and back *)
53
(* All (free) variables have to be declared in the Z3 context *)
54
(**************************************************************)
55

    
56
let is_init_name = "__is_init"
57

    
58
let const_defs = Hashtbl.create 13
59
let is_const id = Hashtbl.mem const_defs id
60
let get_const id = Hashtbl.find const_defs id
61
                 
62
(* expressions are only basic constructs here, no more ite, tuples,
63
   arrows, fby, ... *)
64

    
65
(* Set of hash to support memoization *)
66
let expr_hash: (expr * Utils.tag) list ref = ref []
67
let ze_hash: (Z3.Expr.expr, Utils.tag) Hashtbl.t = Hashtbl.create 13
68
let e_hash: (Utils.tag, Z3.Expr.expr) Hashtbl.t = Hashtbl.create 13
69
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
70
let pp_e_map fmt = List.iter (fun (e,t) -> Format.fprintf fmt "%i -> %a@ " t Printers.pp_expr e) !expr_hash
71
let pp_ze_hash fmt = pp_hash
72
                      (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))
73
                      Format.pp_print_int
74
                      fmt
75
                      ze_hash
76
let pp_e_hash fmt = pp_hash
77
                      Format.pp_print_int
78
                      (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))
79
                      fmt
80
                      e_hash                              
81
let mem_expr e =
82
  (* Format.eprintf "Searching for %a in map: @[<v 0>%t@]"
83
   *   Printers.pp_expr e
84
   *   pp_e_map; *)
85
  let res = List.exists (fun (e',_) -> Corelang.is_eq_expr e e') !expr_hash in
86
  (* Format.eprintf "found?%b@." res; *)
87
  res
88
  
89
let mem_zexpr ze =
90
  Hashtbl.mem ze_hash ze
91
let get_zexpr e =
92
  let eref, uid = List.find (fun (e',_) -> Corelang.is_eq_expr e e') !expr_hash in
93
  (* Format.eprintf "found expr=%a id=%i@." Printers.pp_expr eref eref.expr_tag; *)
94
  Hashtbl.find e_hash uid
95
let get_expr ze =
96
  let uid = Hashtbl.find ze_hash ze in
97
  let e,_ = List.find (fun (e,t) -> t = uid) !expr_hash in
98
  e
99
  
100
let neg_ze z3e = Z3.Boolean.mk_not !ctx z3e 
101
let is_init_z3e =
102
  Z3.Expr.mk_const_s !ctx is_init_name  Zustre_common.bool_sort 
103

    
104
let get_zid (ze:Z3.Expr.expr) : Utils.tag = 
105
  try
106
    if Z3.Expr.equal ze is_init_z3e then -1 else
107
      if Z3.Expr.equal ze (neg_ze is_init_z3e) then -2 else
108
    Hashtbl.find ze_hash ze
109
  with _ -> (Format.eprintf "Looking for ze %s in Hash %a"
110
               (Z3.Expr.to_string ze)
111
               (fun fmt hash -> Hashtbl.iter (fun ze uid -> Format.fprintf fmt "%s -> %i@ " (Z3.Expr.to_string ze) uid) hash ) ze_hash;
112
             assert false)
113
let add_expr =
114
  let cpt = ref 0 in
115
  fun e ze ->
116
  incr cpt;
117
  let uid = !cpt in
118
  expr_hash := (e, uid)::!expr_hash;
119
  Hashtbl.add e_hash uid ze;
120
  Hashtbl.add ze_hash ze uid
121

    
122
  
123
let expr_to_z3_expr, zexpr_to_expr =
124
  (* List to store converted expression. *)
125
  (* let hash = ref [] in
126
   * let comp_expr e (e', _) = Corelang.is_eq_expr e e' in
127
   * let comp_zexpr ze (_, ze') = Z3.Expr.equal ze ze' in *)
128
  
129
  let rec e2ze e =
130
    if mem_expr e then (
131
      get_zexpr e
132
    )
133
    else (
134
      let res =
135
        match e.expr_desc with
136
        | Expr_const c ->
137
           let z3e = Zustre_common.horn_const_to_expr c in
138
           add_expr e z3e;
139
           z3e
140
        | Expr_ident id -> (
141
          if is_const id then (
142
            let c = get_const id in
143
            let z3e = Zustre_common.horn_const_to_expr c in
144
            add_expr e z3e;
145
            z3e
146
        )
147
        else (
148
          let fdecl_id = Zustre_common.get_fdecl id in
149
          let z3e = Z3.Expr.mk_const_f !ctx fdecl_id in
150
          add_expr e z3e;
151
          z3e
152
          )
153
        )
154
      | Expr_appl (id,args, None) (* no reset *) ->
155
         let z3e = Zustre_common.horn_basic_app id e2ze (Corelang.expr_list_of_expr args) in
156
         add_expr e z3e;
157
         z3e
158
      | Expr_tuple [e] ->
159
         let z3e = e2ze e in
160
         add_expr e z3e;
161
         z3e
162
      | _ -> ( match e.expr_desc with Expr_tuple _ -> Format.eprintf "tuple e2ze(%a)@.@?" Printers.pp_expr e
163
                                    | _ -> Format.eprintf "e2ze(%a)@.@?" Printers.pp_expr e)
164
                 ; assert false
165
      in
166
      res
167
    )
168
  in
169
  let rec ze2e ze =
170
    let ze_name ze =
171
      let fd = Z3.Expr.get_func_decl ze in
172
      Z3.Symbol.to_string (Z3.FuncDecl.get_name fd)
173
    in
174
    if mem_zexpr ze then
175
      None, Some (get_expr ze)
176
    else
177
      let open Corelang in
178
      let fd = Z3.Expr.get_func_decl ze in
179
      let zel = Z3.Expr.get_args ze in
180
      match Z3.Symbol.to_string (Z3.FuncDecl.get_name fd), zel with
181
      (*      | var, [] -> (* should be in env *) get_e *)
182

    
183
      (* Extracting IsInit status *)
184
      | "not", [ze] when ze_name ze = is_init_name ->
185
         Some false, None
186
      | name, [] when name = is_init_name -> Some true, None
187
      (* Other constructs are converted to a lustre expression *)
188
      | op, _ -> (
189
        
190
        
191
        if Z3.Expr.is_numeral ze then
192
          let e =
193
            if Z3.Arithmetic.is_real ze then
194
              let num =  Num.num_of_ratio (Z3.Arithmetic.Real.get_ratio ze) in
195
              let s = Z3.Arithmetic.Real.numeral_to_string ze in
196
              mkexpr
197
                Location.dummy_loc
198
                (Expr_const
199
                   (Const_real
200
                      (num, 0, s)))
201
            else if Z3.Arithmetic.is_int ze then
202
              mkexpr
203
                Location.dummy_loc
204
                (Expr_const
205
                   (Const_int
206
                      (Big_int.int_of_big_int (Z3.Arithmetic.Integer.get_big_int ze))))
207
            else if Z3.Expr.is_const ze then
208
              match Z3.Expr.to_string ze with
209
              | "true" -> mkexpr Location.dummy_loc
210
                            (Expr_const (Const_tag (tag_true)))
211
              | "false" ->
212
                 mkexpr Location.dummy_loc
213
                   (Expr_const (Const_tag (tag_false)))
214
              | _ -> assert false
215
            else
216
              (
217
                Format.eprintf "Const err: %s %b@." (Z3.Expr.to_string ze) (Z3.Expr.is_const ze);
218
                assert false (* a numeral but no int nor real *)
219
              )
220
          in
221
          None, Some e
222
        else
223
          match op with
224
          | "not" | "=" | "-" | "*" | "/"
225
            | ">=" | "<=" | ">" | "<" 
226
            ->
227
             let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in
228
             None, Some (mkpredef_call Location.dummy_loc op args)
229
          | "+" -> ( (* Special treatment of + for 2+ args *)
230
            let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in
231
            let e = match args with
232
                [] -> assert false
233
              | [hd] -> hd
234
              | e1::e2::tl ->
235
                 let first_binary_and = mkpredef_call Location.dummy_loc op [e1;e2] in
236
                 if tl = [] then first_binary_and else
237
                   List.fold_left (fun e e_new ->
238
                       mkpredef_call Location.dummy_loc op [e;e_new]
239
                     ) first_binary_and tl
240
                 
241
            in
242
            None, Some e 
243
          )
244
          | "and" | "or" -> (
245
            (* Special case since it can contain is_init pred *)
246
            let args = List.map (fun ze -> ze2e ze) zel in
247
            let op = if op = "and" then "&&" else if op = "or" then "||" else assert false in 
248
            match args with
249
            | [] -> assert false
250
            | [hd] -> hd
251
            | hd::tl ->
252
               List.fold_left
253
                 (fun (is_init_opt1, expr_opt1) (is_init_opt2, expr_opt2) ->
254
                   (match is_init_opt1, is_init_opt2 with
255
                      None, x | x, None -> x
256
                      | Some _, Some _ -> assert false),
257
                   (match expr_opt1, expr_opt2 with
258
                    | None, x | x, None -> x
259
                    | Some e1, Some e2 ->
260
                       Some (mkpredef_call Location.dummy_loc op [e1; e2])
261
                 ))
262
                 hd tl 
263
          )
264
          | op -> 
265
             let args = List.map (fun ze ->  (snd (ze2e ze))) zel in
266
             Format.eprintf "deal with op %s (nb args: %i). Expr is %s@."  op (List.length args) (Z3.Expr.to_string ze); assert false
267
      )
268
  in
269
  (fun e -> e2ze e), (fun ze -> ze2e ze)
270

    
271
               
272
let zexpr_to_guard_list ze =
273
  let init_opt, expr_opt = zexpr_to_expr ze in
274
  (match init_opt with
275
   | None -> []
276
   |Some b -> [IsInit, b]
277
  ) @ (match expr_opt with
278
       | None -> []
279
       | Some e -> [Expr e, true]
280
      )
281
                
282
               
283
let simplify_neg_guard l =
284
  List.map (fun (g,posneg) ->
285
      match g with
286
      | IsInit -> g, posneg
287
      | Expr g ->
288
          if posneg then
289
            Expr (Corelang.push_negations g),
290
            true
291
          else
292
            (* Pushing the negation in the expression *)
293
            Expr(Corelang.push_negations ~neg:true g),
294
            true
295
    ) l 
296

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

    
427
        true, l
428
        
429
         
430
    )
431
         
432
  )
433
  with Zustre_common.UnknownFunction(id, msg) -> (
434
    report ~level:1 msg;
435
    true, l (* keeping everything. *)
436
  )
437
      
438
  
439

    
440

    
441
(**************************************************************)
442

    
443
  
444
let clean_sys sys =
445
  List.fold_left (fun accu (guards, updates) ->
446
      let sat, guards' =  check_sat (List.map (fun (g, pn) -> Expr g, pn) guards) in
447
      (*Format.eprintf "Guard: %a@.Guard cleaned: %a@.Sat? %b@."
448
        (fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr))  guards
449
        (fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr))  guards'
450
        sat
451

    
452
      ;*)
453
        if sat then
454
        (List.map (fun (e, b) -> (deelem e, b)) guards', updates)::accu
455
      else
456
        accu
457
    )
458
    [] sys
459

    
460
(* Most costly function: has the be efficiently implemented.  All
461
   registered guards are initially produced by the call to
462
   combine_guards. We csan normalize the guards to ease the
463
   comparisons.
464

    
465
   We assume that gl1 and gl2 are already both satisfiable and in a
466
   kind of reduced form. Let lshort and llong be the short and long
467
   list of gl1, gl2. We check whether each element elong of llong is
468
   satisfiable with lshort. If no, stop. If yes, we search to reduce
469
   the list. If elong => eshort_i, we can remove eshort_i from
470
   lshort. we can continue with this lshort shortened, lshort'; it is
471
   not necessary to add yet elong in lshort' since we already know
472
   rthat elong is somehow reduced with respect to other elements of
473
   llong. If eshort_i => elong, then we keep ehosrt_i in lshort and do
474
   not store elong.
475

    
476
   After iterating through llong, we have a shortened version of
477
   lshort + some elements of llong that have to be remembered. We add
478
   them to this new consolidated list. 
479

    
480
 *)
481

    
482
(* combine_guards ~fresh:Some(e,b) gl1 gl2 returns ok, gl with ok=true
483
   when (e=b) ang gl1 and gl2 is satisfiable and gl is a consilidated
484
   version of it.  *)
485
let combine_guards ?(fresh=None) gl1 gl2 =
486
  (* Filtering out trivial cases. More semantics ones would have to be
487
     addressed later *)
488
  let check_sat e = (* temp function before we clean the original one *)
489
    let ok, _ = check_sat e in
490
    ok
491
  in
492
  let implies (e1,pn1) (e2,pn2) =
493
    let e2z e pn =
494
      match e with
495
        | IsInit -> if pn then is_init_z3e else neg_ze is_init_z3e
496
        | Expr e -> expr_to_z3_expr (if pn then e else (Corelang.push_negations ~neg:true e))
497
      in
498
    implies (e2z e1 pn1) (e2z e2 pn2)
499
  in
500
  let lshort, llong =
501
    if List.length gl1 > List.length gl2 then gl2, gl1 else gl1, gl2
502
  in
503
  let merge long short =
504
    let short, long_sel, ok = 
505
    List.fold_left (fun (short,long_sel, ok) long_e ->
506
        if not ok then
507
          [],[], false (* Propagating unsat case *)
508
        else if check_sat (long_e::short) then
509
          let short, keep_long_e =
510
            List.fold_left (fun (accu_short, keep_long_e) eshort_i ->
511
                if not keep_long_e then (* shorten the algo *)
512
                  eshort_i :: accu_short, false
513
                else (* keep_long_e = true in the following *)
514
                  if implies eshort_i long_e then
515
                    (* First case is trying to remove long_e!
516

    
517
                     Since short is already normalized, we can remove
518
                     long_e. If later long_e is stronger than another
519
                     element of short, then necessarily eshort_i =>
520
                     long_e ->
521
                     that_other_element_of_short. Contradiction. *)
522
                    eshort_i::accu_short, false
523
                  else if implies long_e eshort_i then 
524
                    (* removing eshort_i, keeping long_e. *)
525
                    accu_short, true
526
                  else (* Not comparable, keeping both *)
527
                    eshort_i::accu_short, true
528
              )
529
              ([],true) (* Initially we assume that we will keep long_e *)
530
              short
531
          in
532
          if keep_long_e then
533
            short, long_e::long_sel, true
534
          else
535
            short, long_sel, true
536
        else
537
          [],[],false
538
      ) (short, [], true) long
539
    in
540
    ok, long_sel@short
541
  in
542
  let ok, l = match fresh with
543
    | None -> true, []
544
    | Some g -> merge [g] []
545
  in
546
  if not ok then
547
    false, []
548
  else
549
    let ok, lshort = merge lshort l in
550
    if not ok then
551
      false, []
552
    else
553
      merge llong lshort
554
    
555

    
556
(* Encode "If gel1=posneg then gel2":
557
   - Compute the combination of guarded exprs in gel1 and gel2:
558
     - Each guarded_expr in gel1 is transformed as a guard: the
559
       expression is associated to posneg.
560
     - Existing guards in gel2 are concatenated to that list of guards
561
     - We keep expr in the ge of gel2 as the legitimate expression 
562
 *)
563
let concatenate_ge gel1 posneg gel2 =
564
  let l, all_invalid =
565
    List.fold_left (
566
        fun (accu, all_invalid) (g2,e2) ->
567
        List.fold_left (
568
            fun (accu, all_invalid) (g1,e1) ->
569
            (* Format.eprintf "@[<v 2>Combining guards: (%a=%b) AND [%a] AND [%a]@ "
570
             *  pp_elem e1
571
             *  posneg
572
             *  pp_guard_list g1
573
             *  pp_guard_list g2; *)
574

    
575
            let ok, gl = combine_guards ~fresh:(Some(e1,posneg)) g1 g2 in
576
            (* Format.eprintf "@]@ Result is [%a]@ "
577
             *   pp_guard_list gl; *)
578

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

    
676
(* Takes a list of guarded exprs (ge) and a guard
677
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.
678

    
679
When a given ge doesn't mention positively or negatively such guards, it is duplicated in both lists *)
680
let split_mdefs elem (mdefs: guarded_expr list) =
681
  List.fold_left (
682
      fun (selected, left_out)
683
          ((guards, expr) as ge) ->
684
      (* select the element of guards that match the argument elem *)
685
      let sel, others_guards = List.partition (select_elem elem) guards in
686
      match sel with
687
      (* we extract the element from the list and add it to the
688
         appropriate list *)
689
      | [_, sel_status] ->
690
         if sel_status then
691
           (others_guards,expr)::selected, left_out
692
         else selected, (others_guards,expr)::left_out
693
      | [] -> (* no such guard exists, we have to duplicate the
694
              guard_expr in both lists *)
695
         ge::selected, ge::left_out
696
      | _ -> (
697
        Format.eprintf "@.Spliting list on elem %a.@.List:%a@."
698
          pp_elem elem
699
          pp_mdefs mdefs;
700
        assert false (* more then one element selected. Should
701
                          not happen , or trival dead code like if
702
                              x then if not x then dead code *)
703
      )
704
    ) ([],[]) mdefs
705
    
706
let split_mem_defs
707
      (elem: element)
708
      (mem_defs: (ident * guarded_expr list) list)
709
      :
710
      ((ident * mdef_t) list) * ((ident * mdef_t) list)
711
  
712
  =
713
  List.fold_right (fun (m,mdefs)
714
                       (accu_pos, accu_neg) ->
715
      let pos, neg =
716
        split_mdefs elem mdefs 
717
      in
718
      (m, pos)::accu_pos,
719
      (m, neg)::accu_neg
720
    ) mem_defs ([],[])
721

    
722

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

    
728
(* Previous version of the function: way too costly 
729
let pick_guard mem_defs : expr option =  
730
  let gel = List.flatten (List.map snd mem_defs) in
731
  let gl = List.flatten (List.map fst gel) in
732
  let all_guards =
733
    List.map (
734
        (* selecting guards and getting rid of boolean *)
735
        fun (e,b) ->
736
        match e with
737
        | Expr e -> e
738
        | _ -> assert false
739
      (* should have been filtered out
740
                                      yet *)
741
      ) gl
742
  in
743
  (* TODO , one could sort by occurence and provided the most common
744
     one *)
745
  try
746
  Some (List.hd all_guards)  
747
  with _ -> None
748
   *)
749

    
750
(* Returning the first non empty guard expression *)
751
let rec pick_guard mem_defs : expr option =
752
  match mem_defs with
753
  | [] -> None
754
  | (_, gel)::tl -> (
755
    let found =
756
      List.fold_left (fun found (g,_) ->
757
          if found = None then
758
            match g with
759
            | [] -> None
760
            | (Expr e, _)::_ -> Some e
761
            | (IsInit, _)::_ -> assert false (* should be removed already *)
762
          else
763
            found
764
        ) None gel
765
    in
766
    if found = None then pick_guard tl else found
767
  )
768
          
769

    
770
(* Transform a list of variable * guarded exprs into a list of guarded pairs (variable, expressions)
771
*)
772
let rec build_switch_sys
773
          (mem_defs : (Utils.ident * guarded_expr list) list )
774
          prefix
775
        :
776
          ((expr * bool) list * (ident * expr) list ) list =
777
  (* if all mem_defs have empty guards, we are done, return prefix,
778
     mem_defs expr.
779

    
780
     otherwise pick a guard in one of the mem, eg (g, b) then for each
781
     other mem, one need to select the same guard g with the same
782
     status b, *)
783
  if List.for_all (fun (m,mdefs) ->
784
         (* All defs are unguarded *)
785
         match mdefs with
786
         | [[], _] -> true
787
         | _ -> false
788
       ) mem_defs
789
  then
790
    [prefix ,
791
     List.map (fun (m,gel) ->
792
         match gel with
793
         | [_,e] ->
794
            let e =
795
              match e with
796
              | Expr e -> e
797
              | _ -> assert false (* No IsInit expression *)
798
            in
799
            m,e
800
         | _ -> assert false
801
       ) mem_defs]
802
  else
803
    (* Picking a guard *)
804
    let elem_opt : expr option = pick_guard mem_defs in
805
    match elem_opt with
806
      None -> []
807
    | Some elem -> (
808
      let pos, neg =
809
        split_mem_defs
810
          (Expr elem)
811
          mem_defs
812
      in
813
      (* Special cases to avoid useless computations: true, false conditions *)
814
      match elem.expr_desc with
815
      | Expr_ident "true"  ->   build_switch_sys pos prefix
816
      | Expr_const (Const_tag tag) when tag = Corelang.tag_true
817
        ->   build_switch_sys pos prefix
818
      | Expr_ident "false" ->   build_switch_sys neg prefix
819
      | Expr_const (Const_tag tag) when tag = Corelang.tag_false 
820
        ->   build_switch_sys neg prefix
821
      | _ -> (* Regular case *)
822
         (* let _ = (
823
          *     Format.eprintf "Expr is %a@." Printers.pp_expr elem;
824
          *     match elem.expr_desc with
825
          *     | Expr_const _ -> Format.eprintf "a const@."
826
          *                     
827
          *     | Expr_ident _ -> Format.eprintf "an ident@."
828
          *     | _ -> Format.eprintf "something else@."
829
          *   )
830
          * in *)
831
         let clean l =
832
           let l = List.map (fun (e,b) -> (Expr e), b) l in
833
           let ok, l = check_sat l in
834
           let l = List.map (fun (e,b) -> deelem e, b) l in
835
           ok, l
836
         in
837
         let pos_prefix = (elem, true)::prefix in
838
         let neg_prefix = (elem, false)::prefix in
839
         let ok_pos, pos_prefix = clean pos_prefix in         
840
         let ok_neg, neg_prefix = clean neg_prefix in         
841
         (if ok_pos then build_switch_sys pos pos_prefix else [])
842
         @
843
           (if ok_neg then build_switch_sys neg neg_prefix else [])
844
    )
845

    
846

    
847
      
848
(* Take a normalized node and extract a list of switches: (cond,
849
   update) meaning "if cond then update" where update shall define all
850
   node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *)
851
let node_as_switched_sys consts (mems:var_decl list) nd =
852
  (* rescheduling node: has been scheduled already, no need to protect
853
     the call to schedule_node *)
854
  let nd_report = Scheduling.schedule_node nd in
855
  let schedule = nd_report.Scheduling_type.schedule in
856
  let eqs, auts = Corelang.get_node_eqs nd in
857
  assert (auts = []); (* Automata should be expanded by now *)
858
  let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in
859
  let defs : (ident,  guarded_expr list) Hashtbl.t = Hashtbl.create 13 in
860
  let add_def = add_def defs in
861

    
862
  let vars = Corelang.get_node_vars nd in
863
  (* Registering all locals variables as Z3 predicates. Will be use to
864
     simplify the expansion *) 
865
  let _ =
866
    List.iter (fun v ->
867
        let fdecl = Z3.FuncDecl.mk_func_decl_s
868
                      !ctx
869
                      v.var_id
870
                      []
871
                      (Zustre_common.type_to_sort v.var_type)
872
        in
873
        ignore (Zustre_common.register_fdecl v.var_id fdecl)
874
      ) vars
875
  in
876
  let _ =
877
    List.iter (fun c -> Hashtbl.add const_defs c.const_id c.const_value) consts
878
  in
879

    
880
  
881
  (* Registering node equations: identifying mem definitions and
882
     storing others in the "defs" hashtbl.
883

    
884
     Each assign is stored in a hash tbl as list of guarded
885
     expressions. The memory definition is also "rewritten" as such a
886
     list of guarded assigns.  *)
887
  let mem_defs =
888
    List.fold_left (fun accu eq ->
889
        match eq.eq_lhs with
890
        | [vid] ->
891
           (* Only focus on non memory definitions *)
892
           if not (List.exists (fun v -> v.var_id = vid) mems) then (
893
             report ~level:3 (fun fmt ->
894
                 Format.fprintf fmt "Registering variable %s@." vid);
895
             add_def vid eq.eq_rhs;
896
             accu
897
           )
898
           else
899
             (
900
               match eq.eq_rhs.expr_desc with
901
               | Expr_pre def_m ->
902
                  report ~level:3 (fun fmt ->
903
                      Format.fprintf fmt "Preparing mem %s@." vid);
904
                  (vid, rewrite defs def_m)::accu
905
               | _ -> assert false
906
             )
907
        | _ -> assert false (* should have been removed by normalization *)
908
      ) [] sorted_eqs
909
  in
910

    
911
  
912
  report ~level:2 (fun fmt -> Format.fprintf fmt "Printing out (guarded) memories definitions (may takes time)@.");
913
  (* Printing memories definitions *)
914
  report ~level:3
915
    (fun fmt ->
916
      Format.fprintf fmt
917
        "@[<v 0>%a@]@ "
918
        (Utils.fprintf_list ~sep:"@ "
919
           (fun fmt (m,mdefs) ->
920
             Format.fprintf fmt
921
               "%s -> [@[<v 0>%a@] ]@ "
922
               m
923
               (Utils.fprintf_list ~sep:"@ "
924
                  pp_guard_expr) mdefs
925
        ))
926
        mem_defs);
927
  (* Format.eprintf "Split init@."; *)
928
  let init_defs, update_defs =
929
    split_init mem_defs 
930
  in
931
  report ~level:3
932
    (fun fmt ->
933
      Format.fprintf fmt
934
        "@[<v 0>Init:@ %a@ Step@ %a@]@ "
935
        (Utils.fprintf_list ~sep:"@ "
936
           (fun fmt (m,mdefs) ->
937
             Format.fprintf fmt
938
               "%s -> @[<v 0>[%a@] ]@ "
939
               m
940
               (Utils.fprintf_list ~sep:"@ "
941
                  pp_guard_expr) mdefs
942
        ))
943
        init_defs
944
        (Utils.fprintf_list ~sep:"@ "
945
           (fun fmt (m,mdefs) ->
946
             Format.fprintf fmt
947
               "%s -> @[<v 0>[%a@] ]@ "
948
               m
949
               (Utils.fprintf_list ~sep:"@ "
950
                  pp_guard_expr) mdefs
951
        ))
952
        update_defs);
953
  (* Format.eprintf "Build init@."; *)
954

    
955
  let sw_init= 
956
    build_switch_sys init_defs []
957
  in
958
  (* Format.eprintf "Build step@."; *)
959
  let sw_sys =
960
    build_switch_sys update_defs []
961
  in
962
  let sw_init, sw_sys = clean_sys sw_init, clean_sys sw_sys in
963

    
964

    
965
  (* Some additional checks *)
966
  let pp_gl pp_expr =
967
    fprintf_list ~sep:", " (fun fmt (e,b) -> Format.fprintf fmt "%s%a" (if b then "" else "NOT ") pp_expr e)
968
  in
969
  let pp_gl_short = pp_gl (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag) in
970
  let pp_up fmt up = List.iter (fun (id,e) -> Format.fprintf fmt "%s->%i; " id e.expr_tag) up in
971
  
972
  if false then
973
    begin
974
      Format.eprintf "@.@.CHECKING!!!!!!!!!!!@.";
975
      Format.eprintf "Any duplicate expression in guards?@.";
976
      
977
      let sw_sys =
978
        List.map (fun (gl, up) ->
979
            let gl = List.sort (fun (e,b) (e',b') ->
980
                         let res = compare e.expr_tag e'.expr_tag in
981
                         if res = 0 then (Format.eprintf "Same exprs?@.%a@.%a@.@."
982
                                            Printers.pp_expr e
983
                                            Printers.pp_expr e'
984
                                         );
985
                         res
986
                       ) gl in
987
            gl, up
988
          ) sw_sys 
989
      in
990
      Format.eprintf "Another check for duplicates in guard list@.";
991
      List.iter (fun (gl, _) ->
992
          let rec aux hd l =
993
            match l with
994
              [] -> ()
995
            | (e,b)::tl -> let others = hd@tl in
996
                           List.iter (fun (e',_) -> if Corelang.is_eq_expr e e' then
997
                                                      (Format.eprintf "Same exprs?@.%a@.%a@.@."
998
                                                         Printers.pp_expr e
999
                                                         Printers.pp_expr e'
1000
                             )) others;
1001
                           aux ((e,b)::hd) tl
1002
          in
1003
          aux [] gl
1004
        ) sw_sys;
1005
      Format.eprintf "Checking duplicates in updates@.";
1006
      let rec check_dup_up accu l =
1007
        match l with
1008
        | [] -> ()
1009
        | ((gl, up) as hd)::tl ->
1010
           let others = accu@tl in
1011
           List.iter (fun (gl',up') -> if up = up' then
1012
                                         Format.eprintf "Same updates?@.%a@.%a@.%a@.%a@.@."
1013

    
1014
                                           pp_gl_short gl
1015
                                           pp_up up
1016
                                           pp_gl_short gl'
1017
                                           pp_up up'
1018
                                       
1019
             ) others;
1020
           
1021
           
1022

    
1023
           check_dup_up (hd::accu) tl
1024
           
1025
      in
1026
      check_dup_up [] sw_sys;
1027
      let sw_sys =
1028
        List.sort (fun (gl1, _) (gl2, _) ->
1029
            let glid gl = List.map (fun (e,_) -> e.expr_tag) gl in
1030
            
1031
            let res = compare (glid gl1) (glid gl2) in
1032
            if res = 0 then Format.eprintf "Same guards?@.%a@.%a@.@."
1033
                              pp_gl_short gl1 pp_gl_short gl2
1034
            ;
1035
              res
1036

    
1037
          ) sw_sys
1038

    
1039
      in
1040
      ()
1041
    end;
1042
  
1043

    
1044
  (* Iter through the elements and gather them by updates *)
1045
  let module UpMap =
1046
    struct
1047
      include Map.Make (
1048
                  struct
1049
                    type t = (ident * expr) list
1050
                    let compare l1 l2 =
1051
                      let proj l = List.map (fun (s,e) -> s, e.expr_tag) l in
1052
                      compare (proj l1) (proj l2) 
1053
                  end)
1054
      let pp = pp_up 
1055
    end
1056
  in
1057
  let module Guards = struct
1058
      include Set.Make (
1059
                  struct
1060
                    type t = (expr * bool) 
1061
                    let compare l1 l2 =
1062
                      let proj (e,b) = e.expr_tag, b in
1063
                      compare (proj l1) (proj l2) 
1064
                  end)
1065
      let pp_short fmt s = pp_gl_short fmt (elements s)
1066
      let pp_long fmt s = pp_gl Printers.pp_expr fmt (elements s)
1067
    end
1068
  in
1069
  let process sys =
1070
    (* The map will associate to each update up the pair (set, set
1071
       list) where set is the share guards and set list a list of
1072
       disjunctive guards. Each set represents a conjunction of
1073
       expressions. *)
1074
    let map = 
1075
      List.fold_left (fun map (gl,up) ->
1076
          (* creating a new set to describe gl *)
1077
          let new_set =
1078
            List.fold_left
1079
              (fun set g -> Guards.add g set)
1080
              Guards.empty
1081
              gl
1082
          in
1083
          (* updating the map with up -> new_set *)
1084
          if UpMap.mem up map then
1085
            let (shared, disj) = UpMap.find up map in
1086
            let new_shared = Guards.inter shared new_set in
1087
            let remaining_shared = Guards.diff shared new_shared in
1088
            let remaining_new_set = Guards.diff new_set new_shared in
1089
            (* Adding remaining_shared to all elements of disj *)
1090
            let disj' = List.map (fun gs -> Guards.union remaining_shared gs) disj in
1091
            UpMap.add up (new_shared, remaining_new_set::disj') map
1092
          else
1093
            UpMap.add up (new_set, []) map
1094
        ) UpMap.empty sys
1095
    in
1096
     let rec mk_binop op l = match l with
1097
         [] -> assert false
1098
       | [e] -> e
1099
       | hd::tl -> Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl]
1100
    in
1101
    let gl_as_expr gl =
1102
      let gl = Guards.elements gl in
1103
      let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in 
1104
      match gl with
1105
        [] -> []
1106
      | [e] -> [export e]
1107
      | _ ->
1108
         [mk_binop "&&"
1109
            (List.map export gl)]
1110
    in
1111
    let rec clean_disj disj =
1112
      match disj with
1113
      | [] | [_] -> [] 
1114
      | _::_::_ -> (
1115
        (* First basic version: producing a DNF One can later, (1)
1116
           simplify it with z3, or (2) build the compact tree with
1117
           maximum shared subexpression (and simplify it with z3) *)
1118
        let elems = List.fold_left (fun accu gl -> (gl_as_expr gl) @ accu) [] disj in
1119
        let or_expr = mk_binop "||" elems in
1120
        [or_expr]
1121

    
1122

    
1123
         (* TODO disj*)
1124
      (* get the item that occurs in most case *)
1125
      (* List.fold_left (fun accu s ->
1126
       *     List.fold_left (fun accu (e,b) ->
1127
       *         if List.mem_assoc (e.expr_tag, b)
1128
       *       ) accu (Guards.elements s)
1129
       *   ) [] disj *)
1130

    
1131
      )
1132
    in
1133
    Format.eprintf "Map: %i elements@." (UpMap.cardinal map);
1134
    UpMap.fold (fun up (common, disj) accu ->
1135
        Format.eprintf
1136
          "Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@."
1137
          Guards.pp_short common
1138
          (fprintf_list ~sep:";@ " Guards.pp_long) disj
1139
          UpMap.pp up;
1140
        let disj = clean_disj disj in
1141
        let guard_expr = (gl_as_expr common)@disj in
1142
        
1143
        ((match guard_expr with
1144
         | [] -> None
1145
         | _ -> Some (mk_binop "&&" guard_expr)), up)::accu
1146
      ) map []
1147
    
1148
  in
1149
  process sw_init, process sw_sys