src/HOL/Tools/ATP_Manager/SystemOnTPTP
author blanchet
Wed, 24 Mar 2010 14:49:32 +0100
changeset 35969 c9565298df9e
parent 32435 711d680eab26
child 36287 96f45c5ffb36
permissions -rwxr-xr-x
added support for Sledgehammer parameters; this change goes hand in hand with f8c738abaed8
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
31833
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
    13
my $SystemOnTPTPFormReplyURL =
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
    14
  "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
28573
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    15
29590
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    16
# default parameters
28573
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    17
my %URLParameters = (
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    18
    "NoHTML" => 1,
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    19
    "QuietFlag" => "-q01",
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    20
    "SubmitButton" => "RunSelectedSystems",
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    21
    "ProblemSource" => "UPLOAD",
32435
711d680eab26 New option ForceSystem that makes sure we *really* get the system we ask for
nipkow
parents: 32327
diff changeset
    22
    "ForceSystem" => "-force",
29590
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
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    25
#----Get format and transform options if specified
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    26
my %Options;
31833
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
    27
getopts("hwxs:t:c:",\%Options);
29590
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    28
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    29
#----Usage
30874
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
    30
sub usage() {
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
    31
  print("Usage: remote [<options>] <File name>\n");
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
    32
  print("    <options> are ...\n");
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
    33
  print("    -h            - print this help\n");
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
    34
  print("    -w            - list available ATP systems\n");
31833
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
    35
  print("    -x            - use X2TPTP to convert output of prover\n");
30874
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
    36
  print("    -s<system>    - specified system to use\n");
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
    37
  print("    -t<timelimit> - CPU time limit for system\n");
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
    38
  print("    -c<command>   - custom command for system\n");
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
    39
  print("    <File name>   - TPTP problem file\n");
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
    40
  exit(0);
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
    41
}
29590
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    42
if (exists($Options{'h'})) {
30874
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
    43
  usage();
29590
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    44
}
31833
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
    45
29590
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    46
#----What systems flag
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    47
if (exists($Options{'w'})) {
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    48
    $URLParameters{"SubmitButton"} = "ListSystems";
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    49
    delete($URLParameters{"ProblemSource"});
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    50
}
31833
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
    51
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
    52
#----X2TPTP
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
    53
if (exists($Options{'x'})) {
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
    54
    $URLParameters{"X2TPTP"} = "-S";
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
    55
}
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
    56
29590
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    57
#----Selected system
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    58
my $System;
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    59
if (exists($Options{'s'})) {
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    60
    $System = $Options{'s'};
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    61
} else {
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    62
    # use Vampire as default
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    63
    $System = "Vampire---9.0";
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    64
}
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    65
$URLParameters{"System___$System"} = $System;
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    66
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    67
#----Time limit
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    68
if (exists($Options{'t'})) {
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    69
    $URLParameters{"TimeLimit___$System"} = $Options{'t'};
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    70
}
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    71
#----Custom command
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    72
if (exists($Options{'c'})) {
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    73
    $URLParameters{"Command___$System"} = $Options{'c'};
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
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    76
#----Get single file name
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    77
if (exists($URLParameters{"ProblemSource"})) {
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    78
    if (scalar(@ARGV) >= 1) {
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    79
        $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    80
    } else {
30874
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
    81
      print("Missing problem file\n");
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
    82
      usage();
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
    83
      die;
29590
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    84
    }
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    85
}
28573
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    86
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    87
# Query Server
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    88
my $Agent = LWP::UserAgent->new;
29590
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    89
if (exists($Options{'t'})) {
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    90
  # give server more time to respond
30534
0ac3db5a59a8 removed connection check;
immler@in.tum.de
parents: 29590
diff changeset
    91
  $Agent->timeout($Options{'t'} + 10);
29590
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    92
}
28573
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    93
my $Request = POST($SystemOnTPTPFormReplyURL,
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    94
	Content_Type => 'form-data',Content => \%URLParameters);
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
    95
my $Response = $Agent->request($Request);
29590
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    96
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
    97
#catch errors / failure
31833
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
    98
if(!$Response->is_success) {
30535
db8b10fd51a4 show certain errors to the user
immler@in.tum.de
parents: 30534
diff changeset
    99
  print "HTTP-Error: " . $Response->message . "\n";
db8b10fd51a4 show certain errors to the user
immler@in.tum.de
parents: 30534
diff changeset
   100
  exit(-1);
29590
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
   101
} elsif (exists($Options{'w'})) {
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
   102
  print $Response->content;
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
   103
  exit (0);
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
   104
} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
   105
  print "Specified System $1 does not exist\n";
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29588
diff changeset
   106
  exit(-1);
31833
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
   107
} elsif (exists($Options{'x'}) &&
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
   108
  $Response->content =~
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
   109
    /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
   110
  $Response->content !~ /ERROR: Could not form TPTP format derivation/ )
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
   111
{
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
   112
  # converted output: extract proof
30874
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   113
  my @lines = split( /\n/, $Response->content);
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   114
  my $extract = "";
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   115
  foreach my $line (@lines){
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   116
      #ignore comments
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   117
      if ($line !~ /^%/ && !($line eq "")) {
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   118
          $extract .= "$line";
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   119
      }
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   120
  }
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   121
  # insert newlines after ').'
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   122
  $extract =~ s/\s//g;
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   123
  $extract =~ s/\)\.cnf/\)\.\ncnf/g;
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   124
31833
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
   125
  print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
30874
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   126
  # orientation for res_reconstruct.ML
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   127
  print "# SZS output start CNFRefutation.\n";
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   128
  print "$extract\n";
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   129
  print "# SZS output end CNFRefutation.\n";
31833
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
   130
  # can be useful for debugging; Isabelle ignores this
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
   131
  print "============== original response from SystemOnTPTP: ==============\n";
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
   132
  print $Response->content;
30874
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   133
  exit(0);
31833
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
   134
} elsif (!exists($Options{'x'})) {
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
   135
  # pass output directly to Isabelle
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
   136
  print $Response->content;
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
   137
  exit(0);
9ab1326ed98d use X2TPTP optionally and only for remote_spass;
immler@in.tum.de
parents: 30979
diff changeset
   138
}else {
30874
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   139
  print "Remote-script could not extract proof:\n".$Response->content;
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30535
diff changeset
   140
  exit(-1);
28573
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
   141
}
6403f0e16269 ** Update from Fabian **
wenzelm
parents:
diff changeset
   142