Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: remote_atp Sprache: XML

Original von: Isabelle^©

#!/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.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.