| 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
|
seal: now deals with enum