robustly parse Z3 4.0's output (with outcome appearing on first rather than last line)
authorblanchet
Thu May 17 13:36:23 2012 +0200 (2012-05-17)
changeset 479404ef90b51641e
parent 47939 9ff976a6c2cb
child 47941 22e001795641
robustly parse Z3 4.0's output (with outcome appearing on first rather than last line)
src/HOL/Tools/SMT/smt_setup_solvers.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Thu May 17 13:36:23 2012 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Thu May 17 13:36:23 2012 +0200
     1.3 @@ -143,7 +143,7 @@
     1.4      |> not (Config.get ctxt SMT_Config.oracle) ?
     1.5           append ["DISPLAY_PROOF=true","PROOF_MODE=2"]
     1.6  
     1.7 -  fun z3_on_last_line solver_name lines =
     1.8 +  fun z3_on_first_or_last_line solver_name lines =
     1.9      let
    1.10        fun junk l =
    1.11          if String.isPrefix "WARNING: Out of allocated virtual memory" l
    1.12 @@ -152,9 +152,15 @@
    1.13            String.isPrefix "WARNING" l orelse
    1.14            String.isPrefix "ERROR" l orelse
    1.15            forall Symbol.is_ascii_blank (Symbol.explode l)
    1.16 +      val lines = filter_out junk lines
    1.17 +      fun outcome split =
    1.18 +        the_default ("", []) (try split lines)
    1.19 +        |>> outcome_of "unsat" "sat" "unknown" solver_name
    1.20      in
    1.21 -      the_default ("", []) (try (swap o split_last) (filter_out junk lines))
    1.22 -      |>> outcome_of "unsat" "sat" "unknown" solver_name
    1.23 +      (* Starting with version 4.0, Z3 puts the outcome on the first line of the
    1.24 +         output rather than on the last line. *)
    1.25 +      outcome (fn lines => (hd lines, tl lines))
    1.26 +      handle SMT_Failure.SMT _ => outcome (swap o split_last)
    1.27      end
    1.28  
    1.29    fun mk is_remote = {
    1.30 @@ -165,7 +171,7 @@
    1.31      options = z3_options,
    1.32      default_max_relevant = 350 (* FUDGE *),
    1.33      supports_filter = true,
    1.34 -    outcome = z3_on_last_line,
    1.35 +    outcome = z3_on_first_or_last_line,
    1.36      cex_parser = SOME Z3_Model.parse_counterex,
    1.37      reconstruct = SOME Z3_Proof_Reconstruction.reconstruct }
    1.38  in