1 #!/usr/bin/env perl |
|
2 # |
|
3 # Wrapper for custom remote provers on SystemOnTPTP |
|
4 # Author: Fabian Immler, TU Muenchen |
|
5 # Author: Jasmin Blanchette, TU Muenchen |
|
6 # |
|
7 |
|
8 use warnings; |
|
9 use strict; |
|
10 use Getopt::Std; |
|
11 use HTTP::Request::Common; |
|
12 use LWP; |
|
13 |
|
14 my $SystemOnTPTPFormReplyURL = |
|
15 "http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply"; |
|
16 |
|
17 # default parameters |
|
18 my %URLParameters = ( |
|
19 "NoHTML" => 1, |
|
20 "QuietFlag" => "-q01", |
|
21 "SubmitButton" => "RunSelectedSystems", |
|
22 "ProblemSource" => "UPLOAD", |
|
23 "ForceSystem" => "-force", |
|
24 ); |
|
25 |
|
26 #----Get format and transform options if specified |
|
27 my %Options; |
|
28 getopts("hws:t:c:q:",\%Options); |
|
29 |
|
30 #----Usage |
|
31 sub usage() { |
|
32 print("Usage: remote_atp [<options>] <file_name>\n"); |
|
33 print("Options:\n"); |
|
34 print(" -h print this help\n"); |
|
35 print(" -w list available ATPs\n"); |
|
36 print(" -s<system> ATP to use\n"); |
|
37 print(" -t<time_limit> CPU time limit for ATP\n"); |
|
38 print(" -c<command> custom ATP invocation command\n"); |
|
39 print(" -q<num> quietness level (0 = most verbose, 3 = least verbose)\n"); |
|
40 print(" <file_name> TPTP problem file\n"); |
|
41 exit(0); |
|
42 } |
|
43 if (exists($Options{'h'})) { |
|
44 usage(); |
|
45 } |
|
46 |
|
47 #----What systems flag |
|
48 if (exists($Options{'w'})) { |
|
49 $URLParameters{"SubmitButton"} = "ListSystems"; |
|
50 delete($URLParameters{"ProblemSource"}); |
|
51 } |
|
52 |
|
53 #----X2TPTP |
|
54 if (exists($Options{'x'})) { |
|
55 $URLParameters{"X2TPTP"} = "-S"; |
|
56 } |
|
57 |
|
58 #----Selected system |
|
59 my $System; |
|
60 if (exists($Options{'s'})) { |
|
61 $System = $Options{'s'}; |
|
62 } else { |
|
63 # use Vampire as default |
|
64 $System = "Vampire---9.0"; |
|
65 } |
|
66 $URLParameters{"System___$System"} = $System; |
|
67 |
|
68 #----Time limit |
|
69 if (exists($Options{'t'})) { |
|
70 $URLParameters{"TimeLimit___$System"} = $Options{'t'}; |
|
71 } |
|
72 #----Custom command |
|
73 if (exists($Options{'c'})) { |
|
74 $URLParameters{"Command___$System"} = $Options{'c'}; |
|
75 } |
|
76 #----Quietness |
|
77 if (exists($Options{'q'})) { |
|
78 $URLParameters{"QuietFlag"} = "-q" . $Options{'q'}; |
|
79 } |
|
80 |
|
81 #----Get single file name |
|
82 if (exists($URLParameters{"ProblemSource"})) { |
|
83 if (scalar(@ARGV) >= 1) { |
|
84 $URLParameters{"UPLOADProblem"} = [shift(@ARGV)]; |
|
85 } else { |
|
86 print("Missing problem file\n"); |
|
87 usage(); |
|
88 die; |
|
89 } |
|
90 } |
|
91 |
|
92 # Query Server |
|
93 my $Agent = LWP::UserAgent->new; |
|
94 $Agent->env_proxy; |
|
95 $Agent->agent("Sledgehammer"); |
|
96 if (exists($Options{'t'})) { |
|
97 # give server more time to respond |
|
98 $Agent->timeout($Options{'t'} + 15); |
|
99 } |
|
100 my $Request = POST($SystemOnTPTPFormReplyURL, |
|
101 Content_Type => 'form-data',Content => \%URLParameters); |
|
102 my $Response = $Agent->request($Request); |
|
103 |
|
104 #catch errors / failure |
|
105 if(!$Response->is_success) { |
|
106 my $message = $Response->message; |
|
107 $message =~ s/ \(Bad hostname ['"][^'"]*['"]\)//; |
|
108 print "HTTP error: " . $message . "\n"; |
|
109 exit(-1); |
|
110 } elsif (exists($Options{'w'})) { |
|
111 print $Response->content; |
|
112 exit (0); |
|
113 } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) { |
|
114 print "The ATP \"$1\" is not available at SystemOnTPTP\n"; |
|
115 exit(-1); |
|
116 } else { |
|
117 print $Response->content; |
|
118 exit(0); |
|
119 } |
|