# HG changeset patch
# User blanchet
# Date 1401723266 -7200
# Node ID f028d93798e685cee341a7e632aaeaaefa74df00
# Parent  87b4d54b1fbe6c956a9eb7548cb6a9cf79328860
simplified counterexample handling

diff -r 87b4d54b1fbe -r f028d93798e6 src/HOL/Tools/SMT2/smt2_failure.ML
--- 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
 
diff -r 87b4d54b1fbe -r f028d93798e6 src/HOL/Tools/SMT2/smt2_solver.ML
--- 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)
 
diff -r 87b4d54b1fbe -r f028d93798e6 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
--- 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