src/HOL/Tools/res_atp.ML
changeset 15919 b30a35432f5a
parent 15782 a1863ea9052b
child 16039 dfe264950511
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue May 03 10:33:31 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue May 03 14:27:21 2005 +0200
     1.3 @@ -180,22 +180,28 @@
     1.4                               val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring);
     1.5                               val _ = TextIO.flushOut outfile;
     1.6                               val _ =  TextIO.closeOut outfile
     1.7 +                             val spass_home = getenv "SPASS_HOME"
     1.8                            in
     1.9                             (* without paramodulation *)
    1.10                             (warning ("goalstring in call_res_tac is: "^goalstring));
    1.11                             (warning ("prob file in cal_res_tac is: "^probfile));
    1.12 +                                                       Watcher.callResProvers(childout,
    1.13 +                            [("spass",thmstr,goalstring,spass_home,  
    1.14 +                             "-DocProof", 
    1.15 +                             clasimpfile, axfile, hypsfile, probfile)]);
    1.16 +
    1.17                              Watcher.callResProvers(childout,
    1.18 -                            [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS",  
    1.19 +                            [("spass",thmstr,goalstring,spass_home,  
    1.20                               "-FullRed=0%-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", 
    1.21                               clasimpfile, axfile, hypsfile, probfile)]);
    1.22  
    1.23                             (* with paramodulation *)
    1.24                             (*Watcher.callResProvers(childout,
    1.25 -                                  [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS",
    1.26 +                                  [("spass",thmstr,goalstring,spass_home,
    1.27                                    "-FullRed=0%-ISPm=1%-Split=0%-PObv=0%-DocProof", 
    1.28                                      prob_path)]); *)
    1.29                            (* Watcher.callResProvers(childout,
    1.30 -                           [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS", 
    1.31 +                           [("spass",thmstr,goalstring,spass_home, 
    1.32                             "-DocProof",  prob_path)]);*)
    1.33                             dummy_tac
    1.34                           end
    1.35 @@ -282,24 +288,32 @@
    1.36  (******************************************************************)
    1.37  (*FIX changed to clasimp_file *)
    1.38  fun isar_atp' (thms, thm) =
    1.39 -    let val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.40 +    let 
    1.41 +	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.42          val _= (warning ("in isar_atp'"))
    1.43          val prems  = prems_of thm
    1.44          val sign = sign_of_thm thm
    1.45          val thms_string = Meson.concat_with_and (map string_of_thm thms) 
    1.46          val thmstring = string_of_thm thm
    1.47          val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
    1.48 -        (* set up variables for writing out the clasimps to a tptp file *)
    1.49 +        
    1.50 +	(* set up variables for writing out the clasimps to a tptp file *)
    1.51 +	val (clause_arr, num_of_clauses) = ResClasimp.write_out_clasimp (File.sysify_path clasimp_file) 
    1.52 +        val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) )  
    1.53  
    1.54 -         val clause_arr = write_out_clasimp (File.sysify_path clasimp_file) clause_arr
    1.55 -        val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) )  
    1.56          (* cq: add write out clasimps to file *)
    1.57 -        (* cq:create watcher and pass to isar_atp_aux *) 
    1.58 -        (*val tenth_ax = fst( Array.sub(clause_arr, 10))  
    1.59 -        val _ = (warning ("tenth axiom in array is: "^tenth_ax))         
    1.60 -        val _ = (warning ("num_of_clauses is: "^(string_of_int (!num_of_clauses))) )  *)      
    1.61 -                               
    1.62 -        val (childin,childout,pid) = Watcher.createWatcher(thm)
    1.63 +        (* cq:create watcher and pass to isar_atp_aux *)
    1.64 +        (* tracing *) 
    1.65 +        (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
    1.66 +         val tenth_ax_thms = Recon_Transfer.memo_find_clause (tenth_ax, clause_tab)
    1.67 +         val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
    1.68 +         val _ = (warning ("tenth axiom in array is: "^tenth_ax))         
    1.69 +         val _ = (warning ("tenth axiom in table is: "^clause_str))         
    1.70 +                 
    1.71 +         val _ = (warning ("num_of_clauses is: "^(string_of_int (num_of_clauses))) )     
    1.72 +         *)             
    1.73 +        
    1.74 +        val (childin,childout,pid) = Watcher.createWatcher(thm,clause_arr, num_of_clauses)
    1.75          val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid )))
    1.76      in
    1.77  	case prems of [] => ()