1 #!/usr/bin/env perl |
|
2 # |
|
3 # Wrapper for custom remote provers on SystemOnTPTP |
|
4 # Author: Fabian Immler, TU Muenchen |
|
5 # |
|
6 |
|
7 use warnings; |
|
8 use strict; |
|
9 use Getopt::Std; |
|
10 use HTTP::Request::Common; |
|
11 use LWP; |
|
12 |
|
13 my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply"; |
|
14 |
|
15 # default parameters |
|
16 my %URLParameters = ( |
|
17 "NoHTML" => 1, |
|
18 "QuietFlag" => "-q01", |
|
19 "X2TPTP" => "-S", |
|
20 "SubmitButton" => "RunSelectedSystems", |
|
21 "ProblemSource" => "UPLOAD", |
|
22 ); |
|
23 |
|
24 #----Get format and transform options if specified |
|
25 my %Options; |
|
26 getopts("hws:t:c:",\%Options); |
|
27 |
|
28 #----Usage |
|
29 sub usage() { |
|
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(" -s<system> - specified system to use\n"); |
|
35 print(" -t<timelimit> - CPU time limit for system\n"); |
|
36 print(" -c<command> - custom command for system\n"); |
|
37 print(" <File name> - TPTP problem file\n"); |
|
38 exit(0); |
|
39 } |
|
40 if (exists($Options{'h'})) { |
|
41 usage(); |
|
42 } |
|
43 #----What systems flag |
|
44 if (exists($Options{'w'})) { |
|
45 $URLParameters{"SubmitButton"} = "ListSystems"; |
|
46 delete($URLParameters{"ProblemSource"}); |
|
47 } |
|
48 #----Selected system |
|
49 my $System; |
|
50 if (exists($Options{'s'})) { |
|
51 $System = $Options{'s'}; |
|
52 } else { |
|
53 # use Vampire as default |
|
54 $System = "Vampire---9.0"; |
|
55 } |
|
56 $URLParameters{"System___$System"} = $System; |
|
57 |
|
58 #----Time limit |
|
59 if (exists($Options{'t'})) { |
|
60 $URLParameters{"TimeLimit___$System"} = $Options{'t'}; |
|
61 } |
|
62 #----Custom command |
|
63 if (exists($Options{'c'})) { |
|
64 $URLParameters{"Command___$System"} = $Options{'c'}; |
|
65 } |
|
66 |
|
67 #----Get single file name |
|
68 if (exists($URLParameters{"ProblemSource"})) { |
|
69 if (scalar(@ARGV) >= 1) { |
|
70 $URLParameters{"UPLOADProblem"} = [shift(@ARGV)]; |
|
71 } else { |
|
72 print("Missing problem file\n"); |
|
73 usage(); |
|
74 die; |
|
75 } |
|
76 } |
|
77 |
|
78 # Query Server |
|
79 my $Agent = LWP::UserAgent->new; |
|
80 if (exists($Options{'t'})) { |
|
81 # give server more time to respond |
|
82 $Agent->timeout($Options{'t'} + 10); |
|
83 } |
|
84 my $Request = POST($SystemOnTPTPFormReplyURL, |
|
85 Content_Type => 'form-data',Content => \%URLParameters); |
|
86 my $Response = $Agent->request($Request); |
|
87 |
|
88 #catch errors / failure |
|
89 if(! $Response->is_success){ |
|
90 print "HTTP-Error: " . $Response->message . "\n"; |
|
91 exit(-1); |
|
92 } elsif (exists($Options{'w'})) { |
|
93 print $Response->content; |
|
94 exit (0); |
|
95 } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) { |
|
96 print "Specified System $1 does not exist\n"; |
|
97 exit(-1); |
|
98 } elsif ($Response->content =~ /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/) { |
|
99 my @lines = split( /\n/, $Response->content); |
|
100 my $extract = ""; |
|
101 foreach my $line (@lines){ |
|
102 #ignore comments |
|
103 if ($line !~ /^%/ && !($line eq "")) { |
|
104 $extract .= "$line"; |
|
105 } |
|
106 } |
|
107 # insert newlines after ').' |
|
108 $extract =~ s/\s//g; |
|
109 $extract =~ s/\)\.cnf/\)\.\ncnf/g; |
|
110 |
|
111 # orientation for res_reconstruct.ML |
|
112 print "# SZS output start CNFRefutation.\n"; |
|
113 print "$extract\n"; |
|
114 print "# SZS output end CNFRefutation.\n"; |
|
115 exit(0); |
|
116 } else { |
|
117 print "Remote-script could not extract proof:\n".$Response->content; |
|
118 exit(-1); |
|
119 } |
|
120 |
|