improved proof parsing
authorpaulson
Wed Sep 21 18:35:31 2005 +0200 (2005-09-21)
changeset 17569c1143a96f6d7
parent 17568 e93f7510e1e1
child 17570 92958a0b834c
improved proof parsing
src/HOL/Tools/ATP/AtpCommunication.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
     1.1 --- a/src/HOL/Tools/ATP/AtpCommunication.ML	Wed Sep 21 18:35:19 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML	Wed Sep 21 18:35:31 2005 +0200
     1.3 @@ -44,13 +44,11 @@
     1.4       o snd o cut_after ":"
     1.5       o snd o cut_after "Here is a proof with"
     1.6       o fst o cut_after " ||  -> .") s
     1.7 -  else if cut_exists start_V8 s then
     1.8 +  else if cut_exists end_V8 s then
     1.9      (kill_lines 0    (*Vampire 8.0*)
    1.10 -     o snd o cut_after start_V8
    1.11       o fst o cut_before end_V8) s
    1.12    else if cut_exists end_E s then
    1.13      (kill_lines 0    (*eproof*)
    1.14 -     o snd o cut_after start_E
    1.15       o fst o cut_before end_E) s
    1.16    else "??extract_proof failed" (*Couldn't find a proof*)
    1.17  end;
    1.18 @@ -61,124 +59,82 @@
    1.19  (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    1.20  (*********************************************************************************)
    1.21  
    1.22 -fun startTransfer (startS,endS)
    1.23 -      (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) =
    1.24 - let val thisLine = TextIO.inputLine fromChild
    1.25 -     fun transferInput currentString =
    1.26 +fun startTransfer (endS, fromChild, toParent, ppid, goalstring, childCmd, clause_arr) =
    1.27 + let fun transferInput currentString =
    1.28        let val thisLine = TextIO.inputLine fromChild
    1.29        in
    1.30  	if thisLine = "" (*end of file?*)
    1.31  	then (File.write (File.tmp_path (Path.basic"extraction_failed")) 
    1.32 -	                 ("start bracket: " ^ startS ^
    1.33 -	                  "\nend bracket: " ^ endS ^
    1.34 +	                 ("end bracket: " ^ endS ^
    1.35  	                  "\naccumulated text: " ^ currentString);
    1.36  	      raise EOF)                    
    1.37  	else if String.isPrefix endS thisLine
    1.38  	then let val proofextract = extract_proof (currentString^thisLine)
    1.39  	     in
    1.40  	       File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; 
    1.41 -	       Recon_Transfer.prover_lemma_list proofextract goalstring toParent ppid clause_arr
    1.42 +	       (if endS = end_V8 (*vampire?*)
    1.43 +		then Recon_Transfer.vamp_lemma_list
    1.44 +		else Recon_Transfer.e_lemma_list)
    1.45 +	           proofextract goalstring toParent ppid clause_arr
    1.46  	     end
    1.47  	else transferInput (currentString^thisLine)
    1.48        end
    1.49   in
    1.50 -   if thisLine = "" then false
    1.51 -   else if String.isPrefix startS thisLine
    1.52 -   then
    1.53 -    (File.append (File.tmp_path (Path.basic "transfer_start"))
    1.54 -		 ("about to transfer proof, first line is: " ^ thisLine);
    1.55 -     transferInput thisLine;
    1.56 -     true) handle EOF => false
    1.57 -   else
    1.58 -      startTransfer (startS,endS)
    1.59 -                    (fromChild, toParent, ppid, goalstring,
    1.60 -		     childCmd, clause_arr)
    1.61 - end
    1.62 +     transferInput "";  true
    1.63 + end handle EOF => false
    1.64 +
    1.65 +fun signal_parent (toParent, ppid, msg, goalstring) =
    1.66 + (TextIO.output (toParent, msg);
    1.67 +  TextIO.output (toParent, goalstring^"\n");
    1.68 +  TextIO.flushOut toParent;
    1.69 +  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.70 +  (*Space apart signals arising from multiple subgoals*)
    1.71 +  Posix.Process.sleep(Time.fromMilliseconds 200));
    1.72  
    1.73  (*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
    1.74  fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) =
    1.75 - let val proof_file = TextIO.openAppend
    1.76 -	   (File.platform_path(File.tmp_path (Path.basic "vampire_proof")))
    1.77 -     val _ = File.write (File.tmp_path (Path.basic "vampire_checking_prf"))
    1.78 -			("checking if proof found. childCmd is " ^ childCmd ^
    1.79 -			 "\ngoalstring is: " ^ goalstring)
    1.80 -     val thisLine = TextIO.inputLine fromChild
    1.81 + let val thisLine = TextIO.inputLine fromChild
    1.82   in   
    1.83 -     File.write (File.tmp_path (Path.basic "vampire_response")) thisLine;
    1.84 +     File.append (File.tmp_path (Path.basic "proof")) thisLine;
    1.85       if thisLine = "" 
    1.86 -     then (TextIO.output (proof_file, "No proof output seen \n");
    1.87 -	   TextIO.closeOut proof_file;
    1.88 +     then (File.append (File.tmp_path (Path.basic "proof"))
    1.89 +                      "No proof output seen \n";
    1.90  	   false)
    1.91 -     else if String.isPrefix "Refutation found. Thanks to Tanya" thisLine
    1.92 +     else if String.isPrefix start_V8 thisLine
    1.93       then
    1.94 -       startTransfer (start_V8, end_V8)
    1.95 -	      (fromChild, toParent, ppid, goalstring,
    1.96 -	       childCmd, clause_arr)
    1.97 +       startTransfer (end_V8, fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
    1.98       else if (String.isPrefix "Satisfiability detected" thisLine) orelse
    1.99               (String.isPrefix "Refutation not found" thisLine)
   1.100       then
   1.101 -       (TextIO.output (toParent, "Failure\n");
   1.102 -	TextIO.output (toParent, goalstring^"\n");
   1.103 -	TextIO.flushOut toParent;
   1.104 -	TextIO.output (proof_file, thisLine);
   1.105 -	TextIO.closeOut proof_file;
   1.106 -	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.107 -	(* Attempt to prevent several signals from turning up simultaneously *)
   1.108 -	Posix.Process.sleep(Time.fromSeconds 1);
   1.109 +       (signal_parent (toParent, ppid, "Failure\n", goalstring);
   1.110  	true)
   1.111       else
   1.112 -       (TextIO.output (proof_file, thisLine);
   1.113 -	TextIO.flushOut proof_file;
   1.114 -	checkVampProofFound  (fromChild, toParent, ppid, 
   1.115 -	   goalstring,childCmd, clause_arr))
   1.116 +        checkVampProofFound  (fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
   1.117    end
   1.118  
   1.119  
   1.120  (*Called from watcher. Returns true if the E process has returned a verdict.*)
   1.121  fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd, clause_arr) = 
   1.122 - let val E_proof_file = TextIO.openAppend
   1.123 -	   (File.platform_path(File.tmp_path (Path.basic "e_proof")))
   1.124 -     val _ = File.write (File.tmp_path (Path.basic "e_checking_prf"))
   1.125 -			("checking if proof found. childCmd is " ^ childCmd ^
   1.126 -			 "\ngoalstring is: " ^ goalstring)
   1.127 -     val thisLine = TextIO.inputLine fromChild  
   1.128 + let val thisLine = TextIO.inputLine fromChild  
   1.129   in   
   1.130 -     File.write (File.tmp_path (Path.basic "e_response")) thisLine;
   1.131 +     File.append (File.tmp_path (Path.basic "proof")) thisLine;
   1.132       if thisLine = "" 
   1.133 -     then (TextIO.output (E_proof_file, "No proof output seen \n");
   1.134 -	    TextIO.closeOut E_proof_file;
   1.135 -	    false)
   1.136 -     else if thisLine = "# TSTP exit status: Unsatisfiable\n"
   1.137 +     then (File.append (File.tmp_path (Path.basic "proof"))
   1.138 +                      "No proof output seen \n";
   1.139 +	   false)
   1.140 +     else if String.isPrefix start_E thisLine
   1.141       then      
   1.142 -       startTransfer (start_E, end_E)
   1.143 -             (fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
   1.144 +       startTransfer (end_E, fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
   1.145       else if String.isPrefix "# Problem is satisfiable" thisLine
   1.146       then  
   1.147 -       (TextIO.output (toParent, "Invalid\n");
   1.148 -	TextIO.output (toParent, goalstring^"\n");
   1.149 -	TextIO.flushOut toParent;
   1.150 -	TextIO.output (E_proof_file, thisLine);
   1.151 -	TextIO.closeOut E_proof_file;
   1.152 -	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.153 -	(* Attempt to prevent several signals from turning up simultaneously *)
   1.154 -	Posix.Process.sleep(Time.fromSeconds 1);
   1.155 +       (signal_parent (toParent, ppid, "Invalid\n", goalstring);
   1.156  	true)
   1.157       else if String.isPrefix "# Failure: Resource limit exceeded" thisLine
   1.158       then  (*In fact, E distingishes "out of time" and "out of memory"*)
   1.159 -       (File.write (File.tmp_path (Path.basic "e_response")) thisLine;
   1.160 -	TextIO.output (toParent, "Failure\n");
   1.161 -	TextIO.output (toParent, goalstring^"\n");
   1.162 -	TextIO.flushOut toParent;
   1.163 -	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.164 -	TextIO.output (E_proof_file, "signalled parent\n");
   1.165 -	TextIO.closeOut E_proof_file;
   1.166 -	(* Attempt to prevent several signals from turning up simultaneously *)
   1.167 -	Posix.Process.sleep(Time.fromSeconds 1);
   1.168 +       (signal_parent (toParent, ppid, "Failure\n", goalstring);
   1.169  	true)
   1.170       else
   1.171 -	(TextIO.output (E_proof_file, thisLine);
   1.172 -	TextIO.flushOut E_proof_file;
   1.173 -	checkEProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr))
   1.174 +	checkEProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
   1.175   end
   1.176  
   1.177  
   1.178 @@ -207,7 +163,7 @@
   1.179      then 
   1.180        let val proofextract = extract_proof (currentString^thisLine)
   1.181        in 
   1.182 -	 File.write (File.tmp_path (Path.basic"spass_extracted_prf")) proofextract;
   1.183 +	 File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract;
   1.184  	 if !reconstruct 
   1.185  	 then (spass_reconstruct_tac proofextract goalstring toParent ppid sg_num 
   1.186  		clause_arr thm; ())
   1.187 @@ -246,8 +202,6 @@
   1.188                            thm, sg_num, clause_arr) = 
   1.189   let val spass_proof_file = TextIO.openAppend
   1.190             (File.platform_path(File.tmp_path (Path.basic "spass_proof")))
   1.191 -     val _ = File.write(File.tmp_path (Path.basic "spass_checking_prf"))
   1.192 -		("checking if proof found, thm is: "^(string_of_thm thm))
   1.193       val thisLine = TextIO.inputLine fromChild  
   1.194   in    
   1.195       File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
   1.196 @@ -263,24 +217,14 @@
   1.197       then  
   1.198         (TextIO.output (spass_proof_file, thisLine);
   1.199  	TextIO.closeOut spass_proof_file;
   1.200 -	TextIO.output (toParent, "Invalid\n");
   1.201 -	TextIO.output (toParent, goalstring^"\n");
   1.202 -	TextIO.flushOut toParent;
   1.203 -	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.204 -	(* Attempt to prevent several signals from turning up simultaneously *)
   1.205 -	Posix.Process.sleep(Time.fromSeconds 1);
   1.206 +	signal_parent (toParent, ppid, "Invalid\n", goalstring);
   1.207  	true)
   1.208       else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
   1.209               thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
   1.210       then  
   1.211 -       (TextIO.output (toParent, "Failure\n");
   1.212 -	TextIO.output (toParent, goalstring^"\n");
   1.213 -	TextIO.flushOut toParent;
   1.214 -	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.215 +       (signal_parent (toParent, ppid, "Failure\n", goalstring);
   1.216  	TextIO.output (spass_proof_file, "signalled parent\n");
   1.217  	TextIO.closeOut spass_proof_file;
   1.218 -	(* Attempt to prevent several signals from turning up simultaneously *)
   1.219 -	Posix.Process.sleep(Time.fromSeconds 1);
   1.220  	true)
   1.221      else
   1.222         (TextIO.output (spass_proof_file, thisLine);
     2.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Sep 21 18:35:19 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Sep 21 18:35:31 2005 +0200
     2.3 @@ -189,7 +189,7 @@
     2.4      get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) clause_arr
     2.5    end;
     2.6      
     2.7 - (*String contains multiple lines, terminated with newline characters.
     2.8 + (*String contains multiple lines.
     2.9    A list consisting of the first number in each line is returned. *)
    2.10  fun get_linenums proofstr = 
    2.11    let val numerics = String.tokens (not o Char.isDigit)
    2.12 @@ -198,9 +198,22 @@
    2.13        val lines = String.tokens (fn c => c = #"\n") proofstr
    2.14    in  List.mapPartial (firstno o numerics) lines  end
    2.15  
    2.16 -fun get_axiom_names_vamp_E proofstr clause_arr  =
    2.17 +fun get_axiom_names_e proofstr clause_arr  =
    2.18     get_axiom_names (get_linenums proofstr) clause_arr;
    2.19      
    2.20 + (*String contains multiple lines. We want those of the form 
    2.21 +     "*********** [448, input] ***********".
    2.22 +  A list consisting of the first number in each line is returned. *)
    2.23 +fun get_vamp_linenums proofstr = 
    2.24 +  let val toks = String.tokens (not o Char.isAlphaNum)
    2.25 +      fun inputno [n,"input"] = Int.fromString n
    2.26 +        | inputno _ = NONE
    2.27 +      val lines = String.tokens (fn c => c = #"\n") proofstr
    2.28 +  in  List.mapPartial (inputno o toks) lines  end
    2.29 +
    2.30 +fun get_axiom_names_vamp proofstr clause_arr  =
    2.31 +   get_axiom_names (get_vamp_linenums proofstr) clause_arr;
    2.32 +    
    2.33  
    2.34  (***********************************************)
    2.35  (* get axioms for reconstruction               *)
    2.36 @@ -303,7 +316,9 @@
    2.37        (* Attempt to prevent several signals from turning up simultaneously *)
    2.38        Posix.Process.sleep(Time.fromSeconds 1); ());
    2.39  
    2.40 -val prover_lemma_list = prover_lemma_list_aux get_axiom_names_vamp_E;
    2.41 +val e_lemma_list = prover_lemma_list_aux get_axiom_names_e;
    2.42 +
    2.43 +val vamp_lemma_list = prover_lemma_list_aux get_axiom_names_vamp;
    2.44  
    2.45  val spass_lemma_list = prover_lemma_list_aux get_axiom_names_spass;
    2.46