contrib/SystemOnTPTP/remote
author wenzelm
Sat Nov 15 21:31:13 2008 +0100 (2008-11-15)
changeset 28797 9dcd32ee5dbe
parent 28573 6403f0e16269
child 29587 96599d8d8268
permissions -rwxr-xr-x
rewrite_proof: simplified simprocs (no name required);
     1 #!/usr/bin/env perl
     2 #
     3 # Wrapper for custom remote provers on SystemOnTPTP
     4 # Author: Fabian Immler, TU Muenchen
     5 #
     6 # Similar to the vampire wrapper, but compatible provers can be passed in the
     7 # command line, with %s for the problemfile e.g. 
     8 #
     9 # ./remote Vampire---9.0 jumpirefix --output_syntax tptp --mode casc -t 3600 %s
    10 # ./remote Vampire---10.0 drakosha.pl 60 %s
    11 # ./remote SPASS---3.01 SPASS -Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof %s
    12 # ./remote Metis---2.1 metis --show proof --show saturation %s
    13 # ./remote SNARK---20080805r005 run-snark %s
    14 
    15 use warnings;
    16 use strict;
    17 
    18 use Getopt::Std;
    19 use HTTP::Request::Common;
    20 use LWP::UserAgent;
    21 
    22 # address of proof-server
    23 my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
    24 
    25 if(scalar(@ARGV) < 2) {
    26     print "prover and command missing";
    27     exit -1;
    28 }
    29 my $prover = shift(@ARGV);
    30 my $command = shift(@ARGV);
    31 
    32 # pass arguments
    33 my $options = "";
    34 while(scalar(@ARGV)>1){
    35 	$options.=" ".shift(@ARGV);
    36 }
    37 # last argument is problemfile to be uploaded
    38 my $problem = [shift(@ARGV)];
    39 
    40 # fill in form
    41 my %URLParameters = (
    42     "NoHTML" => 1,
    43     "QuietFlag" => "-q01",
    44     "X2TPTP" => "-S",
    45     "SubmitButton" => "RunSelectedSystems",
    46     "ProblemSource" => "UPLOAD",
    47     "UPLOADProblem" => $problem,
    48     "System___$prover" => "$prover",
    49     "Format___$prover" => "tptp",
    50     "Command___$prover" => "$command $options %s"
    51 );
    52 
    53 # Query Server
    54 my $Agent = LWP::UserAgent->new;
    55 my $Request = POST($SystemOnTPTPFormReplyURL,
    56 	Content_Type => 'form-data',Content => \%URLParameters);
    57 my $Response = $Agent->request($Request);
    58   
    59 #catch errors, let isabelle/watcher know
    60 if($Response->is_success && $Response->content !~ /NO SOLUTION OUTPUT BY SYSTEM/
    61 && $Response->content =~ m/%\s*Result\s*:\s*Unsatisfiable.*?\n%\s*Output\s*:\s*.*?Refutation.*?\n/){
    62     # convert to isabelle-friendly format
    63     my @lines = split( /%\s*Result\s*:\s*Unsatisfiable.*?\n%\s*Output\s*:\s*.*?Refutation.*?\n/, $Response->content);
    64     @lines = split( /\n/, $lines[1]);    my $extract = "";
    65     my $inproof = 0 > 1;
    66     my $ende = 0 > 1;
    67     foreach my $line (@lines){
    68         if(! $ende){
    69             #ignore comments
    70             if(! $inproof){
    71                 if ($line !~ /^%/ && !($line eq "")) {
    72                     $extract .= "$line";
    73                     $inproof = 1;
    74                 }
    75             } else {
    76                 if ($line !~ /^%/) {
    77                     $extract .= "$line";
    78                 } else {
    79                     $ende = 1;
    80                 }
    81             }
    82         }
    83     }
    84     # insert newlines after '.'
    85     $extract =~ s/\s//g;
    86     $extract =~ s/\)\.cnf/\)\.\ncnf/g;
    87     print "# SZS output start CNFRefutation.\n";
    88     print "$extract\n";
    89     print "# SZS output end CNFRefutation.\n";
    90 } else {
    91 	print "HTTP-Request: " . $Response->message;
    92 	print "\nCANNOT PROVE: \n";
    93   print $Response->content;
    94 }
    95