src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
3 # Wrapper for custom remote provers on SystemOnTPTP
4 # Author: Fabian Immler, TU Muenchen
10 use HTTP::Request::Common;
13 my $SystemOnTPTPFormReplyURL =
14 "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
19 "QuietFlag" => "-q01",
20 "SubmitButton" => "RunSelectedSystems",
21 "ProblemSource" => "UPLOAD",
24 #----Get format and transform options if specified
26 getopts("hwxs:t:c:",\%Options);
30 print("Usage: remote [<options>] <File name>\n");
31 print(" <options> are ...\n");
32 print(" -h - print this help\n");
33 print(" -w - list available ATP systems\n");
34 print(" -x - use X2TPTP to convert output of prover\n");
35 print(" -s<system> - specified system to use\n");
36 print(" -t<timelimit> - CPU time limit for system\n");
37 print(" -c<command> - custom command for system\n");
38 print(" <File name> - TPTP problem file\n");
41 if (exists($Options{'h'})) {
45 #----What systems flag
46 if (exists($Options{'w'})) {
47 $URLParameters{"SubmitButton"} = "ListSystems";
48 delete($URLParameters{"ProblemSource"});
52 if (exists($Options{'x'})) {
53 $URLParameters{"X2TPTP"} = "-S";
58 if (exists($Options{'s'})) {
59 $System = $Options{'s'};
61 # use Vampire as default
62 $System = "Vampire---9.0";
64 $URLParameters{"System___$System"} = $System;
67 if (exists($Options{'t'})) {
68 $URLParameters{"TimeLimit___$System"} = $Options{'t'};
71 if (exists($Options{'c'})) {
72 $URLParameters{"Command___$System"} = $Options{'c'};
75 #----Get single file name
76 if (exists($URLParameters{"ProblemSource"})) {
77 if (scalar(@ARGV) >= 1) {
78 $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
80 print("Missing problem file\n");
87 my $Agent = LWP::UserAgent->new;
88 if (exists($Options{'t'})) {
89 # give server more time to respond
90 $Agent->timeout($Options{'t'} + 10);
92 my $Request = POST($SystemOnTPTPFormReplyURL,
93 Content_Type => 'form-data',Content => \%URLParameters);
94 my $Response = $Agent->request($Request);
96 #catch errors / failure
97 if(!$Response->is_success) {
98 print "HTTP-Error: " . $Response->message . "\n";
100 } elsif (exists($Options{'w'})) {
101 print $Response->content;
103 } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
104 print "Specified System $1 does not exist\n";
106 } elsif (exists($Options{'x'}) &&
107 $Response->content =~
108 /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
109 $Response->content !~ /ERROR: Could not form TPTP format derivation/ )
111 # converted output: extract proof
112 my @lines = split( /\n/, $Response->content);
114 foreach my $line (@lines){
116 if ($line !~ /^%/ && !($line eq "")) {
120 # insert newlines after ').'
122 $extract =~ s/\)\.cnf/\)\.\ncnf/g;
124 print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
125 # orientation for res_reconstruct.ML
126 print "# SZS output start CNFRefutation.\n";
128 print "# SZS output end CNFRefutation.\n";
129 # can be useful for debugging; Isabelle ignores this
130 print "============== original response from SystemOnTPTP: ==============\n";
131 print $Response->content;
133 } elsif (!exists($Options{'x'})) {
134 # pass output directly to Isabelle
135 print $Response->content;
138 print "Remote-script could not extract proof:\n".$Response->content;