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 = |
|
14 "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply"; |
|
15 |
|
16 # default parameters |
|
17 my %URLParameters = ( |
|
18 "NoHTML" => 1, |
|
19 "QuietFlag" => "-q01", |
|
20 "SubmitButton" => "RunSelectedSystems", |
|
21 "ProblemSource" => "UPLOAD", |
|
22 ); |
|
23 |
|
24 #----Get format and transform options if specified |
|
25 my %Options; |
|
26 getopts("hwxs: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(" -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"); |
|
39 exit(0); |
|
40 } |
|
41 if (exists($Options{'h'})) { |
|
42 usage(); |
|
43 } |
|
44 |
|
45 #----What systems flag |
|
46 if (exists($Options{'w'})) { |
|
47 $URLParameters{"SubmitButton"} = "ListSystems"; |
|
48 delete($URLParameters{"ProblemSource"}); |
|
49 } |
|
50 |
|
51 #----X2TPTP |
|
52 if (exists($Options{'x'})) { |
|
53 $URLParameters{"X2TPTP"} = "-S"; |
|
54 } |
|
55 |
|
56 #----Selected system |
|
57 my $System; |
|
58 if (exists($Options{'s'})) { |
|
59 $System = $Options{'s'}; |
|
60 } else { |
|
61 # use Vampire as default |
|
62 $System = "Vampire---9.0"; |
|
63 } |
|
64 $URLParameters{"System___$System"} = $System; |
|
65 |
|
66 #----Time limit |
|
67 if (exists($Options{'t'})) { |
|
68 $URLParameters{"TimeLimit___$System"} = $Options{'t'}; |
|
69 } |
|
70 #----Custom command |
|
71 if (exists($Options{'c'})) { |
|
72 $URLParameters{"Command___$System"} = $Options{'c'}; |
|
73 } |
|
74 |
|
75 #----Get single file name |
|
76 if (exists($URLParameters{"ProblemSource"})) { |
|
77 if (scalar(@ARGV) >= 1) { |
|
78 $URLParameters{"UPLOADProblem"} = [shift(@ARGV)]; |
|
79 } else { |
|
80 print("Missing problem file\n"); |
|
81 usage(); |
|
82 die; |
|
83 } |
|
84 } |
|
85 |
|
86 # Query Server |
|
87 my $Agent = LWP::UserAgent->new; |
|
88 if (exists($Options{'t'})) { |
|
89 # give server more time to respond |
|
90 $Agent->timeout($Options{'t'} + 10); |
|
91 } |
|
92 my $Request = POST($SystemOnTPTPFormReplyURL, |
|
93 Content_Type => 'form-data',Content => \%URLParameters); |
|
94 my $Response = $Agent->request($Request); |
|
95 |
|
96 #catch errors / failure |
|
97 if(!$Response->is_success) { |
|
98 print "HTTP-Error: " . $Response->message . "\n"; |
|
99 exit(-1); |
|
100 } elsif (exists($Options{'w'})) { |
|
101 print $Response->content; |
|
102 exit (0); |
|
103 } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) { |
|
104 print "Specified System $1 does not exist\n"; |
|
105 exit(-1); |
|
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/ ) |
|
110 { |
|
111 # converted output: extract proof |
|
112 my @lines = split( /\n/, $Response->content); |
|
113 my $extract = ""; |
|
114 foreach my $line (@lines){ |
|
115 #ignore comments |
|
116 if ($line !~ /^%/ && !($line eq "")) { |
|
117 $extract .= "$line"; |
|
118 } |
|
119 } |
|
120 # insert newlines after ').' |
|
121 $extract =~ s/\s//g; |
|
122 $extract =~ s/\)\.cnf/\)\.\ncnf/g; |
|
123 |
|
124 print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n"; |
|
125 # orientation for res_reconstruct.ML |
|
126 print "# SZS output start CNFRefutation.\n"; |
|
127 print "$extract\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; |
|
132 exit(0); |
|
133 } elsif (!exists($Options{'x'})) { |
|
134 # pass output directly to Isabelle |
|
135 print $Response->content; |
|
136 exit(0); |
|
137 }else { |
|
138 print "Remote-script could not extract proof:\n".$Response->content; |
|
139 exit(-1); |
|
140 } |
|
141 |
|