#!/usr/bin/env perl
#
# Wrapper for custom remote provers on SystemOnTPTP
# Author: Fabian Immler, TU Muenchen
# Author: Jasmin Blanchette, TU Muenchen
#
use warnings;
use strict;
use Getopt::Std;
use HTTP::Request::Common;
use LWP;
my $SystemOnTPTPFormReplyURL =
"http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply";
# default parameters
my %URLParameters = (
"NoHTML" => 1,
"QuietFlag" => "-q01",
"SubmitButton" => "RunSelectedSystems",
"ProblemSource" => "UPLOAD",
"ForceSystem" => "-force",
);
#----Get format and transform options if specified
my %Options;
getopts("hws:t:c:q:",\%Options);
#----Usage
sub usage() {
print("Usage: remote_atp [<options>] <file_name>\n");
print("Options:\n");
print(" -h print this help\n");
print(" -w list available ATPs\n");
print(" -s<system> ATP to use\n");
print(" -t<time_limit> CPU time limit for ATP\n");
print(" -c<command> custom ATP invocation command\n");
print(" -q<num> quietness level (0 = most verbose, 3 = least verbose)\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'};
}
#----Quietness
if (exists($Options{'q'})) {
$URLParameters{"QuietFlag"} = "-q" . $Options{'q'};
}
#----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;
$Agent->env_proxy;
$Agent->agent("Sledgehammer");
if (exists($Options{'t'})) {
# give server more time to respond
$Agent->timeout($Options{'t'} + 15);
}
my $Request = POST($SystemOnTPTPFormReplyURL,
Content_Type => 'form-data',Content => \%URLParameters);
my $Response = $Agent->request($Request);
#catch errors / failure
if(!$Response->is_success) {
my $message = $Response->message;
$message =~ s/ \(Bad hostname ['"][^'"]*['"]\)//;
print "HTTP error: " . $message . "\n";
exit(-1);
} elsif (exists($Options{'w'})) {
print $Response->content;
exit (0);
} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
print "The ATP \"$1\" is not available at SystemOnTPTP\n";
exit(-1);
} else {
print $Response->content;
exit(0);
}
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|