1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/contrib/SystemOnTPTP/vampire	Fri Oct 03 14:06:19 2008 +0200
     1.3 @@ -0,0 +1,60 @@
     1.4 +#!/usr/bin/env perl
     1.5 +#
     1.6 +# Vampire Wrapper for SystemOnTPTP
     1.7 +# Author: Fabian Immler, TU Muenchen
     1.8 +#
     1.9 +# - querys a Vampire theorem prover on SystemOnTPTP
    1.10 +#   (http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP)
    1.11 +# - behaves like a local Vampire
    1.12 +# => can be used for Isabelle when Vampire is not available (e.g. on a Mac)
    1.13 +#
    1.14 +
    1.15 +use warnings;
    1.16 +use strict;
    1.17 +
    1.18 +use Getopt::Std;
    1.19 +use HTTP::Request::Common;
    1.20 +use LWP::UserAgent;
    1.21 +
    1.22 +# address of proof-server
    1.23 +my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
    1.24 +
    1.25 +#name of prover and its executable on the server, e.g.
    1.26 +# Vampire---9.0
    1.27 +# jumpirefix
    1.28 +my $prover = "Vampire---9.0";
    1.29 +my $command = "jumpirefix";
    1.30 +
    1.31 +# pass arguments
    1.32 +my $options = "";
    1.33 +while(scalar(@ARGV)>1){
    1.34 +	$options.=" ".shift(@ARGV);
    1.35 +}
    1.36 +# last argument is problemfile to be uploaded
    1.37 +my $problem = [shift(@ARGV)];
    1.38 +
    1.39 +# fill in form
    1.40 +my %URLParameters = (
    1.41 +    "NoHTML" => 1,
    1.42 +    "QuietFlag" => "-q01",
    1.43 +    "SubmitButton" => "RunSelectedSystems",
    1.44 +    "ProblemSource" => "UPLOAD",
    1.45 +    "UPLOADProblem" => $problem,
    1.46 +    "System___$prover" => "$prover",
    1.47 +    "Format___$prover" => "tptp",
    1.48 +    "Command___$prover" => "$command $options %s"
    1.49 +);
    1.50 +
    1.51 +# Query Server
    1.52 +my $Agent = LWP::UserAgent->new;
    1.53 +my $Request = POST($SystemOnTPTPFormReplyURL,
    1.54 +	Content_Type => 'form-data',Content => \%URLParameters);
    1.55 +my $Response = $Agent->request($Request);
    1.56 +    
    1.57 +#catch errors, let isabelle/watcher know
    1.58 +if($Response->is_success){
    1.59 +	print $Response->content;
    1.60 +} else {
    1.61 +	print $Response->message;
    1.62 +	print "\nCANNOT PROVE\n";
    1.63 +}