contrib/SystemOnTPTP/vampire
author wenzelm
Sat Nov 15 21:31:13 2008 +0100 (2008-11-15)
changeset 28797 9dcd32ee5dbe
parent 28474 d0b8b0a1fca5
permissions -rwxr-xr-x
rewrite_proof: simplified simprocs (no name required);
     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 }