Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal / seal_extract.ml @ 3b7f916b

History | View | Annotate | Download (33 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
       Format.eprintf "Checking implication: %s => %s? "
329
        (Z3.Expr.to_string ze1) (Z3.Expr.to_string ze2)
330
        ; 
331
      let solver = Z3.Solver.mk_simple_solver !ctx in
332
      let tgt = Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_implies !ctx ze1 ze2) in
333
      let res =
334
        try
335
          let status_res = Z3.Solver.check solver [tgt] in
336
          match status_res with
337
          | Z3.Solver.UNSATISFIABLE -> Format.eprintf "Valid!@."; 
338
             true
339
          | _ -> Format.eprintf "not proved valid@."; 
340
             false
341
        with Zustre_common.UnknownFunction(id, msg) -> (
342
          report ~level:1 msg;
343
          false
344
        )
345
      in
346
      Hashtbl.add ze_implies_hash (ze1_uid,ze2_uid) res ;
347
      res
348
    end
349
                                               
350
let rec simplify zl =
351
  match zl with
352
  | [] | [_] -> zl
353
  | hd::tl -> (
354
    (* Forall e in tl, checking whether hd => e or e => hd, to keep hd
355
     in the first case and e in the second one *)
356
    let tl = simplify tl in
357
    let keep_hd, tl =
358
      List.fold_left (fun (keep_hd, accu) e ->
359
          if implies hd e then
360
            true, accu (* throwing away e *)
361
          else if implies e hd then
362
            false, e::accu (* throwing away hd *)
363
          else
364
            keep_hd, e::accu (* keeping both *)
365
        ) (true,[]) tl
366
    in
367
    (* Format.eprintf "keep_hd?%b hd=%s, tl=[%a]@."
368
     *   keep_hd
369
     *   (Z3.Expr.to_string hd)
370
     * (Utils.fprintf_list ~sep:"; " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) tl
371
     *   ; *)
372
    if keep_hd then
373
      hd::tl
374
    else
375
      tl
376
  )
377
  
378
let check_sat ?(just_check=false) (l:guard) : bool * guard =
379
  (* Syntactic simplification *)
380
  if false then
381
    Format.eprintf "Before simplify: %a@." pp_guard_list l; 
382
  let l = simplify_neg_guard l in
383
  if false then (
384
    Format.eprintf "After simplify: %a@." pp_guard_list l; 
385
    Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " pp_guard_list l;
386
  );
387
  let solver = Z3.Solver.mk_simple_solver !ctx in
388
  try (
389
    let zl =
390
      List.map (fun (e, posneg) ->
391
          let ze =
392
            match e with
393
            | IsInit -> is_init_z3e
394
            | Expr e -> expr_to_z3_expr e 
395
          in
396
          if posneg then
397
            ze
398
          else
399
            neg_ze ze
400
        ) l
401
    in
402
    if false then Format.eprintf "Z3 exprs1: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; 
403
    let zl = simplify zl in
404
        if false then Format.eprintf "Z3 exprs2: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; 
405
    let status_res = Z3.Solver.check solver zl in
406
     if false then Format.eprintf "Z3 status: %s@ @]@. " (Z3.Solver.string_of_status status_res); 
407
    match status_res with
408
    | Z3.Solver.UNSATISFIABLE -> false, []
409
    | _ -> (
410
      if false && just_check then
411
        true, l
412
      else
413
        (* TODO: may be reactivate but it may create new expressions *)
414
        (* let l = goal_simplify zl in *)
415
        let l = List.fold_left
416
                  (fun accu ze -> accu @ (zexpr_to_guard_list ze))
417
                  []
418
                  zl
419
        in
420
  (* Format.eprintf "@.@[<v 2>Check_Sat:@ before: %a@ after:
421
       %a@. Goal precise? %b/%b@]@.@. " * pp_guard_list l
422
       pp_guard_list l' * (Z3.Goal.is_precise goal) *
423
       (Z3.Goal.is_precise goal'); *)
424
  
425

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

    
439

    
440
(**************************************************************)
441

    
442
  
443
let clean_sys sys =
444
  List.fold_left (fun accu (guards, updates) ->
445
      (*let guards' = clean_guard guards in*)
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 {expr with expr_desc = 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 (fun (g,tuple) -> g, Expr {expr with expr_desc = Expr_tuple tuple}) gtuples
649
    | Expr_fby _
650
      | Expr_appl _
651
                  (* Should be removed by mormalization and inlining *)
652
      -> Format.eprintf "Pb expr: %a@.@?" Printers.pp_expr expr; assert false
653
    | Expr_array _ | Expr_access _ | Expr_power _
654
                                                (* Arrays not handled here yet *)
655
      -> assert false
656
    | Expr_pre _ -> (* Not rewriting mem assign *)
657
       assert false
658
  in
659
  (* Format.eprintf "Rewriting %a as [@[<v 0>%a@]]@ "
660
   *   Printers.pp_expr expr
661
   *   (Utils.fprintf_list ~sep:"@ "
662
   *        pp_guard_expr) res; *)
663
  res
664
and add_def defs vid expr =
665
  let vid_defs = rewrite defs expr in
666
  (* Format.eprintf "Add_def: %s = %a@. -> @[<v 0>%a@]@."
667
   *     vid
668
   *     Printers.pp_expr expr
669
   *     (
670
   *       (Utils.fprintf_list ~sep:"@ "
671
   *          pp_guard_expr)) vid_defs;  *)
672
  Hashtbl.add defs vid vid_defs
673

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

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

    
720

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

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

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

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

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

    
850

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

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

    
884
  
885
  (* Registering node equations: identifying mem definitions and
886
     storing others in the "defs" hashtbl.
887

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

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

    
959
  let sw_init= 
960
    build_switch_sys init_defs []
961
  in
962
  (* Format.eprintf "Build step@."; *)
963
  let sw_sys =
964
    build_switch_sys update_defs []
965
  in
966
  clean_sys sw_init, clean_sys sw_sys
967