Project

General

Profile

Revision 81229f63 src/tools/seal/seal_extract.ml

View differences:

src/tools/seal/seal_extract.ml
325 325
    Hashtbl.find ze_implies_hash (ze1_uid, ze2_uid)
326 326
  else
327 327
    begin
328
       Format.eprintf "Checking implication: %s => %s? "
329
        (Z3.Expr.to_string ze1) (Z3.Expr.to_string ze2)
330
        ; 
328
      if !debug then (
329
        Format.eprintf "Checking implication: %s => %s? "
330
          (Z3.Expr.to_string ze1) (Z3.Expr.to_string ze2)
331
      ); 
331 332
      let solver = Z3.Solver.mk_simple_solver !ctx in
332 333
      let tgt = Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_implies !ctx ze1 ze2) in
333 334
      let res =
334 335
        try
335 336
          let status_res = Z3.Solver.check solver [tgt] in
336 337
          match status_res with
337
          | Z3.Solver.UNSATISFIABLE -> Format.eprintf "Valid!@."; 
338
          | Z3.Solver.UNSATISFIABLE -> if !debug then Format.eprintf "Valid!@."; 
338 339
             true
339
          | _ -> Format.eprintf "not proved valid@."; 
340
          | _ -> if !debug then Format.eprintf "not proved valid@."; 
340 341
             false
341 342
        with Zustre_common.UnknownFunction(id, msg) -> (
342 343
          report ~level:1 msg;
......
442 443
  
443 444
let clean_sys sys =
444 445
  List.fold_left (fun accu (guards, updates) ->
445
      (*let guards' = clean_guard guards in*)
446 446
      let sat, guards' =  check_sat (List.map (fun (g, pn) -> Expr g, pn) guards) in
447 447
      (*Format.eprintf "Guard: %a@.Guard cleaned: %a@.Sat? %b@."
448 448
        (fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr))  guards
......
597 597
       let args = rewrite args in
598 598
       List.map (fun (guards, e) ->
599 599
           guards,
600
           Expr {expr with expr_desc = Expr_appl(id, deelem e, None)}
600
           Expr (Corelang.mkexpr expr.expr_loc (Expr_appl(id, deelem e, None)))
601 601
         ) args 
602 602
    | Expr_const _  -> [[], Expr expr]
603 603
    | Expr_ident id ->
......
645 645
       in
646 646
       let gtuples = aux gell in
647 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
648
       List.map
649
         (fun (g,tuple) -> g, Expr (Corelang.mkexpr expr.expr_loc (Expr_tuple tuple)))
650
         gtuples
649 651
    | Expr_fby _
650 652
      | Expr_appl _
651 653
                  (* Should be removed by mormalization and inlining *)
......
834 836
         in
835 837
         let pos_prefix = (elem, true)::prefix in
836 838
         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 839
         let ok_pos, pos_prefix = clean pos_prefix in         
841 840
         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 841
         (if ok_pos then build_switch_sys pos pos_prefix else [])
846 842
         @
847 843
           (if ok_neg then build_switch_sys neg neg_prefix else [])
......
963 959
  let sw_sys =
964 960
    build_switch_sys update_defs []
965 961
  in
966
  clean_sys sw_init, clean_sys sw_sys
967
 
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

Also available in: Unified diff