lustrec / src / tools / seal / seal_extract.ml @ 81229f63
History  View  Annotate  Download (39.2 KB)
1 
open Lustre_types 

2 
open Utils 
3 
open Seal_utils 
4 
open Zustre_data (* Access to Z3 context *) 
5 

6  
7 
(* Switched system extraction: expression are memoized *) 
8 
(*let expr_mem = Hashtbl.create 13*) 
9 

10 
type element = IsInit  Expr of expr 
11 

12 
type guard = (element * bool) list 
13 
type guarded_expr = guard * element 
14 
type mdef_t = guarded_expr list 
15  
16 
let pp_elem fmt e = 
17 
match e with 
18 
 IsInit > Format.fprintf fmt "init" 
19 
 Expr e > Format.fprintf fmt "%a" Printers.pp_expr e 
20  
21 
let pp_guard_list fmt gl = 
22 
(fprintf_list ~sep:"; " 
23 
(fun fmt (e,b) > if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) fmt gl 
24 

25 
let pp_guard_expr fmt (gl,e) = 
26 
Format.fprintf fmt "%a > %a" 
27 
pp_guard_list gl 
28 
pp_elem e 
29  
30 
let pp_mdefs fmt gel = fprintf_list ~sep:"@ " pp_guard_expr fmt gel 
31  
32 

33 
let add_init defs vid = 
34 
Hashtbl.add defs vid [[], IsInit] 
35  
36 
let deelem e = match e with 
37 
Expr e > e 
38 
 IsInit > assert false (* Wasn't expecting isinit here: we are building values! *) 
39  
40 
let is_eq_elem elem elem' = 
41 
match elem, elem' with 
42 
 IsInit, IsInit > true 
43 
 Expr e, Expr e' > e = e' (* 
44 
Corelang.is_eq_expr e e' *) 
45 
 _ > false 
46  
47 
let select_elem elem (gelem, _) = 
48 
is_eq_elem elem gelem 
49  
50  
51 
(**************************************************************) 
52 
(* Convert from Lustre expressions to Z3 expressions and back *) 
53 
(* All (free) variables have to be declared in the Z3 context *) 
54 
(**************************************************************) 
55  
56 
let is_init_name = "__is_init" 
57  
58 
let const_defs = Hashtbl.create 13 
59 
let is_const id = Hashtbl.mem const_defs id 
60 
let get_const id = Hashtbl.find const_defs id 
61 

62 
(* expressions are only basic constructs here, no more ite, tuples, 
63 
arrows, fby, ... *) 
64  
65 
(* Set of hash to support memoization *) 
66 
let expr_hash: (expr * Utils.tag) list ref = ref [] 
67 
let ze_hash: (Z3.Expr.expr, Utils.tag) Hashtbl.t = Hashtbl.create 13 
68 
let e_hash: (Utils.tag, Z3.Expr.expr) Hashtbl.t = Hashtbl.create 13 
69 
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 
70 
let pp_e_map fmt = List.iter (fun (e,t) > Format.fprintf fmt "%i > %a@ " t Printers.pp_expr e) !expr_hash 
71 
let pp_ze_hash fmt = pp_hash 
72 
(fun fmt e > Format.fprintf fmt "%s" (Z3.Expr.to_string e)) 
73 
Format.pp_print_int 
74 
fmt 
75 
ze_hash 
76 
let pp_e_hash fmt = pp_hash 
77 
Format.pp_print_int 
78 
(fun fmt e > Format.fprintf fmt "%s" (Z3.Expr.to_string e)) 
79 
fmt 
80 
e_hash 
81 
let mem_expr e = 
82 
(* Format.eprintf "Searching for %a in map: @[<v 0>%t@]" 
83 
* Printers.pp_expr e 
84 
* pp_e_map; *) 
85 
let res = List.exists (fun (e',_) > Corelang.is_eq_expr e e') !expr_hash in 
86 
(* Format.eprintf "found?%b@." res; *) 
87 
res 
88 

89 
let mem_zexpr ze = 
90 
Hashtbl.mem ze_hash ze 
91 
let get_zexpr e = 
92 
let eref, uid = List.find (fun (e',_) > Corelang.is_eq_expr e e') !expr_hash in 
93 
(* Format.eprintf "found expr=%a id=%i@." Printers.pp_expr eref eref.expr_tag; *) 
94 
Hashtbl.find e_hash uid 
95 
let get_expr ze = 
96 
let uid = Hashtbl.find ze_hash ze in 
97 
let e,_ = List.find (fun (e,t) > t = uid) !expr_hash in 
98 
e 
99 

100 
let neg_ze z3e = Z3.Boolean.mk_not !ctx z3e 
101 
let is_init_z3e = 
102 
Z3.Expr.mk_const_s !ctx is_init_name Zustre_common.bool_sort 
103  
104 
let get_zid (ze:Z3.Expr.expr) : Utils.tag = 
105 
try 
106 
if Z3.Expr.equal ze is_init_z3e then 1 else 
107 
if Z3.Expr.equal ze (neg_ze is_init_z3e) then 2 else 
108 
Hashtbl.find ze_hash ze 
109 
with _ > (Format.eprintf "Looking for ze %s in Hash %a" 
110 
(Z3.Expr.to_string ze) 
111 
(fun fmt hash > Hashtbl.iter (fun ze uid > Format.fprintf fmt "%s > %i@ " (Z3.Expr.to_string ze) uid) hash ) ze_hash; 
112 
assert false) 
113 
let add_expr = 
114 
let cpt = ref 0 in 
115 
fun e ze > 
116 
incr cpt; 
117 
let uid = !cpt in 
118 
expr_hash := (e, uid)::!expr_hash; 
119 
Hashtbl.add e_hash uid ze; 
120 
Hashtbl.add ze_hash ze uid 
121  
122 

123 
let expr_to_z3_expr, zexpr_to_expr = 
124 
(* List to store converted expression. *) 
125 
(* let hash = ref [] in 
126 
* let comp_expr e (e', _) = Corelang.is_eq_expr e e' in 
127 
* let comp_zexpr ze (_, ze') = Z3.Expr.equal ze ze' in *) 
128 

129 
let rec e2ze e = 
130 
if mem_expr e then ( 
131 
get_zexpr e 
132 
) 
133 
else ( 
134 
let res = 
135 
match e.expr_desc with 
136 
 Expr_const c > 
137 
let z3e = Zustre_common.horn_const_to_expr c in 
138 
add_expr e z3e; 
139 
z3e 
140 
 Expr_ident id > ( 
141 
if is_const id then ( 
142 
let c = get_const id in 
143 
let z3e = Zustre_common.horn_const_to_expr c in 
144 
add_expr e z3e; 
145 
z3e 
146 
) 
147 
else ( 
148 
let fdecl_id = Zustre_common.get_fdecl id in 
149 
let z3e = Z3.Expr.mk_const_f !ctx fdecl_id in 
150 
add_expr e z3e; 
151 
z3e 
152 
) 
153 
) 
154 
 Expr_appl (id,args, None) (* no reset *) > 
155 
let z3e = Zustre_common.horn_basic_app id e2ze (Corelang.expr_list_of_expr args) in 
156 
add_expr e z3e; 
157 
z3e 
158 
 Expr_tuple [e] > 
159 
let z3e = e2ze e in 
160 
add_expr e z3e; 
161 
z3e 
162 
 _ > ( match e.expr_desc with Expr_tuple _ > Format.eprintf "tuple e2ze(%a)@.@?" Printers.pp_expr e 
163 
 _ > Format.eprintf "e2ze(%a)@.@?" Printers.pp_expr e) 
164 
; assert false 
165 
in 
166 
res 
167 
) 
168 
in 
169 
let rec ze2e ze = 
170 
let ze_name ze = 
171 
let fd = Z3.Expr.get_func_decl ze in 
172 
Z3.Symbol.to_string (Z3.FuncDecl.get_name fd) 
173 
in 
174 
if mem_zexpr ze then 
175 
None, Some (get_expr ze) 
176 
else 
177 
let open Corelang in 
178 
let fd = Z3.Expr.get_func_decl ze in 
179 
let zel = Z3.Expr.get_args ze in 
180 
match Z3.Symbol.to_string (Z3.FuncDecl.get_name fd), zel with 
181 
(*  var, [] > (* should be in env *) get_e *) 
182  
183 
(* Extracting IsInit status *) 
184 
 "not", [ze] when ze_name ze = is_init_name > 
185 
Some false, None 
186 
 name, [] when name = is_init_name > Some true, None 
187 
(* Other constructs are converted to a lustre expression *) 
188 
 op, _ > ( 
189 

190 

191 
if Z3.Expr.is_numeral ze then 
192 
let e = 
193 
if Z3.Arithmetic.is_real ze then 
194 
let num = Num.num_of_ratio (Z3.Arithmetic.Real.get_ratio ze) in 
195 
let s = Z3.Arithmetic.Real.numeral_to_string ze in 
196 
mkexpr 
197 
Location.dummy_loc 
198 
(Expr_const 
199 
(Const_real 
200 
(num, 0, s))) 
201 
else if Z3.Arithmetic.is_int ze then 
202 
mkexpr 
203 
Location.dummy_loc 
204 
(Expr_const 
205 
(Const_int 
206 
(Big_int.int_of_big_int (Z3.Arithmetic.Integer.get_big_int ze)))) 
207 
else if Z3.Expr.is_const ze then 
208 
match Z3.Expr.to_string ze with 
209 
 "true" > mkexpr Location.dummy_loc 
210 
(Expr_const (Const_tag (tag_true))) 
211 
 "false" > 
212 
mkexpr Location.dummy_loc 
213 
(Expr_const (Const_tag (tag_false))) 
214 
 _ > assert false 
215 
else 
216 
( 
217 
Format.eprintf "Const err: %s %b@." (Z3.Expr.to_string ze) (Z3.Expr.is_const ze); 
218 
assert false (* a numeral but no int nor real *) 
219 
) 
220 
in 
221 
None, Some e 
222 
else 
223 
match op with 
224 
 "not"  "="  ""  "*"  "/" 
225 
 ">="  "<="  ">"  "<" 
226 
> 
227 
let args = List.map (fun ze > Utils.desome (snd (ze2e ze))) zel in 
228 
None, Some (mkpredef_call Location.dummy_loc op args) 
229 
 "+" > ( (* Special treatment of + for 2+ args *) 
230 
let args = List.map (fun ze > Utils.desome (snd (ze2e ze))) zel in 
231 
let e = match args with 
232 
[] > assert false 
233 
 [hd] > hd 
234 
 e1::e2::tl > 
235 
let first_binary_and = mkpredef_call Location.dummy_loc op [e1;e2] in 
236 
if tl = [] then first_binary_and else 
237 
List.fold_left (fun e e_new > 
238 
mkpredef_call Location.dummy_loc op [e;e_new] 
239 
) first_binary_and tl 
240 

241 
in 
242 
None, Some e 
243 
) 
244 
 "and"  "or" > ( 
245 
(* Special case since it can contain is_init pred *) 
246 
let args = List.map (fun ze > ze2e ze) zel in 
247 
let op = if op = "and" then "&&" else if op = "or" then "" else assert false in 
248 
match args with 
249 
 [] > assert false 
250 
 [hd] > hd 
251 
 hd::tl > 
252 
List.fold_left 
253 
(fun (is_init_opt1, expr_opt1) (is_init_opt2, expr_opt2) > 
254 
(match is_init_opt1, is_init_opt2 with 
255 
None, x  x, None > x 
256 
 Some _, Some _ > assert false), 
257 
(match expr_opt1, expr_opt2 with 
258 
 None, x  x, None > x 
259 
 Some e1, Some e2 > 
260 
Some (mkpredef_call Location.dummy_loc op [e1; e2]) 
261 
)) 
262 
hd tl 
263 
) 
264 
 op > 
265 
let args = List.map (fun ze > (snd (ze2e ze))) zel in 
266 
Format.eprintf "deal with op %s (nb args: %i). Expr is %s@." op (List.length args) (Z3.Expr.to_string ze); assert false 
267 
) 
268 
in 
269 
(fun e > e2ze e), (fun ze > ze2e ze) 
270  
271 

272 
let zexpr_to_guard_list ze = 
273 
let init_opt, expr_opt = zexpr_to_expr ze in 
274 
(match init_opt with 
275 
 None > [] 
276 
Some b > [IsInit, b] 
277 
) @ (match expr_opt with 
278 
 None > [] 
279 
 Some e > [Expr e, true] 
280 
) 
281 

282 

283 
let simplify_neg_guard l = 
284 
List.map (fun (g,posneg) > 
285 
match g with 
286 
 IsInit > g, posneg 
287 
 Expr g > 
288 
if posneg then 
289 
Expr (Corelang.push_negations g), 
290 
true 
291 
else 
292 
(* Pushing the negation in the expression *) 
293 
Expr(Corelang.push_negations ~neg:true g), 
294 
true 
295 
) l 
296  
297 
(* TODO: 
298 
individuellement demander si g1 => g2. Si c'est le cas, on peut ne garder que g1 dans la liste 
299 
*) 
300 
(*****************************************************************) 
301 
(* Checking sat(isfiability) of an expression and simplifying it *) 
302 
(* All (free) variables have to be declared in the Z3 context *) 
303 
(*****************************************************************) 
304 
(* 
305 
let goal_simplify zl = 
306 
let goal = Z3.Goal.mk_goal !ctx false false false in 
307 
Z3.Goal.add goal zl; 
308 
let goal' = Z3.Goal.simplify goal None in 
309 
(* Format.eprintf "Goal before: %s@.Goal after : %s@.Sat? %s@." 
310 
* (Z3.Goal.to_string goal) 
311 
* (Z3.Goal.to_string goal') 
312 
* (Z3.Solver.string_of_status status_res) 
313 
* ; *) 
314 
let ze = Z3.Goal.as_expr goal' in 
315 
(* Format.eprintf "as an expr: %s@." (Z3.Expr.to_string ze); *) 
316 
zexpr_to_guard_list ze 
317 
*) 
318 

319 
let implies = 
320 
let ze_implies_hash : ((Utils.tag * Utils.tag), bool) Hashtbl.t = Hashtbl.create 13 in 
321 
fun ze1 ze2 > 
322 
let ze1_uid = get_zid ze1 in 
323 
let ze2_uid = get_zid ze2 in 
324 
if Hashtbl.mem ze_implies_hash (ze1_uid, ze2_uid) then 
325 
Hashtbl.find ze_implies_hash (ze1_uid, ze2_uid) 
326 
else 
327 
begin 
328 
if !debug then ( 
329 
Format.eprintf "Checking implication: %s => %s? " 
330 
(Z3.Expr.to_string ze1) (Z3.Expr.to_string ze2) 
331 
); 
332 
let solver = Z3.Solver.mk_simple_solver !ctx in 
333 
let tgt = Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_implies !ctx ze1 ze2) in 
334 
let res = 
335 
try 
336 
let status_res = Z3.Solver.check solver [tgt] in 
337 
match status_res with 
338 
 Z3.Solver.UNSATISFIABLE > if !debug then Format.eprintf "Valid!@."; 
339 
true 
340 
 _ > if !debug then Format.eprintf "not proved valid@."; 
341 
false 
342 
with Zustre_common.UnknownFunction(id, msg) > ( 
343 
report ~level:1 msg; 
344 
false 
345 
) 
346 
in 
347 
Hashtbl.add ze_implies_hash (ze1_uid,ze2_uid) res ; 
348 
res 
349 
end 
350 

351 
let rec simplify zl = 
352 
match zl with 
353 
 []  [_] > zl 
354 
 hd::tl > ( 
355 
(* Forall e in tl, checking whether hd => e or e => hd, to keep hd 
356 
in the first case and e in the second one *) 
357 
let tl = simplify tl in 
358 
let keep_hd, tl = 
359 
List.fold_left (fun (keep_hd, accu) e > 
360 
if implies hd e then 
361 
true, accu (* throwing away e *) 
362 
else if implies e hd then 
363 
false, e::accu (* throwing away hd *) 
364 
else 
365 
keep_hd, e::accu (* keeping both *) 
366 
) (true,[]) tl 
367 
in 
368 
(* Format.eprintf "keep_hd?%b hd=%s, tl=[%a]@." 
369 
* keep_hd 
370 
* (Z3.Expr.to_string hd) 
371 
* (Utils.fprintf_list ~sep:"; " (fun fmt e > Format.fprintf fmt "%s" (Z3.Expr.to_string e))) tl 
372 
* ; *) 
373 
if keep_hd then 
374 
hd::tl 
375 
else 
376 
tl 
377 
) 
378 

379 
let check_sat ?(just_check=false) (l:guard) : bool * guard = 
380 
(* Syntactic simplification *) 
381 
if false then 
382 
Format.eprintf "Before simplify: %a@." pp_guard_list l; 
383 
let l = simplify_neg_guard l in 
384 
if false then ( 
385 
Format.eprintf "After simplify: %a@." pp_guard_list l; 
386 
Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " pp_guard_list l; 
387 
); 
388 
let solver = Z3.Solver.mk_simple_solver !ctx in 
389 
try ( 
390 
let zl = 
391 
List.map (fun (e, posneg) > 
392 
let ze = 
393 
match e with 
394 
 IsInit > is_init_z3e 
395 
 Expr e > expr_to_z3_expr e 
396 
in 
397 
if posneg then 
398 
ze 
399 
else 
400 
neg_ze ze 
401 
) l 
402 
in 
403 
if false then Format.eprintf "Z3 exprs1: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e > Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; 
404 
let zl = simplify zl in 
405 
if false then Format.eprintf "Z3 exprs2: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e > Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; 
406 
let status_res = Z3.Solver.check solver zl in 
407 
if false then Format.eprintf "Z3 status: %s@ @]@. " (Z3.Solver.string_of_status status_res); 
408 
match status_res with 
409 
 Z3.Solver.UNSATISFIABLE > false, [] 
410 
 _ > ( 
411 
if false && just_check then 
412 
true, l 
413 
else 
414 
(* TODO: may be reactivate but it may create new expressions *) 
415 
(* let l = goal_simplify zl in *) 
416 
let l = List.fold_left 
417 
(fun accu ze > accu @ (zexpr_to_guard_list ze)) 
418 
[] 
419 
zl 
420 
in 
421 
(* Format.eprintf "@.@[<v 2>Check_Sat:@ before: %a@ after: 
422 
%a@. Goal precise? %b/%b@]@.@. " * pp_guard_list l 
423 
pp_guard_list l' * (Z3.Goal.is_precise goal) * 
424 
(Z3.Goal.is_precise goal'); *) 
425 

426  
427 
true, l 
428 

429 

430 
) 
431 

432 
) 
433 
with Zustre_common.UnknownFunction(id, msg) > ( 
434 
report ~level:1 msg; 
435 
true, l (* keeping everything. *) 
436 
) 
437 

438 

439  
440  
441 
(**************************************************************) 
442  
443 

444 
let clean_sys sys = 
445 
List.fold_left (fun accu (guards, updates) > 
446 
let sat, guards' = check_sat (List.map (fun (g, pn) > Expr g, pn) guards) in 
447 
(*Format.eprintf "Guard: %a@.Guard cleaned: %a@.Sat? %b@." 
448 
(fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr)) guards 
449 
(fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr)) guards' 
450 
sat 
451  
452 
;*) 
453 
if sat then 
454 
(List.map (fun (e, b) > (deelem e, b)) guards', updates)::accu 
455 
else 
456 
accu 
457 
) 
458 
[] sys 
459  
460 
(* Most costly function: has the be efficiently implemented. All 
461 
registered guards are initially produced by the call to 
462 
combine_guards. We csan normalize the guards to ease the 
463 
comparisons. 
464  
465 
We assume that gl1 and gl2 are already both satisfiable and in a 
466 
kind of reduced form. Let lshort and llong be the short and long 
467 
list of gl1, gl2. We check whether each element elong of llong is 
468 
satisfiable with lshort. If no, stop. If yes, we search to reduce 
469 
the list. If elong => eshort_i, we can remove eshort_i from 
470 
lshort. we can continue with this lshort shortened, lshort'; it is 
471 
not necessary to add yet elong in lshort' since we already know 
472 
rthat elong is somehow reduced with respect to other elements of 
473 
llong. If eshort_i => elong, then we keep ehosrt_i in lshort and do 
474 
not store elong. 
475  
476 
After iterating through llong, we have a shortened version of 
477 
lshort + some elements of llong that have to be remembered. We add 
478 
them to this new consolidated list. 
479  
480 
*) 
481  
482 
(* combine_guards ~fresh:Some(e,b) gl1 gl2 returns ok, gl with ok=true 
483 
when (e=b) ang gl1 and gl2 is satisfiable and gl is a consilidated 
484 
version of it. *) 
485 
let combine_guards ?(fresh=None) gl1 gl2 = 
486 
(* Filtering out trivial cases. More semantics ones would have to be 
487 
addressed later *) 
488 
let check_sat e = (* temp function before we clean the original one *) 
489 
let ok, _ = check_sat e in 
490 
ok 
491 
in 
492 
let implies (e1,pn1) (e2,pn2) = 
493 
let e2z e pn = 
494 
match e with 
495 
 IsInit > if pn then is_init_z3e else neg_ze is_init_z3e 
496 
 Expr e > expr_to_z3_expr (if pn then e else (Corelang.push_negations ~neg:true e)) 
497 
in 
498 
implies (e2z e1 pn1) (e2z e2 pn2) 
499 
in 
500 
let lshort, llong = 
501 
if List.length gl1 > List.length gl2 then gl2, gl1 else gl1, gl2 
502 
in 
503 
let merge long short = 
504 
let short, long_sel, ok = 
505 
List.fold_left (fun (short,long_sel, ok) long_e > 
506 
if not ok then 
507 
[],[], false (* Propagating unsat case *) 
508 
else if check_sat (long_e::short) then 
509 
let short, keep_long_e = 
510 
List.fold_left (fun (accu_short, keep_long_e) eshort_i > 
511 
if not keep_long_e then (* shorten the algo *) 
512 
eshort_i :: accu_short, false 
513 
else (* keep_long_e = true in the following *) 
514 
if implies eshort_i long_e then 
515 
(* First case is trying to remove long_e! 
516  
517 
Since short is already normalized, we can remove 
518 
long_e. If later long_e is stronger than another 
519 
element of short, then necessarily eshort_i => 
520 
long_e > 
521 
that_other_element_of_short. Contradiction. *) 
522 
eshort_i::accu_short, false 
523 
else if implies long_e eshort_i then 
524 
(* removing eshort_i, keeping long_e. *) 
525 
accu_short, true 
526 
else (* Not comparable, keeping both *) 
527 
eshort_i::accu_short, true 
528 
) 
529 
([],true) (* Initially we assume that we will keep long_e *) 
530 
short 
531 
in 
532 
if keep_long_e then 
533 
short, long_e::long_sel, true 
534 
else 
535 
short, long_sel, true 
536 
else 
537 
[],[],false 
538 
) (short, [], true) long 
539 
in 
540 
ok, long_sel@short 
541 
in 
542 
let ok, l = match fresh with 
543 
 None > true, [] 
544 
 Some g > merge [g] [] 
545 
in 
546 
if not ok then 
547 
false, [] 
548 
else 
549 
let ok, lshort = merge lshort l in 
550 
if not ok then 
551 
false, [] 
552 
else 
553 
merge llong lshort 
554 

555  
556 
(* Encode "If gel1=posneg then gel2": 
557 
 Compute the combination of guarded exprs in gel1 and gel2: 
558 
 Each guarded_expr in gel1 is transformed as a guard: the 
559 
expression is associated to posneg. 
560 
 Existing guards in gel2 are concatenated to that list of guards 
561 
 We keep expr in the ge of gel2 as the legitimate expression 
562 
*) 
563 
let concatenate_ge gel1 posneg gel2 = 
564 
let l, all_invalid = 
565 
List.fold_left ( 
566 
fun (accu, all_invalid) (g2,e2) > 
567 
List.fold_left ( 
568 
fun (accu, all_invalid) (g1,e1) > 
569 
(* Format.eprintf "@[<v 2>Combining guards: (%a=%b) AND [%a] AND [%a]@ " 
570 
* pp_elem e1 
571 
* posneg 
572 
* pp_guard_list g1 
573 
* pp_guard_list g2; *) 
574  
575 
let ok, gl = combine_guards ~fresh:(Some(e1,posneg)) g1 g2 in 
576 
(* Format.eprintf "@]@ Result is [%a]@ " 
577 
* pp_guard_list gl; *) 
578  
579 
if ok then 
580 
(gl, e2)::accu, false 
581 
else ( 
582 
accu, all_invalid 
583 
) 
584 
) (accu, all_invalid) gel1 
585 
) ([], true) gel2 
586 
in 
587 
not all_invalid, l 
588 

589 
(* Rewrite the expression expr, replacing any occurence of a variable 
590 
by its definition. 
591 
*) 
592 
let rec rewrite defs expr : guarded_expr list = 
593 
let rewrite = rewrite defs in 
594 
let res = 
595 
match expr.expr_desc with 
596 
 Expr_appl (id, args, None) > 
597 
let args = rewrite args in 
598 
List.map (fun (guards, e) > 
599 
guards, 
600 
Expr (Corelang.mkexpr expr.expr_loc (Expr_appl(id, deelem e, None))) 
601 
) args 
602 
 Expr_const _ > [[], Expr expr] 
603 
 Expr_ident id > 
604 
if Hashtbl.mem defs id then 
605 
Hashtbl.find defs id 
606 
else 
607 
(* id should be an input *) 
608 
[[], Expr expr] 
609 
 Expr_ite (g, e1, e2) > 
610 
let g = rewrite g and 
611 
e1 = rewrite e1 and 
612 
e2 = rewrite e2 in 
613 
let ok_then, g_then = concatenate_ge g true e1 in 
614 
let ok_else, g_else = concatenate_ge g false e2 in 
615 
(if ok_then then g_then else [])@ 
616 
(if ok_else then g_else else []) 
617 
 Expr_merge (g, branches) > 
618 
assert false (* TODO: deal with merges *) 
619 

620 
 Expr_when (e, _, _) > rewrite e 
621 
 Expr_arrow _ > [[], IsInit] (* At this point the only arrow should be true > false *) 
622 
 Expr_tuple el > 
623 
(* Each expr is associated to its flatten guarded expr list *) 
624 
let gell = List.map rewrite el in 
625 
(* Computing all combinations: we obtain a list of guarded tuple *) 
626 
let rec aux gell : (guard * expr list) list = 
627 
match gell with 
628 
 [] > assert false (* Not happening *) 
629 
 [gel] > List.map (fun (g,e) > g, [deelem e]) gel 
630 
 gel::getl > 
631 
let getl = aux getl in 
632 
List.fold_left ( 
633 
fun accu (g,e) > 
634 
List.fold_left ( 
635 
fun accu (gl, minituple) > 
636 
let is_compat, guard_comb = combine_guards g gl in 
637 
if is_compat then 
638 
let new_gt : guard * expr list = (guard_comb, (deelem e)::minituple) in 
639 
new_gt::accu 
640 
else 
641 
accu 
642 

643 
) accu getl 
644 
) [] gel 
645 
in 
646 
let gtuples = aux gell in 
647 
(* Rebuilding the valid type: guarded expr list (with tuple exprs) *) 
648 
List.map 
649 
(fun (g,tuple) > g, Expr (Corelang.mkexpr expr.expr_loc (Expr_tuple tuple))) 
650 
gtuples 
651 
 Expr_fby _ 
652 
 Expr_appl _ 
653 
(* Should be removed by mormalization and inlining *) 
654 
> Format.eprintf "Pb expr: %a@.@?" Printers.pp_expr expr; assert false 
655 
 Expr_array _  Expr_access _  Expr_power _ 
656 
(* Arrays not handled here yet *) 
657 
> assert false 
658 
 Expr_pre _ > (* Not rewriting mem assign *) 
659 
assert false 
660 
in 
661 
(* Format.eprintf "Rewriting %a as [@[<v 0>%a@]]@ " 
662 
* Printers.pp_expr expr 
663 
* (Utils.fprintf_list ~sep:"@ " 
664 
* pp_guard_expr) res; *) 
665 
res 
666 
and add_def defs vid expr = 
667 
let vid_defs = rewrite defs expr in 
668 
(* Format.eprintf "Add_def: %s = %a@. > @[<v 0>%a@]@." 
669 
* vid 
670 
* Printers.pp_expr expr 
671 
* ( 
672 
* (Utils.fprintf_list ~sep:"@ " 
673 
* pp_guard_expr)) vid_defs; *) 
674 
Hashtbl.add defs vid vid_defs 
675  
676 
(* Takes a list of guarded exprs (ge) and a guard 
677 
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. 
678  
679 
When a given ge doesn't mention positively or negatively such guards, it is duplicated in both lists *) 
680 
let split_mdefs elem (mdefs: guarded_expr list) = 
681 
List.fold_left ( 
682 
fun (selected, left_out) 
683 
((guards, expr) as ge) > 
684 
(* select the element of guards that match the argument elem *) 
685 
let sel, others_guards = List.partition (select_elem elem) guards in 
686 
match sel with 
687 
(* we extract the element from the list and add it to the 
688 
appropriate list *) 
689 
 [_, sel_status] > 
690 
if sel_status then 
691 
(others_guards,expr)::selected, left_out 
692 
else selected, (others_guards,expr)::left_out 
693 
 [] > (* no such guard exists, we have to duplicate the 
694 
guard_expr in both lists *) 
695 
ge::selected, ge::left_out 
696 
 _ > ( 
697 
Format.eprintf "@.Spliting list on elem %a.@.List:%a@." 
698 
pp_elem elem 
699 
pp_mdefs mdefs; 
700 
assert false (* more then one element selected. Should 
701 
not happen , or trival dead code like if 
702 
x then if not x then dead code *) 
703 
) 
704 
) ([],[]) mdefs 
705 

706 
let split_mem_defs 
707 
(elem: element) 
708 
(mem_defs: (ident * guarded_expr list) list) 
709 
: 
710 
((ident * mdef_t) list) * ((ident * mdef_t) list) 
711 

712 
= 
713 
List.fold_right (fun (m,mdefs) 
714 
(accu_pos, accu_neg) > 
715 
let pos, neg = 
716 
split_mdefs elem mdefs 
717 
in 
718 
(m, pos)::accu_pos, 
719 
(m, neg)::accu_neg 
720 
) mem_defs ([],[]) 
721  
722  
723 
(* Split a list of mem_defs into init and step lists of guarded 
724 
expressions per memory. *) 
725 
let split_init mem_defs = 
726 
split_mem_defs IsInit mem_defs 
727  
728 
(* Previous version of the function: way too costly 
729 
let pick_guard mem_defs : expr option = 
730 
let gel = List.flatten (List.map snd mem_defs) in 
731 
let gl = List.flatten (List.map fst gel) in 
732 
let all_guards = 
733 
List.map ( 
734 
(* selecting guards and getting rid of boolean *) 
735 
fun (e,b) > 
736 
match e with 
737 
 Expr e > e 
738 
 _ > assert false 
739 
(* should have been filtered out 
740 
yet *) 
741 
) gl 
742 
in 
743 
(* TODO , one could sort by occurence and provided the most common 
744 
one *) 
745 
try 
746 
Some (List.hd all_guards) 
747 
with _ > None 
748 
*) 
749  
750 
(* Returning the first non empty guard expression *) 
751 
let rec pick_guard mem_defs : expr option = 
752 
match mem_defs with 
753 
 [] > None 
754 
 (_, gel)::tl > ( 
755 
let found = 
756 
List.fold_left (fun found (g,_) > 
757 
if found = None then 
758 
match g with 
759 
 [] > None 
760 
 (Expr e, _)::_ > Some e 
761 
 (IsInit, _)::_ > assert false (* should be removed already *) 
762 
else 
763 
found 
764 
) None gel 
765 
in 
766 
if found = None then pick_guard tl else found 
767 
) 
768 

769  
770 
(* Transform a list of variable * guarded exprs into a list of guarded pairs (variable, expressions) 
771 
*) 
772 
let rec build_switch_sys 
773 
(mem_defs : (Utils.ident * guarded_expr list) list ) 
774 
prefix 
775 
: 
776 
((expr * bool) list * (ident * expr) list ) list = 
777 
(* if all mem_defs have empty guards, we are done, return prefix, 
778 
mem_defs expr. 
779  
780 
otherwise pick a guard in one of the mem, eg (g, b) then for each 
781 
other mem, one need to select the same guard g with the same 
782 
status b, *) 
783 
if List.for_all (fun (m,mdefs) > 
784 
(* All defs are unguarded *) 
785 
match mdefs with 
786 
 [[], _] > true 
787 
 _ > false 
788 
) mem_defs 
789 
then 
790 
[prefix , 
791 
List.map (fun (m,gel) > 
792 
match gel with 
793 
 [_,e] > 
794 
let e = 
795 
match e with 
796 
 Expr e > e 
797 
 _ > assert false (* No IsInit expression *) 
798 
in 
799 
m,e 
800 
 _ > assert false 
801 
) mem_defs] 
802 
else 
803 
(* Picking a guard *) 
804 
let elem_opt : expr option = pick_guard mem_defs in 
805 
match elem_opt with 
806 
None > [] 
807 
 Some elem > ( 
808 
let pos, neg = 
809 
split_mem_defs 
810 
(Expr elem) 
811 
mem_defs 
812 
in 
813 
(* Special cases to avoid useless computations: true, false conditions *) 
814 
match elem.expr_desc with 
815 
 Expr_ident "true" > build_switch_sys pos prefix 
816 
 Expr_const (Const_tag tag) when tag = Corelang.tag_true 
817 
> build_switch_sys pos prefix 
818 
 Expr_ident "false" > build_switch_sys neg prefix 
819 
 Expr_const (Const_tag tag) when tag = Corelang.tag_false 
820 
> build_switch_sys neg prefix 
821 
 _ > (* Regular case *) 
822 
(* let _ = ( 
823 
* Format.eprintf "Expr is %a@." Printers.pp_expr elem; 
824 
* match elem.expr_desc with 
825 
*  Expr_const _ > Format.eprintf "a const@." 
826 
* 
827 
*  Expr_ident _ > Format.eprintf "an ident@." 
828 
*  _ > Format.eprintf "something else@." 
829 
* ) 
830 
* in *) 
831 
let clean l = 
832 
let l = List.map (fun (e,b) > (Expr e), b) l in 
833 
let ok, l = check_sat l in 
834 
let l = List.map (fun (e,b) > deelem e, b) l in 
835 
ok, l 
836 
in 
837 
let pos_prefix = (elem, true)::prefix in 
838 
let neg_prefix = (elem, false)::prefix in 
839 
let ok_pos, pos_prefix = clean pos_prefix in 
840 
let ok_neg, neg_prefix = clean neg_prefix in 
841 
(if ok_pos then build_switch_sys pos pos_prefix else []) 
842 
@ 
843 
(if ok_neg then build_switch_sys neg neg_prefix else []) 
844 
) 
845  
846  
847 

848 
(* Take a normalized node and extract a list of switches: (cond, 
849 
update) meaning "if cond then update" where update shall define all 
850 
node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *) 
851 
let node_as_switched_sys consts (mems:var_decl list) nd = 
852 
(* rescheduling node: has been scheduled already, no need to protect 
853 
the call to schedule_node *) 
854 
let nd_report = Scheduling.schedule_node nd in 
855 
let schedule = nd_report.Scheduling_type.schedule in 
856 
let eqs, auts = Corelang.get_node_eqs nd in 
857 
assert (auts = []); (* Automata should be expanded by now *) 
858 
let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in 
859 
let defs : (ident, guarded_expr list) Hashtbl.t = Hashtbl.create 13 in 
860 
let add_def = add_def defs in 
861  
862 
let vars = Corelang.get_node_vars nd in 
863 
(* Registering all locals variables as Z3 predicates. Will be use to 
864 
simplify the expansion *) 
865 
let _ = 
866 
List.iter (fun v > 
867 
let fdecl = Z3.FuncDecl.mk_func_decl_s 
868 
!ctx 
869 
v.var_id 
870 
[] 
871 
(Zustre_common.type_to_sort v.var_type) 
872 
in 
873 
ignore (Zustre_common.register_fdecl v.var_id fdecl) 
874 
) vars 
875 
in 
876 
let _ = 
877 
List.iter (fun c > Hashtbl.add const_defs c.const_id c.const_value) consts 
878 
in 
879  
880 

881 
(* Registering node equations: identifying mem definitions and 
882 
storing others in the "defs" hashtbl. 
883  
884 
Each assign is stored in a hash tbl as list of guarded 
885 
expressions. The memory definition is also "rewritten" as such a 
886 
list of guarded assigns. *) 
887 
let mem_defs = 
888 
List.fold_left (fun accu eq > 
889 
match eq.eq_lhs with 
890 
 [vid] > 
891 
(* Only focus on non memory definitions *) 
892 
if not (List.exists (fun v > v.var_id = vid) mems) then ( 
893 
report ~level:3 (fun fmt > 
894 
Format.fprintf fmt "Registering variable %s@." vid); 
895 
add_def vid eq.eq_rhs; 
896 
accu 
897 
) 
898 
else 
899 
( 
900 
match eq.eq_rhs.expr_desc with 
901 
 Expr_pre def_m > 
902 
report ~level:3 (fun fmt > 
903 
Format.fprintf fmt "Preparing mem %s@." vid); 
904 
(vid, rewrite defs def_m)::accu 
905 
 _ > assert false 
906 
) 
907 
 _ > assert false (* should have been removed by normalization *) 
908 
) [] sorted_eqs 
909 
in 
910  
911 

912 
report ~level:2 (fun fmt > Format.fprintf fmt "Printing out (guarded) memories definitions (may takes time)@."); 
913 
(* Printing memories definitions *) 
914 
report ~level:3 
915 
(fun fmt > 
916 
Format.fprintf fmt 
917 
"@[<v 0>%a@]@ " 
918 
(Utils.fprintf_list ~sep:"@ " 
919 
(fun fmt (m,mdefs) > 
920 
Format.fprintf fmt 
921 
"%s > [@[<v 0>%a@] ]@ " 
922 
m 
923 
(Utils.fprintf_list ~sep:"@ " 
924 
pp_guard_expr) mdefs 
925 
)) 
926 
mem_defs); 
927 
(* Format.eprintf "Split init@."; *) 
928 
let init_defs, update_defs = 
929 
split_init mem_defs 
930 
in 
931 
report ~level:3 
932 
(fun fmt > 
933 
Format.fprintf fmt 
934 
"@[<v 0>Init:@ %a@ Step@ %a@]@ " 
935 
(Utils.fprintf_list ~sep:"@ " 
936 
(fun fmt (m,mdefs) > 
937 
Format.fprintf fmt 
938 
"%s > @[<v 0>[%a@] ]@ " 
939 
m 
940 
(Utils.fprintf_list ~sep:"@ " 
941 
pp_guard_expr) mdefs 
942 
)) 
943 
init_defs 
944 
(Utils.fprintf_list ~sep:"@ " 
945 
(fun fmt (m,mdefs) > 
946 
Format.fprintf fmt 
947 
"%s > @[<v 0>[%a@] ]@ " 
948 
m 
949 
(Utils.fprintf_list ~sep:"@ " 
950 
pp_guard_expr) mdefs 
951 
)) 
952 
update_defs); 
953 
(* Format.eprintf "Build init@."; *) 
954  
955 
let sw_init= 
956 
build_switch_sys init_defs [] 
957 
in 
958 
(* Format.eprintf "Build step@."; *) 
959 
let sw_sys = 
960 
build_switch_sys update_defs [] 
961 
in 
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 