lustrec / src / tools / seal / seal_extract.ml @ 3b7f916b
History  View  Annotate  Download (33 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 
Format.eprintf "Checking implication: %s => %s? " 
329 
(Z3.Expr.to_string ze1) (Z3.Expr.to_string ze2) 
330 
; 
331 
let solver = Z3.Solver.mk_simple_solver !ctx in 
332 
let tgt = Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_implies !ctx ze1 ze2) in 
333 
let res = 
334 
try 
335 
let status_res = Z3.Solver.check solver [tgt] in 
336 
match status_res with 
337 
 Z3.Solver.UNSATISFIABLE > Format.eprintf "Valid!@."; 
338 
true 
339 
 _ > Format.eprintf "not proved valid@."; 
340 
false 
341 
with Zustre_common.UnknownFunction(id, msg) > ( 
342 
report ~level:1 msg; 
343 
false 
344 
) 
345 
in 
346 
Hashtbl.add ze_implies_hash (ze1_uid,ze2_uid) res ; 
347 
res 
348 
end 
349 

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

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

425  
426 
true, l 
427 

428 

429 
) 
430 

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

437 

438  
439  
440 
(**************************************************************) 
441  
442 

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

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

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

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

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

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

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