src/HOL/Library/Old_SMT/smt_failure.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Old_SMT/smt_failure.ML	Thu Aug 28 00:40:38 2014 +0200
@@ -0,0 +1,61 @@
+(*  Title:      HOL/Library/Old_SMT/smt_failure.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Failures and exception of SMT.
+*)
+
+signature SMT_FAILURE =
+sig
+  type counterexample = {
+    is_real_cex: bool,
+    free_constraints: term list,
+    const_defs: term list}
+  datatype failure =
+    Counterexample of counterexample |
+    Time_Out |
+    Out_Of_Memory |
+    Abnormal_Termination of int |
+    Other_Failure of string
+  val pretty_counterexample: Proof.context -> counterexample -> Pretty.T
+  val string_of_failure: Proof.context -> failure -> string
+  exception SMT of failure
+end
+
+structure SMT_Failure: SMT_FAILURE =
+struct
+
+type counterexample = {
+  is_real_cex: bool,
+  free_constraints: term list,
+  const_defs: term list}
+
+datatype failure =
+  Counterexample of counterexample |
+  Time_Out |
+  Out_Of_Memory |
+  Abnormal_Termination of int |
+  Other_Failure of string
+
+fun pretty_counterexample ctxt {is_real_cex, free_constraints, const_defs} =
+  let
+    val msg =
+      if is_real_cex then "Counterexample found (possibly spurious)"
+      else "Potential counterexample found"
+  in
+    if null free_constraints andalso null const_defs then Pretty.str msg
+    else
+      Pretty.big_list (msg ^ ":")
+        (map (Syntax.pretty_term ctxt) (free_constraints @ const_defs))
+  end
+
+fun string_of_failure ctxt (Counterexample cex) =
+      Pretty.string_of (pretty_counterexample ctxt cex)
+  | 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