Revision 51ec4e8c
Added by PierreLoïc Garoche about 5 years ago
src/tools/zustre/zustre_common.ml  

104  104 
try 
105  105 
Hashtbl.find decls id 
106  106 
with Not_found > (Format.eprintf "Unable to find func_decl %s@.@?" id; raise Not_found) 
107  
108 
let pp_fdecls fmt = 

109 
Format.fprintf fmt "Registered fdecls: @[%a@]@ " 

110 
(Utils.fprintf_list ~sep:"@ " Format.pp_print_string) (Hashtbl.fold (fun id _ accu > id::accu) decls []) 

111  
107  112 

108  113 
let decl_var id = 
109  114 
Format.eprintf "Declaring var %s@." id.var_id; 
...  ...  
120  125 
fdecl 
121  126 

122  127  
123 
(* Quantifiying universally all occuring variables *) 

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

125 
(* let fds = Z3.Expr.get_args expr in *) 

126 
(* Format.eprintf "Expr %s: args: [%a]@." *) 

127 
(* (Z3.Expr.to_string expr) *) 

128 
(* (Utils.fprintf_list ~sep:", " (fun fmt e > Format.pp_print_string fmt (Z3.Expr.to_string e))) fds; *) 

129  
130 
(* Old code relying on provided vars *) 

131 
let sorts = (List.map (fun id > type_to_sort id.var_type) vars) in 

132 
let symbols = (List.map (fun id > Z3.FuncDecl.get_name (get_fdecl id.var_id)) vars) in 

133 


134 
(* New code: we extract vars from expr *) 

135 
let module FDSet = Set.Make (struct type t = Z3.FuncDecl.func_decl 

136 
let compare = compare 

137 
let hash = Hashtbl.hash 

138 
end) 

139 
in 

140 
let rec get_expr_vars e = 

141 
let open Utils in 

142 
let nb_args = Z3.Expr.get_num_args e in 

143 
if nb_args <= 0 then ( 

144 
let fdecl = Z3.Expr.get_func_decl e in 

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

146 
Format.eprintf "Extracting info about %s: [@?" (Z3.Expr.to_string e); 

147 
let dkind = Z3.FuncDecl.get_decl_kind fdecl in 

148 
match dkind with Z3enums.OP_UNINTERPRETED > ( 

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

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

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

152 
(* match p with *) 

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

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

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

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

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

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

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

160 


161 
(* ) params; *) 

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

163 
FDSet.singleton fdecl 

164 
) 

165 
 _ > FDSet.empty 

166 
) 

167 
else (*if nb_args > 0 then*) 

168 
List.fold_left 

169 
(fun accu e > FDSet.union accu (get_expr_vars e)) 

170 
FDSet.empty (Z3.Expr.get_args e) 

171 
in 

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

173 
let sorts = List.map Z3.FuncDecl.get_range vars in 

174 
let symbols = List.map Z3.FuncDecl.get_name vars in 

175 


176 
let expr = Z3.Quantifier.mk_forall 

177 
!ctx (* context *) 

178 
sorts (* sort list*) 

179 
symbols (* symbol list *) 

180 
expr (* expression *) 

181 
None (* quantifier weight, None means 1 *) 

182 
[] (* pattern list ? *) 

183 
[] (* ? *) 

184 
None (* ? *) 

185 
None (* ? *) 

186 
in 

187 
Z3.Fixedpoint.add_rule !fp 

188 
(Z3.Quantifier.expr_of_quantifier expr) 

189 
None 

190  
191  
192  128 
(** Conversion functions 
193  129  
194  130 
The following is similar to the Horn backend. Each printing function 
...  ...  
682  618 
in 
683  619 
e, rs 
684  620  
685 


621  
622 
(*********************************************************) 

623  
624 
(* Quantifiying universally all occuring variables *) 

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

626 
(* let fds = Z3.Expr.get_args expr in *) 

627 
(* Format.eprintf "Expr %s: args: [%a]@." *) 

628 
(* (Z3.Expr.to_string expr) *) 

629 
(* (Utils.fprintf_list ~sep:", " (fun fmt e > Format.pp_print_string fmt (Z3.Expr.to_string e))) fds; *) 

630  
631 
(* (\* Old code relying on provided vars *\) *) 

632 
(* let sorts = (List.map (fun id > type_to_sort id.var_type) vars) in *) 

633 
(* let symbols = (List.map (fun id > Z3.FuncDecl.get_name (get_fdecl id.var_id)) vars) in *) 

634 


635 
(* New code: we extract vars from expr *) 

636 
let module FDSet = Set.Make (struct type t = Z3.FuncDecl.func_decl 

637 
let compare = compare 

638 
let hash = Hashtbl.hash 

639 
end) 

640 
in 

641 
let rec get_expr_vars e = 

642 
let open Utils in 

643 
let nb_args = Z3.Expr.get_num_args e in 

644 
if nb_args <= 0 then ( 

645 
let fdecl = Z3.Expr.get_func_decl e in 

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

647 
Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string e); 

648 
let dkind = Z3.FuncDecl.get_decl_kind fdecl in 

649 
match dkind with Z3enums.OP_UNINTERPRETED > ( 

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

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

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

653 
(* match p with *) 

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

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

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

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

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

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

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

661 


662 
(* ) params; *) 

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

664 
FDSet.singleton fdecl 

665 
) 

666 
 _ > FDSet.empty 

667 
) 

668 
else (*if nb_args > 0 then*) 

669 
List.fold_left 

670 
(fun accu e > FDSet.union accu (get_expr_vars e)) 

671 
FDSet.empty (Z3.Expr.get_args e) 

672 
in 

673 
let extracted_vars = FDSet.elements (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in 

674 
let extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in 

675 
let extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in 

676  
677 
Format.eprintf "Declaring rule: %s with variables %a@." 

678 
(Z3.Expr.to_string expr) 

679 
(Utils.fprintf_list ~sep:", " (fun fmt e > Format.fprintf fmt "%s" (Z3.Expr.to_string e))) (List.map horn_var_to_expr vars) 

680 
; 

681 
let expr = Z3.Quantifier.mk_forall_const 

682 
!ctx (* context *) 

683 
(List.map horn_var_to_expr vars) (* TODO provide bounded variables as expr *) 

684 
(* sorts (\* sort list*\) *) 

685 
(* symbols (\* symbol list *\) *) 

686 
expr (* expression *) 

687 
None (* quantifier weight, None means 1 *) 

688 
[] (* pattern list ? *) 

689 
[] (* ? *) 

690 
None (* ? *) 

691 
None (* ? *) 

692 
in 

693 
Format.eprintf "OK@.@?"; 

694  
695  
696 
TODO: bizarre la declaration de INIT tout seul semble poser pb. 

697 


698 
Z3.Fixedpoint.add_rule !fp 

699 
(Z3.Quantifier.expr_of_quantifier expr) 

700 
None 

701  
702 
(********************************************************) 

703 


686  704 
let machine_reset machines m = 
687  705 
let locals = local_memory_vars machines m in 
688  706 

...  ...  
772  790 
 [] > 
773  791 
begin 
774  792 
(* Rule for single predicate : "; Stateless step rule @." *) 
793 
let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in 

775  794 
add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head) 
776  795 

777  796 
end 
...  ...  
781  800 
let body_with_asserts = 
782  801 
Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl) 
783  802 
in 
803 
let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in 

784  804 
add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head) 
785  805 
end 
786  806 
end 
...  ...  
798  818 
(get_fdecl (machine_reset_name m.mname.node_id)) 
799  819 
(List.map (horn_var_to_expr) vars) 
800  820 
in 
821  
801  822 

802  823 
let _ = 
803  824 
add_rule vars (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head) 
...  ...  
844  865 
end 
845  866  
846  867  
868  
869 
(* Debug functions *) 

870  
871 
let rec extract_expr_fds e = 

872 
Format.eprintf "@[<v 2>Extracting fundecls from expr %s@ " 

873 
(Z3.Expr.to_string e); 

874 


875 
(* Removing quantifier is there are some *) 

876 
let e = (* I didn't found a nicer way to do it than with an exception. My 

877 
bad *) 

878 
try 

879 
let eq = Z3.Quantifier.quantifier_of_expr e in 

880 
let e2 = Z3.Quantifier.get_body eq in 

881 
Format.eprintf "Extracted quantifier body@ "; 

882 
e2 

883 


884 
with _ > Format.eprintf "No quantifier info@ "; e 

885 
in 

886 
let _ = 

887 
try 

888 
( 

889 
let fd = Z3.Expr.get_func_decl e in 

890 
let fd_symbol = Z3.FuncDecl.get_name fd in 

891 
let fd_name = Z3.Symbol.to_string fd_symbol in 

892 
if not (Hashtbl.mem decls fd_name) then 

893 
register_fdecl fd_name fd; 

894 
Format.eprintf "fdecls (%s): %s@ " 

895 
fd_name 

896 
(Z3.FuncDecl.to_string fd); 

897 
try 

898 
( 

899 
let args = Z3.Expr.get_args e in 

900 
Format.eprintf "@[<v>@ "; 

901 
List.iter extract_expr_fds args; 

902 
Format.eprintf "@]@ "; 

903 
) 

904 
with _ > 

905 
Format.eprintf "Impossible to extract fundecl args for expression %s@ " 

906 
(Z3.Expr.to_string e) 

907 
) 

908 
with _ > 

909 
Format.eprintf "Impossible to extract anything from expression %s@ " 

910 
(Z3.Expr.to_string e) 

911 
in 

912 
Format.eprintf "@]@ " 

913 


914  
847  915 
(* Local Variables: *) 
848  916 
(* compilecommand:"make C ../.." *) 
849  917 
(* End: *) 
Also available in: Unified diff
Try to debug the use of Z3 API. Still having troubles