# HG changeset patch
# User blanchet
# Date 1306188093 -7200
# Node ID 26111aafab123e929ba0b59b643eb29eb1407292
# Parent  96f62b77748f95f8ffc0d1b1d33c1b19df817fee
detect inappropriate problems and crashes better in Waldmeister

diff -r 96f62b77748f -r 26111aafab12 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue May 24 00:01:33 2011 +0200
@@ -395,10 +395,15 @@
       (case hard_timeout of
         NONE => I
       | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
+    fun failed failure =
+      ({outcome = SOME failure, message = "", used_facts = [],
+        run_time_in_msecs = NONE}, ~1)
     val ({outcome, message, used_facts, run_time_in_msecs}
          : Sledgehammer_Provers.prover_result,
         time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
       let
+        val _ = if is_appropriate_prop concl_t then ()
+                else raise Fail "inappropriate"
         val facts =
           Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
               (the_default default_max_relevant max_relevant)
@@ -410,9 +415,8 @@
            facts = facts |> map Sledgehammer_Provers.Untranslated_Fact,
            smt_filter = NONE}
       in prover params (K "") problem end)) ()
-      handle TimeLimit.TimeOut =>
-             ({outcome = SOME ATP_Proof.TimedOut, message = "", used_facts = [],
-               run_time_in_msecs = NONE}, ~1)
+      handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
+           | Fail "inappropriate" => failed ATP_Proof.Inappropriate
     val time_prover = run_time_in_msecs |> the_default ~1
   in
     case outcome of
diff -r 96f62b77748f -r 26111aafab12 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue May 24 00:01:33 2011 +0200
@@ -20,6 +20,7 @@
     UnsoundProof of bool * string list |
     CantConnect |
     TimedOut |
+    Inappropriate |
     OutOfResources |
     SpassTooOld |
     VampireTooOld |
@@ -70,6 +71,7 @@
   UnsoundProof of bool * string list |
   CantConnect |
   TimedOut |
+  Inappropriate |
   OutOfResources |
   SpassTooOld |
   VampireTooOld |
@@ -143,6 +145,8 @@
     \Isabelle developers."
   | string_for_failure CantConnect = "Cannot connect to remote server."
   | string_for_failure TimedOut = "Timed out."
+  | string_for_failure Inappropriate =
+    "The problem lies outside the prover's scope."
   | string_for_failure OutOfResources = "The prover ran out of resources."
   | string_for_failure SpassTooOld =
     "Isabelle requires a more recent version of SPASS with support for the \
diff -r 96f62b77748f -r 26111aafab12 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue May 24 00:01:33 2011 +0200
@@ -383,7 +383,8 @@
      [(Unprovable, "says Satisfiable"),
       (IncompleteUnprovable, "says Unknown"),
       (IncompleteUnprovable, "says GaveUp"),
-      (TimedOut, "says Timeout")],
+      (TimedOut, "says Timeout"),
+      (Inappropriate, "says Inappropriate")],
    conj_sym_kind = conj_sym_kind,
    prem_kind = prem_kind,
    formats = formats,
@@ -420,8 +421,10 @@
 val remote_waldmeister =
   remote_atp waldmeisterN "Waldmeister" ["710"]
              [("#START OF PROOF", "Proved Goals:")]
-             [(OutOfResources, "Too many function symbols")] Hypothesis
-             Hypothesis [CNF_UEQ] (K (100, ["poly_args"]) (* FUDGE *))
+             [(OutOfResources, "Too many function symbols"),
+              (Crashed, "Unrecoverable Segmentation Fault")]
+             Hypothesis Hypothesis [CNF_UEQ]
+             (K (100, ["poly_args"]) (* FUDGE *))
 
 (* Setup *)