|
1 #!/usr/bin/env perl |
|
2 # |
|
3 # Wrapper for custom remote provers on SystemOnTPTP |
|
4 # Author: Fabian Immler, TU Muenchen |
|
5 # |
|
6 # Similar to the vampire wrapper, but compatible provers can be passed in the |
|
7 # command line, with %s for the problemfile e.g. |
|
8 # |
|
9 # ./remote Vampire---9.0 jumpirefix --output_syntax tptp --mode casc -t 3600 %s |
|
10 # ./remote Vampire---10.0 drakosha.pl 60 %s |
|
11 # ./remote SPASS---3.01 SPASS -Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof %s |
|
12 # ./remote Metis---2.1 metis --show proof --show saturation %s |
|
13 # ./remote SNARK---20080805r005 run-snark %s |
|
14 |
|
15 use warnings; |
|
16 use strict; |
|
17 |
|
18 use Getopt::Std; |
|
19 use HTTP::Request::Common; |
|
20 use LWP::UserAgent; |
|
21 |
|
22 # address of proof-server |
|
23 my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply"; |
|
24 |
|
25 if(scalar(@ARGV) < 2) { |
|
26 print "prover and command missing"; |
|
27 exit -1; |
|
28 } |
|
29 my $prover = shift(@ARGV); |
|
30 my $command = shift(@ARGV); |
|
31 |
|
32 # pass arguments |
|
33 my $options = ""; |
|
34 while(scalar(@ARGV)>1){ |
|
35 $options.=" ".shift(@ARGV); |
|
36 } |
|
37 # last argument is problemfile to be uploaded |
|
38 my $problem = [shift(@ARGV)]; |
|
39 |
|
40 # fill in form |
|
41 my %URLParameters = ( |
|
42 "NoHTML" => 1, |
|
43 "QuietFlag" => "-q01", |
|
44 "X2TPTP" => "-S", |
|
45 "SubmitButton" => "RunSelectedSystems", |
|
46 "ProblemSource" => "UPLOAD", |
|
47 "UPLOADProblem" => $problem, |
|
48 "System___$prover" => "$prover", |
|
49 "Format___$prover" => "tptp", |
|
50 "Command___$prover" => "$command $options %s" |
|
51 ); |
|
52 |
|
53 # Query Server |
|
54 my $Agent = LWP::UserAgent->new; |
|
55 my $Request = POST($SystemOnTPTPFormReplyURL, |
|
56 Content_Type => 'form-data',Content => \%URLParameters); |
|
57 my $Response = $Agent->request($Request); |
|
58 |
|
59 #catch errors, let isabelle/watcher know |
|
60 if($Response->is_success && $Response->content !~ /NO SOLUTION OUTPUT BY SYSTEM/ |
|
61 && $Response->content =~ m/%\s*Result\s*:\s*Unsatisfiable.*?\n%\s*Output\s*:\s*.*?Refutation.*?\n/){ |
|
62 # convert to isabelle-friendly format |
|
63 my @lines = split( /%\s*Result\s*:\s*Unsatisfiable.*?\n%\s*Output\s*:\s*.*?Refutation.*?\n/, $Response->content); |
|
64 @lines = split( /\n/, $lines[1]); my $extract = ""; |
|
65 my $inproof = 0 > 1; |
|
66 my $ende = 0 > 1; |
|
67 foreach my $line (@lines){ |
|
68 if(! $ende){ |
|
69 #ignore comments |
|
70 if(! $inproof){ |
|
71 if ($line !~ /^%/ && !($line eq "")) { |
|
72 $extract .= "$line"; |
|
73 $inproof = 1; |
|
74 } |
|
75 } else { |
|
76 if ($line !~ /^%/) { |
|
77 $extract .= "$line"; |
|
78 } else { |
|
79 $ende = 1; |
|
80 } |
|
81 } |
|
82 } |
|
83 } |
|
84 # insert newlines after '.' |
|
85 $extract =~ s/\s//g; |
|
86 $extract =~ s/\)\.cnf/\)\.\ncnf/g; |
|
87 print "# SZS output start CNFRefutation.\n"; |
|
88 print "$extract\n"; |
|
89 print "# SZS output end CNFRefutation.\n"; |
|
90 } else { |
|
91 print "HTTP-Request: " . $Response->message; |
|
92 print "\nCANNOT PROVE: \n"; |
|
93 print $Response->content; |
|
94 } |
|
95 |