first version of structured proof reconstruction
authorpaulson
Wed Jan 03 10:59:06 2007 +0100 (2007-01-03)
changeset 219777f7177a95189
parent 21976 1f608af40542
child 21978 72c21698a055
first version of structured proof reconstruction
src/HOL/ATP_Linkup.thy
src/HOL/IsaMakefile
src/HOL/Tools/ATP/AtpCommunication.ML
src/HOL/Tools/ATP/watcher.ML
     1.1 --- a/src/HOL/ATP_Linkup.thy	Tue Jan 02 22:43:05 2007 +0100
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Wed Jan 03 10:59:06 2007 +0100
     1.3 @@ -10,10 +10,10 @@
     1.4  imports Map Hilbert_Choice
     1.5  uses
     1.6    "Tools/polyhash.ML"
     1.7 -  "Tools/ATP/AtpCommunication.ML"
     1.8 +  "Tools/res_clause.ML"
     1.9 +  "Tools/res_reconstruct.ML"
    1.10    "Tools/ATP/watcher.ML"
    1.11    "Tools/ATP/reduce_axiomsN.ML"
    1.12 -  "Tools/res_clause.ML"
    1.13    ("Tools/res_hol_clause.ML")
    1.14    ("Tools/res_axioms.ML")
    1.15    ("Tools/res_atp.ML")
     2.1 --- a/src/HOL/IsaMakefile	Tue Jan 02 22:43:05 2007 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Wed Jan 03 10:59:06 2007 +0100
     2.3 @@ -96,7 +96,7 @@
     2.4    OrderedGroup.ML OrderedGroup.thy Orderings.thy Power.thy PreList.thy		\
     2.5    Product_Type.thy ROOT.ML Recdef.thy Record.thy Refute.thy Relation.thy	\
     2.6    Relation_Power.thy Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy		\
     2.7 -  Sum_Type.thy Tools/ATP/AtpCommunication.ML Tools/ATP/reduce_axiomsN.ML	\
     2.8 +  Sum_Type.thy Tools/res_reconstruct.ML Tools/ATP/reduce_axiomsN.ML	\
     2.9    Tools/ATP/watcher.ML Tools/cnf_funcs.ML Tools/datatype_abs_proofs.ML		\
    2.10    Tools/datatype_aux.ML Tools/datatype_codegen.ML				\
    2.11    Tools/datatype_hooks.ML Tools/datatype_package.ML				\
     3.1 --- a/src/HOL/Tools/ATP/AtpCommunication.ML	Tue Jan 02 22:43:05 2007 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,238 +0,0 @@
     3.4 -(*  Title:      VampCommunication.ml
     3.5 -    ID:         $Id$
     3.6 -    Author:     Claire Quigley
     3.7 -    Copyright   2004  University of Cambridge
     3.8 -*)
     3.9 -
    3.10 -(***************************************************************************)
    3.11 -(*  Code to deal with the transfer of proofs from a Vampire process          *)
    3.12 -(***************************************************************************)
    3.13 -signature ATP_COMMUNICATION =
    3.14 -  sig
    3.15 -    val checkEProofFound: 
    3.16 -          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    3.17 -          string * thm * int * string Vector.vector -> bool
    3.18 -    val checkVampProofFound: 
    3.19 -          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    3.20 -          string * thm * int * string Vector.vector -> bool
    3.21 -    val checkSpassProofFound:  
    3.22 -          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    3.23 -          string * thm * int * string Vector.vector -> bool
    3.24 -    val signal_parent:  
    3.25 -          TextIO.outstream * Posix.Process.pid * string * string -> unit
    3.26 -  end;
    3.27 -
    3.28 -structure AtpCommunication : ATP_COMMUNICATION =
    3.29 -struct
    3.30 -
    3.31 -val trace_path = Path.basic "atp_trace";
    3.32 -
    3.33 -fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s 
    3.34 -              else ();
    3.35 -
    3.36 -exception EOF;
    3.37 -
    3.38 -(**** retrieve the axioms that were used in the proof ****)
    3.39 -
    3.40 -(*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*)
    3.41 -fun get_axiom_names (thm_names: string vector) step_nums = 
    3.42 -    let fun is_axiom n = n <= Vector.length thm_names 
    3.43 -        fun index i = Vector.sub(thm_names, i-1)
    3.44 -        val axnums = List.filter is_axiom step_nums
    3.45 -        val axnames = sort_distinct string_ord (map index axnums)
    3.46 -    in
    3.47 -	if length axnums = length step_nums then "UNSOUND!!" :: axnames
    3.48 -	else axnames
    3.49 -    end
    3.50 -
    3.51 - (*String contains multiple lines. We want those of the form 
    3.52 -     "253[0:Inp] et cetera..."
    3.53 -  A list consisting of the first number in each line is returned. *)
    3.54 -fun get_spass_linenums proofstr = 
    3.55 -  let val toks = String.tokens (not o Char.isAlphaNum)
    3.56 -      fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
    3.57 -        | inputno _ = NONE
    3.58 -      val lines = String.tokens (fn c => c = #"\n") proofstr
    3.59 -  in  List.mapPartial (inputno o toks) lines  end
    3.60 -
    3.61 -fun get_axiom_names_spass proofstr thm_names =
    3.62 -   get_axiom_names thm_names (get_spass_linenums proofstr);
    3.63 -    
    3.64 -fun not_comma c = c <>  #",";
    3.65 -
    3.66 -val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c);
    3.67 -
    3.68 -
    3.69 -(*A valid TSTP axiom line has the form  cnf(NNN,axiom,...) where NNN is a positive integer.*)
    3.70 -fun parse_tstp_line s =
    3.71 -  let val ss = Substring.full (unprefix "cnf(" (nospaces s))
    3.72 -      val (intf,rest) = Substring.splitl not_comma ss
    3.73 -      val (rolef,rest) = Substring.splitl not_comma (Substring.triml 1 rest)
    3.74 -      (*We only allow negated_conjecture because the line number will be removed in
    3.75 -        get_axiom_names above, while suppressing the UNSOUND warning*)
    3.76 -      val ints = if Substring.string rolef mem_string ["axiom","negated_conjecture"]
    3.77 -                 then Substring.string intf 
    3.78 -                 else "error" 
    3.79 -  in  Int.fromString ints  end
    3.80 -  handle Fail _ => NONE; 
    3.81 -
    3.82 -fun get_axiom_names_tstp proofstr thm_names =
    3.83 -   get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofstr));
    3.84 -    
    3.85 - (*String contains multiple lines. We want those of the form 
    3.86 -     "*********** [448, input] ***********".
    3.87 -  A list consisting of the first number in each line is returned. *)
    3.88 -fun get_vamp_linenums proofstr = 
    3.89 -  let val toks = String.tokens (not o Char.isAlphaNum)
    3.90 -      fun inputno [ntok,"input"] = Int.fromString ntok
    3.91 -        | inputno _ = NONE
    3.92 -      val lines = String.tokens (fn c => c = #"\n") proofstr
    3.93 -  in  List.mapPartial (inputno o toks) lines  end
    3.94 -
    3.95 -fun get_axiom_names_vamp proofstr thm_names =
    3.96 -   get_axiom_names thm_names (get_vamp_linenums proofstr);
    3.97 -    
    3.98 -fun rules_to_string [] = "NONE"
    3.99 -  | rules_to_string xs = space_implode "  " xs
   3.100 -
   3.101 -
   3.102 -(*The signal handler in watcher.ML must be able to read the output of this.*)
   3.103 -fun prover_lemma_list_aux getax proofstr probfile toParent ppid thm_names = 
   3.104 - let val _ = trace
   3.105 -               ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
   3.106 -                "\nprobfile is " ^ probfile ^
   3.107 -                "  num of clauses is " ^ string_of_int (Vector.length thm_names))
   3.108 -     val ax_str = rules_to_string (getax proofstr thm_names)
   3.109 -    in 
   3.110 -	 trace ("\nDone. Lemma list is " ^ ax_str);
   3.111 -         TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^
   3.112 -                  ax_str ^ "\n");
   3.113 -	 TextIO.output (toParent, probfile ^ "\n");
   3.114 -	 TextIO.flushOut toParent;
   3.115 -	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
   3.116 -    end
   3.117 -    handle exn => (*FIXME: exn handler is too general!*)
   3.118 -     (trace ("\nprover_lemma_list_aux: In exception handler: " ^ 
   3.119 -             Toplevel.exn_message exn);
   3.120 -      TextIO.output (toParent, "Translation failed for the proof: " ^ 
   3.121 -                     String.toString proofstr ^ "\n");
   3.122 -      TextIO.output (toParent, probfile);
   3.123 -      TextIO.flushOut toParent;
   3.124 -      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
   3.125 -
   3.126 -val e_lemma_list = prover_lemma_list_aux get_axiom_names_tstp;
   3.127 -
   3.128 -val vamp_lemma_list = prover_lemma_list_aux get_axiom_names_vamp;
   3.129 -
   3.130 -val spass_lemma_list = prover_lemma_list_aux get_axiom_names_spass;
   3.131 -
   3.132 -
   3.133 -(**** Extracting proofs from an ATP's output ****)
   3.134 -
   3.135 -(*Return everything in s that comes before the string t*)
   3.136 -fun cut_before t s = 
   3.137 -  let val (s1,s2) = Substring.position t (Substring.full s)
   3.138 -  in  if Substring.size s2 = 0 then error "cut_before: string not found" 
   3.139 -      else Substring.string s2
   3.140 -  end;
   3.141 -
   3.142 -val start_E = "# Proof object starts here."
   3.143 -val end_E   = "# Proof object ends here."
   3.144 -val start_V6 = "%================== Proof: ======================"
   3.145 -val end_V6   = "%==============  End of proof. =================="
   3.146 -val start_V8 = "=========== Refutation =========="
   3.147 -val end_V8 = "======= End of refutation ======="
   3.148 -val end_SPASS = "Formulae used in the proof"
   3.149 -
   3.150 -(*********************************************************************************)
   3.151 -(*  Inspect the output of an ATP process to see if it has found a proof,     *)
   3.152 -(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
   3.153 -(*********************************************************************************)
   3.154 -
   3.155 -fun startTransfer (endS, fromChild, toParent, ppid, probfile, th, sgno, thm_names) =
   3.156 - let fun transferInput currentString =
   3.157 -      let val thisLine = TextIO.inputLine fromChild
   3.158 -      in
   3.159 -	if thisLine = "" (*end of file?*)
   3.160 -	then (trace ("\n extraction_failed.  End bracket: " ^ endS ^
   3.161 -	             "\naccumulated text: " ^ currentString);
   3.162 -	      raise EOF)                    
   3.163 -	else if String.isPrefix endS thisLine
   3.164 -	then let val proofextract = currentString ^ cut_before endS thisLine
   3.165 -	         val lemma_list = if endS = end_V8 then vamp_lemma_list
   3.166 -			  	  else if endS = end_SPASS then spass_lemma_list
   3.167 -			  	  else e_lemma_list
   3.168 -	     in
   3.169 -	       trace ("\nExtracted proof:\n" ^ proofextract); 
   3.170 -	       lemma_list proofextract probfile toParent ppid thm_names
   3.171 -	     end
   3.172 -	else transferInput (currentString^thisLine)
   3.173 -      end
   3.174 - in
   3.175 -     transferInput "";  true
   3.176 - end handle EOF => false
   3.177 -
   3.178 -
   3.179 -(*The signal handler in watcher.ML must be able to read the output of this.*)
   3.180 -fun signal_parent (toParent, ppid, msg, probfile) =
   3.181 - (TextIO.output (toParent, msg);
   3.182 -  TextIO.output (toParent, probfile ^ "\n");
   3.183 -  TextIO.flushOut toParent;
   3.184 -  trace ("\nSignalled parent: " ^ msg ^ probfile);
   3.185 -  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   3.186 -  (*Give the parent time to respond before possibly sending another signal*)
   3.187 -  OS.Process.sleep (Time.fromMilliseconds 600));
   3.188 -
   3.189 -(*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
   3.190 -fun checkVampProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) =
   3.191 - let val thisLine = TextIO.inputLine fromChild
   3.192 - in   
   3.193 -     trace thisLine;
   3.194 -     if thisLine = "" 
   3.195 -     then (trace "\nNo proof output seen"; false)
   3.196 -     else if String.isPrefix start_V8 thisLine
   3.197 -     then startTransfer (end_V8, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   3.198 -     else if (String.isPrefix "Satisfiability detected" thisLine) orelse
   3.199 -             (String.isPrefix "Refutation not found" thisLine)
   3.200 -     then (signal_parent (toParent, ppid, "Failure\n", probfile);
   3.201 -	   true)
   3.202 -     else checkVampProofFound  (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   3.203 -  end
   3.204 -
   3.205 -(*Called from watcher. Returns true if the E process has returned a verdict.*)
   3.206 -fun checkEProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) = 
   3.207 - let val thisLine = TextIO.inputLine fromChild  
   3.208 - in   
   3.209 -     trace thisLine;
   3.210 -     if thisLine = "" then (trace "\nNo proof output seen"; false)
   3.211 -     else if String.isPrefix start_E thisLine
   3.212 -     then startTransfer (end_E, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   3.213 -     else if String.isPrefix "# Problem is satisfiable" thisLine
   3.214 -     then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   3.215 -	   true)
   3.216 -     else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine
   3.217 -     then (signal_parent (toParent, ppid, "Failure\n", probfile);
   3.218 -	   true)
   3.219 -     else checkEProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   3.220 - end;
   3.221 -
   3.222 -(*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
   3.223 -fun checkSpassProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) = 
   3.224 - let val thisLine = TextIO.inputLine fromChild  
   3.225 - in    
   3.226 -     trace thisLine;
   3.227 -     if thisLine = "" then (trace "\nNo proof output seen"; false)
   3.228 -     else if String.isPrefix "Here is a proof" thisLine
   3.229 -     then      
   3.230 -        startTransfer (end_SPASS, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   3.231 -     else if thisLine = "SPASS beiseite: Completion found.\n"
   3.232 -     then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   3.233 -	   true)
   3.234 -     else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
   3.235 -             thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
   3.236 -     then (signal_parent (toParent, ppid, "Failure\n", probfile);
   3.237 -	   true)
   3.238 -    else checkSpassProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   3.239 - end
   3.240 -
   3.241 -end;
     4.1 --- a/src/HOL/Tools/ATP/watcher.ML	Tue Jan 02 22:43:05 2007 +0100
     4.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Wed Jan 03 10:59:06 2007 +0100
     4.3 @@ -27,6 +27,7 @@
     4.4  	TextIO.instream * TextIO.outstream * Posix.Process.pid
     4.5  val killWatcher : Posix.Process.pid -> unit
     4.6  val killChild  : ('a, 'b) Unix.proc -> OS.Process.status
     4.7 +val command_sep : char
     4.8  val setting_sep : char
     4.9  val reapAll : unit -> unit
    4.10  end
    4.11 @@ -225,11 +226,11 @@
    4.12  	     then (* check here for prover label on child*)
    4.13  	       let val _ = trace ("\nInput available from child: " ^ file)
    4.14  		   val childDone = (case prover of
    4.15 -		       "vampire" => AtpCommunication.checkVampProofFound
    4.16 +		       "vampire" => ResReconstruct.checkVampProofFound
    4.17  			    (childIn, toParentStr, ppid, file, th, sgno, thm_names)  
    4.18 -		     | "E" => AtpCommunication.checkEProofFound
    4.19 +		     | "E" => ResReconstruct.checkEProofFound
    4.20  			    (childIn, toParentStr, ppid, file, th, sgno, thm_names)             
    4.21 -		     | "spass" => AtpCommunication.checkSpassProofFound
    4.22 +		     | "spass" => ResReconstruct.checkSpassProofFound
    4.23  			    (childIn, toParentStr, ppid, file, th, sgno, thm_names)  
    4.24  		     | _ => (trace ("\nBad prover! " ^ prover); true) )
    4.25  		in
    4.26 @@ -363,7 +364,7 @@
    4.27  	    else ())
    4.28       fun proofHandler _ = 
    4.29         let val _ = trace("\nIn signal handler for pid " ^ string_of_pid childpid)
    4.30 -           val outcome = TextIO.inputLine childin
    4.31 +           val outcome = ResReconstruct.restore_newlines (TextIO.inputLine childin)
    4.32  	   val probfile = TextIO.inputLine childin
    4.33  	   val sgno = number_from_filename probfile
    4.34  	   val text = string_of_subgoal th sgno