# HG changeset patch # User paulson # Date 1166817642 -3600 # Node ID f386d7eb17d15c84e20e7309d604739fc26b76b1 # Parent dab16d14db609faafcf0f01e5a2c52172dc88814 tidying the ATP communications diff -r dab16d14db60 -r f386d7eb17d1 src/HOL/Tools/ATP/AtpCommunication.ML --- a/src/HOL/Tools/ATP/AtpCommunication.ML Fri Dec 22 20:58:14 2006 +0100 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML Fri Dec 22 21:00:42 2006 +0100 @@ -11,10 +11,10 @@ sig val checkEProofFound: TextIO.instream * TextIO.outstream * Posix.Process.pid * - string * string Vector.vector -> bool + string * thm * int * string Vector.vector -> bool val checkVampProofFound: TextIO.instream * TextIO.outstream * Posix.Process.pid * - string * string Vector.vector -> bool + string * thm * int * string Vector.vector -> bool val checkSpassProofFound: TextIO.instream * TextIO.outstream * Posix.Process.pid * string * thm * int * string Vector.vector -> bool @@ -32,7 +32,6 @@ exception EOF; - (**** retrieve the axioms that were used in the proof ****) (*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*) @@ -59,20 +58,23 @@ fun get_axiom_names_spass proofstr thm_names = get_axiom_names thm_names (get_spass_linenums proofstr); - (*String contains multiple lines. We want those of the form - "number : ...: ...: initial..." *) -fun get_e_linenums proofstr = - let val fields = String.fields (fn c => c = #":") - val nospaces = String.translate (fn c => if c = #" " then "" else str c) - fun initial s = String.isPrefix "initial" (nospaces s) - fun firstno (line :: _ :: _ :: rule :: _) = - if initial rule then Int.fromString line else NONE - | firstno _ = NONE - val lines = String.tokens (fn c => c = #"\n") proofstr - in List.mapPartial (firstno o fields) lines end +fun not_comma c = c <> #","; -fun get_axiom_names_e proofstr thm_names = - get_axiom_names thm_names (get_e_linenums proofstr); +(*A valid TSTP axiom line has the form cnf(NNN,axiom,...) where NNN is a positive integer.*) +fun parse_tstp_line s = + let val ss = Substring.full (unprefix "cnf(" (nospaces s)) + val (intf,rest) = Substring.splitl not_comma ss + val (rolef,rest) = Substring.splitl not_comma (Substring.triml 1 rest) + (*We only allow negated_conjecture because the line number will be removed in + get_axiom_names above, while suppressing the UNSOUND warning*) + val ints = if Substring.string rolef mem_string ["axiom","negated_conjecture"] + then Substring.string intf + else "error" + in Int.fromString ints end + handle Fail _ => NONE; + +fun get_axiom_names_tstp proofstr thm_names = + get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofstr)); (*String contains multiple lines. We want those of the form "*********** [448, input] ***********". @@ -97,8 +99,7 @@ ("\n\nGetting lemma names. proofstr is " ^ proofstr ^ "\nprobfile is " ^ probfile ^ " num of clauses is " ^ string_of_int (Vector.length thm_names)) - val axiom_names = getax proofstr thm_names - val ax_str = rules_to_string axiom_names + val ax_str = rules_to_string (getax proofstr thm_names) in trace ("\nDone. Lemma list is " ^ ax_str); TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^ @@ -116,7 +117,7 @@ TextIO.flushOut toParent; Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)); -val e_lemma_list = prover_lemma_list_aux get_axiom_names_e; +val e_lemma_list = prover_lemma_list_aux get_axiom_names_tstp; val vamp_lemma_list = prover_lemma_list_aux get_axiom_names_vamp; @@ -128,9 +129,9 @@ (*Return everything in s that comes before the string t*) fun cut_before t s = let val (s1,s2) = Substring.position t (Substring.full s) - val _ = Substring.size s2 <> 0 - orelse error "cut_before: string not found" - in Substring.string s2 end; + in if Substring.size s2 = 0 then error "cut_before: string not found" + else Substring.string s2 + end; val start_E = "# Proof object starts here." val end_E = "# Proof object ends here." @@ -145,7 +146,7 @@ (* and if so, transfer output to the input pipe of the main Isabelle process *) (*********************************************************************************) -fun startTransfer (endS, fromChild, toParent, ppid, probfile, thm_names) = +fun startTransfer (endS, fromChild, toParent, ppid, probfile, th, sgno, thm_names) = let fun transferInput currentString = let val thisLine = TextIO.inputLine fromChild in @@ -156,6 +157,7 @@ else if String.isPrefix endS thisLine then let val proofextract = currentString ^ cut_before endS thisLine val lemma_list = if endS = end_V8 then vamp_lemma_list + else if endS = end_SPASS then spass_lemma_list else e_lemma_list in trace ("\nExtracted proof:\n" ^ proofextract); @@ -179,82 +181,47 @@ OS.Process.sleep (Time.fromMilliseconds 600)); (*Called from watcher. Returns true if the Vampire process has returned a verdict.*) -fun checkVampProofFound (fromChild, toParent, ppid, probfile, thm_names) = +fun checkVampProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) = let val thisLine = TextIO.inputLine fromChild in trace thisLine; if thisLine = "" then (trace "\nNo proof output seen"; false) else if String.isPrefix start_V8 thisLine - then startTransfer (end_V8, fromChild, toParent, ppid, probfile, thm_names) + then startTransfer (end_V8, fromChild, toParent, ppid, probfile, th, sgno, thm_names) else if (String.isPrefix "Satisfiability detected" thisLine) orelse (String.isPrefix "Refutation not found" thisLine) then (signal_parent (toParent, ppid, "Failure\n", probfile); true) - else checkVampProofFound (fromChild, toParent, ppid, probfile, thm_names) + else checkVampProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) end (*Called from watcher. Returns true if the E process has returned a verdict.*) -fun checkEProofFound (fromChild, toParent, ppid, probfile, thm_names) = +fun checkEProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) = let val thisLine = TextIO.inputLine fromChild in trace thisLine; if thisLine = "" then (trace "\nNo proof output seen"; false) else if String.isPrefix start_E thisLine - then startTransfer (end_E, fromChild, toParent, ppid, probfile, thm_names) + then startTransfer (end_E, fromChild, toParent, ppid, probfile, th, sgno, thm_names) else if String.isPrefix "# Problem is satisfiable" thisLine then (signal_parent (toParent, ppid, "Invalid\n", probfile); true) else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine then (signal_parent (toParent, ppid, "Failure\n", probfile); true) - else checkEProofFound (fromChild, toParent, ppid, probfile, thm_names) - end - -(*FIXME: can't these two functions be replaced by startTransfer above?*) -fun transferSpassInput (fromChild, toParent, ppid, probfile, - currentString, thm, sg_num, thm_names) = - let val thisLine = TextIO.inputLine fromChild - in - trace thisLine; - if thisLine = "" (*end of file?*) - then (trace ("\nspass_extraction_failed: " ^ currentString); - raise EOF) - else if String.isPrefix "Formulae used in the proof" thisLine - then - let val proofextract = currentString ^ cut_before end_SPASS thisLine - in - trace ("\nextracted spass proof: " ^ proofextract); - spass_lemma_list proofextract probfile toParent ppid thm_names - end - else transferSpassInput (fromChild, toParent, ppid, probfile, - currentString ^ thisLine, thm, sg_num, thm_names) + else checkEProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) end; -(*Inspect the output of a SPASS process to see if it has found a proof, - and if so, transfer output to the input pipe of the main Isabelle process*) -fun startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,thm_names) = - let val thisLine = TextIO.inputLine fromChild - in - if thisLine = "" then false - else if String.isPrefix "Here is a proof" thisLine then - (trace ("\nabout to transfer SPASS proof:\n"); - transferSpassInput (fromChild, toParent, ppid, probfile, thisLine, - thm, sg_num,thm_names); - true) handle EOF => false - else startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,thm_names) - end - - (*Called from watcher. Returns true if the SPASS process has returned a verdict.*) -fun checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, thm_names) = +fun checkSpassProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) = let val thisLine = TextIO.inputLine fromChild in trace thisLine; if thisLine = "" then (trace "\nNo proof output seen"; false) - else if thisLine = "SPASS beiseite: Proof found.\n" + else if String.isPrefix "Here is a proof" thisLine then - startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, thm_names) + startTransfer (end_SPASS, fromChild, toParent, ppid, probfile, th, sgno, thm_names) else if thisLine = "SPASS beiseite: Completion found.\n" then (signal_parent (toParent, ppid, "Invalid\n", probfile); true) @@ -262,7 +229,7 @@ thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" then (signal_parent (toParent, ppid, "Failure\n", probfile); true) - else checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, thm_names) + else checkSpassProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) end end; diff -r dab16d14db60 -r f386d7eb17d1 src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Fri Dec 22 20:58:14 2006 +0100 +++ b/src/HOL/Tools/ATP/watcher.ML Fri Dec 22 21:00:42 2006 +0100 @@ -226,9 +226,9 @@ let val _ = trace ("\nInput available from child: " ^ file) val childDone = (case prover of "vampire" => AtpCommunication.checkVampProofFound - (childIn, toParentStr, ppid, file, thm_names) + (childIn, toParentStr, ppid, file, th, sgno, thm_names) | "E" => AtpCommunication.checkEProofFound - (childIn, toParentStr, ppid, file, thm_names) + (childIn, toParentStr, ppid, file, th, sgno, thm_names) | "spass" => AtpCommunication.checkSpassProofFound (childIn, toParentStr, ppid, file, th, sgno, thm_names) | _ => (trace ("\nBad prover! " ^ prover); true) ) diff -r dab16d14db60 -r f386d7eb17d1 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Fri Dec 22 20:58:14 2006 +0100 +++ b/src/HOL/Tools/meson.ML Fri Dec 22 21:00:42 2006 +0100 @@ -193,7 +193,7 @@ (*** The basic CNF transformation ***) -val max_clauses = ref 20; +val max_clauses = ref 40; fun sum x y = if x < !max_clauses andalso y < !max_clauses then x+y else !max_clauses; fun prod x y = if x < !max_clauses andalso y < !max_clauses then x*y else !max_clauses; @@ -648,7 +648,7 @@ (*Top-level conversion to meta-level clauses. Each clause has leading !!-bound universal variables, to express generality. To get - disjunctions instead of meta-clauses, remove "make_meta_clauses" below.*) + meta-clauses instead of disjunctions, uncomment "make_meta_clauses" below.*) val make_clauses_tac = SUBGOAL (fn (prop,_) => @@ -658,7 +658,7 @@ (fn hyps => (Method.insert_tac (map forall_intr_vars - (make_meta_clauses (make_clauses hyps))) 1)), + ( (**make_meta_clauses**) (make_clauses hyps))) 1)), REPEAT_DETERM_N (length ts) o (etac thin_rl)] end); diff -r dab16d14db60 -r f386d7eb17d1 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Fri Dec 22 20:58:14 2006 +0100 +++ b/src/HOL/Tools/res_atp.ML Fri Dec 22 21:00:42 2006 +0100 @@ -807,7 +807,7 @@ let val Eprover = helper_path "E_HOME" "eproof" in ("E", Eprover, - "--tstp-in%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) :: + "--tstp-in%--tstp-out%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) :: make_atp_list xs (n+1) end else error ("Invalid prover name: " ^ !prover) diff -r dab16d14db60 -r f386d7eb17d1 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Fri Dec 22 20:58:14 2006 +0100 +++ b/src/HOL/Tools/res_axioms.ML Fri Dec 22 21:00:42 2006 +0100 @@ -23,14 +23,14 @@ val atpset_rules_of: Proof.context -> (string * thm) list end; -structure ResAxioms: RES_AXIOMS = +structure ResAxioms = struct (*For running the comparison between combinators and abstractions. CANNOT be a ref, as the setting is used while Isabelle is built. Currently FALSE, i.e. all the "abstraction" code below is unused, but so far it seems to be inferior to combinators...*) -val abstract_lambdas = false; +val abstract_lambdas = true; val trace_abs = ref false; @@ -527,9 +527,6 @@ (**** Extract and Clausify theorems from a theory's claset and simpset ****) -(*Preserve the name of "th" after the transformation "f"*) -fun preserve_name f th = PureThy.put_name_hint (PureThy.get_name_hint th) (f th); - fun rules_of_claset cs = let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs val intros = safeIs @ hazIs