blanchet@58058: (*  Title:      HOL/Library/Old_SMT/old_smt_failure.ML
boehmes@40424:     Author:     Sascha Boehme, TU Muenchen
boehmes@40424: 
boehmes@40424: Failures and exception of SMT.
boehmes@40424: *)
boehmes@40424: 
blanchet@58058: signature OLD_SMT_FAILURE =
boehmes@40424: sig
boehmes@40828:   type counterexample = {
boehmes@40828:     is_real_cex: bool,
boehmes@40828:     free_constraints: term list,
boehmes@40828:     const_defs: term list}
boehmes@40424:   datatype failure =
boehmes@40828:     Counterexample of counterexample |
boehmes@40424:     Time_Out |
boehmes@40424:     Out_Of_Memory |
boehmes@40561:     Abnormal_Termination of int |
boehmes@40424:     Other_Failure of string
boehmes@40828:   val pretty_counterexample: Proof.context -> counterexample -> Pretty.T
boehmes@40424:   val string_of_failure: Proof.context -> failure -> string
boehmes@40424:   exception SMT of failure
boehmes@40424: end
boehmes@40424: 
blanchet@58058: structure Old_SMT_Failure: OLD_SMT_FAILURE =
boehmes@40424: struct
boehmes@40424: 
boehmes@40828: type counterexample = {
boehmes@40828:   is_real_cex: bool,
boehmes@40828:   free_constraints: term list,
boehmes@40828:   const_defs: term list}
boehmes@40828: 
boehmes@40424: datatype failure =
boehmes@40828:   Counterexample of counterexample |
boehmes@40424:   Time_Out |
boehmes@40424:   Out_Of_Memory |
boehmes@40561:   Abnormal_Termination of int |
boehmes@40424:   Other_Failure of string
boehmes@40424: 
boehmes@40828: fun pretty_counterexample ctxt {is_real_cex, free_constraints, const_defs} =
boehmes@40828:   let
boehmes@40828:     val msg =
boehmes@40828:       if is_real_cex then "Counterexample found (possibly spurious)"
boehmes@40828:       else "Potential counterexample found"
boehmes@40828:   in
boehmes@40828:     if null free_constraints andalso null const_defs then Pretty.str msg
boehmes@40828:     else
boehmes@40828:       Pretty.big_list (msg ^ ":")
boehmes@40828:         (map (Syntax.pretty_term ctxt) (free_constraints @ const_defs))
boehmes@40828:   end
boehmes@40828: 
boehmes@40828: fun string_of_failure ctxt (Counterexample cex) =
boehmes@40828:       Pretty.string_of (pretty_counterexample ctxt cex)
boehmes@40424:   | string_of_failure _ Time_Out = "Timed out"
boehmes@40424:   | string_of_failure _ Out_Of_Memory = "Ran out of memory"
boehmes@40561:   | string_of_failure _ (Abnormal_Termination err) =
boehmes@40561:       "Solver terminated abnormally with error code " ^ string_of_int err
boehmes@40424:   | string_of_failure _ (Other_Failure msg) = msg
boehmes@40424: 
boehmes@40424: exception SMT of failure
boehmes@40424: 
boehmes@40424: end