Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

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

  
7 7
(* Switched system extraction: expression are memoized *)
8 8
(*let expr_mem = Hashtbl.create 13*)
9
    
10
let add_init defs vid =
11
  Hashtbl.add defs vid [[], IsInit]
12 9

  
10
let add_init defs vid = Hashtbl.add defs vid [ [], IsInit ]
13 11

  
14 12
(**************************************************************)
15 13
(* Convert from Lustre expressions to Z3 expressions and back *)
......
19 17
let is_init_name = "__is_init"
20 18

  
21 19
let const_defs = Hashtbl.create 13
20

  
22 21
let is_const id = Hashtbl.mem const_defs id
23
let is_enum_const id = Hashtbl.mem Zustre_data.const_tags id  
22

  
23
let is_enum_const id = Hashtbl.mem Zustre_data.const_tags id
24

  
24 25
let get_const id = Hashtbl.find const_defs id
25
                 
26
(* expressions are only basic constructs here, no more ite, tuples,
27
   arrows, fby, ... *)
26

  
27
(* expressions are only basic constructs here, no more ite, tuples, arrows, fby,
28
   ... *)
28 29

  
29 30
(* Set of hash to support memoization *)
30
let expr_hash: (expr * Utils.tag) list ref = ref []
31
let ze_hash: (Z3.Expr.expr, Utils.tag) Hashtbl.t = Hashtbl.create 13
32
let e_hash: (Utils.tag, Z3.Expr.expr) Hashtbl.t = Hashtbl.create 13
33
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
34
let pp_e_map fmt = List.iter (fun (e,t) -> Format.fprintf fmt "%i -> %a@ " t Printers.pp_expr e) !expr_hash
35
let pp_ze_hash fmt = pp_hash
36
                      (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))
37
                      Format.pp_print_int
38
                      fmt
39
                      ze_hash
40
let pp_e_hash fmt = pp_hash
41
                      Format.pp_print_int
42
                      (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))
43
                      fmt
44
                      e_hash                              
31
let expr_hash : (expr * Utils.tag) list ref = ref []
32

  
33
let ze_hash : (Z3.Expr.expr, Utils.tag) Hashtbl.t = Hashtbl.create 13
34

  
35
let e_hash : (Utils.tag, Z3.Expr.expr) Hashtbl.t = Hashtbl.create 13
36

  
37
let pp_hash pp_key pp_v fmt h =
38
  Hashtbl.iter
39
    (fun key v -> Format.fprintf fmt "%a -> %a@ " pp_key key pp_v v)
40
    h
41

  
42
let pp_e_map fmt =
43
  List.iter
44
    (fun (e, t) -> Format.fprintf fmt "%i -> %a@ " t Printers.pp_expr e)
45
    !expr_hash
46

  
47
let pp_ze_hash fmt =
48
  pp_hash
49
    (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))
50
    Format.pp_print_int fmt ze_hash
51

  
52
let pp_e_hash fmt =
53
  pp_hash Format.pp_print_int
54
    (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))
55
    fmt e_hash
56

  
45 57
let mem_expr e =
46 58
  (* Format.eprintf "Searching for %a in map: @[<v 0>%t@]"
47 59
   *   Printers.pp_expr e
48 60
   *   pp_e_map; *)
49
  let res = List.exists (fun (e',_) -> Corelang.is_eq_expr e e') !expr_hash in
61
  let res = List.exists (fun (e', _) -> Corelang.is_eq_expr e e') !expr_hash in
50 62
  (* Format.eprintf "found?%b@." res; *)
51 63
  res
52
  
53
let mem_zexpr ze =
54
  Hashtbl.mem ze_hash ze
64

  
65
let mem_zexpr ze = Hashtbl.mem ze_hash ze
66

  
55 67
let get_zexpr e =
56
  let _, uid = List.find (fun (e',_) -> Corelang.is_eq_expr e e') !expr_hash in
68
  let _, uid = List.find (fun (e', _) -> Corelang.is_eq_expr e e') !expr_hash in
57 69
  (* Format.eprintf "found expr=%a id=%i@." Printers.pp_expr eref eref.expr_tag; *)
58 70
  Hashtbl.find e_hash uid
71

  
59 72
let get_expr ze =
60 73
  let uid = Hashtbl.find ze_hash ze in
61
  let e,_ = List.find (fun (_, t) -> t = uid) !expr_hash in
74
  let e, _ = List.find (fun (_, t) -> t = uid) !expr_hash in
62 75
  e
63
  
64
let neg_ze z3e = Z3.Boolean.mk_not !ctx z3e 
65
let is_init_z3e =
66
  Z3.Expr.mk_const_s !ctx is_init_name  Zustre_common.bool_sort 
67 76

  
68
let get_zid (ze:Z3.Expr.expr) : Utils.tag = 
77
let neg_ze z3e = Z3.Boolean.mk_not !ctx z3e
78

  
79
let is_init_z3e = Z3.Expr.mk_const_s !ctx is_init_name Zustre_common.bool_sort
80

  
81
let get_zid (ze : Z3.Expr.expr) : Utils.tag =
69 82
  try
70
    if Z3.Expr.equal ze is_init_z3e then -1 else
71
      if Z3.Expr.equal ze (neg_ze is_init_z3e) then -2 else
72
    Hashtbl.find ze_hash ze
73
  with _ -> (Format.eprintf "Looking for ze %s in Hash %a"
74
               (Z3.Expr.to_string ze)
75
               (fun fmt hash -> Hashtbl.iter (fun ze uid -> Format.fprintf fmt "%s -> %i@ " (Z3.Expr.to_string ze) uid) hash ) ze_hash;
76
             assert false)
83
    if Z3.Expr.equal ze is_init_z3e then -1
84
    else if Z3.Expr.equal ze (neg_ze is_init_z3e) then -2
85
    else Hashtbl.find ze_hash ze
86
  with _ ->
87
    Format.eprintf "Looking for ze %s in Hash %a" (Z3.Expr.to_string ze)
88
      (fun fmt hash ->
89
        Hashtbl.iter
90
          (fun ze uid ->
91
            Format.fprintf fmt "%s -> %i@ " (Z3.Expr.to_string ze) uid)
92
          hash)
93
      ze_hash;
94
    assert false
95

  
77 96
let add_expr =
78 97
  let cpt = ref 0 in
79 98
  fun e ze ->
80
  incr cpt;
81
  let uid = !cpt in
82
  expr_hash := (e, uid)::!expr_hash;
83
  Hashtbl.add e_hash uid ze;
84
  Hashtbl.add ze_hash ze uid
99
    incr cpt;
100
    let uid = !cpt in
101
    expr_hash := (e, uid) :: !expr_hash;
102
    Hashtbl.add e_hash uid ze;
103
    Hashtbl.add ze_hash ze uid
85 104

  
86
  
87 105
let expr_to_z3_expr, zexpr_to_expr =
88 106
  (* List to store converted expression. *)
89 107
  (* let hash = ref [] in
90 108
   * let comp_expr e (e', _) = Corelang.is_eq_expr e e' in
91 109
   * let comp_zexpr ze (_, ze') = Z3.Expr.equal ze ze' in *)
92
  
93 110
  let rec e2ze e =
94
    (* Format.eprintf "e2ze %a: %a@." Printers.pp_expr e Types.print_ty e.expr_type; *)
95
    if mem_expr e then (
96
      get_zexpr e
97
    )
98
    else (
111
    (* Format.eprintf "e2ze %a: %a@." Printers.pp_expr e Types.print_ty
112
       e.expr_type; *)
113
    if mem_expr e then get_zexpr e
114
    else
99 115
      let res =
100 116
        match e.expr_desc with
101 117
        | Expr_const c ->
102
           let z3e = Zustre_common.horn_const_to_expr c in
103
           add_expr e z3e;
104
           z3e
105
        | Expr_ident id -> (
118
          let z3e = Zustre_common.horn_const_to_expr c in
119
          add_expr e z3e;
120
          z3e
121
        | Expr_ident id ->
106 122
          if is_const id then (
107 123
            let c = get_const id in
108 124
            let z3e = Zustre_common.horn_const_to_expr c in
109 125
            add_expr e z3e;
110
            z3e
111
          )
126
            z3e)
112 127
          else if is_enum_const id then (
113 128
            let z3e = Zustre_common.horn_tag_to_expr id in
114 129
            add_expr e z3e;
115
            z3e
116
          )
117
          else (
130
            z3e)
131
          else
118 132
            let fdecl_id = Zustre_common.get_fdecl id in
119 133
            let z3e = Z3.Expr.mk_const_f !ctx fdecl_id in
120 134
            add_expr e z3e;
121 135
            z3e
122
          )
123
        )
124
        | Expr_appl (id,args, None) (* no reset *) ->
125
           let el = Corelang.expr_list_of_expr args in
126
           
127
           let eltyp = List.map (fun e -> e.expr_type) el in
128
           let elv = List.map e2ze el in
129
           let z3e = Zustre_common.horn_basic_app id elv (eltyp, e.expr_type) in
130
           add_expr e z3e;
131
           z3e
132
        | Expr_tuple [e] ->
133
           let z3e = e2ze e in
134
           add_expr e z3e;
135
           z3e
136
        | _ -> ( match e.expr_desc with Expr_tuple _ -> Format.eprintf "tuple e2ze(%a)@.@?" Printers.pp_expr e
137
                                      | _ -> Format.eprintf "e2ze(%a)@.@?" Printers.pp_expr e)
138
             ; assert false
136
        | Expr_appl (id, args, None) (* no reset *) ->
137
          let el = Corelang.expr_list_of_expr args in
138

  
139
          let eltyp = List.map (fun e -> e.expr_type) el in
140
          let elv = List.map e2ze el in
141
          let z3e = Zustre_common.horn_basic_app id elv (eltyp, e.expr_type) in
142
          add_expr e z3e;
143
          z3e
144
        | Expr_tuple [ e ] ->
145
          let z3e = e2ze e in
146
          add_expr e z3e;
147
          z3e
148
        | _ ->
149
          (match e.expr_desc with
150
          | Expr_tuple _ ->
151
            Format.eprintf "tuple e2ze(%a)@.@?" Printers.pp_expr e
152
          | _ ->
153
            Format.eprintf "e2ze(%a)@.@?" Printers.pp_expr e);
154
          assert false
139 155
      in
140 156
      res
141
    )
142 157
  in
143 158
  let rec ze2e ze =
144 159
    let ze_name ze =
145 160
      let fd = Z3.Expr.get_func_decl ze in
146 161
      Z3.Symbol.to_string (Z3.FuncDecl.get_name fd)
147 162
    in
148
    if mem_zexpr ze then
149
      None, Some (get_expr ze)
163
    if mem_zexpr ze then None, Some (get_expr ze)
150 164
    else
151 165
      let open Corelang in
152 166
      let fd = Z3.Expr.get_func_decl ze in
153 167
      let zel = Z3.Expr.get_args ze in
154 168
      match Z3.Symbol.to_string (Z3.FuncDecl.get_name fd), zel with
155
      (*      | var, [] -> (* should be in env *) get_e *)
169
      (* | var, [] -> (* should be in env *) get_e *)
156 170

  
157 171
      (* Extracting IsInit status *)
158
      | "not", [ze] when ze_name ze = is_init_name ->
159
         Some false, None
160
      | name, [] when name = is_init_name -> Some true, None
172
      | "not", [ ze ] when ze_name ze = is_init_name ->
173
        Some false, None
174
      | name, [] when name = is_init_name ->
175
        Some true, None
161 176
      (* Other constructs are converted to a lustre expression *)
162 177
      | op, _ -> (
163
        
164
        
165 178
        if Z3.Expr.is_numeral ze then
166 179
          let e =
167 180
            if Z3.Arithmetic.is_real ze then
168 181
              let s = Z3.Arithmetic.Real.numeral_to_string ze in
169 182
              (* Use to return a Num.ratio. Now Q.t *)
170 183
              let ratio = Z3.Arithmetic.Real.get_ratio ze in
171
              (*let num =  Num.num_of_ratio ratio in
172
              let real = Real.create_num num s in*)
184
              (* let num = Num.num_of_ratio ratio in let real = Real.create_num
185
                 num s in*)
173 186
              let real = Real.create_q ratio s in
174
              mkexpr
175
                Location.dummy_loc
176
                (Expr_const
177
                   (Const_real real))
187
              mkexpr Location.dummy_loc (Expr_const (Const_real real))
178 188
            else if Z3.Arithmetic.is_int ze then
179
              mkexpr
180
                Location.dummy_loc
189
              mkexpr Location.dummy_loc
181 190
                (Expr_const
182
                   (Const_int 
183
                      (Z.to_int (Z3.Arithmetic.Integer.get_big_int ze))))
191
                   (Const_int (Z.to_int (Z3.Arithmetic.Integer.get_big_int ze))))
184 192
            else if Z3.Expr.is_const ze then
185 193
              match Z3.Expr.to_string ze with
186
              | "true" -> mkexpr Location.dummy_loc
187
                            (Expr_const (Const_tag (tag_true)))
194
              | "true" ->
195
                mkexpr Location.dummy_loc (Expr_const (Const_tag tag_true))
188 196
              | "false" ->
189
                 mkexpr Location.dummy_loc
190
                   (Expr_const (Const_tag (tag_false)))
191
              | _ -> assert false
192
            else
193
              (
194
                Format.eprintf "Const err: %s %b@." (Z3.Expr.to_string ze) (Z3.Expr.is_const ze);
195
                assert false (* a numeral but no int nor real *)
196
              )
197
                mkexpr Location.dummy_loc (Expr_const (Const_tag tag_false))
198
              | _ ->
199
                assert false
200
            else (
201
              Format.eprintf "Const err: %s %b@." (Z3.Expr.to_string ze)
202
                (Z3.Expr.is_const ze);
203
              assert false (* a numeral but no int nor real *))
197 204
          in
198 205
          None, Some e
199 206
        else
200 207
          match op with
201
          | "not" | "=" | "-" | "*" | "/"
202
            | ">=" | "<=" | ">" | "<" 
203
            ->
204
             let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in
205
             None, Some (mkpredef_call Location.dummy_loc op args)
206
          | "+" -> ( (* Special treatment of + for 2+ args *)
208
          | "not" | "=" | "-" | "*" | "/" | ">=" | "<=" | ">" | "<" ->
207 209
            let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in
208
            let e = match args with
209
                [] -> assert false
210
              | [hd] -> hd
211
              | e1::e2::tl ->
212
                 let first_binary_and = mkpredef_call Location.dummy_loc op [e1;e2] in
213
                 if tl = [] then first_binary_and else
214
                   List.fold_left (fun e e_new ->
215
                       mkpredef_call Location.dummy_loc op [e;e_new]
216
                     ) first_binary_and tl
217
                 
210
            None, Some (mkpredef_call Location.dummy_loc op args)
211
          | "+" ->
212
            (* Special treatment of + for 2+ args *)
213
            let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in
214
            let e =
215
              match args with
216
              | [] ->
217
                assert false
218
              | [ hd ] ->
219
                hd
220
              | e1 :: e2 :: tl ->
221
                let first_binary_and =
222
                  mkpredef_call Location.dummy_loc op [ e1; e2 ]
223
                in
224
                if tl = [] then first_binary_and
225
                else
226
                  List.fold_left
227
                    (fun e e_new ->
228
                      mkpredef_call Location.dummy_loc op [ e; e_new ])
229
                    first_binary_and tl
218 230
            in
219
            None, Some e 
220
          )
231

  
232
            None, Some e
221 233
          | "and" | "or" -> (
222 234
            (* Special case since it can contain is_init pred *)
223 235
            let args = List.map (fun ze -> ze2e ze) zel in
224
            let op = if op = "and" then "&&" else if op = "or" then "||" else assert false in 
236
            let op =
237
              if op = "and" then "&&"
238
              else if op = "or" then "||"
239
              else assert false
240
            in
225 241
            match args with
226
            | [] -> assert false
227
            | [hd] -> hd
228
            | hd::tl ->
229
               List.fold_left
230
                 (fun (is_init_opt1, expr_opt1) (is_init_opt2, expr_opt2) ->
231
                   (match is_init_opt1, is_init_opt2 with
232
                      None, x | x, None -> x
233
                      | Some _, Some _ -> assert false),
234
                   (match expr_opt1, expr_opt2 with
235
                    | None, x | x, None -> x
242
            | [] ->
243
              assert false
244
            | [ hd ] ->
245
              hd
246
            | hd :: tl ->
247
              List.fold_left
248
                (fun (is_init_opt1, expr_opt1) (is_init_opt2, expr_opt2) ->
249
                  ( (match is_init_opt1, is_init_opt2 with
250
                    | None, x | x, None ->
251
                      x
252
                    | Some _, Some _ ->
253
                      assert false),
254
                    match expr_opt1, expr_opt2 with
255
                    | None, x | x, None ->
256
                      x
236 257
                    | Some e1, Some e2 ->
237
                       Some (mkpredef_call Location.dummy_loc op [e1; e2])
238
                 ))
239
                 hd tl 
240
          )
241
          | op -> 
242
             let args = List.map (fun ze ->  (snd (ze2e ze))) zel in
243
             Format.eprintf "deal with op %s (nb args: %i). Expr is %s@."  op (List.length args) (Z3.Expr.to_string ze); assert false
244
      )
258
                      Some (mkpredef_call Location.dummy_loc op [ e1; e2 ]) ))
259
                hd tl)
260
          | op ->
261
            let args = List.map (fun ze -> snd (ze2e ze)) zel in
262
            Format.eprintf "deal with op %s (nb args: %i). Expr is %s@." op
263
              (List.length args) (Z3.Expr.to_string ze);
264
            assert false)
245 265
  in
246
  (fun e -> e2ze e), (fun ze -> ze2e ze)
266
  (fun e -> e2ze e), fun ze -> ze2e ze
247 267

  
248
               
249 268
let zexpr_to_guard_list ze =
250 269
  let init_opt, expr_opt = zexpr_to_expr ze in
251
  (match init_opt with
252
   | None -> []
253
   |Some b -> [IsInit, b]
254
  ) @ (match expr_opt with
255
       | None -> []
256
       | Some e -> [Expr e, true]
257
      )
258
                
259
               
270
  (match init_opt with None -> [] | Some b -> [ IsInit, b ])
271
  @ match expr_opt with None -> [] | Some e -> [ Expr e, true ]
272

  
260 273
let simplify_neg_guard l =
261
  List.map (fun (g,posneg) ->
274
  List.map
275
    (fun (g, posneg) ->
262 276
      match g with
263
      | IsInit -> g, posneg
277
      | IsInit ->
278
        g, posneg
264 279
      | Expr g ->
265
          if posneg then
266
            Expr (Corelang.push_negations g),
267
            true
268
          else
269
            (* Pushing the negation in the expression *)
270
            Expr(Corelang.push_negations ~neg:true g),
271
            true
272
    ) l 
280
        if posneg then Expr (Corelang.push_negations g), true
281
        else
282
          (* Pushing the negation in the expression *)
283
          Expr (Corelang.push_negations ~neg:true g), true)
284
    l
273 285

  
274
(* TODO:
275
individuellement demander si g1 => g2. Si c'est le cas, on peut ne garder que g1 dans la liste
276
*)    
286
(* TODO: individuellement demander si g1 => g2. Si c'est le cas, on peut ne
287
   garder que g1 dans la liste *)
277 288
(*****************************************************************)
278 289
(* Checking sat(isfiability) of an expression and simplifying it *)
279 290
(* All (free) variables have to be declared in the Z3 context    *)
280 291
(*****************************************************************)
281
(*
282
let goal_simplify zl =
283
  let goal = Z3.Goal.mk_goal !ctx false false false in
284
  Z3.Goal.add goal zl;
285
  let goal' = Z3.Goal.simplify goal None in
286
  (* Format.eprintf "Goal before: %s@.Goal after : %s@.Sat? %s@."
287
   *   (Z3.Goal.to_string goal)
288
   *   (Z3.Goal.to_string goal')
289
   *   (Z3.Solver.string_of_status status_res) 
290
   * ; *)
291
  let ze = Z3.Goal.as_expr goal' in
292
  (* Format.eprintf "as an expr: %s@." (Z3.Expr.to_string ze); *)
293
  zexpr_to_guard_list ze
294
  *)
295
  
292
(* let goal_simplify zl = let goal = Z3.Goal.mk_goal !ctx false false false in
293
   Z3.Goal.add goal zl; let goal' = Z3.Goal.simplify goal None in (*
294
   Format.eprintf "Goal before: %s@.Goal after : %s@.Sat? %s@." *
295
   (Z3.Goal.to_string goal) * (Z3.Goal.to_string goal') *
296
   (Z3.Solver.string_of_status status_res) * ; *) let ze = Z3.Goal.as_expr goal'
297
   in (* Format.eprintf "as an expr: %s@." (Z3.Expr.to_string ze); *)
298
   zexpr_to_guard_list ze *)
299

  
296 300
let implies =
297
  let ze_implies_hash : ((Utils.tag * Utils.tag), bool) Hashtbl.t  = Hashtbl.create 13 in
301
  let ze_implies_hash : (Utils.tag * Utils.tag, bool) Hashtbl.t =
302
    Hashtbl.create 13
303
  in
298 304
  fun ze1 ze2 ->
299
  let ze1_uid = get_zid ze1 in
300
  let ze2_uid = get_zid ze2 in
301
  if Hashtbl.mem ze_implies_hash (ze1_uid, ze2_uid) then
302
    Hashtbl.find ze_implies_hash (ze1_uid, ze2_uid)
303
  else
304
    begin
305
      if !seal_debug then (
306
        report ~level:6 (fun fmt -> Format.fprintf fmt "Checking implication: %s => %s?@ "
307
          (Z3.Expr.to_string ze1) (Z3.Expr.to_string ze2)
308
      )); 
305
    let ze1_uid = get_zid ze1 in
306
    let ze2_uid = get_zid ze2 in
307
    if Hashtbl.mem ze_implies_hash (ze1_uid, ze2_uid) then
308
      Hashtbl.find ze_implies_hash (ze1_uid, ze2_uid)
309
    else (
310
      if !seal_debug then
311
        report ~level:6 (fun fmt ->
312
            Format.fprintf fmt "Checking implication: %s => %s?@ "
313
              (Z3.Expr.to_string ze1) (Z3.Expr.to_string ze2));
309 314
      let solver = Z3.Solver.mk_simple_solver !ctx in
310 315
      let tgt = Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_implies !ctx ze1 ze2) in
311 316
      let res =
312 317
        try
313
          let status_res = Z3.Solver.check solver [tgt] in
318
          let status_res = Z3.Solver.check solver [ tgt ] in
314 319
          match status_res with
315
          | Z3.Solver.UNSATISFIABLE -> if !seal_debug then
316
                                         report ~level:6 (fun fmt -> Format.fprintf fmt "Valid!@ "); 
317
             true
318
          | _ -> if !seal_debug then report ~level:6 (fun fmt -> Format.fprintf fmt "not proved valid@ "); 
319
             false
320
        with Zustre_common.UnknownFunction(_, msg) -> (
320
          | Z3.Solver.UNSATISFIABLE ->
321
            if !seal_debug then
322
              report ~level:6 (fun fmt -> Format.fprintf fmt "Valid!@ ");
323
            true
324
          | _ ->
325
            if !seal_debug then
326
              report ~level:6 (fun fmt ->
327
                  Format.fprintf fmt "not proved valid@ ");
328
            false
329
        with Zustre_common.UnknownFunction (_, msg) ->
321 330
          report ~level:1 msg;
322 331
          false
323
        )
324 332
      in
325
      Hashtbl.add ze_implies_hash (ze1_uid,ze2_uid) res ;
326
      res
327
    end
328
                                               
333
      Hashtbl.add ze_implies_hash (ze1_uid, ze2_uid) res;
334
      res)
335

  
329 336
let rec simplify zl =
330 337
  match zl with
331
  | [] | [_] -> zl
332
  | hd::tl -> (
333
    (* Forall e in tl, checking whether hd => e or e => hd, to keep hd
334
     in the first case and e in the second one *)
338
  | [] | [ _ ] ->
339
    zl
340
  | hd :: tl ->
341
    (* Forall e in tl, checking whether hd => e or e => hd, to keep hd in the
342
       first case and e in the second one *)
335 343
    let tl = simplify tl in
336 344
    let keep_hd, tl =
337
      List.fold_left (fun (keep_hd, accu) e ->
338
          if implies hd e then
339
            true, accu (* throwing away e *)
340
          else if implies e hd then
341
            false, e::accu (* throwing away hd *)
342
          else
343
            keep_hd, e::accu (* keeping both *)
344
        ) (true,[]) tl
345
      List.fold_left
346
        (fun (keep_hd, accu) e ->
347
          if implies hd e then true, accu (* throwing away e *)
348
          else if implies e hd then false, e :: accu (* throwing away hd *)
349
          else keep_hd, e :: accu (* keeping both *))
350
        (true, []) tl
345 351
    in
346 352
    (* Format.eprintf "keep_hd?%b hd=%s, tl=[%a]@."
347 353
     *   keep_hd
348 354
     *   (Z3.Expr.to_string hd)
349 355
     * (Utils.fprintf_list ~sep:"; " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) tl
350 356
     *   ; *)
351
    if keep_hd then
352
      hd::tl
353
    else
354
      tl
355
  )
356
  
357
let check_sat ?(just_check=false) (l: elem_boolexpr guard) : bool * (elem_boolexpr guard) =
357
    if keep_hd then hd :: tl else tl
358

  
359
let check_sat ?(just_check = false) (l : elem_boolexpr guard) :
360
    bool * elem_boolexpr guard =
358 361
  (* Syntactic simplification *)
359
  if false then
360
    Format.eprintf "Before simplify: %a@." (pp_guard_list pp_elem) l; 
362
  if false then Format.eprintf "Before simplify: %a@." (pp_guard_list pp_elem) l;
361 363
  let l = simplify_neg_guard l in
362 364
  if false then (
363
    Format.eprintf "After simplify: %a@." (pp_guard_list pp_elem) l; 
364
    Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " (pp_guard_list pp_elem)l;
365
  );
366
  
365
    Format.eprintf "After simplify: %a@." (pp_guard_list pp_elem) l;
366
    Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " (pp_guard_list pp_elem) l);
367

  
367 368
  let solver = Z3.Solver.mk_simple_solver !ctx in
368
  try (
369
  try
369 370
    let zl =
370
      List.map (fun (e, posneg) ->
371
      List.map
372
        (fun (e, posneg) ->
371 373
          let ze =
372
            match e with
373
            | IsInit -> is_init_z3e
374
            | Expr e -> expr_to_z3_expr e 
374
            match e with IsInit -> is_init_z3e | Expr e -> expr_to_z3_expr e
375 375
          in
376
          if posneg then
377
            ze
378
          else
379
            neg_ze ze
380
        ) l
376
          if posneg then ze else neg_ze ze)
377
        l
381 378
    in
382
    if false then Format.eprintf "Z3 exprs1: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; 
379
    if false then
380
      Format.eprintf "Z3 exprs1: [%a]@ "
381
        (fprintf_list ~sep:",@ " (fun fmt e ->
382
             Format.fprintf fmt "%s" (Z3.Expr.to_string e)))
383
        zl;
383 384
    let zl = simplify zl in
384
    if false then Format.eprintf "Z3 exprs2: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; 
385
    if false then
386
      Format.eprintf "Z3 exprs2: [%a]@ "
387
        (fprintf_list ~sep:",@ " (fun fmt e ->
388
             Format.fprintf fmt "%s" (Z3.Expr.to_string e)))
389
        zl;
385 390
    (* Format.eprintf "Calling Z3@."; *)
386 391
    let status_res = Z3.Solver.check solver zl in
387 392
    (* Format.eprintf "Z3 done@."; *)
388
     if false then Format.eprintf "Z3 status: %s@ @]@. " (Z3.Solver.string_of_status status_res); 
393
    if false then
394
      Format.eprintf "Z3 status: %s@ @]@. "
395
        (Z3.Solver.string_of_status status_res);
389 396
    match status_res with
390
    | Z3.Solver.UNSATISFIABLE -> false, []
391
    | _ -> (
392
      if false && just_check then
393
        true, l
397
    | Z3.Solver.UNSATISFIABLE ->
398
      false, []
399
    | _ ->
400
      if false && just_check then true, l
394 401
      else
395 402
        (* TODO: may be reactivate but it may create new expressions *)
396 403
        (* let l = goal_simplify zl in *)
397
        let l = List.fold_left
398
                  (fun accu ze -> accu @ (zexpr_to_guard_list ze))
399
                  []
400
                  zl
404
        let l =
405
          List.fold_left (fun accu ze -> accu @ zexpr_to_guard_list ze) [] zl
401 406
        in
402
  (* Format.eprintf "@.@[<v 2>Check_Sat:@ before: %a@ after:
403
       %a@. Goal precise? %b/%b@]@.@. " * pp_guard_list l
404
       pp_guard_list l' * (Z3.Goal.is_precise goal) *
405
       (Z3.Goal.is_precise goal'); *)
406
  
407 407

  
408
        (* Format.eprintf "@.@[<v 2>Check_Sat:@ before: %a@ after: %a@. Goal
409
           precise? %b/%b@]@.@. " * pp_guard_list l pp_guard_list l' *
410
           (Z3.Goal.is_precise goal) * (Z3.Goal.is_precise goal'); *)
408 411
        true, l
409
        
410
         
411
    )
412
         
413
  )
414
  with Zustre_common.UnknownFunction(_, msg) -> (
412
  with Zustre_common.UnknownFunction (_, msg) ->
415 413
    report ~level:1 msg;
416
    true, l (* keeping everything. *)
417
  )
418
      
419
  
420

  
414
    true, l
415
(* keeping everything. *)
421 416

  
422 417
(**************************************************************)
423 418

  
424
  
425 419
let clean_sys sys =
426
  List.fold_left (fun accu (guards, updates) ->
427
      let sat, guards' =  check_sat (List.map (fun (g, pn) -> Expr g, pn) guards) in
428
      (*Format.eprintf "Guard: %a@.Guard cleaned: %a@.Sat? %b@."
429
        (fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr))  guards
430
        (fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr))  guards'
431
        sat
432

  
433
      ;*)
434
        if sat then
435
        (List.map (fun (e, b) -> (deelem e, b)) guards', updates)::accu
436
      else
437
        accu
438
    )
420
  List.fold_left
421
    (fun accu (guards, updates) ->
422
      let sat, guards' =
423
        check_sat (List.map (fun (g, pn) -> Expr g, pn) guards)
424
      in
425
      (*Format.eprintf "Guard: %a@.Guard cleaned: %a@.Sat? %b@." (fprintf_list
426
        ~sep:"@ " (pp_guard_expr Printers.pp_expr)) guards (fprintf_list ~sep:"@
427
        " (pp_guard_expr Printers.pp_expr)) guards' sat
428

  
429
        ;*)
430
      if sat then
431
        (List.map (fun (e, b) -> deelem e, b) guards', updates) :: accu
432
      else accu)
439 433
    [] sys
440 434

  
441
(* Most costly function: has the be efficiently implemented.  All
442
   registered guards are initially produced by the call to
443
   combine_guards. We csan normalize the guards to ease the
444
   comparisons.
445

  
446
   We assume that gl1 and gl2 are already both satisfiable and in a
447
   kind of reduced form. Let lshort and llong be the short and long
448
   list of gl1, gl2. We check whether each element elong of llong is
449
   satisfiable with lshort. If no, stop. If yes, we search to reduce
450
   the list. If elong => eshort_i, we can remove eshort_i from
451
   lshort. we can continue with this lshort shortened, lshort'; it is
452
   not necessary to add yet elong in lshort' since we already know
453
   rthat elong is somehow reduced with respect to other elements of
454
   llong. If eshort_i => elong, then we keep ehosrt_i in lshort and do
455
   not store elong.
456

  
457
   After iterating through llong, we have a shortened version of
458
   lshort + some elements of llong that have to be remembered. We add
459
   them to this new consolidated list. 
460

  
461
 *)
462

  
463
(* combine_guards ~fresh:Some(e,b) gl1 gl2 returns ok, gl with ok=true
464
   when (e=b) ang gl1 and gl2 is satisfiable and gl is a consilidated
465
   version of it.  *)
466
let combine_guards ?(fresh=None) gl1 gl2 =
467
  (* Filtering out trivial cases. More semantics ones would have to be
468
     addressed later *)
469
  let check_sat e = (* temp function before we clean the original one *)
435
(* Most costly function: has the be efficiently implemented. All registered
436
   guards are initially produced by the call to combine_guards. We csan
437
   normalize the guards to ease the comparisons.
438

  
439
   We assume that gl1 and gl2 are already both satisfiable and in a kind of
440
   reduced form. Let lshort and llong be the short and long list of gl1, gl2. We
441
   check whether each element elong of llong is satisfiable with lshort. If no,
442
   stop. If yes, we search to reduce the list. If elong => eshort_i, we can
443
   remove eshort_i from lshort. we can continue with this lshort shortened,
444
   lshort'; it is not necessary to add yet elong in lshort' since we already
445
   know rthat elong is somehow reduced with respect to other elements of llong.
446
   If eshort_i => elong, then we keep ehosrt_i in lshort and do not store elong.
447

  
448
   After iterating through llong, we have a shortened version of lshort + some
449
   elements of llong that have to be remembered. We add them to this new
450
   consolidated list. *)
451

  
452
(* combine_guards ~fresh:Some(e,b) gl1 gl2 returns ok, gl with ok=true when
453
   (e=b) ang gl1 and gl2 is satisfiable and gl is a consilidated version of it. *)
454
let combine_guards ?(fresh = None) gl1 gl2 =
455
  (* Filtering out trivial cases. More semantics ones would have to be addressed
456
     later *)
457
  let check_sat e =
458
    (* temp function before we clean the original one *)
470 459
    (* Format.eprintf "CheckSAT? %a@." (pp_guard_list pp_elem) e; *)
471 460
    let ok, _ = check_sat e in
472 461
    (* Format.eprintf "CheckSAT DONE@."; *)
473 462
    ok
474 463
  in
475
  let implies (e1,pn1) (e2,pn2) =
464
  let implies (e1, pn1) (e2, pn2) =
476 465
    let e2z e pn =
477 466
      match e with
478
        | IsInit -> if pn then is_init_z3e else neg_ze is_init_z3e
479
        | Expr e -> expr_to_z3_expr (if pn then e else (Corelang.push_negations ~neg:true e))
480
      in
467
      | IsInit ->
468
        if pn then is_init_z3e else neg_ze is_init_z3e
469
      | Expr e ->
470
        expr_to_z3_expr (if pn then e else Corelang.push_negations ~neg:true e)
471
    in
481 472
    implies (e2z e1 pn1) (e2z e2 pn2)
482 473
  in
483 474
  let lshort, llong =
484 475
    if List.length gl1 > List.length gl2 then gl2, gl1 else gl1, gl2
485 476
  in
486 477
  let merge long short =
487
    let short, long_sel, ok = 
488
    List.fold_left (fun (short,long_sel, ok) long_e ->
489
        if not ok then
490
          [],[], false (* Propagating unsat case *)
491
        else if check_sat (long_e::short) then
492
          let short, keep_long_e =
493
            List.fold_left (fun (accu_short, keep_long_e) eshort_i ->
494
                if not keep_long_e then (* shorten the algo *)
495
                  eshort_i :: accu_short, false
496
                else (* keep_long_e = true in the following *)
497
                  if implies eshort_i long_e then
478
    let short, long_sel, ok =
479
      List.fold_left
480
        (fun (short, long_sel, ok) long_e ->
481
          if not ok then [], [], false (* Propagating unsat case *)
482
          else if check_sat (long_e :: short) then
483
            let short, keep_long_e =
484
              List.fold_left
485
                (fun (accu_short, keep_long_e) eshort_i ->
486
                  if not keep_long_e then
487
                    (* shorten the algo *)
488
                    eshort_i :: accu_short, false
489
                  else if
490
                    (* keep_long_e = true in the following *)
491
                    implies eshort_i long_e
492
                  then
498 493
                    (* First case is trying to remove long_e!
499 494

  
500
                     Since short is already normalized, we can remove
501
                     long_e. If later long_e is stronger than another
502
                     element of short, then necessarily eshort_i =>
503
                     long_e ->
504
                     that_other_element_of_short. Contradiction. *)
505
                    eshort_i::accu_short, false
506
                  else if implies long_e eshort_i then 
495
                       Since short is already normalized, we can remove long_e.
496
                       If later long_e is stronger than another element of
497
                       short, then necessarily eshort_i => long_e ->
498
                       that_other_element_of_short. Contradiction. *)
499
                    eshort_i :: accu_short, false
500
                  else if implies long_e eshort_i then
507 501
                    (* removing eshort_i, keeping long_e. *)
508 502
                    accu_short, true
509
                  else (* Not comparable, keeping both *)
510
                    eshort_i::accu_short, true
511
              )
512
              ([],true) (* Initially we assume that we will keep long_e *)
513
              short
514
          in
515
          if keep_long_e then
516
            short, long_e::long_sel, true
517
          else
518
            short, long_sel, true
519
        else
520
          [],[],false
521
      ) (short, [], true) long
503
                  else
504
                    (* Not comparable, keeping both *)
505
                    eshort_i :: accu_short, true)
506
                ([], true)
507
                (* Initially we assume that we will keep long_e *)
508
                short
509
            in
510
            if keep_long_e then short, long_e :: long_sel, true
511
            else short, long_sel, true
512
          else [], [], false)
513
        (short, [], true) long
522 514
    in
523
    ok, long_sel@short
515
    ok, long_sel @ short
524 516
  in
525
  let ok, l = match fresh with
526
    | None -> true, []
527
    | Some g -> merge [g] []
528
  in
529
  if not ok then
530
    false, []
517
  let ok, l = match fresh with None -> true, [] | Some g -> merge [ g ] [] in
518
  if not ok then false, []
531 519
  else
532 520
    let ok, lshort = merge lshort l in
533
    if not ok then
534
      false, []
535
    else
536
      merge llong lshort
537
    
538

  
539
(* Encode "If gel1=posneg then gel2":
540
   - Compute the combination of guarded exprs in gel1 and gel2:
541
     - Each guarded_expr in gel1 is transformed as a guard: the
542
       expression is associated to posneg.
543
     - Existing guards in gel2 are concatenated to that list of guards
544
     - We keep expr in the ge of gel2 as the legitimate expression 
545
 *)
521
    if not ok then false, [] else merge llong lshort
522

  
523
(* Encode "If gel1=posneg then gel2": - Compute the combination of guarded exprs
524
   in gel1 and gel2: - Each guarded_expr in gel1 is transformed as a guard: the
525
   expression is associated to posneg. - Existing guards in gel2 are
526
   concatenated to that list of guards - We keep expr in the ge of gel2 as the
527
   legitimate expression *)
546 528
let concatenate_ge gel1 posneg gel2 =
547 529
  let l, all_invalid =
548
    List.fold_left (
549
        fun (accu, all_invalid) (g2,e2) ->
550
        List.fold_left (
551
            fun (accu, all_invalid) (g1,e1) ->
552
            (* Format.eprintf "@[<v 2>Combining guards: (%a=%b) AND [%a] AND [%a]@ "
553
             *  pp_elem e1
554
             *  posneg
555
             *  pp_guard_list g1
556
             *  pp_guard_list g2; *)
557

  
558
            let ok, gl = combine_guards ~fresh:(Some(e1,posneg)) g1 g2 in
559
            (* Format.eprintf "@]@ Result is [%a]@ "
560
             *   pp_guard_list gl; *)
561

  
562
            if ok then
563
              (gl, e2)::accu, false
564
            else (
565
              accu, all_invalid
566
            )
567
          ) (accu, all_invalid) gel1
568
      ) ([], true) gel2
530
    List.fold_left
531
      (fun (accu, all_invalid) (g2, e2) ->
532
        List.fold_left
533
          (fun (accu, all_invalid) (g1, e1) ->
534
            (* Format.eprintf "@[<v 2>Combining guards: (%a=%b) AND [%a] AND
535
               [%a]@ " * pp_elem e1 * posneg * pp_guard_list g1 * pp_guard_list
536
               g2; *)
537
            let ok, gl = combine_guards ~fresh:(Some (e1, posneg)) g1 g2 in
538

  
539
            (* Format.eprintf "@]@ Result is [%a]@ " * pp_guard_list gl; *)
540
            if ok then (gl, e2) :: accu, false else accu, all_invalid)
541
          (accu, all_invalid) gel1)
542
      ([], true) gel2
569 543
  in
570 544
  not all_invalid, l
571 545

  
572
(* Transform the guard expressions ge = [gl1, e1; gl2, e2;...] as
573
   [gl1, e1=id; gl2, e2=id; ...]  *)
546
(* Transform the guard expressions ge = [gl1, e1; gl2, e2;...] as [gl1, e1=id;
547
   gl2, e2=id; ...] *)
574 548
let mk_ge_eq_id ge id =
575 549
  List.map
576 550
    (fun (gl, g_e) ->
577
      gl,
578
      if id = "true" then
579
        g_e
580
      else
581
        match g_e with
582
        | Expr g_e ->
583
           if id = "false" then
584
             Expr (Corelang.push_negations ~neg:true g_e)
585
           else  
586
             let loc = g_e.expr_loc in
587
             Expr(Corelang.mk_eq loc
588
                    g_e
589
                    (Corelang.expr_of_ident id loc))
590
        | _ -> assert false
591
    )  ge 
592

  
593
    (* Rewrite the expression expr, replacing any occurence of a variable
594
   by its definition.
595
     *)
596
let rec rewrite defs expr : elem_guarded_expr list =   
551
      ( gl,
552
        if id = "true" then g_e
553
        else
554
          match g_e with
555
          | Expr g_e ->
556
            if id = "false" then Expr (Corelang.push_negations ~neg:true g_e)
557
            else
558
              let loc = g_e.expr_loc in
559
              Expr (Corelang.mk_eq loc g_e (Corelang.expr_of_ident id loc))
560
          | _ ->
561
            assert false ))
562
    ge
563

  
564
(* Rewrite the expression expr, replacing any occurence of a variable by its
565
   definition. *)
566
let rec rewrite defs expr : elem_guarded_expr list =
597 567
  let rewrite = rewrite defs in
598 568
  let res =
599 569
    match expr.expr_desc with
600 570
    | Expr_appl (id, args, None) ->
601
       let args = rewrite args in
602
       List.map (fun (guards, e) ->
603
       let new_e =
604
         Corelang.mkexpr
605
           expr.expr_loc
606
           (Expr_appl(id, deelem e, None))
607
       in
608
       let new_e = { new_e with expr_type = expr.expr_type; expr_clock = expr.expr_clock } in
609
       guards,
610
       Expr (Corelang.partial_eval new_e) 
611
         ) args 
612
    | Expr_const _  -> [[], Expr expr]
571
      let args = rewrite args in
572
      List.map
573
        (fun (guards, e) ->
574
          let new_e =
575
            Corelang.mkexpr expr.expr_loc (Expr_appl (id, deelem e, None))
576
          in
577
          let new_e =
578
            {
579
              new_e with
580
              expr_type = expr.expr_type;
581
              expr_clock = expr.expr_clock;
582
            }
583
          in
584
          guards, Expr (Corelang.partial_eval new_e))
585
        args
586
    | Expr_const _ ->
587
      [ [], Expr expr ]
613 588
    | Expr_ident id ->
614
       if Hashtbl.mem defs id then
615
         Hashtbl.find defs id
616
       else
617
         (* id should be an input *)
618
         [[], Expr expr]
589
      if Hashtbl.mem defs id then Hashtbl.find defs id
590
      else (* id should be an input *)
591
        [ [], Expr expr ]
619 592
    | Expr_ite (g, e1, e2) ->
620
       let g = rewrite g and
621
           e1 = rewrite e1 and
622
           e2 = rewrite e2 in
623
       let ok_then, g_then = concatenate_ge g true e1 in
624
       let ok_else, g_else = concatenate_ge g false e2 in
625
       (if ok_then then g_then else [])@
626
         (if ok_else then g_else else [])
593
      let g = rewrite g and e1 = rewrite e1 and e2 = rewrite e2 in
594
      let ok_then, g_then = concatenate_ge g true e1 in
595
      let ok_else, g_else = concatenate_ge g false e2 in
596
      (if ok_then then g_then else []) @ if ok_else then g_else else []
627 597
    | Expr_merge (g_id, branches) ->
628
       if Hashtbl.mem defs g_id then
629
         let g = Hashtbl.find defs g_id in
630
         (* Format.eprintf "Expr_merge %s = %a@." g_id (pp_mdefs pp_elem) g ; *)
631
         List.fold_left (fun accu (id, e) ->
632
             let g = mk_ge_eq_id g id in
633
             let e = rewrite e in
634
             let ok, g_eq_id = concatenate_ge g true e in
635
             if ok then g_eq_id@accu else accu
636
           ) [] branches
637
       else
638
         assert false (* g should be defined already *)
598
      if Hashtbl.mem defs g_id then
599
        let g = Hashtbl.find defs g_id in
600
        (* Format.eprintf "Expr_merge %s = %a@." g_id (pp_mdefs pp_elem) g ; *)
601
        List.fold_left
602
          (fun accu (id, e) ->
603
            let g = mk_ge_eq_id g id in
604
            let e = rewrite e in
605
            let ok, g_eq_id = concatenate_ge g true e in
606
            if ok then g_eq_id @ accu else accu)
607
          [] branches
608
      else assert false (* g should be defined already *)
639 609
    | Expr_when (e, id, l) ->
640
       let e = rewrite e in
641
       let id_def = Hashtbl.find defs id in
642
       let clock = mk_ge_eq_id id_def l in
643
       let ok, new_ge = concatenate_ge clock true e in
644
       if ok then new_ge else []
645
    | Expr_arrow _ -> [[], IsInit] (* At this point the only arrow should be true -> false *)
610
      let e = rewrite e in
611
      let id_def = Hashtbl.find defs id in
612
      let clock = mk_ge_eq_id id_def l in
613
      let ok, new_ge = concatenate_ge clock true e in
614
      if ok then new_ge else []
615
    | Expr_arrow _ ->
616
      [ [], IsInit ] (* At this point the only arrow should be true -> false *)
646 617
    | Expr_tuple el ->
647
       (* Each expr is associated to its flatten guarded expr list *)
648
       let gell = List.map rewrite el in
649
       (* Computing all combinations: we obtain a list of guarded tuple *)
650
       let rec aux gell : (elem_boolexpr guard * expr list) list =
651
         match gell with
652
         | [] -> assert false (* Not happening *)
653
         | [gel] -> List.map (fun (g,e) -> g, [deelem e]) gel
654
         | gel::getl ->
655
            let getl = aux getl in
656
            List.fold_left (
657
                fun accu (g,e) ->
658
                List.fold_left (
659
                    fun accu (gl, minituple) ->
660
                    let is_compat, guard_comb = combine_guards g gl in
661
                    if is_compat then
662
                      let new_gt : elem_boolexpr guard * expr list =
663
                        (guard_comb, (deelem e)::minituple) in
664
                      new_gt::accu
665
                    else
666
                      accu
667
                    
668
                  ) accu getl
669
              ) [] gel
670
       in
671
       let gtuples = aux gell in
672
       (* Rebuilding the valid type: guarded expr list (with tuple exprs) *)
673
       List.map
674
         (fun (g,tuple) -> g, Expr (Corelang.mkexpr expr.expr_loc (Expr_tuple tuple)))
675
         gtuples
618
      (* Each expr is associated to its flatten guarded expr list *)
619
      let gell = List.map rewrite el in
620
      (* Computing all combinations: we obtain a list of guarded tuple *)
621
      let rec aux gell : (elem_boolexpr guard * expr list) list =
622
        match gell with
623
        | [] ->
624
          assert false (* Not happening *)
625
        | [ gel ] ->
626
          List.map (fun (g, e) -> g, [ deelem e ]) gel
627
        | gel :: getl ->
628
          let getl = aux getl in
629
          List.fold_left
630
            (fun accu (g, e) ->
631
              List.fold_left
632
                (fun accu (gl, minituple) ->
633
                  let is_compat, guard_comb = combine_guards g gl in
634
                  if is_compat then
635
                    let new_gt : elem_boolexpr guard * expr list =
636
                      guard_comb, deelem e :: minituple
637
                    in
638
                    new_gt :: accu
639
                  else accu)
640
                accu getl)
641
            [] gel
642
      in
643
      let gtuples = aux gell in
644
      (* Rebuilding the valid type: guarded expr list (with tuple exprs) *)
645
      List.map
646
        (fun (g, tuple) ->
647
          g, Expr (Corelang.mkexpr expr.expr_loc (Expr_tuple tuple)))
648
        gtuples
676 649
    | Expr_fby _
677
      | Expr_appl _
678
                  (* Should be removed by normalization and inlining *)
679
      -> Format.eprintf "Pb expr: %a@.@?" Printers.pp_expr expr; assert false
680
    | Expr_array _ | Expr_access _ | Expr_power _
681
                                                (* Arrays not handled here yet *)
682
      -> assert false
683
    | Expr_pre _ -> (* Not rewriting mem assign *)
684
       assert false
650
    | Expr_appl _ (* Should be removed by normalization and inlining *) ->
651
      Format.eprintf "Pb expr: %a@.@?" Printers.pp_expr expr;
652
      assert false
653
    | Expr_array _
654
    | Expr_access _
655
    | Expr_power _ (* Arrays not handled here yet *) ->
656
      assert false
657
    | Expr_pre _ ->
658
      (* Not rewriting mem assign *)
659
      assert false
685 660
  in
686 661
  (* Format.eprintf "Rewriting %a as [@[<v 0>%a@]]@ "
687 662
   *   Printers.pp_expr expr
688 663
   *   (Utils.fprintf_list ~sep:"@ "
689 664
   *        (pp_guard_expr pp_elem)) res; *)
690 665
  res
691
  
666

  
692 667
and add_def defs vid expr =
693 668
  (* Format.eprintf "Add_def: %s = %a@."
694 669
   *   vid
......
697 672
  (* Format.eprintf "-> @[<v 0>%a@]@."
698 673
   *   (Utils.fprintf_list ~sep:"@ "
699 674
   *      (pp_guard_expr pp_elem)) vid_defs; *)
700
  report ~level:6 (fun fmt -> Format.fprintf fmt  "Add_def: %s = %a@. -> @[<v 0>%a@]@."
701
      vid
702
      Printers.pp_expr expr
703
      
704
      (
705
        (Utils.fprintf_list ~sep:"@ "
706
           (pp_guard_expr pp_elem))) vid_defs);
675
  report ~level:6 (fun fmt ->
676
      Format.fprintf fmt "Add_def: %s = %a@. -> @[<v 0>%a@]@." vid
677
        Printers.pp_expr expr
678
        (Utils.fprintf_list ~sep:"@ " (pp_guard_expr pp_elem))
679
        vid_defs);
707 680
  Hashtbl.add defs vid vid_defs;
708 681
  vid_defs
709 682

  
710
(* Takes a list of guarded exprs (ge) and a guard
711
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.
683
(* Takes a list of guarded exprs (ge) and a guard returns the same list of ge
684
   splited into the ones where the guard is true and the ones where it is false.
685
   In both lists the associated ge do not mention that guard anymore.
712 686

  
713
When a given ge doesn't mention positively or negatively such guards, it is duplicated in both lists *)
714
let split_mdefs elem (mdefs: elem_guarded_expr list) =
715
  List.fold_left (
716
      fun (selected, left_out)
717
          ((guards, expr) as ge) ->
687
   When a given ge doesn't mention positively or negatively such guards, it is
688
   duplicated in both lists *)
689
let split_mdefs elem (mdefs : elem_guarded_expr list) =
690
  List.fold_left
691
    (fun (selected, left_out) ((guards, expr) as ge) ->
718 692
      (* select the element of guards that match the argument elem *)
719 693
      let sel, others_guards = List.partition (select_elem elem) guards in
720 694
      match sel with
721
      (* we extract the element from the list and add it to the
722
         appropriate list *)
723
      | [_, sel_status] ->
724
         if sel_status then
725
           (others_guards,expr)::selected, left_out
726
         else selected, (others_guards,expr)::left_out
727
      | [] -> (* no such guard exists, we have to duplicate the
728
              guard_expr in both lists *)
729
         ge::selected, ge::left_out
730
      | _ -> (
731
        Format.eprintf "@.Spliting list on elem %a.@.List:%a@."
732
          pp_elem elem
695
      (* we extract the element from the list and add it to the appropriate list *)
696
      | [ (_, sel_status) ] ->
697
        if sel_status then (others_guards, expr) :: selected, left_out
698
        else selected, (others_guards, expr) :: left_out
699
      | [] ->
700
        (* no such guard exists, we have to duplicate the guard_expr in both
701
           lists *)
702
        ge :: selected, ge :: left_out
703
      | _ ->
704
        Format.eprintf "@.Spliting list on elem %a.@.List:%a@." pp_elem elem
733 705
          (pp_mdefs pp_elem) mdefs;
734
        assert false (* more then one element selected. Should
735
                          not happen , or trival dead code like if
736
                              x then if not x then dead code *)
737
      )
738
    ) ([],[]) mdefs
739
    
740
let split_mem_defs
741
      (elem: element)
742
      (mem_defs: (ident * elem_guarded_expr list) list)
743
      :
744
      ((ident * elem_guarded_expr mdef_t) list) * ((ident * elem_guarded_expr mdef_t) list)
745
  
746
  =
747
  List.fold_right (fun (m,mdefs)
748
                       (accu_pos, accu_neg) ->
749
      let pos, neg =
750
        split_mdefs elem mdefs 
751
      in
752
      (m, pos)::accu_pos,
753
      (m, neg)::accu_neg
754
    ) mem_defs ([],[])
755

  
756

  
757
(* Split a list of mem_defs into init and step lists of guarded
758
   expressions per memory. *)
759
let split_init mem_defs =
760
  split_mem_defs IsInit mem_defs 
761

  
762
(* Previous version of the function: way too costly 
763
let pick_guard mem_defs : expr option =  
764
  let gel = List.flatten (List.map snd mem_defs) in
765
  let gl = List.flatten (List.map fst gel) in
766
  let all_guards =
767
    List.map (
768
        (* selecting guards and getting rid of boolean *)
769
        fun (e,b) ->
770
        match e with
771
        | Expr e -> e
772
        | _ -> assert false
773
      (* should have been filtered out
774
                                      yet *)
775
      ) gl
776
  in
777
  (* TODO , one could sort by occurence and provided the most common
778
     one *)
779
  try
780
  Some (List.hd all_guards)  
781
  with _ -> None
782
   *)
706
        assert false
707
      (* more then one element selected. Should not happen , or trival dead code
708
         like if x then if not x then dead code *))
709
    ([], []) mdefs
710

  
711
let split_mem_defs (elem : element)
712
    (mem_defs : (ident * elem_guarded_expr list) list) :
713
    (ident * elem_guarded_expr mdef_t) list
714
    * (ident * elem_guarded_expr mdef_t) list =
715
  List.fold_right
716
    (fun (m, mdefs) (accu_pos, accu_neg) ->
717
      let pos, neg = split_mdefs elem mdefs in
718
      (m, pos) :: accu_pos, (m, neg) :: accu_neg)
719
    mem_defs ([], [])
720

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

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

  
784 733
(* Returning the first non empty guard expression *)
785 734
let rec pick_guard mem_defs : expr option =
786 735
  match mem_defs with
787
  | [] -> None
788
  | (_, gel)::tl -> (
736
  | [] ->
737
    None
738
  | (_, gel) :: tl ->
789 739
    let found =
790
      List.fold_left (fun found (g,_) ->
740
      List.fold_left
741
        (fun found (g, _) ->
791 742
          if found = None then
792 743
            match g with
793
            | [] -> None
794
            | (Expr e, _)::_ -> Some e
795
            | (IsInit, _)::_ -> assert false (* should be removed already *)
796
          else
797
            found
798
        ) None gel
744
            | [] ->
745
              None
746
            | (Expr e, _) :: _ ->
747
              Some e
748
            | (IsInit, _) :: _ ->
749
              assert false (* should be removed already *)
750
          else found)
751
        None gel
799 752
    in
800 753
    if found = None then pick_guard tl else found
801
  )
802
          
803 754

  
804
(* Transform a list of variable * guarded exprs into a list of guarded pairs (variable, expressions)
805
*)
755
(* Transform a list of variable * guarded exprs into a list of guarded pairs
756
   (variable, expressions) *)
806 757
let rec build_switch_sys
807
          (mem_defs : (Utils.ident * elem_guarded_expr list) list )
808
          prefix
809
        :
810
          ((expr * bool) list * (ident * expr) list ) list =
758
    (mem_defs : (Utils.ident * elem_guarded_expr list) list) prefix :
759
    ((expr * bool) list * (ident * expr) list) list =
811 760
  if !seal_debug then
812
    report ~level:4 (fun fmt -> Format.fprintf fmt "@[<v 2>Build_switch with@ %a@]@."
813
                                  pp_all_defs
814
                                  mem_defs);
815
  (* if all mem_defs have empty guards, we are done, return prefix,
816
     mem_defs expr.
817

  
818
     otherwise pick a guard in one of the mem, eg (g, b) then for each
819
     other mem, one need to select the same guard g with the same
820
     status b, *)
761
    report ~level:4 (fun fmt ->
762
        Format.fprintf fmt "@[<v 2>Build_switch with@ %a@]@." pp_all_defs
763
          mem_defs);
764
  (* if all mem_defs have empty guards, we are done, return prefix, mem_defs
765
     expr.
766

  
767
     otherwise pick a guard in one of the mem, eg (g, b) then for each other
768
     mem, one need to select the same guard g with the same status b, *)
821 769
  let res =
822
  if List.for_all (fun (_, mdefs) ->
823
         (* All defs are unguarded *)
824
         match mdefs with
825
         | [[], _] -> true (* Regular unguarded expression *)
826
         | [] -> true (* A unbalanced definition of the memory. Here
827
                         we have m_{k+1} -> m_k *)
828
         | _ -> false
829
       ) mem_defs
830
  then
831
    [prefix ,
832
     List.map (fun (m,gel) ->
833
         match gel with
834
         | [_,e] ->
835
            let e =
836
              match e with
837
              | Expr e -> e
838
              | _ -> assert false (* No IsInit expression *)
839
            in
840
            m,e
841
         | [] -> m, Corelang.expr_of_ident m Location.dummy_loc
842
         | _ -> assert false
843
       ) mem_defs]
844
  else
845
    (* Picking a guard *)
846
    let elem_opt : expr option = pick_guard mem_defs in
847
    match elem_opt with
848
      None -> (
849
       Format.eprintf "Issues picking guard in mem_defs: %a@." pp_all_defs mem_defs;
850
       assert false (* Otherwise the first case should have matched *)
851
    )
852
    | Some elem -> (
853
      report ~level:4 (fun fmt -> Format.fprintf fmt "selecting guard %a@." Printers.pp_expr elem);
854
      let pos, neg =
855
        split_mem_defs
856
          (Expr elem)
857
          mem_defs
858
      in
859
      report ~level:4 (fun fmt -> Format.fprintf fmt "split by guard done@.");
860
      
861
  (*    Format.eprintf "Selected item %a in@.%a@.POS=%a@.NEG=%a@."
862
        Printers.pp_expr elem
863
        pp_all_defs mem_defs
864
        pp_all_defs pos
865
        pp_all_defs neg
866
        ;
867
   *)
868
      (* Special cases to avoid useless computations: true, false conditions *)
869
      match elem.expr_desc with
870
      (*| Expr_ident "true"  ->   build_switch_sys pos prefix *)
871
      | Expr_const (Const_tag tag) when tag = tag_true
872
        ->   build_switch_sys pos prefix
873
      (*| Expr_ident "false" ->   build_switch_sys neg prefix *)
874
      | Expr_const (Const_tag tag) when tag = tag_false 
875
        ->   build_switch_sys neg prefix
876
      | _ -> (* Regular case *)
877
         report ~level:4 (fun fmt -> Format.fprintf fmt "Building both children branches@."); 
878
         (* let _ = (
879
          *     Format.eprintf "Expr is %a@." Printers.pp_expr elem;
880
          *     match elem.expr_desc with
881
          *     | Expr_const _ -> Format.eprintf "a const@."
882
          *                     
883
          *     | Expr_ident _ -> Format.eprintf "an ident@."
884
          *     | _ -> Format.eprintf "something else@."
885
          *   )
886
          * in *)
887
         let clean l =
888
           let l = List.map (fun (e,b) -> (Expr e), b) l in
889
           report ~level:4 (fun fmt -> Format.fprintf fmt "Checking satisfiability of %a@."
890
                                     (pp_guard_list pp_elem) l
891
             );
892
           let ok, l = check_sat l in
893
           let l = List.map (fun (e,b) -> deelem e, b) l in
894
           ok, l
895
         in
896
         let pos_prefix = (elem, true)::prefix in
897
         let neg_prefix = (elem, false)::prefix in
898
         report ~level:4 (fun fmt -> Format.fprintf fmt "Cleaning branches ...@."); 
899
         let ok_pos, pos_prefix = clean pos_prefix in         
900
         report ~level:4 (fun fmt -> Format.fprintf fmt "Cleaning branche pos done@."); 
901
         let ok_neg, neg_prefix = clean neg_prefix in
902
         report ~level:4 (fun fmt -> Format.fprintf fmt "Cleaning branche neg done@."); 
903
         report ~level:4 (fun fmt -> Format.fprintf fmt "Cleaning branches done@."); 
904
         report ~level:4 (fun fmt -> Format.fprintf fmt "Enforcing %a@." Printers.pp_expr elem);
905
         let ok_l = if ok_pos then build_switch_sys pos pos_prefix else [] in
906
         report ~level:4 (fun fmt -> Format.fprintf fmt "Enforcing not(%a)@." Printers.pp_expr elem);
907
         let nok_l = if ok_neg then build_switch_sys neg neg_prefix else [] in
908
         ok_l @ nok_l
909
    )
770
    if
771
      List.for_all
772
        (fun (_, mdefs) ->
773
          (* All defs are unguarded *)
774
          match mdefs with
775
          | [ ([], _) ] ->
776
            true (* Regular unguarded expression *)
777
          | [] ->
778
            true
779
          (* A unbalanced definition of the memory. Here we have m_{k+1} -> m_k *)
780
          | _ ->
781
            false)
782
        mem_defs
783
    then
784
      [
785
        ( prefix,
786
          List.map
787
            (fun (m, gel) ->
788
              match gel with
789
              | [ (_, e) ] ->
790
                let e =
791
                  match e with Expr e -> e | _ -> assert false
792
                  (* No IsInit expression *)
793
                in
794
                m, e
795
              | [] ->
796
                m, Corelang.expr_of_ident m Location.dummy_loc
797
              | _ ->
798
                assert false)
799
            mem_defs );
800
      ]
801
    else
802
      (* Picking a guard *)
803
      let elem_opt : expr option = pick_guard mem_defs in
804
      match elem_opt with
805
      | None ->
806
        Format.eprintf "Issues picking guard in mem_defs: %a@." pp_all_defs
807
          mem_defs;
808
        assert false (* Otherwise the first case should have matched *)
809
      | Some elem -> (
810
        report ~level:4 (fun fmt ->
811
            Format.fprintf fmt "selecting guard %a@." Printers.pp_expr elem);
812
        let pos, neg = split_mem_defs (Expr elem) mem_defs in
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff