#!/usr/bin/env perl

 #

 # Wrapper for custom remote provers on SystemOnTPTP

 # Author: Fabian Immler, 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",

     );

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

 my %Options;

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

 #----Usage

 sub usage() {

   print("Usage: remote [<options>] <File name>\n");

   print("    <options> are ...\n");

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

   print("    -w            - list available ATP systems\n");

   print("    -x            - use X2TPTP to convert output of prover\n");

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

   print("    -t<timelimit> - CPU time limit for system\n");

   print("    -c<command>   - custom command for system\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);

 } elsif (exists($Options{'x'}) &&

   $Response->content =~

     /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&

   $Response->content !~ /ERROR: Could not form TPTP format derivation/ )

 {

   # converted output: extract proof

   my @lines = split( /\n/, $Response->content);

   my $extract = "";

   foreach my $line (@lines){

       #ignore comments

       if ($line !~ /^%/ && !($line eq "")) {

           $extract .= "$line";

       }

   }

   # insert newlines after ').'

   $extract =~ s/\s//g;

   $extract =~ s/\)\.cnf/\)\.\ncnf/g;

   print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";

   # orientation for res_reconstruct.ML

   print "# SZS output start CNFRefutation.\n";

   print "$extract\n";

   print "# SZS output end CNFRefutation.\n";

   # can be useful for debugging; Isabelle ignores this

   print "============== original response from SystemOnTPTP: ==============\n";

   print $Response->content;

   exit(0);

 } elsif (!exists($Options{'x'})) {

   # pass output directly to Isabelle

   print $Response->content;

   exit(0);

 }else {

   print "Remote-script could not extract proof:\n".$Response->content;

   exit(-1);

 }