|
1 #!/usr/bin/env perl |
|
2 # |
|
3 # Vampire Wrapper for SystemOnTPTP |
|
4 # Author: Fabian Immler, TU Muenchen |
|
5 # |
|
6 # - querys a Vampire theorem prover on SystemOnTPTP |
|
7 # (http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP) |
|
8 # - behaves like a local Vampire |
|
9 # => can be used for Isabelle when Vampire is not available (e.g. on a Mac) |
|
10 # |
|
11 |
|
12 use warnings; |
|
13 use strict; |
|
14 |
|
15 use Getopt::Std; |
|
16 use HTTP::Request::Common; |
|
17 use LWP::UserAgent; |
|
18 |
|
19 # address of proof-server |
|
20 my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply"; |
|
21 |
|
22 #name of prover and its executable on the server, e.g. |
|
23 # Vampire---9.0 |
|
24 # jumpirefix |
|
25 my $prover = "Vampire---9.0"; |
|
26 my $command = "jumpirefix"; |
|
27 |
|
28 # pass arguments |
|
29 my $options = ""; |
|
30 while(scalar(@ARGV)>1){ |
|
31 $options.=" ".shift(@ARGV); |
|
32 } |
|
33 # last argument is problemfile to be uploaded |
|
34 my $problem = [shift(@ARGV)]; |
|
35 |
|
36 # fill in form |
|
37 my %URLParameters = ( |
|
38 "NoHTML" => 1, |
|
39 "QuietFlag" => "-q01", |
|
40 "SubmitButton" => "RunSelectedSystems", |
|
41 "ProblemSource" => "UPLOAD", |
|
42 "UPLOADProblem" => $problem, |
|
43 "System___$prover" => "$prover", |
|
44 "Format___$prover" => "tptp", |
|
45 "Command___$prover" => "$command $options %s" |
|
46 ); |
|
47 |
|
48 # Query Server |
|
49 my $Agent = LWP::UserAgent->new; |
|
50 my $Request = POST($SystemOnTPTPFormReplyURL, |
|
51 Content_Type => 'form-data',Content => \%URLParameters); |
|
52 my $Response = $Agent->request($Request); |
|
53 |
|
54 #catch errors, let isabelle/watcher know |
|
55 if($Response->is_success){ |
|
56 print $Response->content; |
|
57 } else { |
|
58 print $Response->message; |
|
59 print "\nCANNOT PROVE\n"; |
|
60 } |