src/HOL/Tools/ATP/AtpCommunication.ML
author paulson
Mon Oct 10 15:35:29 2005 +0200 (2005-10-10)
changeset 17819 1241e5d31d5b
parent 17773 a7258e1020b7
child 18700 f04a8755d6ca
permissions -rw-r--r--
small tidy-up of utility functions
paulson@17484
     1
(*  Title:      VampCommunication.ml
paulson@17484
     2
    ID:         $Id$
paulson@17484
     3
    Author:     Claire Quigley
paulson@17484
     4
    Copyright   2004  University of Cambridge
paulson@17484
     5
*)
paulson@17484
     6
paulson@17484
     7
(***************************************************************************)
paulson@17484
     8
(*  Code to deal with the transfer of proofs from a Vampire process          *)
paulson@17484
     9
(***************************************************************************)
paulson@17484
    10
signature ATP_COMMUNICATION =
paulson@17484
    11
  sig
paulson@17484
    12
    val reconstruct : bool ref
paulson@17484
    13
    val checkEProofFound: 
paulson@17484
    14
          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
paulson@17772
    15
          string * (ResClause.clause * thm) Array.array -> bool
paulson@17484
    16
    val checkVampProofFound: 
paulson@17484
    17
          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
paulson@17772
    18
          string * (ResClause.clause * thm) Array.array -> bool
paulson@17484
    19
    val checkSpassProofFound:  
paulson@17484
    20
          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
paulson@17772
    21
          string * thm * int * (ResClause.clause * thm) Array.array -> bool
paulson@17773
    22
    val signal_parent:  
paulson@17773
    23
          TextIO.outstream * Posix.Process.pid * string * string -> unit
paulson@17484
    24
  end;
paulson@17484
    25
paulson@17484
    26
structure AtpCommunication : ATP_COMMUNICATION =
paulson@17484
    27
struct
paulson@17484
    28
paulson@17484
    29
(* switch for whether to reconstruct a proof found, or just list the lemmas used *)
paulson@17484
    30
val reconstruct = ref false;
paulson@17484
    31
paulson@17718
    32
val trace_path = Path.basic "atp_trace";
paulson@17718
    33
paulson@17718
    34
fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s 
paulson@17718
    35
              else ();
paulson@17718
    36
paulson@17484
    37
exception EOF;
paulson@17484
    38
paulson@17484
    39
val start_E = "# Proof object starts here."
paulson@17484
    40
val end_E   = "# Proof object ends here."
paulson@17484
    41
val start_V6 = "%================== Proof: ======================"
paulson@17484
    42
val end_V6   = "%==============  End of proof. =================="
paulson@17484
    43
val start_V8 = "=========== Refutation =========="
paulson@17484
    44
val end_V8 = "======= End of refutation ======="
paulson@17484
    45
paulson@17484
    46
(*Identifies the start/end lines of an ATP's output*)
paulson@17484
    47
local open Recon_Parse in
paulson@17484
    48
fun extract_proof s =
paulson@17484
    49
  if cut_exists "Here is a proof with" s then
paulson@17484
    50
    (kill_lines 0
paulson@17484
    51
     o snd o cut_after ":"
paulson@17484
    52
     o snd o cut_after "Here is a proof with"
paulson@17484
    53
     o fst o cut_after " ||  -> .") s
paulson@17569
    54
  else if cut_exists end_V8 s then
paulson@17484
    55
    (kill_lines 0    (*Vampire 8.0*)
paulson@17484
    56
     o fst o cut_before end_V8) s
paulson@17484
    57
  else if cut_exists end_E s then
paulson@17484
    58
    (kill_lines 0    (*eproof*)
paulson@17484
    59
     o fst o cut_before end_E) s
paulson@17484
    60
  else "??extract_proof failed" (*Couldn't find a proof*)
paulson@17484
    61
end;
paulson@17484
    62
paulson@17484
    63
paulson@17484
    64
(*********************************************************************************)
paulson@17484
    65
(*  Inspect the output of an ATP process to see if it has found a proof,     *)
paulson@17484
    66
(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
paulson@17484
    67
(*********************************************************************************)
paulson@17484
    68
paulson@17772
    69
fun startTransfer (endS, fromChild, toParent, ppid, probfile, clause_arr) =
paulson@17569
    70
 let fun transferInput currentString =
paulson@17484
    71
      let val thisLine = TextIO.inputLine fromChild
paulson@17484
    72
      in
paulson@17484
    73
	if thisLine = "" (*end of file?*)
paulson@17718
    74
	then (trace ("\n extraction_failed.  End bracket: " ^ endS ^
paulson@17718
    75
	             "\naccumulated text: " ^ currentString);
paulson@17484
    76
	      raise EOF)                    
paulson@17484
    77
	else if String.isPrefix endS thisLine
paulson@17484
    78
	then let val proofextract = extract_proof (currentString^thisLine)
paulson@17718
    79
	         val lemma_list = if endS = end_V8 
paulson@17718
    80
			  	  then Recon_Transfer.vamp_lemma_list
paulson@17718
    81
			  	  else Recon_Transfer.e_lemma_list
paulson@17484
    82
	     in
paulson@17772
    83
	       trace ("\nExtracted proof:\n" ^ proofextract); 
paulson@17772
    84
	       lemma_list proofextract probfile toParent ppid clause_arr
paulson@17484
    85
	     end
paulson@17484
    86
	else transferInput (currentString^thisLine)
paulson@17484
    87
      end
paulson@17484
    88
 in
paulson@17569
    89
     transferInput "";  true
paulson@17569
    90
 end handle EOF => false
paulson@17569
    91
paulson@17772
    92
paulson@17772
    93
(*The signal handler in watcher.ML must be able to read the output of this.*)
paulson@17772
    94
fun signal_parent (toParent, ppid, msg, probfile) =
paulson@17569
    95
 (TextIO.output (toParent, msg);
paulson@17772
    96
  TextIO.output (toParent, probfile ^ "\n");
paulson@17569
    97
  TextIO.flushOut toParent;
paulson@17772
    98
  trace ("\nSignalled parent: " ^ msg ^ probfile);
paulson@17773
    99
  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
paulson@17773
   100
  (*Give the parent time to respond before possibly sending another signal*)
paulson@17773
   101
  OS.Process.sleep (Time.fromMilliseconds 600));
paulson@17484
   102
paulson@17484
   103
(*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
paulson@17772
   104
fun checkVampProofFound (fromChild, toParent, ppid, probfile, clause_arr) =
paulson@17569
   105
 let val thisLine = TextIO.inputLine fromChild
paulson@17484
   106
 in   
paulson@17718
   107
     trace thisLine;
paulson@17484
   108
     if thisLine = "" 
paulson@17772
   109
     then (trace "\nNo proof output seen"; false)
paulson@17569
   110
     else if String.isPrefix start_V8 thisLine
paulson@17772
   111
     then startTransfer (end_V8, fromChild, toParent, ppid, probfile, clause_arr)
paulson@17484
   112
     else if (String.isPrefix "Satisfiability detected" thisLine) orelse
paulson@17484
   113
             (String.isPrefix "Refutation not found" thisLine)
paulson@17772
   114
     then (signal_parent (toParent, ppid, "Failure\n", probfile);
paulson@17690
   115
	   true)
paulson@17484
   116
     else
paulson@17772
   117
        checkVampProofFound  (fromChild, toParent, ppid, probfile, clause_arr)
paulson@17484
   118
  end
paulson@17484
   119
paulson@17484
   120
paulson@17484
   121
(*Called from watcher. Returns true if the E process has returned a verdict.*)
paulson@17772
   122
fun checkEProofFound (fromChild, toParent, ppid, probfile, clause_arr) = 
paulson@17569
   123
 let val thisLine = TextIO.inputLine fromChild  
paulson@17484
   124
 in   
paulson@17718
   125
     trace thisLine;
paulson@17484
   126
     if thisLine = "" 
paulson@17773
   127
     then (trace "\nNo proof output seen"; false)
paulson@17569
   128
     else if String.isPrefix start_E thisLine
paulson@17484
   129
     then      
paulson@17772
   130
       startTransfer (end_E, fromChild, toParent, ppid, probfile, clause_arr)
paulson@17484
   131
     else if String.isPrefix "# Problem is satisfiable" thisLine
paulson@17772
   132
     then (signal_parent (toParent, ppid, "Invalid\n", probfile);
paulson@17690
   133
	   true)
paulson@17690
   134
     else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine
paulson@17772
   135
     then (signal_parent (toParent, ppid, "Failure\n", probfile);
paulson@17690
   136
	   true)
paulson@17484
   137
     else
paulson@17772
   138
	checkEProofFound (fromChild, toParent, ppid, probfile, clause_arr)
paulson@17484
   139
 end
paulson@17484
   140
paulson@17484
   141
paulson@17484
   142
(**********************************************************************)
paulson@17484
   143
(*  Reconstruct the Spass proof w.r.t. thmstring (string version of   *)
paulson@17484
   144
(*  Isabelle goal to be proved), then transfer the reconstruction     *)
paulson@17484
   145
(*  steps as a string to the input pipe of the main Isabelle process  *)
paulson@17484
   146
(**********************************************************************)
paulson@17484
   147
paulson@17772
   148
fun spass_reconstruct_tac proofextract toParent ppid probfile sg_num clause_arr = 
paulson@17488
   149
 SELECT_GOAL
paulson@17525
   150
  (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac, 
paulson@17488
   151
	   METAHYPS(fn negs => 
paulson@17772
   152
		  Recon_Transfer.spass_reconstruct proofextract probfile 
paulson@17772
   153
				toParent ppid negs clause_arr)]) sg_num;
paulson@17484
   154
paulson@17484
   155
paulson@17772
   156
fun transferSpassInput (fromChild, toParent, ppid, probfile,
paulson@17484
   157
                        currentString, thm, sg_num, clause_arr) = 
paulson@17484
   158
 let val thisLine = TextIO.inputLine fromChild 
paulson@17484
   159
 in 
paulson@17772
   160
    trace thisLine;
paulson@17484
   161
    if thisLine = "" (*end of file?*)
paulson@17718
   162
    then (trace ("\nspass_extraction_failed: " ^ currentString);
paulson@17484
   163
	  raise EOF)                    
paulson@17488
   164
    else if String.isPrefix "--------------------------SPASS-STOP" thisLine
paulson@17484
   165
    then 
paulson@17484
   166
      let val proofextract = extract_proof (currentString^thisLine)
paulson@17484
   167
      in 
paulson@17718
   168
	 trace ("\nextracted spass proof: " ^ proofextract);
paulson@17488
   169
	 if !reconstruct 
paulson@17772
   170
	 then (spass_reconstruct_tac proofextract toParent ppid probfile sg_num 
paulson@17488
   171
		clause_arr thm; ())
paulson@17772
   172
	 else Recon_Transfer.spass_lemma_list proofextract probfile toParent
paulson@17772
   173
	        ppid clause_arr 
paulson@17484
   174
      end
paulson@17772
   175
    else transferSpassInput (fromChild, toParent, ppid, probfile,
paulson@17484
   176
			     (currentString^thisLine), thm, sg_num, clause_arr)
paulson@17484
   177
 end;
paulson@17484
   178
paulson@17484
   179
paulson@17484
   180
(*********************************************************************************)
paulson@17484
   181
(*  Inspect the output of a Spass   process to see if it has found a proof,     *)
paulson@17484
   182
(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
paulson@17484
   183
(*********************************************************************************)
paulson@17484
   184
paulson@17484
   185
 
paulson@17772
   186
fun startSpassTransfer (fromChild, toParent, ppid, probfile,
paulson@17484
   187
                        thm, sg_num,clause_arr) = 
paulson@17484
   188
   let val thisLine = TextIO.inputLine fromChild  
paulson@17484
   189
   in                 
paulson@17484
   190
      if thisLine = "" then false
paulson@17484
   191
      else if String.isPrefix "Here is a proof" thisLine then     
paulson@17772
   192
	 (trace ("\nabout to transfer SPASS proof\n:");
paulson@17772
   193
	  transferSpassInput (fromChild, toParent, ppid, probfile, thisLine, 
paulson@17484
   194
 	                     thm, sg_num,clause_arr);
paulson@17484
   195
	  true) handle EOF => false
paulson@17772
   196
      else startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,clause_arr)
paulson@17484
   197
    end
paulson@17484
   198
paulson@17484
   199
paulson@17718
   200
(*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
paulson@17772
   201
fun checkSpassProofFound (fromChild, toParent, ppid, probfile,
paulson@17484
   202
                          thm, sg_num, clause_arr) = 
paulson@17718
   203
 let val thisLine = TextIO.inputLine fromChild  
paulson@17484
   204
 in    
paulson@17718
   205
     trace thisLine;
paulson@17773
   206
     if thisLine = "" then (trace "\nNo proof output seen"; false)
paulson@17484
   207
     else if thisLine = "SPASS beiseite: Proof found.\n"
paulson@17484
   208
     then      
paulson@17772
   209
        startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, clause_arr)
paulson@17484
   210
     else if thisLine = "SPASS beiseite: Completion found.\n"
paulson@17772
   211
     then (signal_parent (toParent, ppid, "Invalid\n", probfile);
paulson@17718
   212
	   true)
paulson@17484
   213
     else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
paulson@17484
   214
             thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
paulson@17772
   215
     then (signal_parent (toParent, ppid, "Failure\n", probfile);
paulson@17718
   216
	   true)
paulson@17772
   217
    else checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, clause_arr)
paulson@17484
   218
 end
paulson@17484
   219
paulson@17484
   220
end;