--- 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
--- a/src/HOL/Tools/SMT2/smt2_solver.ML Mon Jun 02 17:34:26 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML Mon Jun 02 17:34:26 2014 +0200
@@ -183,9 +183,7 @@
(case outcome output of
(Unsat, ls) =>
(case parse_proof0 of SOME pp => pp outer_ctxt replay_data ls | NONE => ([], []))
- | (result, _) =>
- raise SMT2_Failure.SMT (SMT2_Failure.Counterexample {
- is_real_cex = (result = Sat), free_constraints = [], const_defs = []}))
+ | (result, _) => raise SMT2_Failure.SMT (SMT2_Failure.Counterexample (result = Sat)))
fun replay outcome replay0 oracle outer_ctxt
(replay_data as {context = ctxt, ...} : SMT2_Translate.replay_data) output =
@@ -194,9 +192,7 @@
if not (Config.get ctxt SMT2_Config.oracle) andalso is_some replay0
then the replay0 outer_ctxt replay_data ls
else oracle ()
- | (result, _) =>
- raise SMT2_Failure.SMT (SMT2_Failure.Counterexample {
- is_real_cex = (result = Sat), free_constraints = [], const_defs = []}))
+ | (result, _) => raise SMT2_Failure.SMT (SMT2_Failure.Counterexample (result = Sat)))
val cfalse = Thm.cterm_of @{theory} @{prop False}
in
@@ -297,7 +293,7 @@
local
fun str_of ctxt fail =
- "Solver " ^ SMT2_Config.solver_of ctxt ^ ": " ^ SMT2_Failure.string_of_failure ctxt fail
+ "Solver " ^ SMT2_Config.solver_of ctxt ^ ": " ^ SMT2_Failure.string_of_failure fail
fun safe_solve ctxt wfacts = SOME (apply_solver_and_replay ctxt wfacts)
handle
@@ -305,7 +301,7 @@
(SMT2_Config.verbose_msg ctxt (str_of ctxt) fail; NONE)
| SMT2_Failure.SMT (fail as SMT2_Failure.Time_Out) =>
error ("SMT: Solver " ^ quote (SMT2_Config.solver_of ctxt) ^ ": " ^
- SMT2_Failure.string_of_failure ctxt fail ^ " (setting the " ^
+ SMT2_Failure.string_of_failure fail ^ " (setting the " ^
"configuration option " ^ quote (Config.name_of SMT2_Config.timeout) ^ " might help)")
| SMT2_Failure.SMT fail => error (str_of ctxt fail)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Mon Jun 02 17:34:26 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Mon Jun 02 17:34:26 2014 +0200
@@ -85,8 +85,8 @@
(139, Crashed)]
val smt2_failures = z3_failures @ unix_failures
-fun failure_of_smt2_failure (SMT2_Failure.Counterexample {is_real_cex, ...}) =
- if is_real_cex then Unprovable else GaveUp
+fun failure_of_smt2_failure (SMT2_Failure.Counterexample genuine) =
+ if genuine then Unprovable else GaveUp
| failure_of_smt2_failure SMT2_Failure.Time_Out = TimedOut
| failure_of_smt2_failure (SMT2_Failure.Abnormal_Termination code) =
(case AList.lookup (op =) smt2_failures code of