src/HOL/Tools/SMT/smt_failure.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/smt_failure.ML	Thu Aug 28 00:40:38 2014 +0200
@@ -0,0 +1,40 @@
+(*  Title:      HOL/Tools/SMT/smt_failure.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Failures and exception of SMT.
+*)
+
+signature SMT_FAILURE =
+sig
+  datatype failure =
+    Counterexample of bool |
+    Time_Out |
+    Out_Of_Memory |
+    Abnormal_Termination of int |
+    Other_Failure of string
+  val string_of_failure: failure -> string
+  exception SMT of failure
+end;
+
+structure SMT_Failure: SMT_FAILURE =
+struct
+
+datatype failure =
+  Counterexample of bool |
+  Time_Out |
+  Out_Of_Memory |
+  Abnormal_Termination of int |
+  Other_Failure of string
+
+fun string_of_failure (Counterexample genuine) =
+      if genuine then "Counterexample found (possibly spurious)"
+      else "Potential counterexample found"
+  | string_of_failure Time_Out = "Timed out"
+  | string_of_failure Out_Of_Memory = "Ran out of memory"
+  | string_of_failure (Abnormal_Termination err) =
+      "Solver terminated abnormally with error code " ^ string_of_int err
+  | string_of_failure (Other_Failure msg) = msg
+
+exception SMT of failure
+
+end;