Project

General

Profile

Revision 04a188ec src/tools/seal/seal_extract.ml

View differences:

src/tools/seal/seal_extract.ml
3 3
open Seal_utils			
4 4
open Zustre_data (* Access to Z3 context *)
5 5
   
6

  
6
let _ =
7
  Z3.Params.update_param_value !ctx "timeout" "10000"
8
  
7 9
(* Switched system extraction: expression are memoized *)
8 10
(*let expr_mem = Hashtbl.create 13*)
9 11
    
......
373 375
    in
374 376
    if false then Format.eprintf "Z3 exprs1: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; 
375 377
    let zl = simplify zl in
376
        if false then Format.eprintf "Z3 exprs2: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; 
378
    if false then Format.eprintf "Z3 exprs2: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; 
379
    (* Format.eprintf "Calling Z3@."; *)
377 380
    let status_res = Z3.Solver.check solver zl in
381
    (* Format.eprintf "Z3 done@."; *)
378 382
     if false then Format.eprintf "Z3 status: %s@ @]@. " (Z3.Solver.string_of_status status_res); 
379 383
    match status_res with
380 384
    | Z3.Solver.UNSATISFIABLE -> false, []
......
675 679
  (* Format.eprintf "Rewriting %a as [@[<v 0>%a@]]@ "
676 680
   *   Printers.pp_expr expr
677 681
   *   (Utils.fprintf_list ~sep:"@ "
678
   *        pp_guard_expr) res; *)
682
   *        (pp_guard_expr pp_elem)) res; *)
679 683
  res
680 684
  
681 685
and add_def defs vid expr =
......
685 689
  let vid_defs = rewrite defs expr in
686 690
  (* Format.eprintf "-> @[<v 0>%a@]@."
687 691
   *   (Utils.fprintf_list ~sep:"@ "
688
   *      (pp_guard_expr pp_elem)) vid_defs;   *)
692
   *      (pp_guard_expr pp_elem)) vid_defs; *)
689 693
  report ~level:6 (fun fmt -> Format.fprintf fmt  "Add_def: %s = %a@. -> @[<v 0>%a@]@."
690 694
      vid
691 695
      Printers.pp_expr expr
......
845 849
          (Expr elem)
846 850
          mem_defs
847 851
      in
852
      report ~level:4 (fun fmt -> Format.fprintf fmt "split by guard done@.");
853
      
848 854
  (*    Format.eprintf "Selected item %a in@.%a@.POS=%a@.NEG=%a@."
849 855
        Printers.pp_expr elem
850 856
        pp_all_defs mem_defs
......
861 867
      | Expr_const (Const_tag tag) when tag = tag_false 
862 868
        ->   build_switch_sys neg prefix
863 869
      | _ -> (* Regular case *)
870
         report ~level:4 (fun fmt -> Format.fprintf fmt "Building both children branches@."); 
864 871
         (* let _ = (
865 872
          *     Format.eprintf "Expr is %a@." Printers.pp_expr elem;
866 873
          *     match elem.expr_desc with
......
872 879
          * in *)
873 880
         let clean l =
874 881
           let l = List.map (fun (e,b) -> (Expr e), b) l in
882
           report ~level:4 (fun fmt -> Format.fprintf fmt "Checking satisfiability of %a@."
883
                                     (pp_guard_list pp_elem) l
884
             );
875 885
           let ok, l = check_sat l in
876 886
           let l = List.map (fun (e,b) -> deelem e, b) l in
877 887
           ok, l
878 888
         in
879 889
         let pos_prefix = (elem, true)::prefix in
880 890
         let neg_prefix = (elem, false)::prefix in
891
         report ~level:4 (fun fmt -> Format.fprintf fmt "Cleaning branches ...@."); 
881 892
         let ok_pos, pos_prefix = clean pos_prefix in         
893
         report ~level:4 (fun fmt -> Format.fprintf fmt "Cleaning branche pos done@."); 
882 894
         let ok_neg, neg_prefix = clean neg_prefix in
895
         report ~level:4 (fun fmt -> Format.fprintf fmt "Cleaning branche neg done@."); 
896
         report ~level:4 (fun fmt -> Format.fprintf fmt "Cleaning branches done@."); 
883 897
         report ~level:4 (fun fmt -> Format.fprintf fmt "Enforcing %a@." Printers.pp_expr elem);
884 898
         let ok_l = if ok_pos then build_switch_sys pos pos_prefix else [] in
885 899
         report ~level:4 (fun fmt -> Format.fprintf fmt "Enforcing not(%a)@." Printers.pp_expr elem);
......
946 960
     Each assign is stored in a hash tbl as list of guarded
947 961
     expressions. The memory definition is also "rewritten" as such a
948 962
     list of guarded assigns.  *)
963
  report ~level:1 (fun fmt -> Format.fprintf fmt "registering all definitions in guarded form ...@.");
949 964
  let mem_defs, output_defs =
950 965
    List.fold_left (fun (accu_mems, accu_outputs) eq ->
951 966
        match eq.eq_lhs with
......
984 999
        | _ -> assert false (* should have been removed by normalization *)
985 1000
      ) ([], []) sorted_eqs
986 1001
  in
1002
  report ~level:1 (fun fmt -> Format.fprintf fmt "registering all definitions done@.");
987 1003

  
988 1004
  
989 1005
  report ~level:2 (fun fmt -> Format.fprintf fmt "Printing out (guarded) memories definitions (may takes time)@.");
......
1035 1051
        ))
1036 1052
        update_defs);
1037 1053
  (* Format.eprintf "Build init@."; *)
1038
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build init@.");
1054
  
1055
  report ~level:1 (fun fmt -> Format.fprintf fmt "init/step as a switched system ...@.");
1039 1056
  let sw_init= 
1040 1057
    build_switch_sys init_defs []
1041 1058
  in
1042 1059
  (* Format.eprintf "Build step@."; *)
1043
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build step@.");
1044 1060
  let sw_sys =
1045 1061
    build_switch_sys update_defs []
1046 1062
  in
1063
  report ~level:1 (fun fmt -> Format.fprintf fmt "init/step as a switched system ... done@.");
1047 1064

  
1048
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build init out@.");
1065
  report ~level:1 (fun fmt -> Format.fprintf fmt "output function as a switched system ...@.");
1049 1066
  let init_out =
1050 1067
    build_switch_sys init_out []
1051 1068
  in
1052
  report ~level:4 (fun fmt -> Format.fprintf fmt "Build step out@.");
1069
  (* report ~level:1 (fun fmt -> Format.fprintf fmt "Build step out@."); *)
1053 1070

  
1054 1071
  let update_out =
1055 1072
    build_switch_sys update_out []
1056 1073
  in
1074
  report ~level:1 (fun fmt -> Format.fprintf fmt "output function as a switched system ... done@.");
1075

  
1076
  report ~level:1 (fun fmt -> Format.fprintf fmt "removing dead branches and merging remaining ...@.");
1057 1077

  
1058 1078
  let sw_init = clean_sys sw_init in
1059 1079
  let sw_sys = clean_sys sw_sys in
1060 1080
  let init_out = clean_sys init_out in
1061 1081
  let update_out = clean_sys update_out in
1082
  report ~level:1 (fun fmt -> Format.fprintf fmt "removing dead branches and merging remaining ... done@.");
1062 1083

  
1063 1084
  (* Some additional checks *)
1064 1085
  

Also available in: Unified diff