author | blanchet |
Tue, 24 May 2011 11:55:59 +0200 | |
changeset 42970 | 05d1dc9fefdb |
parent 39152 | f09b378cb252 |
child 43528 | 35f74aafc878 |
permissions | -rwxr-xr-x |
28573 | 1 |
#!/usr/bin/env perl |
2 |
# |
|
3 |
# Wrapper for custom remote provers on SystemOnTPTP |
|
4 |
# Author: Fabian Immler, TU Muenchen |
|
38062 | 5 |
# Author: Jasmin Blanchette, TU Muenchen |
28573 | 6 |
# |
7 |
||
8 |
use warnings; |
|
9 |
use strict; |
|
10 |
use Getopt::Std; |
|
11 |
use HTTP::Request::Common; |
|
29590 | 12 |
use LWP; |
28573 | 13 |
|
31833
9ab1326ed98d
use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents:
30979
diff
changeset
|
14 |
my $SystemOnTPTPFormReplyURL = |
9ab1326ed98d
use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents:
30979
diff
changeset
|
15 |
"http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply"; |
28573 | 16 |
|
29590 | 17 |
# default parameters |
28573 | 18 |
my %URLParameters = ( |
19 |
"NoHTML" => 1, |
|
20 |
"QuietFlag" => "-q01", |
|
21 |
"SubmitButton" => "RunSelectedSystems", |
|
22 |
"ProblemSource" => "UPLOAD", |
|
32435
711d680eab26
New option ForceSystem that makes sure we *really* get the system we ask for
nipkow
parents:
32327
diff
changeset
|
23 |
"ForceSystem" => "-force", |
29590 | 24 |
); |
25 |
||
26 |
#----Get format and transform options if specified |
|
27 |
my %Options; |
|
42970 | 28 |
getopts("hws:t:c:q:",\%Options); |
29590 | 29 |
|
30 |
#----Usage |
|
30874
34927a1e0ae8
reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents:
30535
diff
changeset
|
31 |
sub usage() { |
38062 | 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"); |
|
42970 | 39 |
print(" -q<num> quietness level (0 = most verbose, 3 = least verbose)\n"); |
38062 | 40 |
print(" <file_name> TPTP problem file\n"); |
30874
34927a1e0ae8
reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents:
30535
diff
changeset
|
41 |
exit(0); |
34927a1e0ae8
reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents:
30535
diff
changeset
|
42 |
} |
29590 | 43 |
if (exists($Options{'h'})) { |
30874
34927a1e0ae8
reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents:
30535
diff
changeset
|
44 |
usage(); |
29590 | 45 |
} |
31833
9ab1326ed98d
use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents:
30979
diff
changeset
|
46 |
|
29590 | 47 |
#----What systems flag |
48 |
if (exists($Options{'w'})) { |
|
49 |
$URLParameters{"SubmitButton"} = "ListSystems"; |
|
50 |
delete($URLParameters{"ProblemSource"}); |
|
51 |
} |
|
31833
9ab1326ed98d
use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents:
30979
diff
changeset
|
52 |
|
9ab1326ed98d
use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents:
30979
diff
changeset
|
53 |
#----X2TPTP |
9ab1326ed98d
use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents:
30979
diff
changeset
|
54 |
if (exists($Options{'x'})) { |
9ab1326ed98d
use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents:
30979
diff
changeset
|
55 |
$URLParameters{"X2TPTP"} = "-S"; |
9ab1326ed98d
use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents:
30979
diff
changeset
|
56 |
} |
9ab1326ed98d
use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents:
30979
diff
changeset
|
57 |
|
29590 | 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 |
} |
|
42970 | 76 |
#----Quietness |
77 |
if (exists($Options{'q'})) { |
|
78 |
$URLParameters{"QuietFlag"} = "-q" . $Options{'q'}; |
|
79 |
} |
|
29590 | 80 |
|
81 |
#----Get single file name |
|
82 |
if (exists($URLParameters{"ProblemSource"})) { |
|
83 |
if (scalar(@ARGV) >= 1) { |
|
84 |
$URLParameters{"UPLOADProblem"} = [shift(@ARGV)]; |
|
85 |
} else { |
|
30874
34927a1e0ae8
reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents:
30535
diff
changeset
|
86 |
print("Missing problem file\n"); |
34927a1e0ae8
reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents:
30535
diff
changeset
|
87 |
usage(); |
34927a1e0ae8
reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents:
30535
diff
changeset
|
88 |
die; |
29590 | 89 |
} |
90 |
} |
|
28573 | 91 |
|
92 |
# Query Server |
|
93 |
my $Agent = LWP::UserAgent->new; |
|
39152
f09b378cb252
make remote ATP invocation work for those people who need to go through a proxy;
blanchet
parents:
38094
diff
changeset
|
94 |
$Agent->env_proxy; |
29590 | 95 |
if (exists($Options{'t'})) { |
96 |
# give server more time to respond |
|
30534 | 97 |
$Agent->timeout($Options{'t'} + 10); |
29590 | 98 |
} |
28573 | 99 |
my $Request = POST($SystemOnTPTPFormReplyURL, |
100 |
Content_Type => 'form-data',Content => \%URLParameters); |
|
101 |
my $Response = $Agent->request($Request); |
|
29590 | 102 |
|
103 |
#catch errors / failure |
|
31833
9ab1326ed98d
use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents:
30979
diff
changeset
|
104 |
if(!$Response->is_success) { |
38065 | 105 |
my $message = $Response->message; |
106 |
$message =~ s/ \(Bad hostname ['"][^'"]*['"]\)//; |
|
38094 | 107 |
print "HTTP error: " . $message . "\n"; |
30535 | 108 |
exit(-1); |
29590 | 109 |
} elsif (exists($Options{'w'})) { |
110 |
print $Response->content; |
|
111 |
exit (0); |
|
112 |
} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) { |
|
38065 | 113 |
print "The ATP \"$1\" is not available at SystemOnTPTP\n"; |
29590 | 114 |
exit(-1); |
38042
ef45bcccc9fd
remove needless "-x" option, now that (1) we can't handle remote SPASS anymore; and (2) we can a priori parse the SPASS syntax in "Sledgehammer_Proof_Reconstruct" anyway
blanchet
parents:
38041
diff
changeset
|
115 |
} else { |
31833
9ab1326ed98d
use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents:
30979
diff
changeset
|
116 |
print $Response->content; |
30874
34927a1e0ae8
reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents:
30535
diff
changeset
|
117 |
exit(0); |
28573 | 118 |
} |