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