Project

General

Profile

« Previous | Next » 

Revision 4300981b

Added by Pierre-Loïc Garoche over 3 years ago

Zustre: timeout and slicing

View differences:

src/tools/zustre/zustre_analyze.ml
200 200

  
201 201
      (* Debug instructions *)
202 202
  let rules_expr = Z3.Fixedpoint.get_rules !fp in
203
  if true then
203
  if !debug then
204 204
    Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
205 205
    (Utils.fprintf_list ~sep:"@ "
206 206
       (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
207
    rules_expr;
208
  let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in
209

  
210
  Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
211
  match res_status with
212
  | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex decl_err
213
  
214
  | Z3.Solver.UNSATISFIABLE -> (*build_inv*) (
215
       let expr_opt = Z3.Fixedpoint.get_answer !fp in
216
       match expr_opt with
217
	 None -> Format.eprintf "Unsat No feedback@."
218
       | Some e -> Format.eprintf "Unsat Result: %s@." (Z3.Expr.to_string e)
219
  )
220
  | Z3.Solver.UNKNOWN -> ()
221
      
207
      rules_expr;
208
  try
209
    let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in
210
    
211
    Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
212
    match res_status with
213
    | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex decl_err
214
       
215
    | Z3.Solver.UNSATISFIABLE -> (*build_inv*) (
216
      let expr_opt = Z3.Fixedpoint.get_answer !fp in
217
      match expr_opt with
218
	None -> if !debug then Format.eprintf "Unsat No feedback@."
219
      | Some e -> if !debug then Format.eprintf "Unsat Result: %s@." (Z3.Expr.to_string e)
220
    )
221
    | Z3.Solver.UNKNOWN -> ()
222
  with Z3.Error msg -> Format.eprintf "Z3 failure: %s@." msg; () 
222 223
(* Local Variables: *)
223 224
(* compile-command:"make -C ../.." *)
224 225
(* End: *)

Also available in: Unified diff