#!/usr/bin/env perl

 #

 # Wrapper for custom remote provers on SystemOnTPTP

 # Author: Fabian Immler, TU Muenchen

 # Author: Jasmin Blanchette, TU Muenchen

 #

 use warnings;

 use strict;

 use Getopt::Std;

 use HTTP::Request::Common;

 use LWP;

 my $SystemOnTPTPFormReplyURL =

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

 # default parameters

 my %URLParameters = (

     "NoHTML" => 1,

     "QuietFlag" => "-q01",

     "SubmitButton" => "RunSelectedSystems",

     "ProblemSource" => "UPLOAD",

     "ForceSystem" => "-force",

     );

 #----Get format and transform options if specified

 my %Options;

 getopts("hws:t:c:",\%Options);

 #----Usage

 sub usage() {

   print("Usage: remote_atp [<options>] <file_name>\n");

   print("Options:\n");

   print("    -h              print this help\n");

   print("    -w              list available ATPs\n");

   print("    -s<system>      ATP to use\n");

   print("    -t<time_limit>  CPU time limit for ATP\n");

   print("    -c<command>     custom ATP invocation command\n");

   print("    <file_name>     TPTP problem file\n");

   exit(0);

 }

 if (exists($Options{'h'})) {

   usage();

 }

 #----What systems flag

 if (exists($Options{'w'})) {

     $URLParameters{"SubmitButton"} = "ListSystems";

     delete($URLParameters{"ProblemSource"});

 }

 #----X2TPTP

 if (exists($Options{'x'})) {

     $URLParameters{"X2TPTP"} = "-S";

 }

 #----Selected system

 my $System;

 if (exists($Options{'s'})) {

     $System = $Options{'s'};

 } else {

     # use Vampire as default

     $System = "Vampire---9.0";

 }

 $URLParameters{"System___$System"} = $System;

 #----Time limit

 if (exists($Options{'t'})) {

     $URLParameters{"TimeLimit___$System"} = $Options{'t'};

 }

 #----Custom command

 if (exists($Options{'c'})) {

     $URLParameters{"Command___$System"} = $Options{'c'};

 }

 #----Get single file name

 if (exists($URLParameters{"ProblemSource"})) {

     if (scalar(@ARGV) >= 1) {

         $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];

     } else {

       print("Missing problem file\n");

       usage();

       die;

     }

 }

 # Query Server

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

 if (exists($Options{'t'})) {

   # give server more time to respond

   $Agent->timeout($Options{'t'} + 10);

 }

 my $Request = POST($SystemOnTPTPFormReplyURL,

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

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

 #catch errors / failure

 if(!$Response->is_success) {

   print "HTTP-Error: " . $Response->message . "\n";

   exit(-1);

 } elsif (exists($Options{'w'})) {

   print $Response->content;

   exit (0);

 } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {

   print "Specified system $1 does not exist\n";

   exit(-1);

 } else {

   print $Response->content;

   exit(0);

 }