Revision 8eeec77e
Added by PierreLoïc Garoche almost 4 years ago
src/tools/zustre/zustre_common.ml  

122  122 

123  123  
124  124 
(* Quantifiying universally all occuring variables *) 
125 
let add_rule vars expr = 

125 
let add_rule ?(dont_touch=[]) vars expr =


126  126 
(* let fds = Z3.Expr.get_args expr in *) 
127  127 
(* Format.eprintf "Expr %s: args: [%a]@." *) 
128  128 
(* (Z3.Expr.to_string expr) *) 
...  ...  
143  143 
let nb_args = Z3.Expr.get_num_args e in 
144  144 
if nb_args <= 0 then ( 
145  145 
let fdecl = Z3.Expr.get_func_decl e in 
146 
let params = Z3.FuncDecl.get_parameters fdecl in


146 
(* let params = Z3.FuncDecl.get_parameters fdecl in *)


147  147 
Format.eprintf "Extracting info about %s: [@?" (Z3.Expr.to_string e); 
148  148 
let dkind = Z3.FuncDecl.get_decl_kind fdecl in 
149  149 
match dkind with Z3enums.OP_UNINTERPRETED > ( 
150 
Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE > "true"  OP_UNINTERPRETED > "uninter");


151 
let open Z3.FuncDecl.Parameter in


152 
List.iter (fun p >


153 
match p with


154 
P_Int i > Format.eprintf "int %i" i


155 
 P_Dbl f > Format.eprintf "dbl %f" f


156 
 P_Sym s > Format.eprintf "symb"


157 
 P_Srt s > Format.eprintf "sort"


158 
 P_Ast _ >Format.eprintf "ast"


159 
 P_Fdl f > Format.eprintf "fundecl"


160 
 P_Rat s > Format.eprintf "rat %s" s


150 
(* Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE > "true"  Z3enums.OP_UNINTERPRETED > "uninter"); *)


151 
(* let open Z3.FuncDecl.Parameter in *)


152 
(* List.iter (fun p > *)


153 
(* match p with *)


154 
(* P_Int i > Format.eprintf "int %i" i *)


155 
(*  P_Dbl f > Format.eprintf "dbl %f" f *)


156 
(*  P_Sym s > Format.eprintf "symb" *)


157 
(*  P_Srt s > Format.eprintf "sort" *)


158 
(*  P_Ast _ >Format.eprintf "ast" *)


159 
(*  P_Fdl f > Format.eprintf "fundecl" *)


160 
(*  P_Rat s > Format.eprintf "rat %s" s *)


161  161 

162 
) params;


163 
Format.eprintf "]@.";


162 
(* ) params; *)


163 
(* Format.eprintf "]@."; *)


164  164 
FDSet.singleton fdecl 
165  165 
) 
166  166 
 _ > FDSet.empty 
...  ...  
170  170 
(fun accu e > FDSet.union accu (get_expr_vars e)) 
171  171 
FDSet.empty (Z3.Expr.get_args e) 
172  172 
in 
173 
let vars = FDSet.elements (get_expr_vars expr) in


173 
let vars = FDSet.elements (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in


174  174 
let sorts = List.map Z3.FuncDecl.get_range vars in 
175  175 
let symbols = List.map Z3.FuncDecl.get_name vars in 
176  176 

Also available in: Unified diff
Filtering out ERR and MAIN from the forall quantification