--- a/contrib/SystemOnTPTP/remote Mon Jan 19 23:40:29 2009 +0100
+++ b/contrib/SystemOnTPTP/remote Tue Jan 20 18:10:25 2009 +0100
@@ -3,93 +3,137 @@
# Wrapper for custom remote provers on SystemOnTPTP
# Author: Fabian Immler, TU Muenchen
#
-# Similar to the vampire wrapper, but compatible provers can be passed in the
-# command line, with %s for the problemfile e.g.
-#
-# ./remote Vampire---9.0 jumpirefix --output_syntax tptp --mode casc -t 3600 %s
-# ./remote Vampire---10.0 drakosha.pl 60 %s
-# ./remote SPASS---3.01 SPASS -Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof %s
-# ./remote Metis---2.1 metis --show proof --show saturation %s
-# ./remote SNARK---20080805r005 run-snark %s
use warnings;
use strict;
-
use Getopt::Std;
use HTTP::Request::Common;
-use LWP::UserAgent;
+use LWP;
-# address of proof-server
my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
-if(scalar(@ARGV) < 2) {
- print "prover and command missing";
- exit -1;
-}
-my $prover = shift(@ARGV);
-my $command = shift(@ARGV);
-
-# pass arguments
-my $options = "";
-while(scalar(@ARGV)>1){
- $options.=" ".shift(@ARGV);
-}
-# last argument is problemfile to be uploaded
-my $problem = [shift(@ARGV)];
-
-# fill in form
+# default parameters
my %URLParameters = (
"NoHTML" => 1,
"QuietFlag" => "-q01",
"X2TPTP" => "-S",
"SubmitButton" => "RunSelectedSystems",
"ProblemSource" => "UPLOAD",
- "UPLOADProblem" => $problem,
- "System___$prover" => "$prover",
- "Format___$prover" => "tptp",
- "Command___$prover" => "$command $options %s"
-);
+ );
+
+# check connection
+my $TestAgent = LWP::UserAgent->new;
+$TestAgent->timeout(5);
+my $TestRequest = GET($SystemOnTPTPFormReplyURL);
+my $TestResponse = $TestAgent->request($TestRequest);
+if(! $TestResponse->is_success) {
+ print "HTTP-Error: " . $TestResponse->message . "\n";
+ exit(-1);
+}
+
+#----Get format and transform options if specified
+my %Options;
+getopts("hws:t:c:",\%Options);
+
+#----Usage
+if (exists($Options{'h'})) {
+ print("Usage: remote <options> [<File name>]\n");
+ print(" <options> are ...\n");
+ print(" -h - print this help\n");
+ print(" -w - list available ATP systems\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");
+ print(" <File name> - TPTP problem file\n");
+ exit(0);
+}
+
+#----What systems flag
+if (exists($Options{'w'})) {
+ $URLParameters{"SubmitButton"} = "ListSystems";
+ delete($URLParameters{"ProblemSource"});
+}
+#----Selected system
+my $System;
+if (exists($Options{'s'})) {
+ $System = $Options{'s'};
+} else {
+ # use Vampire as default
+ $System = "Vampire---9.0";
+}
+$URLParameters{"System___$System"} = $System;
+
+#----Time limit
+if (exists($Options{'t'})) {
+ $URLParameters{"TimeLimit___$System"} = $Options{'t'};
+}
+#----Custom command
+if (exists($Options{'c'})) {
+ $URLParameters{"Command___$System"} = $Options{'c'};
+}
+
+#----Get single file name
+if (exists($URLParameters{"ProblemSource"})) {
+ if (scalar(@ARGV) >= 1) {
+ $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
+ } else {
+die("Missing problem file");
+ }
+}
# Query Server
my $Agent = LWP::UserAgent->new;
+if (exists($Options{'t'})) {
+ # give server more time to respond
+ $Agent->timeout($Options{'t'} * 2 + 10);
+}
my $Request = POST($SystemOnTPTPFormReplyURL,
Content_Type => 'form-data',Content => \%URLParameters);
my $Response = $Agent->request($Request);
-
-#catch errors, let isabelle/watcher know
-if($Response->is_success && $Response->content !~ /NO SOLUTION OUTPUT BY SYSTEM/
-&& $Response->content =~ m/%\s*Result\s*:\s*Unsatisfiable.*?\n%\s*Output\s*:\s*.*?Refutation.*?\n/){
- # convert to isabelle-friendly format
- my @lines = split( /%\s*Result\s*:\s*Unsatisfiable.*?\n%\s*Output\s*:\s*.*?Refutation.*?\n/, $Response->content);
- @lines = split( /\n/, $lines[1]); my $extract = "";
- my $inproof = 0 > 1;
- my $ende = 0 > 1;
+
+#catch errors / failure
+if(! $Response->is_success){
+ print "HTTP-Error: " . $Response->message . "\n";
+ exit(-1);
+} elsif (exists($Options{'w'})) {
+ print $Response->content;
+ exit (0);
+} elsif ($Response->content =~ /NO SOLUTION OUTPUT BY SYSTEM/){
+ if ($Response->content =~ /%\s*Result\s*:(.*)\n%\s*Output\s*:(.*)\n%/) {
+ print "No Solution Output\nResult: $1\nOutput: $2\n";
+ } else {
+ print "No Solution Output\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);
+} else {
+ my @lines = split( /\n/, $Response->content);
+ my $extract = "";
foreach my $line (@lines){
- if(! $ende){
- #ignore comments
- if(! $inproof){
- if ($line !~ /^%/ && !($line eq "")) {
- $extract .= "$line";
- $inproof = 1;
- }
- } else {
- if ($line !~ /^%/) {
- $extract .= "$line";
- } else {
- $ende = 1;
- }
- }
+ #ignore comments
+ if ($line !~ /^%/ && !($line eq "")) {
+ $extract .= "$line";
}
}
- # insert newlines after '.'
+ # 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";
-} else {
- print "HTTP-Request: " . $Response->message;
- print "\nCANNOT PROVE: \n";
- print $Response->content;
+ exit(0);
}
--- a/src/HOL/ATP_Linkup.thy Mon Jan 19 23:40:29 2009 +0100
+++ b/src/HOL/ATP_Linkup.thy Tue Jan 20 18:10:25 2009 +0100
@@ -112,10 +112,13 @@
setup {* AtpManager.add_prover "spass_no_tc" (AtpWrapper.spass_opts 40 false) *}
text {* remote provers via SystemOnTPTP *}
-setup {* AtpManager.add_prover "remote_vamp9"
- (AtpWrapper.remote_prover "Vampire---9.0" "jumpirefix --output_syntax tptp --mode casc -t 3600") *}
-setup {* AtpManager.add_prover "remote_vamp10"
- (AtpWrapper.remote_prover "Vampire---10.0" "drakosha.pl 60") *}
+setup {* AtpManager.add_prover "remote_vampire"
+ (AtpWrapper.remote_prover "-s Vampire---9.0 -t 100") *}
+setup {* AtpManager.add_prover "remote_spass"
+ (AtpWrapper.remote_prover "-s SPASS---3.01 -t 100") *}
+setup {* AtpManager.add_prover "remote_e"
+ (AtpWrapper.remote_prover "-s EP---1.0 -t 100") *}
+
subsection {* The Metis prover *}
--- a/src/HOL/Tools/atp_manager.ML Mon Jan 19 23:40:29 2009 +0100
+++ b/src/HOL/Tools/atp_manager.ML Tue Jan 20 18:10:25 2009 +0100
@@ -35,9 +35,9 @@
local
-val atps = ref "e";
+val atps = ref "e remote_e remore_vampire remote_spass";
val max_atps = ref 5; (* ~1 means infinite number of atps *)
-val timeout = ref 60;
+val timeout = ref 100;
in
--- a/src/HOL/Tools/atp_wrapper.ML Mon Jan 19 23:40:29 2009 +0100
+++ b/src/HOL/Tools/atp_wrapper.ML Tue Jan 20 18:10:25 2009 +0100
@@ -12,7 +12,7 @@
val external_prover:
((int -> Path.T) -> Proof.context * thm list * thm -> string list * ResHolClause.axiom_name Vector.vector list) ->
Path.T * string ->
- (string * int -> bool) ->
+ (string -> string option) ->
(string * string vector * Proof.context * thm * int -> string) ->
AtpManager.prover
val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
@@ -30,8 +30,8 @@
val eprover_full: AtpManager.prover
val spass_opts: int -> bool -> AtpManager.prover
val spass: AtpManager.prover
- val remote_prover_opts: int -> bool -> string -> string -> AtpManager.prover
- val remote_prover: string -> string -> AtpManager.prover
+ val remote_prover_opts: int -> bool -> string -> AtpManager.prover
+ val remote_prover: string -> AtpManager.prover
end;
structure AtpWrapper: ATP_WRAPPER =
@@ -47,7 +47,7 @@
(* basic template *)
-fun external_prover write_problem_files (cmd, args) check_success produce_answer subgoalno state =
+fun external_prover write_problem_files (cmd, args) find_failure produce_answer subgoalno state =
let
(* path to unique problem file *)
val destdir' = ! destdir
@@ -70,19 +70,18 @@
if File.exists cmd then File.shell_path cmd ^ " " ^ args
else error ("Bad executable: " ^ Path.implode cmd)
val (proof, rc) = system_out (cmdline ^ " " ^ nth filenames (subgoalno - 1))
- val _ =
- if rc <> 0 then
- warning ("Sledgehammer prover exited with return code " ^ string_of_int rc ^ "\n" ^ cmdline)
- else ()
(* remove *temporary* files *)
val _ = if destdir' = "" then List.app OS.FileSys.remove filenames else ()
-
- val success = check_success (proof, rc)
+
+ (* check for success and print out some information on failure *)
+ val failure = find_failure proof
+ val success = (rc = 0) andalso (not (isSome failure))
val message =
- if success
- then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
- else "Failed."
+ if isSome failure then "Could not prove: " ^ the failure
+ else if rc <> 0
+ then "Exited with return code " ^ string_of_int rc ^ ": " ^ proof
+ else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
in (success, message) end;
@@ -95,7 +94,7 @@
external_prover
(ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const)
command
- ResReconstruct.check_success_e_vamp_spass
+ ResReconstruct.find_failure_e_vamp_spass
(if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp);
(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
@@ -148,7 +147,7 @@
fun spass_opts max_new theory_const = external_prover
(ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const)
(Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof")
- ResReconstruct.check_success_e_vamp_spass
+ ResReconstruct.find_failure_e_vamp_spass
ResReconstruct.lemma_list_dfg;
val spass = spass_opts 40 true;
@@ -156,9 +155,9 @@
(* remote prover invocation via SystemOnTPTP *)
-fun remote_prover_opts max_new theory_const name command =
+fun remote_prover_opts max_new theory_const args =
tptp_prover_opts max_new theory_const
- (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ command);
+ (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", args);
val remote_prover = remote_prover_opts 60 false;
--- a/src/HOL/Tools/res_reconstruct.ML Mon Jan 19 23:40:29 2009 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML Tue Jan 20 18:10:25 2009 +0100
@@ -15,7 +15,7 @@
val strip_prefix: string -> string -> string option
val setup: Context.theory -> Context.theory
(* extracting lemma list*)
- val check_success_e_vamp_spass: string * int -> bool
+ val find_failure_e_vamp_spass: 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 *)
@@ -463,10 +463,9 @@
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 check_success_e_vamp_spass (proof, rc) =
- not (exists (fn s => String.isSubstring s proof)
- (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS))
- andalso (rc = 0);
+ fun find_failure_e_vamp_spass proof =
+ hd (map (fn s => if String.isSubstring s proof then SOME s else NONE)
+ (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS));
(*=== EXTRACTING PROOF-TEXT === *)