contrib/SystemOnTPTP/remote

nicer induction/cases rules for numeral types

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

# check connection
my $TestAgent = LWP::UserAgent->new;
$TestAgent->timeout(5);
my $TestRequest = GET($SystemOnTPTPFormReplyURL);
my $TestResponse = $TestAgent->request($TestRequest);
if(! $TestResponse->is_success) {
  print "HTTP-Error: " . $TestResponse->message . "\n";
  exit(-1);
}

#----Get format and transform options if specified
my %Options;
getopts("hws:t:c:",\%Options);

#----Usage
if (exists($Options{'h'})) {
    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);
}

#----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 {
die("Missing problem file");
    }
}

# Query Server
my $Agent = LWP::UserAgent->new;
if (exists($Options{'t'})) {
  # give server more time to respond
  $Agent->timeout($Options{'t'} * 2 + 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 =~ /NO SOLUTION OUTPUT BY SYSTEM/){
  if ($Response->content =~ /%\s*Result\s*:(.*)\n%\s*Output\s*:(.*)\n%/) {
    print "No Solution Output\nResult: $1\nOutput: $2\n";
  } else {
    print "No Solution Output\n";
  }
  exit(-1);
} elsif ($Response->content =~ /ERROR: Could not form TPTP format derivation/) {
  print "Could not form TPTP format derivation\n";
  exit(-1);
} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
  print "Specified System $1 does not exist\n";
  exit(-1);
} elsif ($Response->content =~ /^\s*$/) {
  print "Empty response (specified bad system? Inappropriate problem file format?)\n";
  exit(-1);
} elsif ($Response->content !~ /%\s*Result\s*:(.*)\n%\s*Output\s*:(.*)\n%/) {
  print "Bad response: \n".$Response->content;
  exit(-1);
} else {
    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);
}