src/HOL/Tools/res_atp.ML

 *)
 
 signature RES_ATP =
 sig
   val axiom_file : Path.T
-  val full_spass: bool ref
-  val spass: bool ref
-  val vampire: bool ref
+  val prover: string ref
   val custom_spass: string list ref
   val hook_count: int ref
 end;
 
 structure ResAtp: RES_ATP =

 val call_atp = ref false;
 val hook_count = ref 0;
 
 fun debug_tac tac = (debug "testing"; tac);
 
-val vampire = ref false;   (* use Vampire as default prover? *)
-val spass = ref true;      (* use spass as default prover *)
-val full_spass = ref true;  (*specifies Auto mode: SPASS can use all inference rules*)
+val prover = ref "spass";   (* use spass as default prover *)
 val custom_spass =   (*specialized options for SPASS*)
       ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
            "-DocProof","-TimeLimit=60"];
 
 val axiom_file = File.tmp_path (Path.basic "axioms");

 (* (ResLib.writeln_strs out (tfree_clss @ dfg_clss); *)
     end;
 
 
 (*********************************************************************)
-(* call SPASS with settings and problem file for the current subgoal *)
-(* should be modified to allow other provers to be called            *)
+(* call prover with settings and problem file for the current subgoal *)
 (*********************************************************************)
 (* now passing in list of skolemized thms and list of sgterms to go with them *)
 fun call_resolve_tac  (thms: thm list list)  sign (sg_terms:  term list) (childin, childout,pid) n  =
   let
     val axfile = (File.platform_path axiom_file)

             val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
 
             val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n)
             val _ = debug ("prob file in call_resolve_tac is " ^ probfile)
           in
-            if !spass
+            if !prover = "spass"
             then
-              let val optionline = (*Custom SPASS options, or default?*)
-		      if !full_spass (*Auto mode: all SPASS inference rules*)
-                      then "-DocProof%-TimeLimit=60%-SOS"
-                      else "-" ^ space_implode "%-" (!custom_spass)
+              let val optionline = 
+		      if !SpassComm.reconstruct 
+		          (*Proof reconstruction works for only a limited set of 
+		            inference rules*)
+                      then "-" ^ space_implode "%-" (!custom_spass)
+                      else "-DocProof%-TimeLimit=60%-SOS" (*Auto mode*)
                   val _ = debug ("SPASS option string is " ^ optionline)
                   val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
                     (*We've checked that SPASS is there for ATP/spassshell to run.*)
               in 
                   ([("spass", thmstr, goalstring,
                      getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
                      optionline, axfile, hypsfile, probfile)] @ 
                   (make_atp_list xs sign (n+1)))
               end
-            else if !vampire 
+            else if !prover = "vampire"
 	    then 
               let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
               in
                 ([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000",
                    axfile, hypsfile, probfile)] @
                  (make_atp_list xs sign (n+1)))
               end
-      	     else
-             let val Eprover = ResLib.helper_path "E_HOME" "eproof"
-              in
-                ([("E", thmstr, goalstring, Eprover, "--tptp-in -l5",
-                   axfile, hypsfile, probfile)] @
-                 (make_atp_list xs sign (n+1)))
-              end
-
+      	     else if !prover = "E"
+      	     then
+	       let val Eprover = ResLib.helper_path "E_HOME" "eproof"
+	       in
+		  ([("E", thmstr, goalstring, Eprover, 
+		     "--tptp-in%-l5%-xAuto%-tAuto%--soft-cpu-limit=60",
+		     axfile, hypsfile, probfile)] @
+		   (make_atp_list xs sign (n+1)))
+	       end
+	     else error ("Invalid prover name: " ^ !prover)
           end
 
     val atp_list = make_atp_list (ListPair.zip (thms, sg_terms)) sign 1
   in
     Watcher.callResProvers(childout,atp_list);

        (call_resolve_tac  (rev sko_thms)
         sign  sg_terms (childin, childout, pid) (List.length sg_terms);
         all_tac thm)
      else
 	
-     ( SELECT_GOAL
+      (SELECT_GOAL
         (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, 
           METAHYPS(fn negs => 
-            (if !spass 
+            (if !prover = "spass" 
              then dfg_inputs_tfrees (make_clauses negs) n tfrees axclauses
              else tptp_inputs_tfrees (make_clauses negs) n tfrees axclauses;
              get_sko_thms tfrees sign sg_terms (childin, childout, pid) 
-                          thm  (n -1) (negs::sko_thms) axclauses; 
-             all_tac))]) n thm )
+                          thm (n-1) (negs::sko_thms) axclauses; 
+             all_tac))]) n thm)
 
 
 
 (**********************************************)
 (* recursively call atp_tac_g on all subgoals *)
 (* sg_term is the nth subgoal as a term - used*)
 (* in proof reconstruction                    *)
 (**********************************************)
 
-fun isar_atp_goal' thm n tfree_lits (childin, childout, pid)  axclauses =
-  let
-    val prems = Thm.prems_of thm
-    (*val sg_term = get_nth k prems*)
-    val sign = sign_of_thm thm
-    val thmstring = string_of_thm thm
+fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) axclauses =
+  let val tfree_lits = isar_atp_h thms
+      val prems = Thm.prems_of thm
+      val sign = sign_of_thm thm
+      val thmstring = string_of_thm thm
   in
-    debug("in isar_atp_goal'");
+    debug ("in isar_atp_aux");
     debug("thmstring in isar_atp_goal': " ^ thmstring);
     (* go and call callResProvers with this subgoal *)
     (* isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; *)
     (* recursive call to pick up the remaining subgoals *)
     (* isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) *)
-    get_sko_thms tfree_lits sign prems (childin, childout, pid) thm n []  axclauses
-  end;
-
-
-(**************************************************)
-(* convert clauses from "assume" to conjecture.   *)
-(* i.e. apply make_clauses and then get tptp for  *)
-(* any hypotheses in the goal produced by assume  *)
-(* statements;                                    *)
-(* write to file "hyps"                           *)
-(**************************************************)
-
-fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) axclauses =
-  let val tfree_lits = isar_atp_h thms
-  in
-    debug ("in isar_atp_aux");
-    isar_atp_goal' thm n_subgoals tfree_lits (childin, childout, pid)  axclauses
+    get_sko_thms tfree_lits sign prems (childin, childout, pid) 
+                 thm n_subgoals []  axclauses
   end;
 
 (******************************************************************)
 (* called in Isar automatically                                   *)
 (* writes out the current clasimpset to a tptp file               *)

     let
       val _= debug ("in isar_atp'")
       val thy = ProofContext.theory_of ctxt
       val prems = Thm.prems_of thm
       val thms_string = Meson.concat_with_and (map string_of_thm thms)
-      val thm_string = string_of_thm thm
       val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) prems)
 
       (*set up variables for writing out the clasimps to a tptp file*)
       val (clause_arr, num_of_clauses, axclauses) =
         ResClasimp.get_clasimp_lemmas thy (hd prems) (*FIXME: hack!! need to do all prems*)

       val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr, num_of_clauses)
       val pid_string =
         string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid)))
     in
       debug ("initial thms: " ^ thms_string);
-      debug ("initial thm: " ^ thm_string);
       debug ("subgoals: " ^ prems_string);
       debug ("pid: "^ pid_string);
       isar_atp_aux thms thm (length prems) (childin, childout, pid) axclauses;
       ()
     end);