src/HOL/Tools/atp_wrapper.ML
changeset 29590 479a2fce65e6
parent 29587 96599d8d8268
child 29593 7b73bd578db2
--- a/src/HOL/Tools/atp_wrapper.ML	Mon Jan 19 20:24:10 2009 +0100
+++ b/src/HOL/Tools/atp_wrapper.ML	Tue Jan 20 16:05:57 2009 +0100
@@ -12,7 +12,7 @@
   val external_prover:
     ((int -> Path.T) -> Proof.context * thm list * thm -> string list * ResHolClause.axiom_name Vector.vector list) ->
     Path.T * string ->
-    (string * int -> bool) ->
+    (string -> string option) ->
     (string * string vector * Proof.context * thm * int -> string) ->
     AtpManager.prover
   val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
@@ -30,8 +30,8 @@
   val eprover_full: AtpManager.prover
   val spass_opts: int -> bool  -> AtpManager.prover
   val spass: AtpManager.prover
-  val remote_prover_opts: int -> bool -> string -> int -> AtpManager.prover
-  val remote_prover: string -> int -> AtpManager.prover
+  val remote_prover_opts: int -> bool -> string -> AtpManager.prover
+  val remote_prover: string -> AtpManager.prover
 end;
 
 structure AtpWrapper: ATP_WRAPPER =
@@ -47,7 +47,7 @@
 
 (* basic template *)
 
-fun external_prover write_problem_files (cmd, args) check_success produce_answer subgoalno state =
+fun external_prover write_problem_files (cmd, args) find_failure produce_answer subgoalno state =
   let
     (* path to unique problem file *)
     val destdir' = ! destdir
@@ -70,19 +70,18 @@
       if File.exists cmd then File.shell_path cmd ^ " " ^ args
       else error ("Bad executable: " ^ Path.implode cmd)
     val (proof, rc) = system_out (cmdline ^ " " ^ nth filenames (subgoalno - 1))
-    val _ =
-      if rc <> 0 then
-        warning ("Sledgehammer prover exited with return code " ^ string_of_int rc ^ "\n" ^ cmdline)
-      else ()
 
     (* remove *temporary* files *)
     val _ = if destdir' = "" then List.app OS.FileSys.remove filenames else ()
-
-    val success = check_success (proof, rc)
+    
+    (* check for success and print out some information on failure *)
+    val failure = find_failure proof
+    val success = (rc = 0) andalso (not (isSome failure))
     val message =
-      if success
-      then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
-      else "Failed."
+      if isSome failure then "Could not prove: " ^ the failure
+      else if rc <> 0
+      then "Exited with return code " ^ string_of_int rc ^ ": " ^ proof 
+      else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
   in (success, message) end;
 
 
@@ -95,7 +94,7 @@
   external_prover
     (ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const)
     command
-    ResReconstruct.check_success_e_vamp_spass
+    ResReconstruct.find_failure_e_vamp_spass
     (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp);
 
 (*arbitrary ATP with TPTP input/output and problemfile as last argument*)
@@ -148,7 +147,7 @@
 fun spass_opts max_new theory_const = external_prover
   (ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const)
   (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof")
-  ResReconstruct.check_success_e_vamp_spass
+  ResReconstruct.find_failure_e_vamp_spass
   ResReconstruct.lemma_list_dfg;
 
 val spass = spass_opts 40 true;
@@ -156,9 +155,9 @@
 
 (* remote prover invocation via SystemOnTPTP *)
 
-fun remote_prover_opts max_new theory_const name timelimit =
+fun remote_prover_opts max_new theory_const args =
   tptp_prover_opts max_new theory_const
-  (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ (string_of_int timelimit));
+  (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", args);
 
 val remote_prover = remote_prover_opts 60 false;