#!/usr/bin/env perl

 #

 # Vampire Wrapper for SystemOnTPTP

 # Author: Fabian Immler, TU Muenchen

 #

 # - querys a Vampire theorem prover on SystemOnTPTP

 #   (http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP)

 # - behaves like a local Vampire

 # => can be used for Isabelle when Vampire is not available (e.g. on a Mac)

 #

 use warnings;

 use strict;

 use Getopt::Std;

 use HTTP::Request::Common;

 use LWP::UserAgent;

 # address of proof-server

 my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";

 #name of prover and its executable on the server, e.g.

 # Vampire---9.0

 # jumpirefix

 my $prover = "Vampire---9.0";

 my $command = "jumpirefix";

 # pass arguments

 my $options = "";

 while(scalar(@ARGV)>1){

 	$options.=" ".shift(@ARGV);

 }

 # last argument is problemfile to be uploaded

 my $problem = [shift(@ARGV)];

 # fill in form

 my %URLParameters = (

     "NoHTML" => 1,

     "QuietFlag" => "-q01",

     "SubmitButton" => "RunSelectedSystems",

     "ProblemSource" => "UPLOAD",

     "UPLOADProblem" => $problem,

     "System___$prover" => "$prover",

     "Format___$prover" => "tptp",

     "Command___$prover" => "$command $options %s"

 );

 # Query Server

 my $Agent = LWP::UserAgent->new;

 my $Request = POST($SystemOnTPTPFormReplyURL,

 	Content_Type => 'form-data',Content => \%URLParameters);

 my $Response = $Agent->request($Request);

 #catch errors, let isabelle/watcher know

 if($Response->is_success){

 	print $Response->content;

 } else {

 	print $Response->message;

 	print "\nCANNOT PROVE\n";

 }