Project

General

Profile

« Previous | Next » 

Revision 51ec4e8c

Added by Pierre-Loïc Garoche about 5 years ago

Try to debug the use of Z3 API. Still having troubles

View differences:

src/tools/zustre/zustre_verifier.ml
83 83
      let mks = S.mk_string !ctx in
84 84
      let params = P.mk_params !ctx in
85 85

  
86
      (* self.fp.set (engine='spacer') *)
86
      (* (\* self.fp.set (engine='spacer') *\) *)
87 87
      P.add_symbol params (mks "engine") (mks "spacer");
88
      (* P.add_symbol params (mks "engine") (mks "pdr");  *)
88 89
      
89 90
       (* #z3.set_option(rational_to_decimal=True) *)
90 91
       (* #self.fp.set('precision',30) *)
......
152 153
	
153 154
	let queries = Z3.Fixedpoint.parse_file !fp "mini.smt2" in
154 155

  
155
      (* Debug instructions *)
156
      let rules_expr = Z3.Fixedpoint.get_rules !fp in
157
      Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
158
      	(Utils.fprintf_list ~sep:"@ "
159
      	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
160
      	rules_expr;
156
	(* Debug instructions *)
157
	
161 158

  
162
	let res_status = Z3.Fixedpoint.query !fp (List.hd queries )in
159
	
160
	let rules_expr = Z3.Fixedpoint.get_rules !fp in
161
	Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
162
      	  (Utils.fprintf_list ~sep:"@ "
163
      	     (fun fmt e ->
164
	       (* let e2 = Z3.Quantifier.get_body eq in *)
165
	       (* let fd = Z3.Expr.get_func_decl e in *)
166
	       Format.fprintf fmt "Rule: %s@."
167
		 (Z3.Expr.to_string e);
168
	     )) rules_expr;
169
	
170
	let _ = List.map extract_expr_fds rules_expr in
171
	Format.eprintf "%t" pp_fdecls;
172
	
173
      	let res_status = Z3.Fixedpoint.query !fp (List.hd queries )in
163 174
	
164 175
	Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status)
165 176
      )
177
      else if false then (
178

  
179
	(* No queries here *)
180
	let _ = Z3.Fixedpoint.parse_file !fp "mini_decl.smt2" in
181

  
182
	(* Debug instructions *)
183
	
184

  
185
	
186
	let rules_expr = Z3.Fixedpoint.get_rules !fp in
187
	Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
188
      	  (Utils.fprintf_list ~sep:"@ "
189
      	     (fun fmt e ->
190
	       (* let e2 = Z3.Quantifier.get_body eq in *)
191
	       (* let fd = Z3.Expr.get_func_decl e in *)
192
	       Format.fprintf fmt "Rule: %s@."
193
		 (Z3.Expr.to_string e);
194
	     )) rules_expr;
195
	
196
	let _ = List.map extract_expr_fds rules_expr in
197
	Format.eprintf "%t" pp_fdecls;
198

  
199
	if !Options.main_node <> "" then
200
      	  begin
201
      	    Zustre_analyze.check machines !Options.main_node
202

  
203
      	  end
204
	else
205
      	  failwith "Require main node";
206

  
207
	()	
208
      )
166 209
      else (
167 210
	
168 211
	
169
      decl_sorts ();
170
      
171
      List.iter (decl_machine machines) (List.rev machines);
212
	decl_sorts ();
213
	
214
	List.iter (decl_machine machines) (List.rev machines);
172 215

  
173 216

  
174
      (* (\* Debug instructions *\) *)
175
      (* let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
176
      (* Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
177
      (* 	(Utils.fprintf_list ~sep:"@ " *)
178
      (* 	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
179
      (* 	rules_expr; *)
217
	(* (\* Debug instructions *\) *)
218
	(* let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
219
	(* Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
220
	(* 	(Utils.fprintf_list ~sep:"@ " *)
221
	(* 	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
222
	(* 	rules_expr; *)
180 223

  
181
      if !Options.main_node <> "" then
182
      	begin
183
      	  Zustre_analyze.check machines !Options.main_node
224
	if !Options.main_node <> "" then
225
      	  begin
226
      	    Zustre_analyze.check machines !Options.main_node
184 227

  
185
      	end
186
      else
187
      	failwith "Require main node";
188
      
189
      ()
228
      	  end
229
	else
230
      	  failwith "Require main node";
231
	
232
	()
190 233
      )
191 234
	
192 235

  
193
  end: VerifierType.S)
236
	    end: VerifierType.S)
194 237
    
195 238
(* Local Variables: *)
196 239
(* compile-command:"make -C ../.." *)

Also available in: Unified diff