1.1 --- a/src/HOL/Tools/ATP_Manager/SystemOnTPTP	Wed Jul 28 11:42:48 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,142 +0,0 @@
     1.4 -#!/usr/bin/env perl
     1.5 -#
     1.6 -# Wrapper for custom remote provers on SystemOnTPTP
     1.7 -# Author: Fabian Immler, TU Muenchen
     1.8 -#
     1.9 -
    1.10 -use warnings;
    1.11 -use strict;
    1.12 -use Getopt::Std;
    1.13 -use HTTP::Request::Common;
    1.14 -use LWP;
    1.15 -
    1.16 -my $SystemOnTPTPFormReplyURL =
    1.17 -  "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
    1.18 -
    1.19 -# default parameters
    1.20 -my %URLParameters = (
    1.21 -    "NoHTML" => 1,
    1.22 -    "QuietFlag" => "-q01",
    1.23 -    "SubmitButton" => "RunSelectedSystems",
    1.24 -    "ProblemSource" => "UPLOAD",
    1.25 -    "ForceSystem" => "-force",
    1.26 -    );
    1.27 -
    1.28 -#----Get format and transform options if specified
    1.29 -my %Options;
    1.30 -getopts("hwxs:t:c:",\%Options);
    1.31 -
    1.32 -#----Usage
    1.33 -sub usage() {
    1.34 -  print("Usage: remote [<options>] <File name>\n");
    1.35 -  print("    <options> are ...\n");
    1.36 -  print("    -h            - print this help\n");
    1.37 -  print("    -w            - list available ATP systems\n");
    1.38 -  print("    -x            - use X2TPTP to convert output of prover\n");
    1.39 -  print("    -s<system>    - specified system to use\n");
    1.40 -  print("    -t<timelimit> - CPU time limit for system\n");
    1.41 -  print("    -c<command>   - custom command for system\n");
    1.42 -  print("    <File name>   - TPTP problem file\n");
    1.43 -  exit(0);
    1.44 -}
    1.45 -if (exists($Options{'h'})) {
    1.46 -  usage();
    1.47 -}
    1.48 -
    1.49 -#----What systems flag
    1.50 -if (exists($Options{'w'})) {
    1.51 -    $URLParameters{"SubmitButton"} = "ListSystems";
    1.52 -    delete($URLParameters{"ProblemSource"});
    1.53 -}
    1.54 -
    1.55 -#----X2TPTP
    1.56 -if (exists($Options{'x'})) {
    1.57 -    $URLParameters{"X2TPTP"} = "-S";
    1.58 -}
    1.59 -
    1.60 -#----Selected system
    1.61 -my $System;
    1.62 -if (exists($Options{'s'})) {
    1.63 -    $System = $Options{'s'};
    1.64 -} else {
    1.65 -    # use Vampire as default
    1.66 -    $System = "Vampire---9.0";
    1.67 -}
    1.68 -$URLParameters{"System___$System"} = $System;
    1.69 -
    1.70 -#----Time limit
    1.71 -if (exists($Options{'t'})) {
    1.72 -    $URLParameters{"TimeLimit___$System"} = $Options{'t'};
    1.73 -}
    1.74 -#----Custom command
    1.75 -if (exists($Options{'c'})) {
    1.76 -    $URLParameters{"Command___$System"} = $Options{'c'};
    1.77 -}
    1.78 -
    1.79 -#----Get single file name
    1.80 -if (exists($URLParameters{"ProblemSource"})) {
    1.81 -    if (scalar(@ARGV) >= 1) {
    1.82 -        $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
    1.83 -    } else {
    1.84 -      print("Missing problem file\n");
    1.85 -      usage();
    1.86 -      die;
    1.87 -    }
    1.88 -}
    1.89 -
    1.90 -# Query Server
    1.91 -my $Agent = LWP::UserAgent->new;
    1.92 -if (exists($Options{'t'})) {
    1.93 -  # give server more time to respond
    1.94 -  $Agent->timeout($Options{'t'} + 10);
    1.95 -}
    1.96 -my $Request = POST($SystemOnTPTPFormReplyURL,
    1.97 -	Content_Type => 'form-data',Content => \%URLParameters);
    1.98 -my $Response = $Agent->request($Request);
    1.99 -
   1.100 -#catch errors / failure
   1.101 -if(!$Response->is_success) {
   1.102 -  print "HTTP-Error: " . $Response->message . "\n";
   1.103 -  exit(-1);
   1.104 -} elsif (exists($Options{'w'})) {
   1.105 -  print $Response->content;
   1.106 -  exit (0);
   1.107 -} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
   1.108 -  print "Specified System $1 does not exist\n";
   1.109 -  exit(-1);
   1.110 -} elsif (exists($Options{'x'}) &&
   1.111 -  $Response->content =~
   1.112 -    /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
   1.113 -  $Response->content !~ /ERROR: Could not form TPTP format derivation/ )
   1.114 -{
   1.115 -  # converted output: extract proof
   1.116 -  my @lines = split( /\n/, $Response->content);
   1.117 -  my $extract = "";
   1.118 -  foreach my $line (@lines){
   1.119 -      #ignore comments
   1.120 -      if ($line !~ /^%/ && !($line eq "")) {
   1.121 -          $extract .= "$line";
   1.122 -      }
   1.123 -  }
   1.124 -  # insert newlines after ').'
   1.125 -  $extract =~ s/\s//g;
   1.126 -  $extract =~ s/\)\.cnf/\)\.\ncnf/g;
   1.127 -
   1.128 -  print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
   1.129 -  # orientation for "sledgehammer_proof_reconstruct.ML"
   1.130 -  print "# SZS output start CNFRefutation.\n";
   1.131 -  print "$extract\n";
   1.132 -  print "# SZS output end CNFRefutation.\n";
   1.133 -  # can be useful for debugging; Isabelle ignores this
   1.134 -  print "============== original response from SystemOnTPTP: ==============\n";
   1.135 -  print $Response->content;
   1.136 -  exit(0);
   1.137 -} elsif (!exists($Options{'x'})) {
   1.138 -  # pass output directly to Isabelle
   1.139 -  print $Response->content;
   1.140 -  exit(0);
   1.141 -}else {
   1.142 -  print "Remote script could not extract proof:\n".$Response->content;
   1.143 -  exit(-1);
   1.144 -}
   1.145 -