Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/VampCommunication.ML
changeset 17315 5bf0e0aacc24
parent 17312 159783c74f75
child 17376 a62e77a9d654
equal deleted inserted replaced
17314:04e21a27c0ad 17315:5bf0e0aacc24 
     7 (***************************************************************************)
 
     7 (***************************************************************************)
 
     8 (*  Code to deal with the transfer of proofs from a Vampire process          *)
 
     8 (*  Code to deal with the transfer of proofs from a Vampire process          *)
 
     9 (***************************************************************************)
 
     9 (***************************************************************************)
 
    10 signature VAMP_COMM =
 
    10 signature VAMP_COMM =
 
    11   sig
 
    11   sig
 
       
    12     val getEInput : TextIO.instream -> string * string * string
 
       
    13     val checkEProofFound: 
       
    14           TextIO.instream * TextIO.outstream * Posix.Process.pid * string * 
       
    15           string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
 
       
    16 
    12     val getVampInput : TextIO.instream -> string * string * string
 
    17     val getVampInput : TextIO.instream -> string * string * string
 
    13     val checkVampProofFound: 
    18     val checkVampProofFound: 
    14           TextIO.instream * TextIO.outstream * Posix.Process.pid * string *
 
    19           TextIO.instream * TextIO.outstream * Posix.Process.pid * string *
 
    15           string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
 
    20           string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
 
    16   end;
 
    21   end;
 
    19 struct
 
    24 struct
 
    20 
    25 
    21 exception EOF;
 
    26 exception EOF;
 
    22 
    27 
    23 (**********************************************************************)
 
    28 (**********************************************************************)
 
    24 (*  Reconstruct the Vampire proof w.r.t. thmstring (string version of   *)
 
    29 (*  Reconstruct the Vampire/E proof w.r.t. thmstring (string version of   *)
 
    25 (*  Isabelle goal to be proved), then transfer the reconstruction     *)
 
    30 (*  Isabelle goal to be proved), then transfer the reconstruction     *)
 
    26 (*  steps as a string to the input pipe of the main Isabelle process  *)
 
    31 (*  steps as a string to the input pipe of the main Isabelle process  *)
 
    27 (**********************************************************************)
 
    32 (**********************************************************************)
 
    28 
    33 
    29 fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num 
    34 fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num 
    30                     clause_arr num_of_clauses =
 
    35                     clause_arr num_of_clauses =
 
    31     SELECT_GOAL
 
    36     SELECT_GOAL
 
    32       (EVERY1
 
    37       (EVERY1
 
    33         [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
 
    38         [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
 
    34 	 METAHYPS(fn negs =>
 
    39 	 METAHYPS(fn negs =>
 
    35 		     (Recon_Transfer.vampString_to_lemmaString proofextract thmstring 
    40 		     (Recon_Transfer.proverString_to_lemmaString proofextract thmstring 
    36 		       goalstring toParent ppid negs clause_arr num_of_clauses))]) sg_num
 
    41 		       goalstring toParent ppid negs clause_arr num_of_clauses))]) sg_num
 
    37 
    42 
    38 
    43 
    39 fun transferVampInput (fromChild, toParent, ppid,thmstring,goalstring, 
       
    40                        currentString, thm, sg_num,clause_arr, num_of_clauses) =
 
       
    41   let val thisLine = TextIO.inputLine fromChild
 
       
    42   in
 
       
    43     if thisLine = "" (*end of file?*)
 
       
    44     then (File.write (File.tmp_path (Path.basic"vampire_extraction_failed")) currentString;
 
       
    45 	  raise EOF)                    
       
    46     else if (thisLine = "%==============  End of proof. ==================\n" )
 
       
    47     then let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
 
       
    48 	 in
 
       
    49 	   File.write (File.tmp_path (Path.basic"vampire_extracted_prf")) proofextract; 
       
    50 	   reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num  
       
    51 	                   clause_arr num_of_clauses thm
 
       
    52 	 end
 
       
    53     else transferVampInput (fromChild, toParent, ppid,thmstring, goalstring, 
       
    54              currentString^thisLine, thm, sg_num, clause_arr, num_of_clauses)
 
       
    55   end;
 
       
    56 
       
    57 
       
    58 (*********************************************************************************)
 
    44 (*********************************************************************************)
 
    59 (*  Inspect the output of a Vampire process to see if it has found a proof,     *)
 
    45 (*  Inspect the output of an ATP process to see if it has found a proof,     *)
 
    60 (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
 
    46 (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
 
    61 (*********************************************************************************)
 
    47 (*********************************************************************************)
 
    62 
    48 
    63 
    49 fun startTransfer (startS,endS)
 
    64 fun startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,
 
    50       (fromChild, toParent, ppid, thmstring,goalstring,childCmd,
 
    65                        thm, sg_num,clause_arr, num_of_clauses) =
 
    51        thm, sg_num,clause_arr, num_of_clauses) =
 
    66     let val thisLine = TextIO.inputLine fromChild
 
    52  let val thisLine = TextIO.inputLine fromChild
 
    67     in
 
    53      fun transferInput currentString =
 
    68       if thisLine = "" then false
 
    54       let val thisLine = TextIO.inputLine fromChild
 
    69       else if (thisLine = "%================== Proof: ======================\n")
 
    55       in
 
    70       then
 
    56 	if thisLine = "" (*end of file?*)
 
    71        (File.append (File.tmp_path (Path.basic "vampire_transfer"))
 
    57 	then (File.write (File.tmp_path (Path.basic"extraction_failed")) 
    72 		    ("about to transfer proof, thm is: " ^ string_of_thm thm);
 
    58 	                 ("start bracket: " ^ startS ^
 
    73 	transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,
 
    59 	                  "\nend bracket: " ^ endS ^
 
    74 			   thisLine, thm, sg_num,clause_arr, num_of_clauses);
 
    60 	                  "\naccumulated text: " ^ currentString);
 
    75 	true) handle EOF => false
 
    61 	      raise EOF)                    
    76       else
 
    62 	else if String.isPrefix endS thisLine
 
    77 	 startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring,
 
    63 	then let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
 
    78 			    childCmd, thm, sg_num,clause_arr, num_of_clauses)
 
    64 	     in
 
    79     end
 
    65 	       File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; 
       
    66 	       reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num  
       
    67 			       clause_arr num_of_clauses thm
 
       
    68 	     end
 
       
    69 	else transferInput (currentString^thisLine)
 
       
    70       end
 
       
    71  in
 
       
    72    if thisLine = "" then false
 
       
    73    else if String.isPrefix startS thisLine
 
       
    74    then
 
       
    75     (File.append (File.tmp_path (Path.basic "transfer_start"))
 
       
    76 		 ("about to transfer proof, thm is: " ^ string_of_thm thm);
 
       
    77      transferInput thisLine;
 
       
    78      true) handle EOF => false
 
       
    79    else
 
       
    80       startTransfer (startS,endS)
 
       
    81                     (fromChild, toParent, ppid, thmstring, goalstring,
 
       
    82 		     childCmd, thm, sg_num,clause_arr, num_of_clauses)
 
       
    83  end
 
    80 
    84 
    81 
    85 
    82 fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, 
    86 fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, 
    83                          thm, sg_num, clause_arr, num_of_clauses) =
 
    87                          thm, sg_num, clause_arr, num_of_clauses) =
 
    84  let val vamp_proof_file = TextIO.openAppend
 
    88  let val proof_file = TextIO.openAppend
 
    85 	   (File.platform_path(File.tmp_path (Path.basic "vampire_proof")))
 
    89 	   (File.platform_path(File.tmp_path (Path.basic "atp_proof")))
 
    86      val _ = File.write (File.tmp_path (Path.basic "vampire_checking_prf"))
 
    90      val _ = File.write (File.tmp_path (Path.basic "atp_checking_prf"))
 
    87 			("checking if proof found, thm is: " ^ string_of_thm thm)
 
    91 			("checking if proof found, thm is: " ^ string_of_thm thm)
 
    88      val thisLine = TextIO.inputLine fromChild
 
    92      val thisLine = TextIO.inputLine fromChild
 
    89  in   
    93  in   
    90      if thisLine = "" 
    94      if thisLine = "" 
    91      then (TextIO.output (vamp_proof_file, ("No proof output seen \n"));
 
    95      then (TextIO.output (proof_file, "No proof output seen \n");
 
    92 	   TextIO.closeOut vamp_proof_file;
 
    96 	   TextIO.closeOut proof_file;
 
    93 	   false)
 
    97 	   false)
 
    94      else if thisLine = "% Proof found. Thanks to Tanya!\n"
 
    98      else if thisLine = "% Proof found. Thanks to Tanya!\n"
 
    95      then
 
    99      then
 
    96       (File.write (File.tmp_path (Path.basic "vampire_response")) thisLine;
 
   100        (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
 
    97        startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring,
 
   101 	startTransfer (Recon_Parse.start_V6, Recon_Parse.end_V6)
 
    98 			  childCmd, thm, sg_num, clause_arr, num_of_clauses))
 
   102 	      (fromChild, toParent, ppid, thmstring, goalstring,
 
    99      else if (thisLine = "% Unprovable.\n" )
 
   103 	       childCmd, thm, sg_num, clause_arr, num_of_clauses))
 
       
   104      else if (thisLine = "% Unprovable.\n" ) orelse
 
       
   105              (thisLine = "% Proof not found. Time limit expired.\n")
 
   100      then
 
   106      then
 
   101       (File.write (File.tmp_path (Path.basic "vampire_response")) thisLine;
 
   107        (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
 
   102        TextIO.output (toParent,childCmd^"\n" );
 
   108 	TextIO.output (toParent,childCmd^"\n");
 
   103        TextIO.flushOut toParent;
 
   109 	TextIO.flushOut toParent;
 
   104        TextIO.output (vamp_proof_file, thisLine);
 
   110 	TextIO.output (proof_file, thisLine);
 
   105        TextIO.closeOut vamp_proof_file;
 
   111 	TextIO.closeOut proof_file;
 
   106        (*TextIO.output (toParent, thisLine);
 
   112  
   107 	TextIO.flushOut toParent;
 
   113 	TextIO.output (toParent, thisLine^"\n");
 
   108 	TextIO.output (toParent, "bar\n");
 
   114 	TextIO.output (toParent, thmstring^"\n");
 
   109 	TextIO.flushOut toParent;*)
 
   115 	TextIO.output (toParent, goalstring^"\n");
 
   110 
   116 	TextIO.flushOut toParent;
 
   111        TextIO.output (toParent, thisLine^"\n");
 
   117 	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
 
   112        TextIO.output (toParent, thmstring^"\n");
 
   118 	(* Attempt to prevent several signals from turning up simultaneously *)
 
   113        TextIO.output (toParent, goalstring^"\n");
 
   119 	Posix.Process.sleep(Time.fromSeconds 1);
 
   114        TextIO.flushOut toParent;
 
   120 	true)
 
   115        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
 
       
   116        (* Attempt to prevent several signals from turning up simultaneously *)
 
       
   117        Posix.Process.sleep(Time.fromSeconds 1);
 
       
   118        true)
 
       
   119      else if (thisLine = "% Proof not found. Time limit expired.\n")
 
       
   120      then
 
       
   121       (File.write (File.tmp_path (Path.basic "vampire_response")) thisLine;
 
       
   122        TextIO.output (toParent,childCmd^"\n" );
 
       
   123        TextIO.flushOut toParent;
 
       
   124        TextIO.output (vamp_proof_file, thisLine);
 
       
   125        TextIO.closeOut vamp_proof_file;
 
       
   126 
       
   127        TextIO.output (toParent, thisLine^"\n");
 
       
   128        TextIO.output (toParent, thmstring^"\n");
 
       
   129        TextIO.output (toParent, goalstring^"\n");
 
       
   130        TextIO.flushOut toParent;
 
       
   131        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
 
       
   132        (* Attempt to prevent several signals from turning up simultaneously *)
 
       
   133        Posix.Process.sleep(Time.fromSeconds 1);
 
       
   134        true)
 
       
   135      else
 
   121      else
 
   136        (TextIO.output (vamp_proof_file, thisLine);
 
   122        (TextIO.output (proof_file, thisLine);
 
   137 	TextIO.flushOut vamp_proof_file;
 
   123 	TextIO.flushOut proof_file;
 
   138 	checkVampProofFound  (fromChild, toParent, ppid, thmstring,
 
   124 	checkVampProofFound  (fromChild, toParent, ppid, thmstring,
 
   139 	   goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses))
 
   125 	   goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses))
 
   140   end
 
   126   end
 
   141 
   127 
   142 
   128 
       
   129 fun checkEProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd,
 
       
   130                       thm, sg_num, clause_arr, num_of_clauses) = 
       
   131  let val E_proof_file = TextIO.openAppend
 
       
   132 	   (File.platform_path(File.tmp_path (Path.basic "eprover_proof")))
 
       
   133      val _ = File.write (File.tmp_path (Path.basic "eprover_checking_prf"))
 
       
   134 			("checking if proof found, thm is: " ^ string_of_thm thm)
 
       
   135      val thisLine = TextIO.inputLine fromChild  
       
   136  in   
       
   137      if thisLine = "" 
       
   138      then (TextIO.output (E_proof_file, ("No proof output seen \n"));
 
       
   139 	    TextIO.closeOut E_proof_file;
 
       
   140 	    false)
 
       
   141      else if thisLine = "# TSTP exit status: Unsatisfiable\n"
 
       
   142      then      
       
   143        (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
 
       
   144        startTransfer (Recon_Parse.start_E, Recon_Parse.end_E)
 
       
   145              (fromChild, toParent, ppid, thmstring, goalstring,
 
       
   146 	      childCmd, thm, sg_num, clause_arr, num_of_clauses))
 
       
   147      else if thisLine= "# Problem is satisfiable (or invalid), generating saturation derivation\n"
 
       
   148      then  
       
   149        (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
 
       
   150 	TextIO.output (toParent,childCmd^"\n" );
 
       
   151 	TextIO.flushOut toParent;
 
       
   152 	TextIO.output (E_proof_file, thisLine);
 
       
   153 	TextIO.closeOut E_proof_file;
 
       
   154 
       
   155 	TextIO.output (toParent, thisLine^"\n");
 
       
   156 	TextIO.output (toParent, thmstring^"\n");
 
       
   157 	TextIO.output (toParent, goalstring^"\n");
 
       
   158 	TextIO.flushOut toParent;
 
       
   159 	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
 
       
   160 	(* Attempt to prevent several signals from turning up simultaneously *)
 
       
   161 	Posix.Process.sleep(Time.fromSeconds 1);
 
       
   162 	 true)
 
       
   163      else if thisLine = "# Failure: Resource limit exceeded (time)\n" 
       
   164      then  
       
   165        (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
 
       
   166 	TextIO.output (toParent, thisLine^"\n");
 
       
   167 	TextIO.output (toParent, thmstring^"\n");
 
       
   168 	TextIO.output (toParent, goalstring^"\n");
 
       
   169 	TextIO.flushOut toParent;
 
       
   170 	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
 
       
   171 	TextIO.output (E_proof_file, "signalled parent\n");
 
       
   172 	TextIO.closeOut E_proof_file;
 
       
   173 	(* Attempt to prevent several signals from turning up simultaneously *)
 
       
   174 	Posix.Process.sleep(Time.fromSeconds 1);
 
       
   175 	true)
 
       
   176      else if thisLine = "# Failure: Resource limit exceeded (memory)\n"
 
       
   177      then
 
       
   178 	(Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
 
       
   179 	 TextIO.output (toParent,childCmd^"\n" );
 
       
   180 	 TextIO.flushOut toParent;
 
       
   181 	 TextIO.output (toParent, thisLine);
 
       
   182 	 TextIO.flushOut toParent;
 
       
   183 	 true)
 
       
   184      else
 
       
   185 	(TextIO.output (E_proof_file, thisLine);
 
       
   186 	TextIO.flushOut E_proof_file;
 
       
   187 	checkEProofFound  (fromChild, toParent, ppid, thmstring,goalstring,
 
       
   188 	childCmd, thm, sg_num, clause_arr, num_of_clauses))
 
       
   189  end
 
       
   190 
       
   191 
   143 (***********************************************************************)
 
   192 (***********************************************************************)
 
   144 (*  Function used by the Isabelle process to read in a Vampire proof   *)
 
   193 (*  Function used by the Isabelle process to read in a Vampire proof   *)
 
   145 (***********************************************************************)
 
   194 (***********************************************************************)
 
   146 
   195 
   147 fun getVampInput instr =
 
   196 fun getVampInput instr =
 
   148     let val thisLine = TextIO.inputLine instr
 
   197     let val thisLine = TextIO.inputLine instr
 
   149 	val _ = File.write (File.tmp_path (Path.basic "vampire_line")) thisLine
 
   198 	val _ = File.write (File.tmp_path (Path.basic "atp_line")) thisLine
 
   150     in    (* reconstructed proof string *)
 
   199     in    (* reconstructed proof string *)
 
   151       if thisLine = "" then ("No output from reconstruction process.\n","","")
 
   200       if thisLine = "" then ("No output from reconstruction process.\n","","")
 
   152       else if String.sub (thisLine, 0) = #"[" orelse
 
   201       else if String.sub (thisLine, 0) = #"[" orelse
 
   153               thisLine = "% Unprovable.\n" orelse
 
   202               thisLine = "% Unprovable.\n" orelse
 
   154               thisLine ="% Proof not found. Time limit expired.\n" orelse
 
   203               thisLine ="% Proof not found. Time limit expired.\n" orelse
 
   164 	     val _ = debug "getVampInput: translation of proof failed"
 
   213 	     val _ = debug "getVampInput: translation of proof failed"
 
   165 	 in (thisLine, thmstring, goalstring) end
 
   214 	 in (thisLine, thmstring, goalstring) end
 
   166       else getVampInput instr
 
   215       else getVampInput instr
 
   167     end
 
   216     end
 
   168 
   217 
       
   218 
       
   219 (*FIXME!!: The following code is a mess. It mostly refers to SPASS-specific things*)
 
       
   220 
       
   221 (***********************************************************************)
 
       
   222 (*  Function used by the Isabelle process to read in an E proof   *)
 
       
   223 (***********************************************************************)
 
       
   224 
       
   225 fun getEInput instr = 
       
   226     let val thisLine = TextIO.inputLine instr 
       
   227         val _ = File.write (File.tmp_path (Path.basic "eprover_line")) thisLine
 
       
   228     in 
       
   229       if thisLine = "" then ("No output from reconstruction process.\n","","")
 
       
   230       else if String.sub (thisLine, 0) = #"["
 
       
   231       then 
       
   232 	let val reconstr = thisLine
 
       
   233 	    val thmstring = TextIO.inputLine instr 
       
   234 	    val goalstring = TextIO.inputLine instr   
       
   235 	in
 
       
   236 	    (reconstr, thmstring, goalstring)
 
       
   237 	end
 
       
   238       else if String.isPrefix "SPASS beiseite:" thisLine (*FIXME: wrong!!*)
 
       
   239       then 
       
   240 	 let val reconstr = thisLine
 
       
   241 	     val thmstring = TextIO.inputLine instr
 
       
   242 	     val goalstring = TextIO.inputLine instr
 
       
   243 	 in
 
       
   244 	     (reconstr, thmstring, goalstring)
 
       
   245 	 end
 
       
   246 
       
   247        else if String.isPrefix "# No proof" thisLine 
       
   248       then 
       
   249 	 let val reconstr = thisLine
 
       
   250 	     val thmstring = TextIO.inputLine instr
 
       
   251 	     val goalstring = TextIO.inputLine instr
 
       
   252 	 in
 
       
   253 	     (reconstr, thmstring, goalstring)
 
       
   254 	 end
 
       
   255 
       
   256        else if String.isPrefix "# Failure" thisLine 
       
   257       then 
       
   258 	 let val reconstr = thisLine
 
       
   259 	     val thmstring = TextIO.inputLine instr
 
       
   260 	     val goalstring = TextIO.inputLine instr
 
       
   261 	 in
 
       
   262 	     (reconstr, thmstring, goalstring)
 
       
   263 	 end
 
       
   264       else if String.isPrefix  "Rules from"  thisLine
 
       
   265       then 
       
   266 	   let val reconstr = thisLine
 
       
   267 	       val thmstring = TextIO.inputLine instr
 
       
   268 	       val goalstring = TextIO.inputLine instr
 
       
   269 	   in
 
       
   270 	       (reconstr, thmstring, goalstring)
 
       
   271 	   end
 
       
   272       else if substring (thisLine, 0,5) = "Proof"
 
       
   273       then
 
       
   274 	let val reconstr = thisLine
 
       
   275 	    val thmstring = TextIO.inputLine instr
 
       
   276 	    val goalstring = TextIO.inputLine instr
 
       
   277 	in
 
       
   278           File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine;
 
       
   279           (reconstr, thmstring, goalstring)
 
       
   280         end
 
       
   281       else if substring (thisLine, 0,1) = "%"
 
       
   282       then
 
       
   283 	let val reconstr = thisLine
 
       
   284 	    val thmstring = TextIO.inputLine instr
 
       
   285 	    val goalstring = TextIO.inputLine instr
 
       
   286 	in
 
       
   287            File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine;
 
       
   288 	   (reconstr, thmstring, goalstring)
 
       
   289 	end
 
       
   290       else getEInput instr
 
       
   291      end
 
       
   292 
   169 end;
 
   293 end;
isabelle