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

    "X2TPTP" => "-S",

    "SubmitButton" => "RunSelectedSystems",

    "ProblemSource" => "UPLOAD",

    );

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

my %Options;

getopts("hws: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("    -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"});

}

#----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 ($Response->content =~ /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/) {

  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;

  # orientation for res_reconstruct.ML

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

  print "$extract\n";

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

  exit(0);

} else {

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

  exit(-1);

}