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