--- a/src/HOL/Library/Old_SMT/smt_failure.ML Thu Aug 28 00:40:38 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-(* 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