contrib/SystemOnTPTP/remote
author wenzelm
Wed Jan 21 23:21:44 2009 +0100 (2009-01-21)
changeset 29606 fedb8be05f24
parent 29590 479a2fce65e6
child 30534 0ac3db5a59a8
permissions -rwxr-xr-x
removed Ids;
     1 #!/usr/bin/env perl
     2 #
     3 # Wrapper for custom remote provers on SystemOnTPTP
     4 # Author: Fabian Immler, TU Muenchen
     5 #
     6 
     7 use warnings;
     8 use strict;
     9 use Getopt::Std;
    10 use HTTP::Request::Common;
    11 use LWP;
    12 
    13 my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
    14 
    15 # default parameters
    16 my %URLParameters = (
    17     "NoHTML" => 1,
    18     "QuietFlag" => "-q01",
    19     "X2TPTP" => "-S",
    20     "SubmitButton" => "RunSelectedSystems",
    21     "ProblemSource" => "UPLOAD",
    22     );
    23 
    24 # check connection
    25 my $TestAgent = LWP::UserAgent->new;
    26 $TestAgent->timeout(5);
    27 my $TestRequest = GET($SystemOnTPTPFormReplyURL);
    28 my $TestResponse = $TestAgent->request($TestRequest);
    29 if(! $TestResponse->is_success) {
    30   print "HTTP-Error: " . $TestResponse->message . "\n";
    31   exit(-1);
    32 }
    33 
    34 #----Get format and transform options if specified
    35 my %Options;
    36 getopts("hws:t:c:",\%Options);
    37 
    38 #----Usage
    39 if (exists($Options{'h'})) {
    40     print("Usage: remote <options> [<File name>]\n");
    41     print("    <options> are ...\n");
    42     print("    -h            - print this help\n");
    43     print("    -w            - list available ATP systems\n");
    44     print("    -s<system>    - specified system to use\n");
    45     print("    -t<timelimit> - CPU time limit for system\n");
    46     print("    -c<command>   - custom command for system\n");
    47     print("    <File name>   - TPTP problem file\n");
    48     exit(0);
    49 }
    50 
    51 #----What systems flag
    52 if (exists($Options{'w'})) {
    53     $URLParameters{"SubmitButton"} = "ListSystems";
    54     delete($URLParameters{"ProblemSource"});
    55 }
    56 #----Selected system
    57 my $System;
    58 if (exists($Options{'s'})) {
    59     $System = $Options{'s'};
    60 } else {
    61     # use Vampire as default
    62     $System = "Vampire---9.0";
    63 }
    64 $URLParameters{"System___$System"} = $System;
    65 
    66 #----Time limit
    67 if (exists($Options{'t'})) {
    68     $URLParameters{"TimeLimit___$System"} = $Options{'t'};
    69 }
    70 #----Custom command
    71 if (exists($Options{'c'})) {
    72     $URLParameters{"Command___$System"} = $Options{'c'};
    73 }
    74 
    75 #----Get single file name
    76 if (exists($URLParameters{"ProblemSource"})) {
    77     if (scalar(@ARGV) >= 1) {
    78         $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
    79     } else {
    80 die("Missing problem file");
    81     }
    82 }
    83 
    84 # Query Server
    85 my $Agent = LWP::UserAgent->new;
    86 if (exists($Options{'t'})) {
    87   # give server more time to respond
    88   $Agent->timeout($Options{'t'} * 2 + 10);
    89 }
    90 my $Request = POST($SystemOnTPTPFormReplyURL,
    91 	Content_Type => 'form-data',Content => \%URLParameters);
    92 my $Response = $Agent->request($Request);
    93 
    94 #catch errors / failure
    95 if(! $Response->is_success){
    96   	print "HTTP-Error: " . $Response->message . "\n";
    97     exit(-1);
    98 } elsif (exists($Options{'w'})) {
    99   print $Response->content;
   100   exit (0);
   101 } elsif ($Response->content =~ /NO SOLUTION OUTPUT BY SYSTEM/){
   102   if ($Response->content =~ /%\s*Result\s*:(.*)\n%\s*Output\s*:(.*)\n%/) {
   103     print "No Solution Output\nResult: $1\nOutput: $2\n";
   104   } else {
   105     print "No Solution Output\n";
   106   }
   107   exit(-1);
   108 } elsif ($Response->content =~ /ERROR: Could not form TPTP format derivation/) {
   109   print "Could not form TPTP format derivation\n";
   110   exit(-1);
   111 } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
   112   print "Specified System $1 does not exist\n";
   113   exit(-1);
   114 } elsif ($Response->content =~ /^\s*$/) {
   115   print "Empty response (specified bad system? Inappropriate problem file format?)\n";
   116   exit(-1);
   117 } elsif ($Response->content !~ /%\s*Result\s*:(.*)\n%\s*Output\s*:(.*)\n%/) {
   118   print "Bad response: \n".$Response->content;
   119   exit(-1);
   120 } else {
   121     my @lines = split( /\n/, $Response->content);
   122     my $extract = "";
   123     foreach my $line (@lines){
   124         #ignore comments
   125         if ($line !~ /^%/ && !($line eq "")) {
   126             $extract .= "$line";
   127         }
   128     }
   129     # insert newlines after ').'
   130     $extract =~ s/\s//g;
   131     $extract =~ s/\)\.cnf/\)\.\ncnf/g;
   132     
   133     # orientation for res_reconstruct.ML
   134     print "# SZS output start CNFRefutation.\n";
   135     print "$extract\n";
   136     print "# SZS output end CNFRefutation.\n";
   137     exit(0);
   138 }
   139