--- a/src/HOL/Tools/SMT2/smt2_failure.ML Mon Jun 02 17:34:26 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_failure.ML Mon Jun 02 17:34:26 2014 +0200
@@ -6,55 +6,34 @@
signature SMT2_FAILURE =
sig
- type counterexample = {
- is_real_cex: bool,
- free_constraints: term list,
- const_defs: term list}
datatype failure =
- Counterexample of counterexample |
+ Counterexample of bool |
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
+ val string_of_failure: failure -> string
exception SMT of failure
end
structure SMT2_Failure: SMT2_FAILURE =
struct
-type counterexample = {
- is_real_cex: bool,
- free_constraints: term list,
- const_defs: term list}
-
datatype failure =
- Counterexample of counterexample |
+ Counterexample of bool |
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)"
+fun string_of_failure (Counterexample genuine) =
+ if genuine 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) =
+ | 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
+ | string_of_failure (Other_Failure msg) = msg
exception SMT of failure