Revision 3b7f916b src/tools/seal/seal_extract.ml
src/tools/seal/seal_extract.ml  

4  4 
open Zustre_data (* Access to Z3 context *) 
5  5 

6  6  
7 
(* Switched system extraction *) 

7 
(* Switched system extraction: expression are memoized *) 

8 
(*let expr_mem = Hashtbl.create 13*) 

9 


8  10 
type element = IsInit  Expr of expr 
11 


9  12 
type guard = (element * bool) list 
10  13 
type guarded_expr = guard * element 
11  14 
type mdef_t = guarded_expr list 
...  ...  
13  16 
let pp_elem fmt e = 
14  17 
match e with 
15  18 
 IsInit > Format.fprintf fmt "init" 
16 
 Expr e > Printers.pp_expr fmt e


19 
 Expr e > Format.fprintf fmt "%a" Printers.pp_expr e


17  20  
18  21 
let pp_guard_list fmt gl = 
19  22 
(fprintf_list ~sep:"; " 
...  ...  
37  40 
let is_eq_elem elem elem' = 
38  41 
match elem, elem' with 
39  42 
 IsInit, IsInit > true 
40 
 Expr e, Expr e' > 

41 
Corelang.is_eq_expr e e' 

43 
 Expr e, Expr e' > e = e' (*


44 
Corelang.is_eq_expr e e' *)


42  45 
 _ > false 
43  46  
44  47 
let select_elem elem (gelem, _) = 
...  ...  
58  61 

59  62 
(* expressions are only basic constructs here, no more ite, tuples, 
60  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 


61  123 
let expr_to_z3_expr, zexpr_to_expr = 
62  124 
(* List to store converted expression. *) 
63 
let hash = ref [] in 

64 
let comp_expr e (e', _) = Corelang.is_eq_expr e e' in 

65 
let comp_zexpr ze (_, ze') = Z3.Expr.equal ze ze' in 

66 
let mem_expr e = List.exists (comp_expr e) !hash in 

67 
let mem_zexpr ze = List.exists (comp_zexpr ze) !hash in 

68 
let get_zexpr e = 

69 
let (_, ze) = List.find (comp_expr e) !hash in 

70 
ze 

71 
in 

72 
let get_expr ze = 

73 
let (e, _) = List.find (comp_zexpr ze) !hash in 

74 
e 

75 
in 

76 
let add_expr e ze = hash := (e, ze)::!hash in 

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 


77  129 
let rec e2ze e = 
78  130 
if mem_expr e then ( 
79  131 
get_zexpr e 
...  ...  
216  268 
in 
217  269 
(fun e > e2ze e), (fun ze > ze2e ze) 
218  270  
219 
let is_init_z3e = Z3.Expr.mk_const_s !ctx is_init_name Zustre_common.bool_sort 

220 
let neg_ze z3e = Z3.Boolean.mk_not !ctx z3e 

221  
271 


222  272 
let zexpr_to_guard_list ze = 
223  273 
let init_opt, expr_opt = zexpr_to_expr ze in 
224  274 
(match init_opt with 
...  ...  
228  278 
 None > [] 
229  279 
 Some e > [Expr e, true] 
230  280 
) 
281 


282 


231  283 
let simplify_neg_guard l = 
232  284 
List.map (fun (g,posneg) > 
233  285 
match g with 
...  ...  
249  301 
(* Checking sat(isfiability) of an expression and simplifying it *) 
250  302 
(* All (free) variables have to be declared in the Z3 context *) 
251  303 
(*****************************************************************) 
304 
(* 

252  305 
let goal_simplify zl = 
253  306 
let goal = Z3.Goal.mk_goal !ctx false false false in 
254  307 
Z3.Goal.add goal zl; 
...  ...  
260  313 
* ; *) 
261  314 
let ze = Z3.Goal.as_expr goal' in 
262  315 
(* Format.eprintf "as an expr: %s@." (Z3.Expr.to_string ze); *) 
263 
ze 

264  
265 
let implies e1 e2 = 

266 
(* Format.eprintf "Checking implication: %s => %s? " 

267 
* (Z3.Expr.to_string e1) (Z3.Expr.to_string e2) 

268 
* ; *) 

269 
let solver = Z3.Solver.mk_simple_solver !ctx in 

270 
let tgt = Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_implies !ctx e1 e2) in 

271 
try 

272 
let status_res = Z3.Solver.check solver [tgt] in 

273 
match status_res with 

274 
 Z3.Solver.UNSATISFIABLE > (* Format.eprintf "Valid!@."; *) 

275 
true 

276 
 _ > (* Format.eprintf "not proved valid@."; *) 

277 
false 

278 
with Zustre_common.UnknownFunction(id, msg) > ( 

279 
report ~level:1 msg; 

280 
false 

281 
) 

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 

282  349 

283  350 
let rec simplify zl = 
284  351 
match zl with 
285  352 
 []  [_] > zl 
286  353 
 hd::tl > ( 
287 
(* Forall e in tl, checking whether hd => e or e => hd, to keep hd 

354 
(* Forall e in tl, checking whether hd => e or e => hd, to keep hd


288  355 
in the first case and e in the second one *) 
289  356 
let tl = simplify tl in 
290  357 
let keep_hd, tl = 
...  ...  
310  377 

311  378 
let check_sat ?(just_check=false) (l:guard) : bool * guard = 
312  379 
(* Syntactic simplification *) 
313 
(* Format.eprintf "Before simplify: %a@." pp_guard_list l; *) 

380 
if false then 

381 
Format.eprintf "Before simplify: %a@." pp_guard_list l; 

314  382 
let l = simplify_neg_guard l in 
315 
(* Format.eprintf "After simplify: %a@." pp_guard_list l; *) 

316 
(* Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " pp_guard_list l; *) 

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 
); 

317  387 
let solver = Z3.Solver.mk_simple_solver !ctx in 
318  388 
try ( 
319  389 
let zl = 
...  ...  
329  399 
neg_ze ze 
330  400 
) l 
331  401 
in 
332 
(* Format.eprintf "Z3 exprs1: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e > Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; *)


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;


333  403 
let zl = simplify zl in 
334 
(* Format.eprintf "Z3 exprs2: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e > Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; *)


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;


335  405 
let status_res = Z3.Solver.check solver zl in 
336 
(* Format.eprintf "Z3 status: %s@ @]@. " (Z3.Solver.string_of_status status_res); *)


406 
if false then Format.eprintf "Z3 status: %s@ @]@. " (Z3.Solver.string_of_status status_res);


337  407 
match status_res with 
338  408 
 Z3.Solver.UNSATISFIABLE > false, [] 
339  409 
 _ > ( 
340  410 
if false && just_check then 
341  411 
true, l 
342  412 
else 
343 
let zl = goal_simplify zl in 

344 
let l = zexpr_to_guard_list zl in 

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 

345  420 
(* Format.eprintf "@.@[<v 2>Check_Sat:@ before: %a@ after: 
346  421 
%a@. Goal precise? %b/%b@]@.@. " * pp_guard_list l 
347  422 
pp_guard_list l' * (Z3.Goal.is_precise goal) * 
...  ...  
381  456 
accu 
382  457 
) 
383  458 
[] sys 
384 


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. *) 

385  485 
let combine_guards ?(fresh=None) gl1 gl2 = 
386  486 
(* Filtering out trivial cases. More semantics ones would have to be 
387  487 
addressed later *) 
388 
let check (gexpr, posneg) l = 

389 
(* Format.eprintf "Checking %a=%b in %a@ " 

390 
* pp_elem gexpr 

391 
* posneg 

392 
* pp_guard_list l 

393 
* ; *) 

394 
(* Check if gepxr is part of l *) 

395 
let sel_fun = select_elem gexpr in 

396 
let ok, res = 

397 
if List.exists sel_fun l then ( 

398 
(* Checking the guard value posneg *) 

399 
let _, status = List.find sel_fun l in 

400 
(* Format.eprintf "Found %a in %a. @ Checking status (%b).@ " 

401 
* pp_elem gexpr 

402 
* pp_guard_list l 

403 
* (status=posneg) 

404 
* ; *) 

405 
status=posneg, l 

406 
) 

407 
else ( 

408 
(* Format.eprintf "Not found.@ "; *) 

409 
(* Valid: no overlap *) 

410 
(* Individual checkat *) 

411 
let ok, e = check_sat ~just_check:true [gexpr, posneg] in 

412 
(* let ok, e = true, [gexpr, posneg] in (* TODO solve the issue with check_sat *) *) 

413 
(* Format.eprintf "Check_sat? %b@ " ok; *) 

414 
if ok then 

415 
let l = e@l in 

416 
let ok, l = check_sat ~just_check:true l in 

417 
(* let ok, l = true, l in (* TODO solve the issue with check_sat *) *) 

418 
ok, l 

419 
else 

420 
false, [] 

421 
) 

422 
in 

423 
(* Format.eprintf "Check sat res: %a@ " 

424 
* pp_guard_list res; *) 

425 
ok, res 

488 
let check_sat e = (* temp function before we clean the original one *) 

489 
let ok, _ = check_sat e in 

490 
ok 

426  491 
in 
427 
let ok, gl = 

428 
List.fold_left ( 

429 
fun (ok, l) g > 

430 
(* Bypass for negative output *) 

431 
if not ok then false, [] 

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 

432  536 
else 
433 
check g l 

434 
) (true, gl2) gl1 

537 
[],[],false 

538 
) (short, [], true) long 

539 
in 

540 
ok, long_sel@short 

435  541 
in 
436 
if ok then 

437 
match fresh with 

438 
None > true, gl 

439 
 Some fresh_g > ( 

440 
(* Checking the fresh element *) 

441 
check fresh_g gl 

442 
) 

443 
else 

542 
let ok, l = match fresh with 

543 
 None > true, [] 

544 
 Some g > merge [g] [] 

545 
in 

546 
if not ok then 

444  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 


445  555  
446 
(* DEBUG 

447 
let combine_guards ?(fresh=None) gl1 gl2 = 

448 
true, 

449 
(match fresh with None > []  Some (gexpr, posneg) > [gexpr, posneg])@gl1@gl2 

450 
*) 

451  556 
(* Encode "If gel1=posneg then gel2": 
452  557 
 Compute the combination of guarded exprs in gel1 and gel2: 
453  558 
 Each guarded_expr in gel1 is transformed as a guard: the 
...  ...  
456  561 
 We keep expr in the ge of gel2 as the legitimate expression 
457  562 
*) 
458  563 
let concatenate_ge gel1 posneg gel2 = 
459 
List.fold_left ( 

460 
fun accu (g2,e2) > 

461 
List.fold_left ( 

462 
fun accu (g1,e1) > 

463 
(* Format.eprintf "@[<v 2>Combining guards: (%a=%b) AND [%a] AND [%a]@ " 

464 
* pp_elem e1 

465 
* posneg 

466 
* pp_guard_list g1 

467 
* pp_guard_list g2; *) 

468 


469 
let ok, gl = combine_guards ~fresh:(Some(e1,posneg)) g1 g2 in 

470 
(* Format.eprintf "@]@ Result is [%a]@ " 

471 
* pp_guard_list gl; *) 

472 


473 
if ok then 

474 
(gl, e2)::accu 

475 
else ( 

476 


477 
accu 

478 
) 

479 
) accu gel1 

480 
) [] gel2 

481  
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 
*) 

482  592 
let rec rewrite defs expr : guarded_expr list = 
483  593 
let rewrite = rewrite defs in 
484  594 
let res = 
...  ...  
500  610 
let g = rewrite g and 
501  611 
e1 = rewrite e1 and 
502  612 
e2 = rewrite e2 in 
503 
(concatenate_ge g true e1)@ 

504 
(concatenate_ge g false e2) 

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 []) 

505  617 
 Expr_merge (g, branches) > 
506  618 
assert false (* TODO: deal with merges *) 
507  619 

...  ...  
611  723 
let split_init mem_defs = 
612  724 
split_mem_defs IsInit mem_defs 
613  725  
614 
let pick_guard mem_defs : expr option = 

726 
(* Previous version of the function: way too costly 

727 
let pick_guard mem_defs : expr option = 

615  728 
let gel = List.flatten (List.map snd mem_defs) in 
616  729 
let gl = List.flatten (List.map fst gel) in 
617  730 
let all_guards = 
...  ...  
630  743 
try 
631  744 
Some (List.hd all_guards) 
632  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  
633  768 
(* Transform a list of variable * guarded exprs into a list of guarded pairs (variable, expressions) 
634  769 
*) 
635  770 
let rec build_switch_sys 
...  ...  
698  833 
ok, l 
699  834 
in 
700  835 
let pos_prefix = (elem, true)::prefix in 
701 
let ok_pos, pos_prefix = clean pos_prefix in 

702  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 

703  841 
let ok_neg, neg_prefix = clean neg_prefix in 
704 


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); 

705  845 
(if ok_pos then build_switch_sys pos pos_prefix else []) 
706  846 
@ 
707  847 
(if ok_neg then build_switch_sys neg neg_prefix else []) 
...  ...  
743  883  
744  884 

745  885 
(* Registering node equations: identifying mem definitions and 
746 
storing others in the "defs" hashtbl. *) 

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. *) 

747  891 
let mem_defs = 
748  892 
List.fold_left (fun accu eq > 
749  893 
match eq.eq_lhs with 
Also available in: Unified diff