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