Revision 73a4995a
Added by Pierre-Loïc Garoche almost 4 years ago
| src/tools/seal/seal_extract.ml | ||
|---|---|---|
| 20 | 20 |
|
| 21 | 21 |
let const_defs = Hashtbl.create 13 |
| 22 | 22 |
let is_const id = Hashtbl.mem const_defs id |
| 23 |
let is_enum_const id = Hashtbl.mem Zustre_data.const_tags id |
|
| 23 | 24 |
let get_const id = Hashtbl.find const_defs id |
| 24 | 25 |
|
| 25 | 26 |
(* expressions are only basic constructs here, no more ite, tuples, |
| ... | ... | |
| 106 | 107 |
let z3e = Zustre_common.horn_const_to_expr c in |
| 107 | 108 |
add_expr e z3e; |
| 108 | 109 |
z3e |
| 109 |
) |
|
| 110 |
else ( |
|
| 111 |
let fdecl_id = Zustre_common.get_fdecl id in |
|
| 112 |
let z3e = Z3.Expr.mk_const_f !ctx fdecl_id in |
|
| 113 |
add_expr e z3e; |
|
| 114 |
z3e |
|
| 110 |
) |
|
| 111 |
else if is_enum_const id then ( |
|
| 112 |
let z3e = Zustre_common.horn_tag_to_expr id in |
|
| 113 |
add_expr e z3e; |
|
| 114 |
z3e |
|
| 115 |
) |
|
| 116 |
else ( |
|
| 117 |
let fdecl_id = Zustre_common.get_fdecl id in |
|
| 118 |
let z3e = Z3.Expr.mk_const_f !ctx fdecl_id in |
|
| 119 |
add_expr e z3e; |
|
| 120 |
z3e |
|
| 115 | 121 |
) |
| 116 | 122 |
) |
| 117 |
| Expr_appl (id,args, None) (* no reset *) -> |
|
| 118 |
let z3e = Zustre_common.horn_basic_app id e2ze (Corelang.expr_list_of_expr args) in |
|
| 119 |
add_expr e z3e; |
|
| 120 |
z3e |
|
| 121 |
| Expr_tuple [e] -> |
|
| 122 |
let z3e = e2ze e in |
|
| 123 |
add_expr e z3e; |
|
| 124 |
z3e |
|
| 125 |
| _ -> ( match e.expr_desc with Expr_tuple _ -> Format.eprintf "tuple e2ze(%a)@.@?" Printers.pp_expr e |
|
| 126 |
| _ -> Format.eprintf "e2ze(%a)@.@?" Printers.pp_expr e) |
|
| 127 |
; assert false
|
|
| 123 |
| Expr_appl (id,args, None) (* no reset *) ->
|
|
| 124 |
let z3e = Zustre_common.horn_basic_app id e2ze (Corelang.expr_list_of_expr args) in
|
|
| 125 |
add_expr e z3e;
|
|
| 126 |
z3e
|
|
| 127 |
| Expr_tuple [e] ->
|
|
| 128 |
let z3e = e2ze e in
|
|
| 129 |
add_expr e z3e;
|
|
| 130 |
z3e
|
|
| 131 |
| _ -> ( match e.expr_desc with Expr_tuple _ -> Format.eprintf "tuple e2ze(%a)@.@?" Printers.pp_expr e
|
|
| 132 |
| _ -> Format.eprintf "e2ze(%a)@.@?" Printers.pp_expr e)
|
|
| 133 |
; assert false |
|
| 128 | 134 |
in |
| 129 | 135 |
res |
| 130 | 136 |
) |
| ... | ... | |
| 827 | 833 |
(Expr elem) |
| 828 | 834 |
mem_defs |
| 829 | 835 |
in |
| 836 |
(* Format.eprintf "Selected item %a in@.%a@.POS=%a@.NEG=%a@." |
|
| 837 |
Printers.pp_expr elem |
|
| 838 |
pp_all_defs mem_defs |
|
| 839 |
pp_all_defs pos |
|
| 840 |
pp_all_defs neg |
|
| 841 |
; |
|
| 842 |
*) |
|
| 830 | 843 |
(* Special cases to avoid useless computations: true, false conditions *) |
| 831 | 844 |
match elem.expr_desc with |
| 832 | 845 |
(*| Expr_ident "true" -> build_switch_sys pos prefix *) |
| ... | ... | |
| 893 | 906 |
(* Filtering out unused vars *) |
| 894 | 907 |
let vars = List.filter (fun v -> not (List.mem v.var_id unused)) vars in |
| 895 | 908 |
(* Registering all locals variables as Z3 predicates. Will be use to |
| 896 |
simplify the expansion *) |
|
| 909 |
simplify the expansion *) |
|
| 910 |
Zustre_common.decl_sorts (); |
|
| 897 | 911 |
let _ = |
| 898 | 912 |
List.iter (fun v -> |
| 899 | 913 |
let fdecl = Z3.FuncDecl.mk_func_decl_s |
Also available in: Unified diff
seal: now deals with enum