# HG changeset patch # User immler@in.tum.de # Date 1238869359 -7200 # Node ID 34927a1e0ae803eeacb5646ddcbb8fa7c67b1b25 # Parent 5106e13d400fa6af8afdc17cca9c645fd1f9edbc reverted to explicitly check the presence of a refutation (compare to 479a2fce65e6); simplified handling of errors in remote script diff -r 5106e13d400f -r 34927a1e0ae8 contrib/SystemOnTPTP/remote --- a/contrib/SystemOnTPTP/remote Fri Apr 03 18:03:29 2009 +0200 +++ b/contrib/SystemOnTPTP/remote Sat Apr 04 20:22:39 2009 +0200 @@ -26,18 +26,20 @@ getopts("hws:t:c:",\%Options); #----Usage +sub usage() { + print("Usage: remote [] \n"); + print(" are ...\n"); + print(" -h - print this help\n"); + print(" -w - list available ATP systems\n"); + print(" -s - specified system to use\n"); + print(" -t - CPU time limit for system\n"); + print(" -c - custom command for system\n"); + print(" - TPTP problem file\n"); + exit(0); +} if (exists($Options{'h'})) { - print("Usage: remote []\n"); - print(" are ...\n"); - print(" -h - print this help\n"); - print(" -w - list available ATP systems\n"); - print(" -s - specified system to use\n"); - print(" -t - CPU time limit for system\n"); - print(" -c - custom command for system\n"); - print(" - TPTP problem file\n"); - exit(0); + usage(); } - #----What systems flag if (exists($Options{'w'})) { $URLParameters{"SubmitButton"} = "ListSystems"; @@ -67,7 +69,9 @@ if (scalar(@ARGV) >= 1) { $URLParameters{"UPLOADProblem"} = [shift(@ARGV)]; } else { -die("Missing problem file"); + print("Missing problem file\n"); + usage(); + die; } } @@ -88,38 +92,29 @@ } elsif (exists($Options{'w'})) { print $Response->content; exit (0); -} elsif ($Response->content =~ /NO SOLUTION OUTPUT BY SYSTEM/){ - print "No Solution Output by System\n"; - exit(-1); -} elsif ($Response->content =~ /ERROR: Could not form TPTP format derivation/) { - print "Could not form TPTP format derivation\n"; - exit(-1); } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) { print "Specified System $1 does not exist\n"; exit(-1); -} elsif ($Response->content =~ /^\s*$/) { - print "Empty response (specified bad system? Inappropriate problem file format?)\n"; - exit(-1); -} elsif ($Response->content !~ /%\s*Result\s*:(.*)\n%\s*Output\s*:(.*)\n%/) { - print "Bad response: \n".$Response->content; - exit(-1); +} elsif ($Response->content =~ /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/) { + my @lines = split( /\n/, $Response->content); + my $extract = ""; + foreach my $line (@lines){ + #ignore comments + if ($line !~ /^%/ && !($line eq "")) { + $extract .= "$line"; + } + } + # insert newlines after ').' + $extract =~ s/\s//g; + $extract =~ s/\)\.cnf/\)\.\ncnf/g; + + # orientation for res_reconstruct.ML + print "# SZS output start CNFRefutation.\n"; + print "$extract\n"; + print "# SZS output end CNFRefutation.\n"; + exit(0); } else { - my @lines = split( /\n/, $Response->content); - my $extract = ""; - foreach my $line (@lines){ - #ignore comments - if ($line !~ /^%/ && !($line eq "")) { - $extract .= "$line"; - } - } - # insert newlines after ').' - $extract =~ s/\s//g; - $extract =~ s/\)\.cnf/\)\.\ncnf/g; - - # orientation for res_reconstruct.ML - print "# SZS output start CNFRefutation.\n"; - print "$extract\n"; - print "# SZS output end CNFRefutation.\n"; - exit(0); + print "Remote-script could not extract proof:\n".$Response->content; + exit(-1); } diff -r 5106e13d400f -r 34927a1e0ae8 src/HOL/Tools/atp_wrapper.ML --- a/src/HOL/Tools/atp_wrapper.ML Fri Apr 03 18:03:29 2009 +0200 +++ b/src/HOL/Tools/atp_wrapper.ML Sat Apr 04 20:22:39 2009 +0200 @@ -102,7 +102,7 @@ (ResAtp.get_relevant max_new theory_const goal n) (ResAtp.write_problem_file false) command - ResReconstruct.find_failure_e_vamp_spass + ResReconstruct.find_failure (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp) timeout n goal; @@ -166,7 +166,7 @@ (ResAtp.write_problem_file true) (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_e_vamp_spass + ResReconstruct.find_failure ResReconstruct.lemma_list_dfg timeout n goal; diff -r 5106e13d400f -r 34927a1e0ae8 src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Fri Apr 03 18:03:29 2009 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Sat Apr 04 20:22:39 2009 +0200 @@ -15,7 +15,7 @@ val strip_prefix: string -> string -> string option val setup: Context.theory -> Context.theory (* extracting lemma list*) - val find_failure_e_vamp_spass: string -> string option + val find_failure: string -> string option val lemma_list_dfg: string * string vector * Proof.context * Thm.thm * int -> string val lemma_list_tstp: string * string vector * Proof.context * Thm.thm * int -> string (* structured proofs *) @@ -459,14 +459,16 @@ (* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *) - val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable","SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"]; + val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable", + "SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"]; val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"]; - val failure_strings_SPASS = ["SPASS beiseite: Completion found.","SPASS beiseite: Ran out of time.", - "SPASS beiseite: Maximal number of loops exceeded."]; - fun find_failure_e_vamp_spass proof = + val failure_strings_SPASS = ["SPASS beiseite: Completion found.", + "SPASS beiseite: Ran out of time.", "SPASS beiseite: Maximal number of loops exceeded."]; + val failure_strings_remote = ["Remote-script could not extract proof"]; + fun find_failure proof = let val failures = map_filter (fn s => if String.isSubstring s proof then SOME s else NONE) - (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS) + (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote) in if null failures then NONE else SOME (hd failures) end; (*=== EXTRACTING PROOF-TEXT === *)