improved SPASS support
authorpaulson
Tue Jan 17 10:26:36 2006 +0100 (2006-01-17)
changeset 18700f04a8755d6ca
parent 18699 f3bfe81b6e58
child 18701 98e6a0a011f3
improved SPASS support
src/HOL/Tools/ATP/AtpCommunication.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/AtpCommunication.ML	Mon Jan 16 21:55:17 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML	Tue Jan 17 10:26:36 2006 +0100
     1.3 @@ -46,11 +46,9 @@
     1.4  (*Identifies the start/end lines of an ATP's output*)
     1.5  local open Recon_Parse in
     1.6  fun extract_proof s =
     1.7 -  if cut_exists "Here is a proof with" s then
     1.8 +  if cut_exists "Formulae used in the proof" s then  (*SPASS*)
     1.9      (kill_lines 0
    1.10 -     o snd o cut_after ":"
    1.11 -     o snd o cut_after "Here is a proof with"
    1.12 -     o fst o cut_after " ||  -> .") s
    1.13 +     o fst o cut_before "Formulae used in the proof") s
    1.14    else if cut_exists end_V8 s then
    1.15      (kill_lines 0    (*Vampire 8.0*)
    1.16       o fst o cut_before end_V8) s
    1.17 @@ -161,7 +159,7 @@
    1.18      if thisLine = "" (*end of file?*)
    1.19      then (trace ("\nspass_extraction_failed: " ^ currentString);
    1.20  	  raise EOF)                    
    1.21 -    else if String.isPrefix "--------------------------SPASS-STOP" thisLine
    1.22 +    else if String.isPrefix "Formulae used in the proof" thisLine
    1.23      then 
    1.24        let val proofextract = extract_proof (currentString^thisLine)
    1.25        in 
    1.26 @@ -189,7 +187,7 @@
    1.27     in                 
    1.28        if thisLine = "" then false
    1.29        else if String.isPrefix "Here is a proof" thisLine then     
    1.30 -	 (trace ("\nabout to transfer SPASS proof\n:");
    1.31 +	 (trace ("\nabout to transfer SPASS proof:\n");
    1.32  	  transferSpassInput (fromChild, toParent, ppid, probfile, thisLine, 
    1.33   	                     thm, sg_num,clause_arr);
    1.34  	  true) handle EOF => false
     2.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon Jan 16 21:55:17 2006 +0100
     2.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Jan 17 10:26:36 2006 +0100
     2.3 @@ -162,15 +162,18 @@
     2.4              (map (ResClause.get_axiomName o #1) 
     2.5  	     (get_clasimp_cls clause_arr step_nums)));   
     2.6  
     2.7 -fun get_axiom_names_spass proofstr clause_arr =
     2.8 -  let (* parse spass proof into datatype *)
     2.9 -      val _ = trace ("\nStarted parsing:\n" ^ proofstr)
    2.10 -      val proof_steps = parse (#1(lex proofstr))
    2.11 -      val _ = trace "\nParsing finished!"
    2.12 -      (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
    2.13 -  in
    2.14 -    get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) clause_arr
    2.15 -  end;
    2.16 + (*String contains multiple lines. We want those of the form 
    2.17 +     "253[0:Inp] et cetera..."
    2.18 +  A list consisting of the first number in each line is returned. *)
    2.19 +fun get_spass_linenums proofstr = 
    2.20 +  let val toks = String.tokens (not o Char.isAlphaNum)
    2.21 +      fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
    2.22 +        | inputno _ = NONE
    2.23 +      val lines = String.tokens (fn c => c = #"\n") proofstr
    2.24 +  in  List.mapPartial (inputno o toks) lines  end
    2.25 +
    2.26 +fun get_axiom_names_spass proofstr clause_arr  =
    2.27 +   get_axiom_names (get_spass_linenums proofstr) clause_arr;
    2.28      
    2.29   (*String contains multiple lines.
    2.30    A list consisting of the first number in each line is returned. *)
    2.31 @@ -189,7 +192,7 @@
    2.32    A list consisting of the first number in each line is returned. *)
    2.33  fun get_vamp_linenums proofstr = 
    2.34    let val toks = String.tokens (not o Char.isAlphaNum)
    2.35 -      fun inputno [n,"input"] = Int.fromString n
    2.36 +      fun inputno [ntok,"input"] = Int.fromString ntok
    2.37          | inputno _ = NONE
    2.38        val lines = String.tokens (fn c => c = #"\n") proofstr
    2.39    in  List.mapPartial (inputno o toks) lines  end
     3.1 --- a/src/HOL/Tools/res_atp.ML	Mon Jan 16 21:55:17 2006 +0100
     3.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Jan 17 10:26:36 2006 +0100
     3.3 @@ -97,20 +97,15 @@
     3.4              (*options are separated by Watcher.setting_sep, currently #"%"*)
     3.5              if !prover = "spass"
     3.6              then
     3.7 -              let val optionline = 
     3.8 +              let val baseopts = "%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
     3.9 +              val infopts = 
    3.10  		      if !AtpCommunication.reconstruct 
    3.11 -		          (*Proof reconstruction works for only a limited set of 
    3.12 -		            inference rules*)
    3.13 -                      then space_implode "%" (!custom_spass) ^
    3.14 -                           "%-DocProof%-TimeLimit=" ^ time
    3.15 -                      else "-DocProof%-SOS%-FullRed=0%-TimeLimit=" ^ time (*Auto mode*)
    3.16 -                  val _ = Output.debug ("SPASS option string is " ^ optionline)
    3.17 -                  val _ = helper_path "SPASS_HOME" "SPASS"
    3.18 -                    (*We've checked that SPASS is there for ATP/spassshell to run.*)
    3.19 -              in 
    3.20 -                  ([("spass", 
    3.21 -                     getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
    3.22 -                     optionline, probfile)] @ 
    3.23 +		          (*Proof reconstruction needs a limited set of inf rules*)
    3.24 +                      then space_implode "%" (!custom_spass)                           
    3.25 +                      else "-Auto%-SOS=1"
    3.26 +                  val spass = helper_path "SPASS_HOME" "SPASS"
    3.27 +            in 
    3.28 +                ([("spass", spass, infopts ^ baseopts, probfile)] @ 
    3.29                    (make_atp_list xs (n+1)))
    3.30                end
    3.31              else if !prover = "vampire"