# HG changeset patch
# User wenzelm
# Date 1227004019 -3600
# Node ID d4d8eba5f78122f2ca0067509fbd341a0ab30a61
# Parent  66d31ca2c5af1e0a8ad8e79c95dee7f3ecb4055f
changes by Fabian Immler:
improved handling of prover errors;
explicit treatment of clauses that are too trivial for resolution;

diff -r 66d31ca2c5af -r d4d8eba5f781 src/HOL/Tools/atp_manager.ML
--- a/src/HOL/Tools/atp_manager.ML	Tue Nov 18 09:41:23 2008 +0100
+++ b/src/HOL/Tools/atp_manager.ML	Tue Nov 18 11:26:59 2008 +0100
@@ -287,6 +287,10 @@
           let
             val _ = register birthtime deadtime (Thread.self (), desc)
             val result = prover i proof_state
+              handle ResHolClause.TOO_TRIVIAL
+                => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
+              | ERROR msg
+                => (false, "Error: " ^ msg)
             val _ = priority (unregister result (Thread.self ()))
           in () end handle Interrupt => ())
       in () end);
diff -r 66d31ca2c5af -r d4d8eba5f781 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Tue Nov 18 09:41:23 2008 +0100
+++ b/src/HOL/Tools/res_hol_clause.ML	Tue Nov 18 11:26:59 2008 +0100
@@ -25,6 +25,7 @@
   datatype literal = Literal of polarity * combterm
   val strip_comb: combterm -> combterm * combterm list
   val literals_of_term: theory -> term -> literal list * typ list
+  exception TOO_TRIVIAL
   val tptp_write_file: theory -> bool -> thm list -> string ->
     (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list *
       ResClause.arityClause list -> string list -> axiom_name list
@@ -164,12 +165,15 @@
 
 fun literals_of_term thy P = literals_of_term1 thy ([],[]) P;
 
+(* Problem too trivial for resolution (empty clause) *)
+exception TOO_TRIVIAL;
+
 (* making axiom and conjecture clauses *)
 fun make_clause thy (clause_id,axiom_name,kind,th) =
     let val (lits,ctypes_sorts) = literals_of_term thy (prop_of th)
     in
         if forall isFalse lits
-        then error "Problem too trivial for resolution (empty clause)"
+        then raise TOO_TRIVIAL
         else
             Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
                     literals = lits, ctypes_sorts = ctypes_sorts}