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

}