--- a/lib/scripts/SystemOnTPTP Sun Jun 28 17:55:44 2009 +0200
+++ b/lib/scripts/SystemOnTPTP Sun Jun 28 18:47:22 2009 +0200
@@ -10,20 +10,20 @@
use HTTP::Request::Common;
use LWP;
-my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
+my $SystemOnTPTPFormReplyURL =
+ "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
# default parameters
my %URLParameters = (
"NoHTML" => 1,
"QuietFlag" => "-q01",
- "X2TPTP" => "-S",
"SubmitButton" => "RunSelectedSystems",
"ProblemSource" => "UPLOAD",
);
#----Get format and transform options if specified
my %Options;
-getopts("hws:t:c:",\%Options);
+getopts("hwxs:t:c:",\%Options);
#----Usage
sub usage() {
@@ -31,6 +31,7 @@
print(" <options> are ...\n");
print(" -h - print this help\n");
print(" -w - list available ATP systems\n");
+ print(" -x - use X2TPTP to convert output of prover\n");
print(" -s<system> - specified system to use\n");
print(" -t<timelimit> - CPU time limit for system\n");
print(" -c<command> - custom command for system\n");
@@ -40,11 +41,18 @@
if (exists($Options{'h'})) {
usage();
}
+
#----What systems flag
if (exists($Options{'w'})) {
$URLParameters{"SubmitButton"} = "ListSystems";
delete($URLParameters{"ProblemSource"});
}
+
+#----X2TPTP
+if (exists($Options{'x'})) {
+ $URLParameters{"X2TPTP"} = "-S";
+}
+
#----Selected system
my $System;
if (exists($Options{'s'})) {
@@ -86,7 +94,7 @@
my $Response = $Agent->request($Request);
#catch errors / failure
-if(! $Response->is_success){
+if(!$Response->is_success) {
print "HTTP-Error: " . $Response->message . "\n";
exit(-1);
} elsif (exists($Options{'w'})) {
@@ -95,7 +103,12 @@
} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
print "Specified System $1 does not exist\n";
exit(-1);
-} elsif ($Response->content =~ /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/) {
+} elsif (exists($Options{'x'}) &&
+ $Response->content =~
+ /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
+ $Response->content !~ /ERROR: Could not form TPTP format derivation/ )
+{
+ # converted output: extract proof
my @lines = split( /\n/, $Response->content);
my $extract = "";
foreach my $line (@lines){
@@ -108,12 +121,20 @@
$extract =~ s/\s//g;
$extract =~ s/\)\.cnf/\)\.\ncnf/g;
+ print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
# orientation for res_reconstruct.ML
print "# SZS output start CNFRefutation.\n";
print "$extract\n";
print "# SZS output end CNFRefutation.\n";
+ # can be useful for debugging; Isabelle ignores this
+ print "============== original response from SystemOnTPTP: ==============\n";
+ print $Response->content;
exit(0);
-} else {
+} elsif (!exists($Options{'x'})) {
+ # pass output directly to Isabelle
+ print $Response->content;
+ exit(0);
+}else {
print "Remote-script could not extract proof:\n".$Response->content;
exit(-1);
}
--- a/src/HOL/ATP_Linkup.thy Sun Jun 28 17:55:44 2009 +0200
+++ b/src/HOL/ATP_Linkup.thy Sun Jun 28 18:47:22 2009 +0200
@@ -115,11 +115,11 @@
text {* remote provers via SystemOnTPTP *}
setup {* AtpManager.add_prover "remote_vampire"
- (AtpWrapper.remote_prover "-s Vampire---9.0") *}
+ (AtpWrapper.remote_prover_opts 60 false "" "Vampire---9") *}
setup {* AtpManager.add_prover "remote_spass"
- (AtpWrapper.remote_prover "-s SPASS---3.01") *}
+ (AtpWrapper.remote_prover_opts 40 true "-x" "SPASS---") *}
setup {* AtpManager.add_prover "remote_e"
- (AtpWrapper.remote_prover "-s EP---1.0") *}
+ (AtpWrapper.remote_prover_opts 100 false "" "EP---") *}
--- a/src/HOL/Tools/atp_wrapper.ML Sun Jun 28 17:55:44 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML Sun Jun 28 18:47:22 2009 +0200
@@ -23,8 +23,9 @@
val eprover_full: AtpManager.prover
val spass_opts: int -> bool -> AtpManager.prover
val spass: AtpManager.prover
- val remote_prover_opts: int -> bool -> string -> AtpManager.prover
- val remote_prover: string -> AtpManager.prover
+ val remote_prover_opts: int -> bool -> string -> string -> AtpManager.prover
+ val remote_prover: string -> string -> AtpManager.prover
+ val refresh_systems: unit -> unit
end;
structure AtpWrapper: ATP_WRAPPER =
@@ -74,20 +75,16 @@
(* write out problem file and call prover *)
val probfile = prob_pathname subgoalno
- val fname = File.platform_path probfile
- val _ = writer fname clauses
- val cmdline =
- if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args
- else error ("Bad executable: " ^ Path.implode cmd)
- val (proof, rc) = system_out (cmdline ^ " " ^ fname)
+ val conj_pos = writer probfile clauses
+ val (proof, rc) = system_out (
+ if File.exists cmd then
+ space_implode " " ["exec", File.shell_path cmd, args, File.platform_path probfile]
+ else error ("Bad executable: " ^ Path.implode cmd))
(* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
val _ =
- if destdir' = "" then OS.FileSys.remove fname
- else
- let val out = TextIO.openOut (fname ^ "_proof")
- val _ = TextIO.output (out, proof)
- in TextIO.closeOut out end
+ if destdir' = "" then File.rm probfile
+ else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof
(* check for success and print out some information on failure *)
val failure = find_failure proof
@@ -95,7 +92,8 @@
val message =
if is_some failure then "External prover failed."
else if rc <> 0 then "External prover failed: " ^ proof
- else "Try this command: " ^ produce_answer name (proof, thm_names, ctxt, th, subgoalno)
+ else "Try this command: " ^
+ produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno)
val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
in (success, message, proof, thm_names, the_filtered_clauses) end;
@@ -112,7 +110,7 @@
(ResHolClause.tptp_write_file (AtpManager.get_full_types()))
command
ResReconstruct.find_failure
- (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
+ (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list false)
timeout ax_clauses fcls name n goal;
(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
@@ -146,7 +144,7 @@
("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
timeout;
-val vampire_full = vampire_opts 60 false;
+val vampire_full = vampire_opts_full 60 false;
(* E prover *)
@@ -177,7 +175,7 @@
(Path.explode "$SPASS_HOME/SPASS",
"-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)
ResReconstruct.find_failure
- ResReconstruct.lemma_list_dfg
+ (ResReconstruct.lemma_list true)
timeout ax_clauses fcls name n goal;
val spass = spass_opts 40 true;
@@ -185,10 +183,32 @@
(* remote prover invocation via SystemOnTPTP *)
-fun remote_prover_opts max_new theory_const args timeout =
- tptp_prover_opts max_new theory_const
- (Path.explode "$ISABELLE_HOME/lib/scripts/SystemOnTPTP", args ^ " -t " ^ string_of_int timeout)
- timeout;
+val systems =
+ Synchronized.var "atp_wrapper_systems" ([]: string list);
+
+fun get_systems () =
+ let
+ val (answer, rc) = system_out (("$ISABELLE_HOME/lib/scripts/SystemOnTPTP" |>
+ Path.explode |> File.shell_path) ^ " -w")
+ in
+ if rc <> 0 then error ("Get available systems from SystemOnTPTP:\n" ^ answer)
+ else split_lines answer
+ end;
+
+fun refresh_systems () = Synchronized.change systems (fn _ =>
+ get_systems());
+
+fun get_system prefix = Synchronized.change_result systems (fn systems =>
+ let val systems = if null systems then get_systems() else systems
+ in (find_first (String.isPrefix prefix) systems, systems) end);
+
+fun remote_prover_opts max_new theory_const args prover_prefix timeout =
+ let val sys = case get_system prover_prefix of
+ NONE => error ("No system like " ^ quote prover_prefix ^ " at SystemOnTPTP")
+ | SOME sys => sys
+ in tptp_prover_opts max_new theory_const
+ (Path.explode "$ISABELLE_HOME/lib/scripts/SystemOnTPTP",
+ args ^ " -t " ^ string_of_int timeout ^ " -s " ^ sys) timeout end;
val remote_prover = remote_prover_opts 60 false;
--- a/src/HOL/Tools/res_atp.ML Sun Jun 28 17:55:44 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML Sun Jun 28 18:47:22 2009 +0200
@@ -296,7 +296,11 @@
(*The rule subsetI is frequently omitted by the relevance filter. This could be theory data
or identified with ATPset (which however is too big currently)*)
-val whitelist = [subsetI];
+val whitelist_fo = [subsetI];
+(* ext has been a 'helper clause', always given to the atps.
+ As such it was not passed to metis, but metis does not include ext (in contrast
+ to the other helper_clauses *)
+val whitelist_ho = [ResHolClause.ext];
(*** retrieve lemmas from clasimpset and atpset, may filter them ***)
@@ -531,10 +535,12 @@
create additional clauses based on the information from extra_cls *)
fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
let
- val white_thms =
- filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths))
+ val isFO = isFO thy goal_cls
+ val white_thms = filter check_named (map ResAxioms.pairname
+ (whitelist_fo @ (if isFO then [] else whitelist_ho) @ chain_ths))
val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
val extra_cls = white_cls @ extra_cls
+ val axcls = white_cls @ axcls
val ccls = subtract_cls goal_cls extra_cls
val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
val ccltms = map prop_of ccls
@@ -545,7 +551,7 @@
(*TFrees in conjecture clauses; TVars in axiom clauses*)
val conjectures = ResHolClause.make_conjecture_clauses dfg thy ccls
val (clnames,axiom_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy axcls)
- val helper_clauses = ResHolClause.get_helper_clauses dfg thy (isFO thy goal_cls) (conjectures, extra_cls, [])
+ val helper_clauses = ResHolClause.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
in
--- a/src/HOL/Tools/res_clause.ML Sun Jun 28 17:55:44 2009 +0200
+++ b/src/HOL/Tools/res_clause.ML Sun Jun 28 18:47:22 2009 +0200
@@ -57,7 +57,6 @@
val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table
val add_arityClause_funcs: arityClause * int Symtab.table -> int Symtab.table
val init_functab: int Symtab.table
- val writeln_strs: TextIO.outstream -> string list -> unit
val dfg_sign: bool -> string -> string
val dfg_of_typeLit: bool -> type_literal -> string
val gen_dfg_cls: int * string * kind * string list * string list * string list -> string
@@ -441,8 +440,6 @@
fun string_of_type_clsname (cls_id,ax_name,idx) =
string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
-fun writeln_strs os = List.app (fn s => TextIO.output (os, s));
-
(**** Producing DFG files ****)
--- a/src/HOL/Tools/res_hol_clause.ML Sun Jun 28 17:55:44 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML Sun Jun 28 18:47:22 2009 +0200
@@ -26,19 +26,21 @@
val strip_comb: combterm -> combterm * combterm list
val literals_of_term: theory -> term -> literal list * typ list
exception TOO_TRIVIAL
- val make_conjecture_clauses: bool -> theory -> thm list -> clause list (* dfg thy ccls *)
+ val make_conjecture_clauses: bool -> theory -> thm list -> clause list
val make_axiom_clauses: bool ->
theory ->
- (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list (* dfg thy axcls *)
+ (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list
val get_helper_clauses: bool ->
theory ->
bool ->
clause list * (thm * (axiom_name * clause_id)) list * string list ->
clause list
- val tptp_write_file: bool -> string ->
- clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
- val dfg_write_file: bool -> string ->
- clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
+ val tptp_write_file: bool -> Path.T ->
+ clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list ->
+ int * int
+ val dfg_write_file: bool -> Path.T ->
+ clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list ->
+ int * int
end
structure ResHolClause: RES_HOL_CLAUSE =
@@ -423,7 +425,7 @@
val S = if needed "c_COMBS"
then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms thy [comb_S])
else []
- val other = cnf_helper_thms thy [ext,fequal_imp_equal,equal_imp_fequal]
+ val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal]
in
map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S))
end;
@@ -469,59 +471,60 @@
(* tptp format *)
-fun tptp_write_file t_full filename clauses =
+fun tptp_write_file t_full file clauses =
let
val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
val (cma, cnh) = count_constants clauses
val params = (t_full, cma, cnh)
val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss)
- val out = TextIO.openOut filename
- in
- List.app (curry TextIO.output out o #1 o (clause2tptp params)) axclauses;
- RC.writeln_strs out tfree_clss;
- RC.writeln_strs out tptp_clss;
- List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses;
- List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses;
- List.app (curry TextIO.output out o #1 o (clause2tptp params)) helper_clauses;
- TextIO.closeOut out
+ val _ =
+ File.write_list file (
+ map (#1 o (clause2tptp params)) axclauses @
+ tfree_clss @
+ tptp_clss @
+ map RC.tptp_classrelClause classrel_clauses @
+ map RC.tptp_arity_clause arity_clauses @
+ map (#1 o (clause2tptp params)) helper_clauses)
+ in (length axclauses + 1, length tfree_clss + length tptp_clss)
end;
(* dfg format *)
-fun dfg_write_file t_full filename clauses =
+fun dfg_write_file t_full file clauses =
let
val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
val (cma, cnh) = count_constants clauses
val params = (t_full, cma, cnh)
val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
- and probname = Path.implode (Path.base (Path.explode filename))
+ and probname = Path.implode (Path.base file)
val axstrs = map (#1 o (clause2dfg params)) axclauses
val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
- val out = TextIO.openOut filename
val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses
val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
- in
- TextIO.output (out, RC.string_of_start probname);
- TextIO.output (out, RC.string_of_descrip probname);
- TextIO.output (out, RC.string_of_symbols
- (RC.string_of_funcs funcs)
- (RC.string_of_preds (cl_preds @ ty_preds)));
- TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
- RC.writeln_strs out axstrs;
- List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses;
- List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses;
- RC.writeln_strs out helper_clauses_strs;
- TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
- RC.writeln_strs out tfree_clss;
- RC.writeln_strs out dfg_clss;
- TextIO.output (out, "end_of_list.\n\n");
- (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
- TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");
- TextIO.output (out, "end_problem.\n");
- TextIO.closeOut out
+ val _ =
+ File.write_list file (
+ RC.string_of_start probname ::
+ RC.string_of_descrip probname ::
+ RC.string_of_symbols (RC.string_of_funcs funcs)
+ (RC.string_of_preds (cl_preds @ ty_preds)) ::
+ "list_of_clauses(axioms,cnf).\n" ::
+ axstrs @
+ map RC.dfg_classrelClause classrel_clauses @
+ map RC.dfg_arity_clause arity_clauses @
+ helper_clauses_strs @
+ ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @
+ tfree_clss @
+ dfg_clss @
+ ["end_of_list.\n\n",
+ (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
+ "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n",
+ "end_problem.\n"])
+
+ in (length axclauses + length classrel_clauses + length arity_clauses +
+ length helper_clauses + 1, length tfree_clss + length dfg_clss)
end;
end
--- a/src/HOL/Tools/res_reconstruct.ML Sun Jun 28 17:55:44 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Sun Jun 28 18:47:22 2009 +0200
@@ -16,10 +16,11 @@
val setup: Context.theory -> Context.theory
(* extracting lemma list*)
val find_failure: string -> string option
- val lemma_list_dfg: string -> string * string vector * Proof.context * Thm.thm * int -> string
- val lemma_list_tstp: string -> string * string vector * Proof.context * Thm.thm * int -> string
+ val lemma_list: bool -> string ->
+ string * string vector * (int * int) * Proof.context * Thm.thm * int -> string
(* structured proofs *)
- val structured_proof: string -> string * string vector * Proof.context * Thm.thm * int -> string
+ val structured_proof: string ->
+ string * string vector * (int * int) * Proof.context * Thm.thm * int -> string
end;
structure ResReconstruct : RES_RECONSTRUCT =
@@ -496,17 +497,17 @@
(* === EXTRACTING LEMMAS === *)
(* lines have the form "cnf(108, axiom, ...",
the number (108) has to be extracted)*)
- fun get_step_nums_tstp proofextract =
+ fun get_step_nums false proofextract =
let val toks = String.tokens (not o Char.isAlphaNum)
fun inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok
+ | inputno ("cnf"::ntok::"negated"::"conjecture"::_) = Int.fromString ntok
| inputno _ = NONE
val lines = split_lines proofextract
in List.mapPartial (inputno o toks) lines end
-
- (*String contains multiple lines. We want those of the form
+ (*String contains multiple lines. We want those of the form
"253[0:Inp] et cetera..."
A list consisting of the first number in each line is returned. *)
- fun get_step_nums_dfg proofextract =
+ | get_step_nums true proofextract =
let val toks = String.tokens (not o Char.isAlphaNum)
fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
| inputno _ = NONE
@@ -514,15 +515,19 @@
in List.mapPartial (inputno o toks) lines end
(*extracting lemmas from tstp-output between the lines from above*)
- fun extract_lemmas get_step_nums (proof, thm_names, _, _, _) =
+ fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) =
let
(* get the names of axioms from their numbers*)
fun get_axiom_names thm_names step_nums =
let
- fun is_axiom n = n <= Vector.length thm_names
+ val last_axiom = Vector.length thm_names
+ fun is_axiom n = n <= last_axiom
+ fun is_conj n = n >= #1 conj_count andalso n < #1 conj_count + #2 conj_count
fun getname i = Vector.sub(thm_names, i-1)
in
- sort_distinct string_ord (filter (fn x => x <> "??.unknown") (map getname (filter is_axiom step_nums)))
+ (sort_distinct string_ord (filter (fn x => x <> "??.unknown")
+ (map getname (filter is_axiom step_nums))),
+ exists is_conj step_nums)
end
val proofextract = get_proof_extract proof
in
@@ -545,22 +550,23 @@
fun sendback_metis_nochained lemmas =
(Markup.markup Markup.sendback o metis_line) (nochained lemmas)
- fun lemma_list_tstp name result =
- let val lemmas = extract_lemmas get_step_nums_tstp result
- in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas end;
- fun lemma_list_dfg name result =
- let val lemmas = extract_lemmas get_step_nums_dfg result
- in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas end;
+
+ fun lemma_list dfg name result =
+ let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
+ in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^
+ (if used_conj then ""
+ else "\nWarning: Goal is provable because context is inconsistent.")
+ end;
(* === Extracting structured Isar-proof === *)
- fun structured_proof name (result as (proof, thm_names, ctxt, goal, subgoalno)) =
+ fun structured_proof name (result as (proof, thm_names, conj_count, ctxt, goal, subgoalno)) =
let
(*Could use split_lines, but it can return blank lines...*)
val lines = String.tokens (equal #"\n");
val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c)
val proofextract = get_proof_extract proof
val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
- val one_line_proof = lemma_list_tstp name result
+ val one_line_proof = lemma_list false name result
val structured = if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
else decode_tstp_file cnfs ctxt goal subgoalno thm_names
in