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