src/HOL/Tools/ATP/watcher.ML
changeset 15782 a1863ea9052b
parent 15774 9df37a0e935d
child 15787 8fad4bd4e53c
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Wed Apr 20 17:19:42 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Wed Apr 20 18:01:50 2005 +0200
     1.3 @@ -75,32 +75,43 @@
     1.4  (*  Send request to Watcher for multiple provers to be called for filenames in arg      *)
     1.5  (*****************************************************************************************)
     1.6  
     1.7 +
     1.8 +
     1.9  (* need to modify to send over hyps file too *)
    1.10  fun callResProvers (toWatcherStr,  []) = (sendOutput (toWatcherStr, "End of calls\n"); 
    1.11                                       TextIO.flushOut toWatcherStr)
    1.12 -|   callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,probfile)::args) =
    1.13 -                                                     let 
    1.14 -                                                        val dfg_dir = File.tmp_path (Path.basic "dfg");
    1.15 -                                                        (* need to check here if the directory exists and, if not, create it*)
    1.16 -                                                         val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic"thmstring_in_watcher")));                                                                                    
    1.17 -                                                         val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
    1.18 +|   callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile,probfile)::args) =
    1.19 +                                                     let val dfg_dir = File.tmp_path (Path.basic "dfg"); 
    1.20 +                                                        (*** need to check here if the directory exists and, if not, create it***)
    1.21 +                                                         val  outfile = TextIO.openAppend(File.sysify_path
    1.22 +                                                                               (File.tmp_path (Path.basic"thmstring_in_watcher")));                                                                         val _ = TextIO.output (outfile, 
    1.23 +                                                                       (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
    1.24                                                           val _ =  TextIO.closeOut outfile
    1.25 +                                                        (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
    1.26 +							val probID = last(explode probfile)
    1.27 +                                                         val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
    1.28 +                                                         (*** only include problem and clasimp for the moment, not sure how to refer to ***)
    1.29 +                                                         (*** hyps/local axioms just now                                                ***)
    1.30 +                                                         val whole_prob_file = Unix.execute("/bin/cat", [(*clasimpfile, axfile, hypsfile,*)probfile,  ">", (File.sysify_path wholefile)])
    1.31                                                           val dfg_create =if File.exists dfg_dir 
    1.32                                                                           then
    1.33 -                                                                             ()
    1.34 +                                                                             ((warning("dfg dir exists"));())
    1.35                                                                           else
    1.36                                                                                 File.mkdir dfg_dir; 
    1.37 -                                                         val probID = last(explode probfile)
    1.38 +                                                         
    1.39                                                           val dfg_path = File.sysify_path dfg_dir;
    1.40 -                                                         val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v2.6.0/TPTP2X/tptp2X", ["-fdfg "^probfile^" -d "^dfg_path])
    1.41 +                                                         val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X",
    1.42 +                                                                                       ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path])
    1.43                                                         (*val _ = Posix.Process.wait ()*)
    1.44                                                         (*val _ =Unix.reap exec_tptp2x*)
    1.45 -                                                         val newfile = dfg_path^"/prob"^"_"^(probID)^".dfg"
    1.46 +                                                         val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
    1.47                                         
    1.48                                                        in   
    1.49                                                           goals_being_watched := (!goals_being_watched) + 1;
    1.50                                                           OS.Process.sleep(Time.fromSeconds 1); 
    1.51 +                     					(warning ("probfile is: "^probfile));
    1.52                                                           (warning("dfg file is: "^newfile));
    1.53 +                                                         (warning ("wholefile is: "^(File.sysify_path wholefile)));
    1.54                                                           sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n"));
    1.55                                                           TextIO.flushOut toWatcherStr;
    1.56                                                           Unix.reap exec_tptp2x; 
    1.57 @@ -108,13 +119,13 @@
    1.58                                                           callResProvers (toWatcherStr,args)
    1.59                                             
    1.60                                                       end
    1.61 -
    1.62 +(*
    1.63  fun callResProversStr (toWatcherStr,  []) =  "End of calls\n" 
    1.64                                       
    1.65 -|   callResProversStr (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings, file)::args) =
    1.66 -                                            ((prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^file^"\n")
    1.67 +|   callResProversStr (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile, probfile)::args) =
    1.68 +                                            ((prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^clasimpfile^"*"^axfile^"*"^hypsfile^"*"^probfile^"\n")
    1.69                                              
    1.70 -                                           )
    1.71 +     *)                                      
    1.72   
    1.73  (**************************************************************)
    1.74  (* Send message to watcher to kill currently running vampires *)
    1.75 @@ -233,7 +244,7 @@
    1.76  
    1.77  
    1.78  
    1.79 -fun setupWatcher () = let
    1.80 +fun setupWatcher (thm) = let
    1.81            (** pipes for communication between parent and watcher **)
    1.82            val p1 = Posix.IO.pipe ()
    1.83            val p2 = Posix.IO.pipe ()
    1.84 @@ -260,6 +271,10 @@
    1.85                        val fromParentIOD = Posix.FileSys.fdToIOD fromParent
    1.86                        val fromParentStr = openInFD ("_exec_in_parent", fromParent)
    1.87                        val toParentStr = openOutFD ("_exec_out_parent", toParent)
    1.88 +                      val sign = sign_of_thm thm
    1.89 +                      val prems = prems_of thm
    1.90 +                      val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
    1.91 +                      val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
    1.92                        (*val goalstr = string_of_thm (the_goal)
    1.93                         val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher")));  
    1.94                        val _ = TextIO.output (outfile,goalstr )
    1.95 @@ -333,12 +348,20 @@
    1.96                      |   checkChildren ((childProc::otherChildren), toParentStr) = 
    1.97                                              let val (childInput,childOutput) =  cmdstreamsOf childProc
    1.98                                                  val childPid = cmdchildPid childProc
    1.99 +                                                (* childCmd is the .dfg file that the problem is in *)
   1.100                                                  val childCmd = fst(snd (cmdchildInfo childProc))
   1.101 +                                                (* now get the number of the subgoal from the filename *)
   1.102 +                                                val sg_num = int_of_string(get_nth 5 (rev(explode childCmd)))
   1.103                                                  val childIncoming = pollChildInput childInput
   1.104                                                  val parentID = Posix.ProcEnv.getppid()
   1.105                                                  val prover = cmdProver childProc
   1.106                                                  val thmstring = cmdThm childProc
   1.107 +                                                val sign = sign_of_thm thm
   1.108 +                                                val prems = prems_of thm
   1.109 +                                                val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   1.110 +                                                val _ = (warning ("subgoals forked to checkChildren: "^prems_string));
   1.111                                                  val goalstring = cmdGoal childProc
   1.112 +                                                                                                       
   1.113                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms")));  
   1.114                                                  val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
   1.115                                                  val _ =  TextIO.closeOut outfile
   1.116 @@ -348,10 +371,10 @@
   1.117                                                    (* check here for prover label on child*)
   1.118                                                     
   1.119                                                    let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));  
   1.120 -                                                val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
   1.121 +                                                val _ = TextIO.output (outfile,(("subgoals forked to checkChildren: "^prems_string)^prover^thmstring^goalstring^childCmd) )
   1.122                                                  val _ =  TextIO.closeOut outfile
   1.123                                                val childDone = (case prover of
   1.124 -                                    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd)     ) )
   1.125 +                                    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num)     ) )
   1.126                                                     in
   1.127                                                      if childDone      (**********************************************)
   1.128                                                      then              (* child has found a proof and transferred it *)
   1.129 @@ -386,6 +409,7 @@
   1.130                  (* takes list of (string, string, string list, string)list proclist *)
   1.131                  (********************************************************************)
   1.132  
   1.133 +           (*** add subgoal id num to this *)
   1.134                     fun execCmds  [] procList = procList
   1.135                     |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  = 
   1.136                                                       if (prover = "spass") 
   1.137 @@ -563,63 +587,19 @@
   1.138  (**********************************************************)
   1.139  fun killWatcher pid= killChild pid;
   1.140  
   1.141 -fun createWatcher () = let val mychild = childInfo (setupWatcher())
   1.142 +fun createWatcher (thm) = let val mychild = childInfo (setupWatcher(thm))
   1.143  			   val streams =snd mychild
   1.144                             val childin = fst streams
   1.145                             val childout = snd streams
   1.146                             val childpid = fst mychild
   1.147 -                           
   1.148 +                           val sign = sign_of_thm thm
   1.149 +                           val prems = prems_of thm
   1.150 +                           val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   1.151 +                           val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
   1.152                             fun vampire_proofHandler (n) =
   1.153                             (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.154 -                           getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )                   
   1.155 +                           getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )               
   1.156                            
   1.157 -                          (* fun spass_proofHandler (n:int) = (
   1.158 -                                                      let val (reconstr, thmstring, goalstring) = getSpassInput childin
   1.159 -                                                          val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
   1.160 -
   1.161 -                                                         val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^"  "^thmstring))
   1.162 -                                                         val _ =  TextIO.closeOut outfile
   1.163 -                                                      in
   1.164 -                                                         Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.165 -                                                          Pretty.writeln(Pretty.str reconstr) ;
   1.166 -                                                         Pretty.writeln(Pretty.str  (oct_char "361"));
   1.167 -                                                         (*killWatcher childpid;*) () 
   1.168 -                                                      end)*)
   1.169 -
   1.170 -
   1.171 -(*
   1.172 -
   1.173 -fun spass_proofHandler (n:int) = (
   1.174 -                                                      let  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
   1.175 -
   1.176 -                                                         val _ = TextIO.output (outfile, ("In signal handler now\n"))
   1.177 -                                                         val _ =  TextIO.closeOut outfile
   1.178 -                                                          val (reconstr, thmstring, goalstring) = getSpassInput childin
   1.179 -                                                         val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
   1.180 -
   1.181 -                                                         val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^"  "^thmstring^goalstring))
   1.182 -                                                         val _ =  TextIO.closeOut outfile
   1.183 -                                                       in
   1.184 -                                                        if ( (substring (reconstr, 0,1))= "[")
   1.185 -                                                         then 
   1.186 -
   1.187 -                                                          let val thm = thm_of_string thmstring
   1.188 -                                                              val clauses = make_clauses [thm]
   1.189 -                                                              val numcls =  ListPair.zip  (numlist (length clauses), map make_meta_clause clauses)
   1.190 -                                                         
   1.191 -                                                          in
   1.192 -                                                             Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.193 -                                                             Recon_Transfer.apply_res_thm reconstr goalstring;
   1.194 -                                                             Pretty.writeln(Pretty.str  (oct_char "361"));
   1.195 -                                                             killWatcher childpid; () 
   1.196 -                                                          end
   1.197 -                                                       else
   1.198 -                                                           Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.199 -                                                              Pretty.writeln(Pretty.str (goalstring^reconstr));
   1.200 -                                                             Pretty.writeln(Pretty.str  (oct_char "361"));
   1.201 -                                                             (*killWatcher childpid; *) reap (childpid,childin, childout);()   
   1.202 -                                                      end )
   1.203 -*)
   1.204  
   1.205  fun spass_proofHandler (n) = (
   1.206                                   let  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
   1.207 @@ -699,8 +679,7 @@
   1.208  
   1.209  
   1.210                          
   1.211 -                       in 
   1.212 -                          IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
   1.213 +                       in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
   1.214                            IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
   1.215                            (childin, childout, childpid)
   1.216