#!/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";
}