1(* Title: HOL/Tools/SMT/smt_failure.ML 2 Author: Sascha Boehme, TU Muenchen 3 4Failures and exception of SMT. 5*) 6 7signature SMT_FAILURE = 8sig 9 datatype failure = 10 Counterexample of bool | 11 Time_Out | 12 Out_Of_Memory | 13 Abnormal_Termination of int | 14 Other_Failure of string 15 val string_of_failure: failure -> string 16 exception SMT of failure 17end; 18 19structure SMT_Failure: SMT_FAILURE = 20struct 21 22datatype failure = 23 Counterexample of bool | 24 Time_Out | 25 Out_Of_Memory | 26 Abnormal_Termination of int | 27 Other_Failure of string 28 29fun string_of_failure (Counterexample genuine) = 30 if genuine then "Counterexample found (possibly spurious)" 31 else "Potential counterexample found" 32 | string_of_failure Time_Out = "Timed out" 33 | string_of_failure Out_Of_Memory = "Ran out of memory" 34 | string_of_failure (Abnormal_Termination err) = 35 "Solver terminated abnormally with error code " ^ string_of_int err 36 | string_of_failure (Other_Failure msg) = msg 37 38exception SMT of failure 39 40end; 41