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 "ForceSystem" => "-force", |
|
23 ); |
|
24 |
|
25 #----Get format and transform options if specified |
|
26 my %Options; |
|
27 getopts("hwxs:t:c:",\%Options); |
|
28 |
|
29 #----Usage |
|
30 sub usage() { |
|
31 print("Usage: remote [<options>] <File name>\n"); |
|
32 print(" <options> are ...\n"); |
|
33 print(" -h - print this help\n"); |
|
34 print(" -w - list available ATP systems\n"); |
|
35 print(" -x - use X2TPTP to convert output of prover\n"); |
|
36 print(" -s<system> - specified system to use\n"); |
|
37 print(" -t<timelimit> - CPU time limit for system\n"); |
|
38 print(" -c<command> - custom command for system\n"); |
|
39 print(" <File name> - TPTP problem file\n"); |
|
40 exit(0); |
|
41 } |
|
42 if (exists($Options{'h'})) { |
|
43 usage(); |
|
44 } |
|
45 |
|
46 #----What systems flag |
|
47 if (exists($Options{'w'})) { |
|
48 $URLParameters{"SubmitButton"} = "ListSystems"; |
|
49 delete($URLParameters{"ProblemSource"}); |
|
50 } |
|
51 |
|
52 #----X2TPTP |
|
53 if (exists($Options{'x'})) { |
|
54 $URLParameters{"X2TPTP"} = "-S"; |
|
55 } |
|
56 |
|
57 #----Selected system |
|
58 my $System; |
|
59 if (exists($Options{'s'})) { |
|
60 $System = $Options{'s'}; |
|
61 } else { |
|
62 # use Vampire as default |
|
63 $System = "Vampire---9.0"; |
|
64 } |
|
65 $URLParameters{"System___$System"} = $System; |
|
66 |
|
67 #----Time limit |
|
68 if (exists($Options{'t'})) { |
|
69 $URLParameters{"TimeLimit___$System"} = $Options{'t'}; |
|
70 } |
|
71 #----Custom command |
|
72 if (exists($Options{'c'})) { |
|
73 $URLParameters{"Command___$System"} = $Options{'c'}; |
|
74 } |
|
75 |
|
76 #----Get single file name |
|
77 if (exists($URLParameters{"ProblemSource"})) { |
|
78 if (scalar(@ARGV) >= 1) { |
|
79 $URLParameters{"UPLOADProblem"} = [shift(@ARGV)]; |
|
80 } else { |
|
81 print("Missing problem file\n"); |
|
82 usage(); |
|
83 die; |
|
84 } |
|
85 } |
|
86 |
|
87 # Query Server |
|
88 my $Agent = LWP::UserAgent->new; |
|
89 if (exists($Options{'t'})) { |
|
90 # give server more time to respond |
|
91 $Agent->timeout($Options{'t'} + 10); |
|
92 } |
|
93 my $Request = POST($SystemOnTPTPFormReplyURL, |
|
94 Content_Type => 'form-data',Content => \%URLParameters); |
|
95 my $Response = $Agent->request($Request); |
|
96 |
|
97 #catch errors / failure |
|
98 if(!$Response->is_success) { |
|
99 print "HTTP-Error: " . $Response->message . "\n"; |
|
100 exit(-1); |
|
101 } elsif (exists($Options{'w'})) { |
|
102 print $Response->content; |
|
103 exit (0); |
|
104 } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) { |
|
105 print "Specified System $1 does not exist\n"; |
|
106 exit(-1); |
|
107 } elsif (exists($Options{'x'}) && |
|
108 $Response->content =~ |
|
109 /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ && |
|
110 $Response->content !~ /ERROR: Could not form TPTP format derivation/ ) |
|
111 { |
|
112 # converted output: extract proof |
|
113 my @lines = split( /\n/, $Response->content); |
|
114 my $extract = ""; |
|
115 foreach my $line (@lines){ |
|
116 #ignore comments |
|
117 if ($line !~ /^%/ && !($line eq "")) { |
|
118 $extract .= "$line"; |
|
119 } |
|
120 } |
|
121 # insert newlines after ').' |
|
122 $extract =~ s/\s//g; |
|
123 $extract =~ s/\)\.cnf/\)\.\ncnf/g; |
|
124 |
|
125 print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n"; |
|
126 # orientation for "sledgehammer_proof_reconstruct.ML" |
|
127 print "# SZS output start CNFRefutation.\n"; |
|
128 print "$extract\n"; |
|
129 print "# SZS output end CNFRefutation.\n"; |
|
130 # can be useful for debugging; Isabelle ignores this |
|
131 print "============== original response from SystemOnTPTP: ==============\n"; |
|
132 print $Response->content; |
|
133 exit(0); |
|
134 } elsif (!exists($Options{'x'})) { |
|
135 # pass output directly to Isabelle |
|
136 print $Response->content; |
|
137 exit(0); |
|
138 }else { |
|
139 print "Remote script could not extract proof:\n".$Response->content; |
|
140 exit(-1); |
|
141 } |
|
142 |
|