Project

General

Profile

Revision 7aaacbc9 src/tools/seal/seal_extract.ml

View differences:

src/tools/seal/seal_extract.ml
15 15
  | IsInit -> Format.fprintf fmt "init"
16 16
  | Expr e -> Printers.pp_expr fmt e
17 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
  
18 22
let pp_guard_expr fmt (gl,e) =
19 23
  Format.fprintf fmt "%a -> %a"
20
    (fprintf_list ~sep:"; "
21
       (fun fmt (e,b) -> if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) gl
24
    pp_guard_list  gl
22 25
    pp_elem e
23 26

  
24 27
let pp_mdefs fmt gel = fprintf_list ~sep:"@ " pp_guard_expr fmt gel
......
222 225
let check_sat, clean_guard = 
223 226
  (
224 227
    fun l ->
228
    (* Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " pp_guard_list l; *)
225 229
    let solver = Z3.Solver.mk_simple_solver !ctx in
226 230
    try (
227 231
    let zl =
......
237 241
            neg_ze ze
238 242
        ) l
239 243
    in
244
    (* Format.eprintf "Z3 exprs: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; *)
240 245
    let status_res = Z3.Solver.check solver zl in
246
    (* Format.eprintf "Z3 status: %s@ @]@. " (Z3.Solver.string_of_status status_res); *)
241 247
    let sat = match status_res with
242 248
      | Z3.Solver.UNSATISFIABLE -> false
243 249
      | _ -> true in
......
268 274
     Z3.Goal.add goal zl;
269 275
    let goal' = Z3.Goal.simplify goal None in
270 276
    
271
    Format.eprintf "Goal before: %s@.Goal after : %s@.Sat? %s@."
272
      (Z3.Goal.to_string goal)
273
      (Z3.Goal.to_string goal')
274
      (Z3.Solver.string_of_status status_res)
275
    ;
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
     * ; *)
276 282
    let ze = Z3.Goal.as_expr goal' in
277
    Format.eprintf "as an expr: %s@." (Z3.Expr.to_string ze);
278
   (* let l =
279
      match zexpr_to_expr ze with
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 
280 289
      | None, None -> []
281 290
      | None, Some e -> [e, true]
282 291
      | _ -> assert false
283
    (*      | Some init, None -> [IsInit, init]
284
      | Some init, Some e -> [IsInit, init; Expr e, true]
285
     *)  in
286
     *)
292
    in
287 293
    l
294
           
295
    
288 296
    )
289 297
      with Zustre_common.UnknownFunction(id, msg) -> (
290 298
      report ~level:1 msg;
......
317 325
  (* Filtering out trivial cases. More semantics ones would have to be
318 326
     addressed later *)
319 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
     * ; *)
320 333
    (* Check if gepxr is part of l *)
321
    let sel_fun = select_elem gexpr in
322
    if List.exists sel_fun l then
334
   let sel_fun = select_elem gexpr in
335
   let ok, res =
336
     if List.exists sel_fun l then (
323 337
      (* Checking the guard value posneg *)
324 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
     * ; *)
325 344
      status=posneg, l
326
    else
345
    )
346
    else (
347
      (* Format.eprintf "Not found.@ "; *)
327 348
      (* Valid: no overlap *)
328 349
      (* Individual checkat *)
329 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; *)
330 353
      if ok then
331 354
        let l = e@l in
332 355
        let ok, l = check_sat l in
356
        (* let ok, l = true, l in (* TODO solve the issue with check_sat *) *)
333 357
        ok, l 
334 358
      else
335
        true, l
359
        false, []
360
     )
361
   in
362
   (* Format.eprintf "Check sat res: %a@ "
363
    *   pp_guard_list res; *)
364
   ok, res
336 365
  in
337 366
  let ok, gl =
338 367
    List.fold_left (
......
351 380
      check fresh_g gl
352 381
    )
353 382
  else
354
    ok, []
383
    false, []
355 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
 *)
356 390
(* Encode "If gel1=posneg then gel2":
357 391
   - Compute the combination of guarded exprs in gel1 and gel2:
358 392
     - Each guarded_expr in gel1 is transformed as a guard: the
......
365 399
      fun accu (g2,e2) ->
366 400
      List.fold_left (
367 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
            
368 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
            
369 412
          if ok then
370 413
            (gl, e2)::accu
371
          else
414
          else (
415
            
372 416
            accu
417
          )
373 418
        ) accu gel1
374 419
    ) [] gel2
375 420

  
376 421
let rec rewrite defs expr : guarded_expr list =
377 422
  let rewrite = rewrite defs in
378
  match expr.expr_desc with
379
  | Expr_appl (id, args, None) ->
380
     let args = rewrite args in
381
     List.map (fun (guards, e) ->
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) ->
382 428
           guards,
383 429
           Expr {expr with expr_desc = Expr_appl(id, deelem e, None)}
384
       ) args 
385
  | Expr_const _  -> [[], Expr expr]
386
  | Expr_ident id ->
387
     if Hashtbl.mem defs id then
388
       Hashtbl.find defs id
389
     else
390
       (* id should be an input *)
391
       [[], Expr expr]
392
  | Expr_ite (g, e1, e2) ->
393
     let g = rewrite g and
394
         e1 = rewrite e1 and
395
         e2 = rewrite e2 in
396
     (concatenate_ge g true e1)@
397
       (concatenate_ge g false e2)
398
  | Expr_merge (g, branches) ->
399
     assert false (* TODO: deal with merges *)
400
    
401
  | Expr_when (e, _, _) -> rewrite e
402
  | Expr_arrow _ -> [[], IsInit] (* At this point the only arrow should be true -> false *)
403
  | Expr_tuple el ->
404
     (* Each expr is associated to its flatten guarded expr list *)
405
     let gell = List.map rewrite el in
406
     (* Computing all combinations: we obtain a list of guarded tuple *)
407
     let rec aux gell : (guard * expr list) list =
408
       match gell with
409
       | [] -> assert false (* Not happening *)
410
       | [gel] -> List.map (fun (g,e) -> g, [deelem e]) gel
411
       | gel::getl ->
412
          let getl = aux getl in
413
          List.fold_left (
414
              fun accu (g,e) ->
415
              List.fold_left (
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 (
416 462
                    fun accu (gl, minituple) ->
417 463
                    let is_compat, guard_comb = combine_guards g gl in
418 464
                    if is_compat then
......
420 466
                      new_gt::accu
421 467
                    else
422 468
                      accu
423
                  
469
                    
424 470
                  ) accu getl
425
            ) [] gel
426
     in
427
     let gtuples = aux gell in
428
     (* Rebuilding the valid type: guarded expr list (with tuple exprs) *)
429
     List.map (fun (g,tuple) -> g, Expr {expr with expr_desc = Expr_tuple tuple}) gtuples
430
  | Expr_fby _
431
    | Expr_appl _
432
                (* Should be removed by mormalization and inlining *)
433
    -> Format.eprintf "Pb expr: %a@.@?" Printers.pp_expr expr; assert false
434
  | Expr_array _ | Expr_access _ | Expr_power _
435
                                              (* Arrays not handled here yet *)
436
    -> assert false
437
  | Expr_pre _ -> (* Not rewriting mem assign *)
438
     assert false
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
439 491
and add_def defs vid expr =
440
  Hashtbl.add defs vid (rewrite defs 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
441 500

  
442 501
(* Takes a list of guarded exprs (ge) and a guard
443 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.
......
608 667
  let _ =
609 668
    List.iter (fun c -> Hashtbl.add const_defs c.const_id c.const_value) consts
610 669
  in
670

  
611 671
  
612 672
  (* Registering node equations: identifying mem definitions and
613 673
     storing others in the "defs" hashtbl. *)
......
685 745
    build_switch_sys update_defs []
686 746
  in
687 747
  clean_sys sw_init, clean_sys sw_sys
748
 

Also available in: Unified diff