1.1 --- a/src/HOL/Tools/ATP/AtpCommunication.ML Fri Dec 22 20:58:14 2006 +0100
1.2 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML Fri Dec 22 21:00:42 2006 +0100
1.3 @@ -11,10 +11,10 @@
1.4 sig
1.5 val checkEProofFound:
1.6 TextIO.instream * TextIO.outstream * Posix.Process.pid *
1.7 - string * string Vector.vector -> bool
1.8 + string * thm * int * string Vector.vector -> bool
1.9 val checkVampProofFound:
1.10 TextIO.instream * TextIO.outstream * Posix.Process.pid *
1.11 - string * string Vector.vector -> bool
1.12 + string * thm * int * string Vector.vector -> bool
1.13 val checkSpassProofFound:
1.14 TextIO.instream * TextIO.outstream * Posix.Process.pid *
1.15 string * thm * int * string Vector.vector -> bool
1.16 @@ -32,7 +32,6 @@
1.17
1.18 exception EOF;
1.19
1.20 -
1.21 (**** retrieve the axioms that were used in the proof ****)
1.22
1.23 (*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*)
1.24 @@ -59,20 +58,23 @@
1.25 fun get_axiom_names_spass proofstr thm_names =
1.26 get_axiom_names thm_names (get_spass_linenums proofstr);
1.27
1.28 - (*String contains multiple lines. We want those of the form
1.29 - "number : ...: ...: initial..." *)
1.30 -fun get_e_linenums proofstr =
1.31 - let val fields = String.fields (fn c => c = #":")
1.32 - val nospaces = String.translate (fn c => if c = #" " then "" else str c)
1.33 - fun initial s = String.isPrefix "initial" (nospaces s)
1.34 - fun firstno (line :: _ :: _ :: rule :: _) =
1.35 - if initial rule then Int.fromString line else NONE
1.36 - | firstno _ = NONE
1.37 - val lines = String.tokens (fn c => c = #"\n") proofstr
1.38 - in List.mapPartial (firstno o fields) lines end
1.39 +fun not_comma c = c <> #",";
1.40
1.41 -fun get_axiom_names_e proofstr thm_names =
1.42 - get_axiom_names thm_names (get_e_linenums proofstr);
1.43 +(*A valid TSTP axiom line has the form cnf(NNN,axiom,...) where NNN is a positive integer.*)
1.44 +fun parse_tstp_line s =
1.45 + let val ss = Substring.full (unprefix "cnf(" (nospaces s))
1.46 + val (intf,rest) = Substring.splitl not_comma ss
1.47 + val (rolef,rest) = Substring.splitl not_comma (Substring.triml 1 rest)
1.48 + (*We only allow negated_conjecture because the line number will be removed in
1.49 + get_axiom_names above, while suppressing the UNSOUND warning*)
1.50 + val ints = if Substring.string rolef mem_string ["axiom","negated_conjecture"]
1.51 + then Substring.string intf
1.52 + else "error"
1.53 + in Int.fromString ints end
1.54 + handle Fail _ => NONE;
1.55 +
1.56 +fun get_axiom_names_tstp proofstr thm_names =
1.57 + get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofstr));
1.58
1.59 (*String contains multiple lines. We want those of the form
1.60 "*********** [448, input] ***********".
1.61 @@ -97,8 +99,7 @@
1.62 ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
1.63 "\nprobfile is " ^ probfile ^
1.64 " num of clauses is " ^ string_of_int (Vector.length thm_names))
1.65 - val axiom_names = getax proofstr thm_names
1.66 - val ax_str = rules_to_string axiom_names
1.67 + val ax_str = rules_to_string (getax proofstr thm_names)
1.68 in
1.69 trace ("\nDone. Lemma list is " ^ ax_str);
1.70 TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^
1.71 @@ -116,7 +117,7 @@
1.72 TextIO.flushOut toParent;
1.73 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
1.74
1.75 -val e_lemma_list = prover_lemma_list_aux get_axiom_names_e;
1.76 +val e_lemma_list = prover_lemma_list_aux get_axiom_names_tstp;
1.77
1.78 val vamp_lemma_list = prover_lemma_list_aux get_axiom_names_vamp;
1.79
1.80 @@ -128,9 +129,9 @@
1.81 (*Return everything in s that comes before the string t*)
1.82 fun cut_before t s =
1.83 let val (s1,s2) = Substring.position t (Substring.full s)
1.84 - val _ = Substring.size s2 <> 0
1.85 - orelse error "cut_before: string not found"
1.86 - in Substring.string s2 end;
1.87 + in if Substring.size s2 = 0 then error "cut_before: string not found"
1.88 + else Substring.string s2
1.89 + end;
1.90
1.91 val start_E = "# Proof object starts here."
1.92 val end_E = "# Proof object ends here."
1.93 @@ -145,7 +146,7 @@
1.94 (* and if so, transfer output to the input pipe of the main Isabelle process *)
1.95 (*********************************************************************************)
1.96
1.97 -fun startTransfer (endS, fromChild, toParent, ppid, probfile, thm_names) =
1.98 +fun startTransfer (endS, fromChild, toParent, ppid, probfile, th, sgno, thm_names) =
1.99 let fun transferInput currentString =
1.100 let val thisLine = TextIO.inputLine fromChild
1.101 in
1.102 @@ -156,6 +157,7 @@
1.103 else if String.isPrefix endS thisLine
1.104 then let val proofextract = currentString ^ cut_before endS thisLine
1.105 val lemma_list = if endS = end_V8 then vamp_lemma_list
1.106 + else if endS = end_SPASS then spass_lemma_list
1.107 else e_lemma_list
1.108 in
1.109 trace ("\nExtracted proof:\n" ^ proofextract);
1.110 @@ -179,82 +181,47 @@
1.111 OS.Process.sleep (Time.fromMilliseconds 600));
1.112
1.113 (*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
1.114 -fun checkVampProofFound (fromChild, toParent, ppid, probfile, thm_names) =
1.115 +fun checkVampProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) =
1.116 let val thisLine = TextIO.inputLine fromChild
1.117 in
1.118 trace thisLine;
1.119 if thisLine = ""
1.120 then (trace "\nNo proof output seen"; false)
1.121 else if String.isPrefix start_V8 thisLine
1.122 - then startTransfer (end_V8, fromChild, toParent, ppid, probfile, thm_names)
1.123 + then startTransfer (end_V8, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
1.124 else if (String.isPrefix "Satisfiability detected" thisLine) orelse
1.125 (String.isPrefix "Refutation not found" thisLine)
1.126 then (signal_parent (toParent, ppid, "Failure\n", probfile);
1.127 true)
1.128 - else checkVampProofFound (fromChild, toParent, ppid, probfile, thm_names)
1.129 + else checkVampProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
1.130 end
1.131
1.132 (*Called from watcher. Returns true if the E process has returned a verdict.*)
1.133 -fun checkEProofFound (fromChild, toParent, ppid, probfile, thm_names) =
1.134 +fun checkEProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) =
1.135 let val thisLine = TextIO.inputLine fromChild
1.136 in
1.137 trace thisLine;
1.138 if thisLine = "" then (trace "\nNo proof output seen"; false)
1.139 else if String.isPrefix start_E thisLine
1.140 - then startTransfer (end_E, fromChild, toParent, ppid, probfile, thm_names)
1.141 + then startTransfer (end_E, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
1.142 else if String.isPrefix "# Problem is satisfiable" thisLine
1.143 then (signal_parent (toParent, ppid, "Invalid\n", probfile);
1.144 true)
1.145 else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine
1.146 then (signal_parent (toParent, ppid, "Failure\n", probfile);
1.147 true)
1.148 - else checkEProofFound (fromChild, toParent, ppid, probfile, thm_names)
1.149 - end
1.150 -
1.151 -(*FIXME: can't these two functions be replaced by startTransfer above?*)
1.152 -fun transferSpassInput (fromChild, toParent, ppid, probfile,
1.153 - currentString, thm, sg_num, thm_names) =
1.154 - let val thisLine = TextIO.inputLine fromChild
1.155 - in
1.156 - trace thisLine;
1.157 - if thisLine = "" (*end of file?*)
1.158 - then (trace ("\nspass_extraction_failed: " ^ currentString);
1.159 - raise EOF)
1.160 - else if String.isPrefix "Formulae used in the proof" thisLine
1.161 - then
1.162 - let val proofextract = currentString ^ cut_before end_SPASS thisLine
1.163 - in
1.164 - trace ("\nextracted spass proof: " ^ proofextract);
1.165 - spass_lemma_list proofextract probfile toParent ppid thm_names
1.166 - end
1.167 - else transferSpassInput (fromChild, toParent, ppid, probfile,
1.168 - currentString ^ thisLine, thm, sg_num, thm_names)
1.169 + else checkEProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
1.170 end;
1.171
1.172 -(*Inspect the output of a SPASS process to see if it has found a proof,
1.173 - and if so, transfer output to the input pipe of the main Isabelle process*)
1.174 -fun startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,thm_names) =
1.175 - let val thisLine = TextIO.inputLine fromChild
1.176 - in
1.177 - if thisLine = "" then false
1.178 - else if String.isPrefix "Here is a proof" thisLine then
1.179 - (trace ("\nabout to transfer SPASS proof:\n");
1.180 - transferSpassInput (fromChild, toParent, ppid, probfile, thisLine,
1.181 - thm, sg_num,thm_names);
1.182 - true) handle EOF => false
1.183 - else startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,thm_names)
1.184 - end
1.185 -
1.186 -
1.187 (*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
1.188 -fun checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, thm_names) =
1.189 +fun checkSpassProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) =
1.190 let val thisLine = TextIO.inputLine fromChild
1.191 in
1.192 trace thisLine;
1.193 if thisLine = "" then (trace "\nNo proof output seen"; false)
1.194 - else if thisLine = "SPASS beiseite: Proof found.\n"
1.195 + else if String.isPrefix "Here is a proof" thisLine
1.196 then
1.197 - startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, thm_names)
1.198 + startTransfer (end_SPASS, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
1.199 else if thisLine = "SPASS beiseite: Completion found.\n"
1.200 then (signal_parent (toParent, ppid, "Invalid\n", probfile);
1.201 true)
1.202 @@ -262,7 +229,7 @@
1.203 thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
1.204 then (signal_parent (toParent, ppid, "Failure\n", probfile);
1.205 true)
1.206 - else checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, thm_names)
1.207 + else checkSpassProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
1.208 end
1.209
1.210 end;
2.1 --- a/src/HOL/Tools/ATP/watcher.ML Fri Dec 22 20:58:14 2006 +0100
2.2 +++ b/src/HOL/Tools/ATP/watcher.ML Fri Dec 22 21:00:42 2006 +0100
2.3 @@ -226,9 +226,9 @@
2.4 let val _ = trace ("\nInput available from child: " ^ file)
2.5 val childDone = (case prover of
2.6 "vampire" => AtpCommunication.checkVampProofFound
2.7 - (childIn, toParentStr, ppid, file, thm_names)
2.8 + (childIn, toParentStr, ppid, file, th, sgno, thm_names)
2.9 | "E" => AtpCommunication.checkEProofFound
2.10 - (childIn, toParentStr, ppid, file, thm_names)
2.11 + (childIn, toParentStr, ppid, file, th, sgno, thm_names)
2.12 | "spass" => AtpCommunication.checkSpassProofFound
2.13 (childIn, toParentStr, ppid, file, th, sgno, thm_names)
2.14 | _ => (trace ("\nBad prover! " ^ prover); true) )
3.1 --- a/src/HOL/Tools/meson.ML Fri Dec 22 20:58:14 2006 +0100
3.2 +++ b/src/HOL/Tools/meson.ML Fri Dec 22 21:00:42 2006 +0100
3.3 @@ -193,7 +193,7 @@
3.4
3.5 (*** The basic CNF transformation ***)
3.6
3.7 -val max_clauses = ref 20;
3.8 +val max_clauses = ref 40;
3.9
3.10 fun sum x y = if x < !max_clauses andalso y < !max_clauses then x+y else !max_clauses;
3.11 fun prod x y = if x < !max_clauses andalso y < !max_clauses then x*y else !max_clauses;
3.12 @@ -648,7 +648,7 @@
3.13
3.14 (*Top-level conversion to meta-level clauses. Each clause has
3.15 leading !!-bound universal variables, to express generality. To get
3.16 - disjunctions instead of meta-clauses, remove "make_meta_clauses" below.*)
3.17 + meta-clauses instead of disjunctions, uncomment "make_meta_clauses" below.*)
3.18 val make_clauses_tac =
3.19 SUBGOAL
3.20 (fn (prop,_) =>
3.21 @@ -658,7 +658,7 @@
3.22 (fn hyps =>
3.23 (Method.insert_tac
3.24 (map forall_intr_vars
3.25 - (make_meta_clauses (make_clauses hyps))) 1)),
3.26 + ( (**make_meta_clauses**) (make_clauses hyps))) 1)),
3.27 REPEAT_DETERM_N (length ts) o (etac thin_rl)]
3.28 end);
3.29
4.1 --- a/src/HOL/Tools/res_atp.ML Fri Dec 22 20:58:14 2006 +0100
4.2 +++ b/src/HOL/Tools/res_atp.ML Fri Dec 22 21:00:42 2006 +0100
4.3 @@ -807,7 +807,7 @@
4.4 let val Eprover = helper_path "E_HOME" "eproof"
4.5 in
4.6 ("E", Eprover,
4.7 - "--tstp-in%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) ::
4.8 + "--tstp-in%--tstp-out%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) ::
4.9 make_atp_list xs (n+1)
4.10 end
4.11 else error ("Invalid prover name: " ^ !prover)
5.1 --- a/src/HOL/Tools/res_axioms.ML Fri Dec 22 20:58:14 2006 +0100
5.2 +++ b/src/HOL/Tools/res_axioms.ML Fri Dec 22 21:00:42 2006 +0100
5.3 @@ -23,14 +23,14 @@
5.4 val atpset_rules_of: Proof.context -> (string * thm) list
5.5 end;
5.6
5.7 -structure ResAxioms: RES_AXIOMS =
5.8 +structure ResAxioms =
5.9 struct
5.10
5.11 (*For running the comparison between combinators and abstractions.
5.12 CANNOT be a ref, as the setting is used while Isabelle is built.
5.13 Currently FALSE, i.e. all the "abstraction" code below is unused, but so far
5.14 it seems to be inferior to combinators...*)
5.15 -val abstract_lambdas = false;
5.16 +val abstract_lambdas = true;
5.17
5.18 val trace_abs = ref false;
5.19
5.20 @@ -527,9 +527,6 @@
5.21
5.22 (**** Extract and Clausify theorems from a theory's claset and simpset ****)
5.23
5.24 -(*Preserve the name of "th" after the transformation "f"*)
5.25 -fun preserve_name f th = PureThy.put_name_hint (PureThy.get_name_hint th) (f th);
5.26 -
5.27 fun rules_of_claset cs =
5.28 let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
5.29 val intros = safeIs @ hazIs