Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal / seal_extract.ml @ 7aaacbc9

History | View | Annotate | Download (24.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 *)
8
type element = IsInit | Expr of expr
9
type guard = (element * bool) list
10
type guarded_expr = guard * element
11
type mdef_t = guarded_expr list
12

    
13
let pp_elem fmt e =
14
  match e with
15
  | IsInit -> Format.fprintf fmt "init"
16
  | Expr e -> Printers.pp_expr fmt e
17

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

    
27
let pp_mdefs fmt gel = fprintf_list ~sep:"@ " pp_guard_expr fmt gel
28

    
29
  
30
let add_init defs vid =
31
  Hashtbl.add defs vid [[], IsInit]
32

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

    
37
let is_eq_elem elem elem' =
38
  match elem, elem' with
39
  | IsInit, IsInit -> true
40
  | Expr e, Expr e' ->
41
     Corelang.is_eq_expr e e'
42
  | _ -> false
43

    
44
let select_elem elem (gelem, _) =
45
  is_eq_elem elem gelem
46

    
47

    
48
(**************************************************************)
49
(* Convert from Lustre expressions to Z3 expressions and back *)
50
(* All (free) variables have to be declared in the Z3 context *)
51
(**************************************************************)
52

    
53
let is_init_name = "__is_init"
54

    
55
let const_defs = Hashtbl.create 13
56
let is_const id = Hashtbl.mem const_defs id
57
let get_const id = Hashtbl.find const_defs id
58
                 
59
(* expressions are only basic constructs here, no more ite, tuples,
60
   arrows, fby, ... *)
61
let expr_to_z3_expr, zexpr_to_expr =
62
  (* List to store converted expression. Some expressions seem to
63
     produce segfaults in z3. Storing the processed ones may solved
64
     the issue. Using list instead of hash to ease the comparison of
65
     expressions. *)
66
  let hash = ref [] in
67
  let comp_expr e (e', _) = Corelang.is_eq_expr e e' in
68
  let comp_zexpr ze (_, ze') = Z3.Expr.equal ze ze' in
69
  let mem_expr e = List.exists (comp_expr e) !hash in
70
  let mem_zexpr ze = List.exists (comp_zexpr ze) !hash in
71
  let get_zexpr e =
72
    let (_, ze) = List.find (comp_expr e) !hash in
73
    ze
74
  in
75
  let get_expr ze =
76
    let (e, _) = List.find (comp_zexpr ze) !hash in
77
    e
78
  in
79
  let add_expr e ze = hash := (e, ze)::!hash in
80
  let rec e2ze e =
81
    if mem_expr e then (
82
      get_zexpr e
83
    )
84
    else (
85
      let res =
86
        match e.expr_desc with
87
        | Expr_const c ->
88
           let z3e = Zustre_common.horn_const_to_expr c in
89
           add_expr e z3e;
90
           z3e
91
        | Expr_ident id -> (
92
          if is_const id then (
93
            let c = get_const id in
94
            let z3e = Zustre_common.horn_const_to_expr c in
95
            add_expr e z3e;
96
            z3e
97
        )
98
        else (
99
          let fdecl_id = Zustre_common.get_fdecl id in
100
          let z3e = Z3.Expr.mk_const_f !ctx fdecl_id in
101
          add_expr e z3e;
102
          z3e
103
          )
104
        )
105
      | Expr_appl (id,args, None) (* no reset *) ->
106
         let z3e = Zustre_common.horn_basic_app id e2ze (Corelang.expr_list_of_expr args) in
107
         add_expr e z3e;
108
         z3e
109
         
110
      | _ -> assert false
111
      in
112
      res
113
    )
114
  in
115
  let rec ze2e ze =
116
    let ze_name ze =
117
      let fd = Z3.Expr.get_func_decl ze in
118
      Z3.Symbol.to_string (Z3.FuncDecl.get_name fd)
119
    in
120
    if mem_zexpr ze then
121
      None, Some (get_expr ze)
122
    else
123
      let open Corelang in
124
      let fd = Z3.Expr.get_func_decl ze in
125
      let zel = Z3.Expr.get_args ze in
126
      match Z3.Symbol.to_string (Z3.FuncDecl.get_name fd), zel with
127
      (*      | var, [] -> (* should be in env *) get_e *)
128

    
129
      (* Extracting IsInit status *)
130
      | "not", [ze] when ze_name ze = is_init_name ->
131
         Some false, None
132
      | name, [] when name = is_init_name -> Some true, None
133
      (* Other constructs are converted to a lustre expression *)
134
      | op, _ -> (
135
        
136
        
137
        if Z3.Expr.is_numeral ze then
138
          let e =
139
            if Z3.Arithmetic.is_real ze then
140
              let num =  Num.num_of_ratio (Z3.Arithmetic.Real.get_ratio ze) in
141
              let s = Z3.Arithmetic.Real.numeral_to_string ze in
142
              mkexpr
143
                Location.dummy_loc
144
                (Expr_const
145
                   (Const_real
146
                      (num, 0, s)))
147
            else if Z3.Arithmetic.is_int ze then
148
              mkexpr
149
                Location.dummy_loc
150
                (Expr_const
151
                   (Const_int
152
                      (Big_int.int_of_big_int (Z3.Arithmetic.Integer.get_big_int ze))))
153
            else if Z3.Expr.is_const ze then
154
              match Z3.Expr.to_string ze with
155
              | "true" -> mkexpr Location.dummy_loc
156
                            (Expr_const (Const_tag (tag_true)))
157
              | "false" ->
158
                 mkexpr Location.dummy_loc
159
                   (Expr_const (Const_tag (tag_false)))
160
              | _ -> assert false
161
            else
162
              (
163
                Format.eprintf "Const err: %s %b@." (Z3.Expr.to_string ze) (Z3.Expr.is_const ze);
164
                assert false (* a numeral but no int nor real *)
165
              )
166
          in
167
          None, Some e
168
        else
169
          match op with
170
          | "not" | "=" | "-" | "*" | "/"
171
            | ">=" | "<=" | ">" | "<" 
172
            ->
173
             let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in
174
             None, Some (mkpredef_call Location.dummy_loc op args)
175
          | "+" -> ( (* Special treatment of + for 2+ args *)
176
            let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in
177
            let e = match args with
178
                [] -> assert false
179
              | [hd] -> hd
180
              | e1::e2::tl ->
181
                 let first_binary_and = mkpredef_call Location.dummy_loc op [e1;e2] in
182
                 if tl = [] then first_binary_and else
183
                   List.fold_left (fun e e_new ->
184
                       mkpredef_call Location.dummy_loc op [e;e_new]
185
                     ) first_binary_and tl
186
                 
187
            in
188
            None, Some e 
189
          )
190
          | "and" -> (
191
            (* Special case since it can contain is_init pred *)
192
            let args = List.map (fun ze -> ze2e ze) zel in
193
            match args with
194
            | [] -> assert false
195
            | [hd] -> hd
196
            | hd::tl ->
197
               List.fold_left
198
                 (fun (is_init_opt1, expr_opt1) (is_init_opt2, expr_opt2) ->
199
                   (match is_init_opt1, is_init_opt2 with
200
                      None, x | x, None -> x
201
                      | Some _, Some _ -> assert false),
202
                   (match expr_opt1, expr_opt2 with
203
                    | None, x | x, None -> x
204
                    | Some e1, Some e2 ->
205
                       Some (mkpredef_call Location.dummy_loc "&&" [e1; e2])
206
                 ))
207
                 hd tl 
208
          )
209
                   
210
          | op -> 
211
             let args = List.map (fun ze ->  (snd (ze2e ze))) zel in
212
             Format.eprintf "deal with op %s (%i). Expr is %s@."  op (List.length args) (Z3.Expr.to_string ze); assert false
213
      )
214
  in
215
  (fun e -> e2ze e), (fun ze -> ze2e ze)
216

    
217
let is_init_z3e = Z3.Expr.mk_const_s !ctx is_init_name  Zustre_common.bool_sort 
218
let neg_ze z3e = Z3.Boolean.mk_not !ctx z3e 
219

    
220
(*****************************************************************)
221
(* Checking sat(isfiability) of an expression and simplifying it *)
222
(* All (free) variables have to be declared in the Z3 context    *)
223
(*****************************************************************)
224
               
225
let check_sat, clean_guard = 
226
  (
227
    fun l ->
228
    (* Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " pp_guard_list l; *)
229
    let solver = Z3.Solver.mk_simple_solver !ctx in
230
    try (
231
    let zl =
232
      List.map (fun (e, posneg) ->
233
          let ze =
234
            match e with
235
            | IsInit -> is_init_z3e
236
            | Expr e -> expr_to_z3_expr e 
237
          in
238
          if posneg then
239
            ze
240
          else
241
            neg_ze ze
242
        ) l
243
    in
244
    (* Format.eprintf "Z3 exprs: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; *)
245
    let status_res = Z3.Solver.check solver zl in
246
    (* Format.eprintf "Z3 status: %s@ @]@. " (Z3.Solver.string_of_status status_res); *)
247
    let sat = match status_res with
248
      | Z3.Solver.UNSATISFIABLE -> false
249
      | _ -> true in
250
    sat, if not sat then [] else l
251
    )
252
    with Zustre_common.UnknownFunction(id, msg) -> (
253
      report ~level:1 msg;
254
      true, l (* keeping everything. *)
255
    )
256
      
257
  
258
  ),
259
  ( fun l ->
260
    try (
261
        let solver = Z3.Solver.mk_simple_solver !ctx in
262
     let zl =
263
    List.map (fun (e, posneg) ->
264
        let ze = expr_to_z3_expr e 
265
        in
266
        if posneg then
267
          ze
268
        else
269
          neg_ze ze
270
      ) l
271
     in
272
     let goal = Z3.Goal.mk_goal !ctx false false false in
273
     let status_res = Z3.Solver.check solver zl in
274
     Z3.Goal.add goal zl;
275
    let goal' = Z3.Goal.simplify goal None in
276
    
277
    (* Format.eprintf "Goal before: %s@.Goal after : %s@.Sat? %s@."
278
     *   (Z3.Goal.to_string goal)
279
     *   (Z3.Goal.to_string goal')
280
     *   (Z3.Solver.string_of_status status_res)
281
     * ; *)
282
    let ze = Z3.Goal.as_expr goal' in
283
    (* Format.eprintf "as an expr: %s@." (Z3.Expr.to_string ze); *)
284
    let l =
285
      (* zexpr_to_expr function returns a pair (is_init option, expr
286
         option). Since we are simplifying /pure/ expression, there
287
         should be not init sub-expressions here.  *)
288
      match zexpr_to_expr ze with 
289
      | None, None -> []
290
      | None, Some e -> [e, true]
291
      | _ -> assert false
292
    in
293
    l
294
           
295
    
296
    )
297
      with Zustre_common.UnknownFunction(id, msg) -> (
298
      report ~level:1 msg;
299
      l (* keeping everything. *)
300
    )
301
  )
302

    
303

    
304
(**************************************************************)
305

    
306
  
307
let clean_sys sys =
308
  List.fold_left (fun accu (guards, updates) ->
309
      let guards' = clean_guard guards in
310
      let sat, _ =  check_sat (List.map (fun (g, pn) -> Expr g, pn) guards') in
311
      (*Format.eprintf "Guard: %a@.Guard cleaned: %a@.Sat? %b@."
312
        (fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr))  guards
313
        (fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr))  guards'
314
        sat
315

    
316
      ;*)
317
        if sat then
318
        (guards', updates)::accu
319
      else
320
        accu
321
    )
322
    [] sys
323
  
324
let combine_guards ?(fresh=None) gl1 gl2 =
325
  (* Filtering out trivial cases. More semantics ones would have to be
326
     addressed later *)
327
  let check (gexpr, posneg) l =
328
    (* Format.eprintf "Checking %a=%b in %a@ "
329
     *   pp_elem gexpr
330
     *   posneg
331
     *   pp_guard_list l
332
     * ; *)
333
    (* Check if gepxr is part of l *)
334
   let sel_fun = select_elem gexpr in
335
   let ok, res =
336
     if List.exists sel_fun l then (
337
      (* Checking the guard value posneg *)
338
      let _, status = List.find sel_fun l in
339
      (* Format.eprintf "Found %a in %a. @ Checking status (%b).@ "
340
     *     pp_elem gexpr
341
     *     pp_guard_list l
342
     *     (status=posneg)
343
     * ; *)
344
      status=posneg, l
345
    )
346
    else (
347
      (* Format.eprintf "Not found.@ "; *)
348
      (* Valid: no overlap *)
349
      (* Individual checkat *)
350
      let ok, e = check_sat [gexpr, posneg] in
351
      (* let ok, e = true, [gexpr, posneg] in (* TODO solve the issue with check_sat *) *)
352
      (* Format.eprintf "Check_sat? %b@ " ok; *)
353
      if ok then
354
        let l = e@l in
355
        let ok, l = check_sat l in
356
        (* let ok, l = true, l in (* TODO solve the issue with check_sat *) *)
357
        ok, l 
358
      else
359
        false, []
360
     )
361
   in
362
   (* Format.eprintf "Check sat res: %a@ "
363
    *   pp_guard_list res; *)
364
   ok, res
365
  in
366
  let ok, gl =
367
    List.fold_left (
368
        fun (ok, l) g ->
369
        (* Bypass for negative output *)
370
        if not ok then false, []
371
        else
372
          check g l 
373
      ) (true, gl2) gl1
374
  in
375
  if ok then
376
    match fresh with
377
      None -> true, gl
378
    | Some fresh_g -> (
379
    (* Checking the fresh element *)
380
      check fresh_g gl
381
    )
382
  else
383
    false, []
384

    
385
(* DEBUG 
386
let combine_guards  ?(fresh=None) gl1 gl2 =
387
  true,
388
  (match fresh with None -> [] | Some (gexpr, posneg) -> [gexpr, posneg])@gl1@gl2
389
 *)
390
(* Encode "If gel1=posneg then gel2":
391
   - Compute the combination of guarded exprs in gel1 and gel2:
392
     - Each guarded_expr in gel1 is transformed as a guard: the
393
       expression is associated to posneg.
394
     - Existing guards in gel2 are concatenated to that list of guards
395
     - We keep expr in the ge of gel2 as the legitimate expression 
396
 *)
397
let concatenate_ge gel1 posneg gel2 =
398
  List.fold_left (
399
      fun accu (g2,e2) ->
400
      List.fold_left (
401
          fun accu (g1,e1) ->
402
           (* Format.eprintf "@[<v 2>Combining guards: (%a=%b) AND [%a] AND [%a]@ "
403
            *  pp_elem e1
404
            *  posneg
405
            *  pp_guard_list g1
406
            *  pp_guard_list g2; *)
407
            
408
          let ok, gl = combine_guards ~fresh:(Some(e1,posneg)) g1 g2 in
409
          (* Format.eprintf "@]@ Result is [%a]@ "
410
           *   pp_guard_list gl; *)
411
            
412
          if ok then
413
            (gl, e2)::accu
414
          else (
415
            
416
            accu
417
          )
418
        ) accu gel1
419
    ) [] gel2
420

    
421
let rec rewrite defs expr : guarded_expr list =
422
  let rewrite = rewrite defs in
423
  let res =
424
    match expr.expr_desc with
425
    | Expr_appl (id, args, None) ->
426
       let args = rewrite args in
427
       List.map (fun (guards, e) ->
428
           guards,
429
           Expr {expr with expr_desc = Expr_appl(id, deelem e, None)}
430
         ) args 
431
    | Expr_const _  -> [[], Expr expr]
432
    | Expr_ident id ->
433
       if Hashtbl.mem defs id then
434
         Hashtbl.find defs id
435
       else
436
         (* id should be an input *)
437
         [[], Expr expr]
438
    | Expr_ite (g, e1, e2) ->
439
       let g = rewrite g and
440
           e1 = rewrite e1 and
441
           e2 = rewrite e2 in
442
       (concatenate_ge g true e1)@
443
         (concatenate_ge g false e2)
444
    | Expr_merge (g, branches) ->
445
       assert false (* TODO: deal with merges *)
446
      
447
    | Expr_when (e, _, _) -> rewrite e
448
    | Expr_arrow _ -> [[], IsInit] (* At this point the only arrow should be true -> false *)
449
    | Expr_tuple el ->
450
       (* Each expr is associated to its flatten guarded expr list *)
451
       let gell = List.map rewrite el in
452
       (* Computing all combinations: we obtain a list of guarded tuple *)
453
       let rec aux gell : (guard * expr list) list =
454
         match gell with
455
         | [] -> assert false (* Not happening *)
456
         | [gel] -> List.map (fun (g,e) -> g, [deelem e]) gel
457
         | gel::getl ->
458
            let getl = aux getl in
459
            List.fold_left (
460
                fun accu (g,e) ->
461
                List.fold_left (
462
                    fun accu (gl, minituple) ->
463
                    let is_compat, guard_comb = combine_guards g gl in
464
                    if is_compat then
465
                      let new_gt : guard * expr list = (guard_comb, (deelem e)::minituple) in
466
                      new_gt::accu
467
                    else
468
                      accu
469
                    
470
                  ) accu getl
471
              ) [] gel
472
       in
473
       let gtuples = aux gell in
474
       (* Rebuilding the valid type: guarded expr list (with tuple exprs) *)
475
       List.map (fun (g,tuple) -> g, Expr {expr with expr_desc = Expr_tuple tuple}) gtuples
476
    | Expr_fby _
477
      | Expr_appl _
478
                  (* Should be removed by mormalization and inlining *)
479
      -> Format.eprintf "Pb expr: %a@.@?" Printers.pp_expr expr; assert false
480
    | Expr_array _ | Expr_access _ | Expr_power _
481
                                                (* Arrays not handled here yet *)
482
      -> assert false
483
    | Expr_pre _ -> (* Not rewriting mem assign *)
484
       assert false
485
  in
486
  (* Format.eprintf "Rewriting %a as [@[<v 0>%a@]]@ "
487
   *   Printers.pp_expr expr
488
   *   (Utils.fprintf_list ~sep:"@ "
489
   *        pp_guard_expr) res; *)
490
  res
491
and add_def defs vid expr =
492
  let vid_defs = rewrite defs expr in
493
  (* Format.eprintf "Add_def: %s = %a@. -> @[<v 0>%a@]@."
494
   *   vid
495
   *   Printers.pp_expr expr
496
   *   (
497
   *     (Utils.fprintf_list ~sep:"@ "
498
   *        pp_guard_expr)) vid_defs; *)
499
  Hashtbl.add defs vid vid_defs
500

    
501
(* Takes a list of guarded exprs (ge) and a guard
502
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.
503

    
504
When a given ge doesn't mention positively or negatively such guards, it is duplicated in both lists *)
505
let split_mdefs elem (mdefs: guarded_expr list) =
506
  List.fold_left (
507
      fun (selected, left_out)
508
          ((guards, expr) as ge) ->
509
      (* select the element of guards that match the argument elem *)
510
      let sel, others_guards = List.partition (select_elem elem) guards in
511
      match sel with
512
      (* we extract the element from the list and add it to the
513
         appropriate list *)
514
      | [_, sel_status] ->
515
         if sel_status then
516
           (others_guards,expr)::selected, left_out
517
         else selected, (others_guards,expr)::left_out
518
      | [] -> (* no such guard exists, we have to duplicate the
519
              guard_expr in both lists *)
520
         ge::selected, ge::left_out
521
      | _ -> (
522
        Format.eprintf "@.Spliting list on elem %a.@.List:%a@."
523
          pp_elem elem
524
          pp_mdefs mdefs;
525
        assert false (* more then one element selected. Should
526
                          not happen , or trival dead code like if
527
                              x then if not x then dead code *)
528
      )
529
    ) ([],[]) mdefs
530
    
531
let split_mem_defs
532
      (elem: element)
533
      (mem_defs: (ident * guarded_expr list) list)
534
      :
535
      ((ident * mdef_t) list) * ((ident * mdef_t) list)
536
  
537
  =
538
  List.fold_right (fun (m,mdefs)
539
                       (accu_pos, accu_neg) ->
540
      let pos, neg =
541
        split_mdefs elem mdefs 
542
      in
543
      (m, pos)::accu_pos,
544
      (m, neg)::accu_neg
545
    ) mem_defs ([],[])
546

    
547

    
548
(* Split a list of mem_defs into init and step lists of guarded
549
   expressions per memory. *)
550
let split_init mem_defs =
551
  split_mem_defs IsInit mem_defs 
552

    
553
let pick_guard mem_defs : expr option =
554
  let gel = List.flatten (List.map snd mem_defs) in
555
  let gl = List.flatten (List.map fst gel) in
556
  let all_guards =
557
    List.map (
558
        (* selecting guards and getting rid of boolean *)
559
        fun (e,b) ->
560
        match e with
561
        | Expr e -> e
562
        | _ -> assert false
563
      (* should have been filtered out
564
                                      yet *)
565
      ) gl
566
  in
567
  (* TODO , one could sort by occurence and provided the most common
568
     one *)
569
  try
570
  Some (List.hd all_guards)  
571
  with _ -> None
572
(* Transform a list of variable * guarded exprs into a list of guarded pairs (variable, expressions)
573
*)
574
let rec build_switch_sys
575
          (mem_defs : (Utils.ident * guarded_expr list) list )
576
          prefix
577
        :
578
          ((expr * bool) list * (ident * expr) list ) list =
579
  (* if all mem_defs have empty guards, we are done, return prefix,
580
     mem_defs expr.
581

    
582
     otherwise pick a guard in one of the mem, eg (g, b) then for each
583
     other mem, one need to select the same guard g with the same status b, *)
584
  if List.for_all (fun (m,mdefs) ->
585
         (* All defs are unguarded *)
586
         match mdefs with
587
         | [[], _] -> true
588
         | _ -> false
589
       ) mem_defs
590
  then
591
    [prefix ,
592
     List.map (fun (m,gel) ->
593
         match gel with
594
         | [_,e] ->
595
            let e =
596
              match e with
597
              | Expr e -> e
598
              | _ -> assert false (* No IsInit expression *)
599
            in
600
            m,e
601
         | _ -> assert false
602
       ) mem_defs]
603
  else
604
    (* Picking a guard *)
605
    let elem_opt : expr option = pick_guard mem_defs in
606
    match elem_opt with
607
      None -> []
608
    | Some elem -> (
609
      let pos, neg =
610
        split_mem_defs
611
          (Expr elem)
612
          mem_defs
613
      in
614
      (* Special cases to avoid useless computations: true, false conditions *)
615
      match elem.expr_desc with
616
      | Expr_ident "true"  ->   build_switch_sys pos prefix
617
      | Expr_const (Const_tag tag) when tag = Corelang.tag_true
618
        ->   build_switch_sys pos prefix
619
      | Expr_ident "false" ->   build_switch_sys neg prefix
620
      | Expr_const (Const_tag tag) when tag = Corelang.tag_false 
621
        ->   build_switch_sys neg prefix
622
      | _ -> (* Regular case *)
623
         (* let _ = (
624
          *     Format.eprintf "Expr is %a@." Printers.pp_expr elem;
625
          *     match elem.expr_desc with
626
          *     | Expr_const _ -> Format.eprintf "a const@."
627
          *                     
628
          *     | Expr_ident _ -> Format.eprintf "an ident@."
629
          *     | _ -> Format.eprintf "something else@."
630
          *   )
631
          * in *)
632
         (build_switch_sys pos ((elem, true)::prefix))
633
         @
634
           (build_switch_sys neg ((elem, false)::prefix))
635
    )
636

    
637

    
638
      
639
(* Take a normalized node and extract a list of switches: (cond,
640
   update) meaning "if cond then update" where update shall define all
641
   node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *)
642
let node_as_switched_sys consts (mems:var_decl list) nd =
643
  (* rescheduling node: has been scheduled already, no need to protect
644
     the call to schedule_node *)
645
  let nd_report = Scheduling.schedule_node nd in
646
  let schedule = nd_report.Scheduling_type.schedule in
647
  let eqs, auts = Corelang.get_node_eqs nd in
648
  assert (auts = []); (* Automata should be expanded by now *)
649
  let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in
650
  let defs : (ident,  guarded_expr list) Hashtbl.t = Hashtbl.create 13 in
651
  let add_def = add_def defs in
652

    
653
  let vars = Corelang.get_node_vars nd in
654
  (* Registering all locals variables as Z3 predicates. Will be use to
655
     simplify the expansion *) 
656
  let _ =
657
    List.iter (fun v ->
658
        let fdecl = Z3.FuncDecl.mk_func_decl_s
659
                      !ctx
660
                      v.var_id
661
                      []
662
                      (Zustre_common.type_to_sort v.var_type)
663
        in
664
        ignore (Zustre_common.register_fdecl v.var_id fdecl)
665
      ) vars
666
  in
667
  let _ =
668
    List.iter (fun c -> Hashtbl.add const_defs c.const_id c.const_value) consts
669
  in
670

    
671
  
672
  (* Registering node equations: identifying mem definitions and
673
     storing others in the "defs" hashtbl. *)
674
  let mem_defs =
675
    List.fold_left (fun accu eq ->
676
        match eq.eq_lhs with
677
        | [vid] ->
678
           (* Only focus on non memory definitions *)
679
           if not (List.exists (fun v -> v.var_id = vid) mems) then (
680
             report ~level:3 (fun fmt ->
681
                 Format.fprintf fmt "Registering variable %s@." vid);
682
             add_def vid eq.eq_rhs;
683
             accu
684
           )
685
           else
686
             (
687
               match eq.eq_rhs.expr_desc with
688
               | Expr_pre def_m ->
689
                  report ~level:3 (fun fmt ->
690
                      Format.fprintf fmt "Preparing mem %s@." vid);
691
                  (vid, rewrite defs def_m)::accu
692
               | _ -> assert false
693
             )
694
        | _ -> assert false (* should have been removed by normalization *)
695
      ) [] sorted_eqs
696
  in
697

    
698
  
699
  report ~level:2 (fun fmt -> Format.fprintf fmt "Printing out (guarded) memories definitions (may takes time)@.");
700
  (* Printing memories definitions *)
701
  report ~level:3
702
    (fun fmt ->
703
      Format.fprintf fmt
704
        "@[<v 0>%a@]@ "
705
        (Utils.fprintf_list ~sep:"@ "
706
           (fun fmt (m,mdefs) ->
707
             Format.fprintf fmt
708
               "%s -> [@[<v 0>%a@] ]@ "
709
               m
710
               (Utils.fprintf_list ~sep:"@ "
711
                  pp_guard_expr) mdefs
712
        ))
713
        mem_defs);
714
  
715
  let init_defs, update_defs =
716
    split_init mem_defs 
717
  in
718
  report ~level:3
719
    (fun fmt ->
720
      Format.fprintf fmt
721
        "@[<v 0>Init:@ %a@ Step@ %a@]@ "
722
        (Utils.fprintf_list ~sep:"@ "
723
           (fun fmt (m,mdefs) ->
724
             Format.fprintf fmt
725
               "%s -> @[<v 0>[%a@] ]@ "
726
               m
727
               (Utils.fprintf_list ~sep:"@ "
728
                  pp_guard_expr) mdefs
729
        ))
730
        init_defs
731
        (Utils.fprintf_list ~sep:"@ "
732
           (fun fmt (m,mdefs) ->
733
             Format.fprintf fmt
734
               "%s -> @[<v 0>[%a@] ]@ "
735
               m
736
               (Utils.fprintf_list ~sep:"@ "
737
                  pp_guard_expr) mdefs
738
        ))
739
        update_defs);
740

    
741
  let sw_init= 
742
    build_switch_sys init_defs []
743
  in
744
  let sw_sys =
745
    build_switch_sys update_defs []
746
  in
747
  clean_sys sw_init, clean_sys sw_sys
748